DeepMind、Signalを4週間で形式検証

Google DeepMindは2026年11月、AIエージェント基盤「AlphaProof Code」を使い、Signalの暗号プロトコルを実装するコードの重要な安全性特性を数学的に検証したと発表しました。研究チームは人間の専門家とAIを組み合わせ、従来は専門家チームが年単位を要し得た作業を4週間で実施。暗号設計だけでなく、端末で動くコードが指定した性質を満たすかを調べました。

研究者はまず、Signalの安全性目標を形式仕様に落とし込み、人間が各仕様を確認しました。Gemini Carbonを用いたエージェント群は証明支援言語Leanで600万行超の証明を生成し、Leanが機械的に検査しました。AIが要確認とした箇所はコードベースの約1％で、専門家は判断が必要な部分にレビューを絞れたといいます。

検証対象では新たな脆弱性は見つかりませんでした。一方、修正済みの既知バグを隔離環境の古いコードに戻すと、システムは安全性を証明できないことを示し、バグを検出しました。DeepMindは仕様と証明などの成果物を公開し、他の検証研究に使えるようにしています。

今回の成果は、AIが重要ソフトの形式検証を広げる可能性を示します。SignalのCTOも、従来より大きな範囲を扱える点を評価しました。銀行や医療機器、電力網などへの応用も期待されますが、今回の検証はSignalの中核暗号コードに限られ、モバイルアプリ全体を検証したものではありません。

実用化には、AIによる検証を大規模なコードベースへ広げ、費用に見合う形で運用できるかが課題です。DeepMindは今回を節目と位置づけつつ、全ソフトウェアへ拡大するには研究が必要だとしています。仕様づくりや証明の節目に人間が関与し、AIの出力を確認する協働体制も重要になります。