2026.11.10 TUE12:02 JSTGoogle
GoogleがAlphaProof Codeを発表
様子見成果物のオープンソース公開
プログラムが正しく動くかを、数学の証明を使って自動で厳密にチェックするAI技術。
- 暗号通信コードのバグや脆弱性を数学的証明によって自動検出可能になった
- Signalプロトコルのコアコードに対して600万行超の検証証明を生成
- 従来数年かかっていた高度なソフトウェア形式検証を4週間で完了した
目線
医療機器や通信などのミッションクリティカルなコードにおける脆弱性検査の手法として成果物の活用を調べる価値がある。
対象
セキュリティエンジニア・暗号プロトコル開発者
使える場面
- 公開された検証用アーティファクトを参照し形式検証の導入可能性を評価する
試すなら
公開された技術論文とLeanコードの検証アーティファクトを確認する
背景
ソフトウェアの動作を数学的に証明する形式検証は最高水準の安全性を保障するが、膨大な作業量を要するため普及が難しかった。
何が変わったか
- 複数のAIエージェントが協調してプログラムの形式証明を行うAlphaProof Codeを発表
- Signal暗号プロトコルの実装コードに対して600万行以上のLean証明コードを生成
- 実コードから数式への翻訳と証明作成を自動化し人間側のレビュー対象をコード全体の1%に削減
使える場面・影響
AIが生成・実装した重要コードのセキュリティ検証を、高速かつ数学的な正確さで行う新たな基盤技術となる。
一次ソース
- Google DeepMind Blogdeepmind.google