Amazon、AI 検証に数学的証明を投資

私たちは、この投資とその理由についてお伝えします。AI エージェントが資金の移動や請求承認、重要インフラの運用といった意思決定を担うようになると、従来のソフトウェアテスト手法ではもはや不十分です。テストは想定したケースしか検証できませんが、数学的証明という根本的に異なるアプローチがあります。これは、どんな入力を与えられてもシステムが誤った振る舞いをしないことを確実にも示すものです。

Lean は、現代のソフトウェア規模で正しさの証明を実用的なものにする可能性を秘めたプログラミング言語です。Amazon は現在、この言語を開発するチームである Lean Focused Research Organization (FRO) に対して、多大かつ長期的な資金支援を行っています。これにより、世界中の開発者が証明を利用可能になることを目指しています。これは FRO の歴史において最大の寄付となります。

Lean は数学、コンピュータサイエンス、物理学など多くの分野で活発なユーザーコミュニティを育んできました。また、Mathlib という包括的な形式化数学ライブラリの創出にもつながり、形式化証明へのさらなる取り組みに火をつけました。さらに、AI の推論能力の発展においても決定的な役割を果たしています。Lean における形式化証明の AI 生成は、誤り率を低く抑えたモデルを訓練する主要な手法の一つとなっており、現在では研究レベルの問題に対する正解を生み出すに至っています。

しかし、私たち Amazon が Lean に最も期待しているのは、アジェンシー・セーフティ（エージェント安全性）やニューロシンボリック AI における役割です。生成 AI と Lean の数学的厳密性を組み合わせることで、検証可能で信頼性の高い AI エージェントの実現が可能になります。このビジョンは業界全体が追いつく前から Lean チームによって推進されてきましたが、現在では私たちのアジェンシー・セーフティ戦略にとってますます重要なものとなっています。

例えば、Amazon Bedrock AgentCore の Policy では、AI エージェントを指定された範囲内に保つポリシー言語の正しさを証明するために Lean ベースの検証を利用しています。このような数学的保証を提供する他社はありません。また、SampCert（AWS Clean Rooms における差分プライバシー保護の有効性を数学的に保証）や AWS Neuron（Amazon の AI アクセラレーションチップへのコンパイル）といったシステムの正しさの根幹にも Lean が支えられています。

ある科学者が最近、LLM と Lean を組み合わせて、Amazon Aurora のセグメント修復プロトコルの正しさを証明しました。これは当社の最も耐久性に重要な分散プロトコルですが、手動で行う場合の数分の一の時間で完了しています。適用事例は急速に増えつつあり、これはまだ始まりに過ぎません。

なぜ Amazon は Lean の開発を FRO 内で、つまり社外で行わせようとするのかと疑問に思うかもしれません。その答えは、ツール自体を自分で評価できる場合にこそ、証明への信頼が高まるからです。顧客、監査人、規制当局は、コミュニティ主導で管理されるツールによって行われた作業を独立して検査・検証できます。これは安全性が極めて重要な AI が必要とする透明性の一種です。

社内においても重要です。開発者コミュニティ（当社エンジニアも含まれます）が大きくなるほど Lean は有用になり、より多くのライブラリやツール、形式化証明が提供されるようになります。この二つの理由から、Lean の基盤となる作業は Lean Focused Research Organization を通じてオープンに行うことが不可欠だと私たちは考えています。