AIが書くコードを、AIが証明する。AlphaProof Codeが示す安全性の新しい確かめ方

AIがコードを書く速度は上がった。では、そのコードを「安全だ」と確かめる速度は追いつくだろうか。Google DeepMindが11月10日に発表したAlphaProof Codeは、この問いに一つの答えを示した。AIエージェントが数学的な証明を組み立て、人間が何を証明すべきかを定める。対象は、暗号化メッセージを支えるSignalプロトコルの実装だ。

設計図から、実際に動くコードへ

暗号方式の安全性を数式で論じても、端末で動くプログラムがその設計どおりとは限らない。今回の研究は、Signalの参照実装「libsignal」の特定バージョンを通常のRustコンパイラでビルドし、AArch64向けの機械語までつないで検証した点に特徴がある。対象には、通信開始時のPQXDHと、鍵を更新し続けるTriple Ratchetが含まれる。

研究チームによると、秘密鍵が後で漏れても過去の通信を守る「前方秘匿性」や、侵害後に安全な状態へ戻る性質など、定めた条件の下で複数の保証を証明した。以前に修正された二つの欠陥を古いコードへ戻す試験では、安全性に反することも検出できたという。検証対象は抽象的な設計モデルだけではなく、コンパイルされた実装まで届いている。

AIが書く600万行、人が読むべき仕様

AlphaProof Codeでは、まず人間とAIが「安全とは何か」をLeanという形式言語で記述する。人間が仕様を確認した後、複数のエージェントが証明を作り、Leanの小さな検証器が成立を機械的に確かめる。研究論文によれば、AIが生成した証明は約650万行。一方、結果を信頼するために人が吟味すべき仕様や機械語の意味づけは、約2万6000行に絞られる。

ただし、証明が通れば現実世界の全ての危険が消えるわけではない。Leanが確かめるのは、承認された仕様に対して証明が正しいかどうかだ。仕様が重要な脅威を見落としていれば、その見落としまで自動で直してはくれない。論文も暗号部品の性質や一部の外部処理を前提に置き、単一端末や固定長のメッセージなど、検証対象の条件を明示している。対象は研究用にビルドした実行ファイルであり、Signalアプリ全体の安全性を保証した発表ではない。

日本の開発現場で問われる「証明したいこと」

AIが書いたコードをAIにレビューさせるだけでは、同じ思い込みを共有する可能性がある。AlphaProof Codeが示したのは、検証器という独立した判定役を工程に入れ、AIの大量の作業を人が確認できる仕様へ結びつける方法だ。日本でも金融、医療、重要インフラのソフトウェアでは、テストの数だけでなく「どの性質を、どんな前提で守るのか」を定義する力が重要になる。

今すぐ全てのアプリに数百万行の証明を付けられるわけではない。だが、人が安全の意味を決め、AIが証明を探し、機械がその筋道を判定する分業は、AI時代の品質保証に具体的な道筋を与えている。

出典：Google DeepMindの発表、研究論文「AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level」