DeepMind、複雑なソフトウェアを深く検証する「AlphaProof Code」を発表

Google DeepMind は、ソフトウェアの形式検証（コードに欠陥がないことを数学的に証明すること）を行うエージェントの仕組み「AlphaProof Code」を発表しました。Signal や Google メッセージで使われる Signal プロトコルの実際のコードについて、主な安全性を証明したといいます。

手順は、まず研究者と複数のモデルが Signal の安全目標を数式の仕様に書き直し、すべてを専門家が確認しました。次に Gemini Carbon を使うエージェントが、証明用の言語 Lean で600万行を超える証明を作りました。エージェントは、人が見直すべき箇所（全体の約1%）も示しました。

設計の段階だけでなく、端末で動く変換後のコードまで、端末が一時的に乗っ取られた前後でもメッセージが守られる、といった性質を証明した点が新しいとしています。広く使われる暗号プロトコルの実装を、AIの有無を問わずこの深さで検証したのは初めてだとしています。

AIがコードの安全性を数学的に証明するところまで来ていることを示す成果です。