Google DeepMindは11月10日、AIエージェントを使ってソフトウェアを数学的に検証するフレームワーク「AlphaProof Code」を発表した。最初の適用先は、SignalやGoogleメッセージのエンドツーエンド暗号化を支えるSignalプロトコルの実装コードで、プロトコルの設計ではなく端末上で実際に動くコンパイル済みコードが仕様どおりに安全であることを、機械検証可能な証明として示した点が主眼になっている。
AlphaProof Codeは複数のLLMと人間の専門家が役割を分担するエージェント型のシステムだ。まず研究者が複数のモデルを使い、Signalのセキュリティ目標を形式的な数学仕様に翻訳する。この仕様はすべて人間の専門家がレビューした。次に、10月に発表されたGemini 4 Carbonを搭載したエージェントが証明を書き、その量は定理証明言語Leanで600万行を超えた。最後にエージェント自身が証明を監査し、コードベースのおよそ1%を人間によるレビュー対象として切り出した。残りはLeanの型検査器が自動で正しさを確認する。
証明の対象となったのは、端末が一時的に乗っ取られた場合でも、その前後のメッセージが保護され続けるといった性質だ。作業期間は4週間で、DeepMindは同規模の検証に専門家チームが従来は年単位を要してきたと説明している。
検証が本当に機能しているかを確かめるため、過去に修正済みの実際のバグ2件を、隔離したSignalコードのコピーに再び入れる実験も行われた。どちらのケースでも、システムはバグ入りのバージョンが安全でないことを機械検証済みの証明として出力した。検証の成果物はGitHub上で公開されており、技術論文「Formal Verification of Signal」も併せて公開されている。
「設計」ではなく「実装」を証明した意味
一般的なソフトウェア開発では、安全性の確認はテストや監査、脆弱性診断に頼っている。テストは用意した入力に対して正しく動くことを確かめるだけなので、想定していない入力や状態の組み合わせで起きるバグは見逃しうる。形式検証はこれと違い、コードがあらゆる入力に対して仕様を満たすことを数学の定理として証明する。Leanはその証明を機械が一行ずつ検査する言語で、証明が通れば人間の思い込みや見落としが入り込む余地はなくなる。代わりに、証明を書く作業そのものが極端に重く、これまでは小規模な部品にしか適用できなかった。
暗号プロトコルの形式検証自体は新しい取り組みではない。Signalプロトコルについても、これまでに設計レベルでの安全性解析は学術的に行われてきた。ただ、設計が正しくても、それを実装したコードにバグがあれば安全性は崩れる。今回DeepMindが強調しているのは、この設計と実装のあいだの溝を埋めた点で、広く使われているプロトコルの実装を形式検証した例は、AIを使うかどうかにかかわらず初めてだとしている。
実装の検証が難しいのは、証明すべき対象が膨大になるためだ。設計レベルなら抽象化したモデルを扱えばよいが、実装では実際のコードの分岐や状態遷移をすべて追う必要がある。600万行という証明の規模は、この作業量をAIエージェントに肩代わりさせた結果といえる。SignalのCTOであるEhren Kret氏も、稼働中のコードを有効なLeanの定理に翻訳できたことを大きな前進だと評価している。
人間が残る工程は仕様作成と1%のレビュー
完全自動化されたわけではない。何を証明すべきかを定める仕様の作成とレビューは人間の専門家が担い、エージェントが判断を保留した約1%のコードも人が確認している。DeepMind自身も、この手法をさらに大規模なソフトウェアに広げるには研究の継続が必要だとしており、計算コストや使用したモデルの規模は公表していない。
DeepMindはこれまでも、2024年に国際数学オリンピックで銀メダル相当の成績を出したAlphaProofで数学の証明を、2025年10月発表のCodeMenderでコードの脆弱性修正を、それぞれAIに担わせてきた。AlphaProof Codeは名前のとおり前者の「証明」の系譜を実在のソフトウェアに持ち込んだもので、CodeMenderのような修正エージェントと組み合わせる方向性もブログ内で示されている。CodeMenderが「見つけたバグを直す」アプローチだったのに対し、AlphaProof Codeは「バグがないことを数学的に示す」アプローチで、セキュリティ保証の強さが異なる。
今後の適用先として、DeepMindは医療機器のファームウェアや電力網のソフトウェアを挙げている。いずれも障害が人命やインフラに直結する領域で、現時点では構想の段階にとどまる。
