11月12日、Manuel Uthが「Google Deepmind's AlphaProof Code verified Signal's cryptographic core in four weeks instead of years」と題した記事を公開した。Google DeepMindが開発したAIシステム「AlphaProof Code」がSignalの暗号コアに対し、通常なら数年を要する数学的検証を4週間・600万行超の証明コード生成によって完了したという報告だ。形式検証という専門領域に、AIエージェントが実用スケールで踏み込んだ事例として注目に値する。
形式検証を「数年から4週間」に短縮
ソフトウェアのセキュリティ要件を数学的に証明する手法を**形式検証（Formal Verification）**という。コードのテストが「バグがないことを確認する」試みであるのに対し、形式検証は「仕様を満たすことを数学的に証明する」より強力なアプローチだ。ただしその分、工数が膨大にかかり、実用的なスケールへの適用は長年の課題とされてきた。
Google DeepMindはこの課題に対し、AIエージェントを活用した形式検証システム「AlphaProof Code」を発表した。なお、AlphaProof Codeは、DeepMindが2024年に数学オリンピック（IMO）問題の証明に適用したAlphaProofとは異なるシステムであり、ソフトウェアコードの形式検証に特化して開発されたものだ。DeepMindの研究者Pushmeet KohliとSwarat Chaudhurによるブログ記事によれば、同システムはSignalの暗号プロトコルに適用され、通常なら数年を要する作業をわずか4週間で完了した。
これまでの検証努力は「理論的な設計段階」で止まっていたという点が重要だ。AlphaProof Codeは、設計レベルではなくユーザーのデバイス上で実際に動作する暗号コアのコード自体を検証対象とした。
どのように動作するか
AlphaProof Codeのアーキテクチャは以下の流れで機能する。
- 仕様の定義：専門家がフォーマルなセキュリティ要件を定義する
- 証明の自動生成：AIエージェントが、定理証明支援系の**Lean言語で600万行以上の証明コード**を自動生成する
- 人間のレビュー：コードベースの**約1%**が人間によるレビュー対象としてフラグされる
- バグ検出：テスト目的で意図的に埋め込まれた2つのバグは即座に検出された
AIエージェントは仕様の作成と、プログラムコードがその仕様を満たすことの証明を、それぞれ独立して担う設計になっている。
なお、元記事では証明生成に用いられたベースモデルとして「Gemini Carbon」という名称が言及されているが、この名称はGoogleの公式発表では現時点で確認が取れていない。また「CodeMender」についても元記事に記載はあるものの、その詳細な仕様や既存ツールとの関係については元記事の範囲内での言及にとどまる点に留意されたい。
SignalのCTOが語る意義
SignalのCTO、Ehren Kretは今回のアプローチについて、「AIの脅威が増大する中で、データプライバシーへの信頼を強化するものだ」と述べている。
Signalは世界的に利用されている暗号化メッセージングアプリであり、その暗号コアの信頼性は多くのユーザーのプライバシーに直結する。Signalが採用するSignal Protocolは、エンドツーエンド暗号化の業界標準として広くほかのサービスにも採用されているプロトコルだ。その実装コードに対して数学的な正しさの証明が与えられたことは、セキュリティ工学の観点からも実用上の意義が大きい。
これまで形式検証が実運用コードに適用されにくかった背景には、証明記述の専門的な難易度と、コードの規模に対して検証コストが指数的に膨らむという構造的な問題がある。AlphaProof Codeはこのボトルネックをエージェントによる自動化で突破しようとするものであり、今回の事例はその現実的な可能性を示した最初の大規模なケースとして位置づけられる。
今後の展開：電力網・医療機器へ
DeepMindはこの手法を、CodeMenderなどのシステムを通じて電力グリッドや医療機器へも展開する計画を明らかにしている。
これらの分野はいずれも、バグや仕様違反が人命に関わる可能性があるクリティカルなシステムだ。医療機器や産業制御システムにおける形式検証の重要性は以前から指摘されてきたが、コスト面での壁から普及が進んでいなかった。形式検証の適用コストがAIによって大幅に下がれば、これまで現実的でなかった領域への展開が現実味を帯びてくる。セキュリティ研究コミュニティにとっても、AIと形式手法の交差点として今後の動向が注目される分野だ。
詳細はGoogle Deepmind's AlphaProof Code verified Signal's cryptographic core in four weeks instead of yearsを参照していただきたい。
