Google DeepMindの研究チームは、AI駆動型の形式検証フレームワーク「AlphaProof Code」を用いて、世界中の通信暗号化を支える「Signalプロトコル」の中核的な暗号学的安全性を数学的に完全証明したことを明らかにしました。数学的推論AIを活用した形式検証の先駆的プロジェクトとして、WIREDなどの主要メディアによって報じられています。
形式検証（フォーマル・ベリフィケーション）は、厳密な数学的論理を用いてソフトウェアが設計仕様通りに誤りなく動作することを証明する手法です。従来は人間の専門家が膨大な時間をかけて数式を記述・構築する必要があり、実用的な普及には高い壁が存在していました。今回の実証では、自律型AIエージェントが数式化から証明の構築、自己修正までの大半を担い、わずか4週間の研究プロジェクトで機械検証可能な厳密な証明を完成させました。
現行仕様の検証において未知の欠陥は見つからなかったものの、既知の脆弱性が存在した旧バージョンのプロトコルに対して検証を実施したところ、過去の欠陥を正確に検知して不合格判定を下すことに成功しました。SignalプロトコルはSignalアプリのみならず、WhatsAppやGoogleメッセージなど世界十数億人が日常的に利用する通信基盤の根幹をなしており、その安全性保証がAIによって数学的に証明された意義は極めて大きいと評価されています。
研究チームは、AIが目標設定から証明までを完全に独断で行うのではなく、人間の専門家が節目ごとに検証結果を精査する協調設計の重要性を強調しています。今回得られた形式仕様と証明データはオープンソースとして公開される予定であり、金融決済や重要インフラ、防衛システムなど、絶対にバグが許されない最重要ソフトウェアの検証基盤として社会実装が加速すると期待されています（一次ソース：WIRED 独占報道（英文））。