Google DeepMind、AIエージェントでSignalの暗号プロトコルを数学的に証明
AlphaProof Code
Google DeepMindが発表したAlphaProof Codeは、人間の専門家と複数のAIエージェントが役割を分担する形式検証フレームワークだ。Gemini Carbonが生成した600万行以上のLean証明を通じ、Signalの暗号プロトコルの実装コードが主要なセキュリティ特性を満たすことをわずか4週間で証明した。これは広く普及したプロトコルの実装が形式検証された初の事例であり、過去に修正された2つの実バグを再導入して検出できることも確認している。
AIエージェントを使って実際のコードを有効なLeanの定理に変換できるのは大きなブレークスルーだ。AIによるセキュリティ脅威が高まる中、Signalプロトコルの実装を厳密に検証できたことで、コードのプライバシー保証への信頼がさらに高まった。
HNでの議論
174- hedora
何かおかしい気がする。彼らは過去にバグがあった自明でない人間が書いたコードを取り上げ、ライブラリ全体を形式的に検証して、バグをゼロ個見つけた？
LLMに証明を書かせることが可能だというのは信じられるが、検証したシステムにバグがゼロだったというのは信じられない。定理を間違えたのか、それともシステムの狭い性質だけを証明したのか疑問だ。
私はClaudeに暗号とデータ保存形式を形式的に検証させたことがある。もっともらしい定理を書き、形式的検証は通ったが、結果のコードには多くのバグがあり、同じものの他の実装がアドホックなテストで見つけていた。
発表の書き方からすると、今後libsignalにはバグがゼロになるはずだ。それが実現するかは時間が経てばわかるだろう。
- thibsrn
素晴らしい、AIの素晴らしいユースケースだ。Googleは大手の中でも有用な貢献とAIシステムの制御の面で最もクリーンだと思う。この新しい証明エージェントは仕様に挑戦しているのではなく、実装だけを対象にしているように見える（私の理解が正しければ）。
このエージェントが従来のコーディングエージェントとどう違うのか気になる。結局のところ、LeanやRocqのコードを書きながらコードベースを反復し実行するという同じように動作するように思える。
- Mizza
もうすぐ、おそらく今後2、3年のうちに、かつて我々のシステム上で検証されていないソフトウェアを_一切_動かしていたなんて信じられない、と狂気じみて思えるようになるだろう。今ではTelnetや平文HTTPを使っていたのが狂気じみて思えるのと同じように。
- andai
今年の初め、古いプロジェクトの大規模なリファクタリングをしていた。当時コーディングエージェントが本当に台頭していて、より自律的な作業をますます信頼できるようになっていたので、試してみるのが楽しみだった。
エージェントは数時間稼働してリファクタリングを完了し、さらに広範なテストスイートも自発的に提供してくれた。テストは全部グリーン！
とても感心したが、少し目を細めて見ると、全体を逆さまに実装していて、無意味なだけでなく（掲げた目標を何も達成していない）、実際に以前より悪くなっていた！
その瞬間まで、AI時代における形式的検証の可能性にかなり強気だった。しかしその惨状を見て、エージェントは書いたコードの数学的証明を書いてもよく、その証明は通り、コードは依然として間違っているかもしれないと気づいた！
- oggy
とてもクールだ。数年前、AlphaZeroのようなアプローチを使って形式的検証のための特化モデルを開発することを考えていた。ここ数ヶ月のニュースを見ると、やらなくてよかったと思う。汎用LLMがすべてを食い尽くしているように見える。
仕様が26k行（Armのセマンティクスを含む）になるというのは興味深い。かなり大きな信頼できる計算基盤だ。シンボリック/計算モデルをゼロから開発する必要があるのだろう。mathlibのように再利用可能なライブラリを開発できるか、そしてそこでのインセンティブがどう働くかは興味深い。AIラボはおそらくこれに特に興味はなく、研究者にとっても報われない仕事になりそうだ。しかし、検証を行う企業や検証済み製品を販売する企業が出現すれば、作業を共有し標準化されたTCBを持つインセンティブが生まれるかもしれない。それは良くも悪くも「対話型定理証明器戦争」に実用的な終止符を打つかもしれない。
開発中のコードにどう影響するかも興味深い。ChatGPTはこれがリリースされた翌日にlibsignalが大幅に変わったと主張している :D おそらくRustでの中間レベルの信頼できないモデルが役立つかもしれない（証明の大部分はRustモデルと仕様を関連付け、その後より機械的な証明がRustモデルとバイナリを関連付ける）。seL4はずっと前にこれをやった。しかしこれが実用的かどうかはわからない。何も聞いたことがない […]
- r0ze-at-hn
私はAIがLeanをコーディングするのがいかに簡単かを利用する実験をしてきた（https://metamagic.substack.com/p/beyond-the-proof-dump-lean-...）といくつかの教訓がある。
1. AI Leanは完璧ではなく、AIはLeanを書いているので簡単にズルができる。AI Leanコードをいじる人は、少なくともAI生成のLeanをレビューするための別の敵対的プロンプトが必要だ。
2. 論文をざっと見ると、バグを再導入して検出できるか確認したが、バグは見つからなかったようだ。Signalは多くの目でレビューされていて素晴らしいのかもしれないが、私たちにとっての本当の話は、AIでLeanに変換し始めると価値は見つかる仮定にあるということだ。論理的に厳密だと思っていたものでも、Leanは修正が必要な小さな点をいくつか見つけた。ファジングに似ていて、コードベースにファジングを導入してバグが見つからなかったことはないので、仕様をLeanに変換する場合も同じだろう。
3. AI経由で（安価に）Leanを生成できる能力は、コーディングにとって非常に興味深いアンロックだ。仕様からLean、そしてコードへと進み、Leanを論理のゲートキーパーとして使える可能性は、研究だけでなく日常的により使われる真の能力になる可能性がある。
- ghm2180
初心者の質問：これらの暗号システム以外に、一般的なソフトウェアの一部に対してこのような証明を構築することは有用だろうか？具体的には：
1. AIエージェントが本番環境のクリティカルパスにある（非決定的な動作が発生する可能性があるが回復可能な）ソフトウェアシステムに適用した人はいるか？
2. どのようなシナリオで最初からLean証明を持つことが理にかなうか？例えばACIDに関する保証を持つデータベースシステムを作りたいなら、最初からこれを持っている方が良いかもしれない。しかしAPIバックエンドサービスを構築するにはおそらくそれほど有用ではないだろう。
- fercircularbuf
素晴らしい。昨年、人々がよりAIに任せるようになるとソフトウェアはもっとバグだらけになるだろうと思っていたが、このようなツールはソフトウェアの未来が実際にはもっと安全に見えるかもしれないという希望を与えてくれる。