AlphaProof Code: 複雑なソフトウェアの深層検証におけるブレークスルー

AlphaProof Code: 複雑なソフトウェアの深層検証におけるブレークスルー

2026年11月10日 リサーチ

Pushmeet Kohli および Swarat Chaudhuri

Google DeepMindの研究者たちが、長年、セキュリティ上の大きな課題とされてきたSignalの暗号化プロトコルのコードを数学的に検証する、新しいエージェント型フレームワークを構築した方法

本日、私たちはソフトウェアセキュリティにおける長年の大きな課題であったマイルストーンを発表します。Google DeepMindの研究者たちは、Signalプロトコル（SignalやGoogleメッセージなどのアプリで数億件のプライベートな会話を保護する技術）の基盤となる実際のコードの重要なセキュリティ特性を、数学的に証明するためにAIエージェントを導きました。

この画期的な発見は、AlphaProof Code を使用して行われました。これは、人間の専門知識とAIエージェントを組み合わせた、前例のない深さでの形式検証のための新しいエージェント型フレームワークです。 形式検証（コードに欠陥がなく正しく実行されることを数学的に証明すること）は、最高のセキュリティ保証基準ですが、困難でしばしば労働集約的です。

私たちの研究は、広く展開されている暗号化プロトコルをこの深さで形式検証するためにAIが使用された初めての事例です。また、AIの有無にかかわらず、この種の広く展開されているプロトコルの実装が形式検証されたのも初めてです。

Signalをどのように検証したか

AlphaProof Codeは、マルチLLMエージェント型フレームワークであり、形式検証の作業を研究チームが行うように分割します。人間の専門家がAIと協力して何を証明するかを決定し、AIエージェントのグループがそれを実行します。

まず、私たちの研究者は、さまざまなモデルを組み合わせてSignalのセキュリティ目標を形式的な数学的仕様に変換しました。人間の専門家がすべてをレビューしました。そこから、Gemini Carbon を搭載したエージェントが証明を実行し、コードの正確さを数学的に証明するコンピュータ言語であるLeanの600万行以上のコードを生成しました。

次に、エージェントは証明を監査し、人間による再確認が必要な領域を特定しました。これはコードベースのわずか1パーセントであり、大幅な時間節約につながりました。Leanは残りを自動的にチェックするため、私たちの専門家は人間の判断が最も重要となるレビューに集中できました。

暗号化プロトコルは、オンラインバンキングからウェブブラウジングまで、ほぼすべてのデジタル通信の基盤となっており、単一の欠陥が数百万人のユーザーを一度に危険にさらす可能性があります。そのため、専門家は何十年もかけてそれらを形式的に分析してきました。

しかし、ほとんどのプロトコルの検証は設計レベルで止まります。私たちのエージェントはさらに進んで、コンパイルされたコードが、デバイスが一時的に侵害された前後でメッセージを保護し続けるといった重要なセキュリティ特性を、デバイスで実行されている正確なコードまで満たしていることを証明しました。実際の脆弱性は、設計と実装の間のギャップに隠れていることが多いため、このギャップを埋めることは、これらの証明をはるかに複雑にします。

この複雑さにもかかわらず、私たちの検証プロセスはわずか4週間で完了しました。これは、歴史的に専門家チームが数年かかる作業であり、Signalのコア暗号化コードが、私たちの専門家が指定したセキュリティ保護を提供することを証明しました。

AlphaProof Codeが正しいコードとバグのあるコードを区別できることを確認するために、以前修正された2つの実際のバグをSignalのコードの分離されたバージョンに再導入しました。どちらの場合も、システムはバグのあるバージョンが安全でないという機械チェック済みの証明を生成しました。

AlphaProof Codeでは、AIエージェントがユーザーが仕様を作成するのを支援し、その後、実装がそれを満たしていることを自律的に証明します。すべての証明はLeanによってチェックされ、エージェントの作業を検証します。

以前の形式検証作業は必然的に小規模な範囲に焦点を当てていましたが、この新しいアプローチは大幅な拡張を可能にします。従来、本番コードが暗号化設計と厳密に一致していることを検証するには、広範な手作業が必要でした。そのため、AIエージェントを使用してライブコードを有効なLean定理に自動的に変換することは、大きなブレークスルーとなります。AI駆動のセキュリティ脅威が増大する中、コアSignalプロトコルが自動定理証明によって厳密に検証されていることは、コードがプライバシー保証を果たしていることへの信頼をさらに高めます。

セキュリティの未来

この長年の課題の達成は、AIがビジネス、政府、および重要インフラストラクチャにエリートレベルのセキュリティ保証をもたらし、エージェント駆動型のサイバー脅威から防御するのにどのように役立つかを示しています。

Signalのコア暗号化の検証は、医療機器のファームウェアから電力網のソフトウェアまで、他の重要なシステムを保護するための基盤を築きます。

これらの技術をスケーリングするには、継続的な研究が必要です。自動化された防御エージェント（CodeMender など）と組み合わせることで、形式検証は、現代のサイバー脅威の速度と規模に対抗し、保護機能が機能することを数学的に証明されたソフトウェアを作成するのに役立ちます。

コミュニティでの使用のために、形式検証アーティファクト をオープンソース化しています。技術論文を以下でご覧ください。

謝辞

この研究は、Swarat Chaudhuri、Andrew Ferraiuolo、Anton Kovsharov、Tej Chajed、Sam Schlesinger、Karn Seth、Jonathan Katz、Charles Sutton、およびPushmeet Kohliによって開発されました。

コードのオープンソース化への協力にEric Wieser氏、プログラム管理サポートにOwen Jones氏、有益な議論にMartín Abadi氏、Christopher Henson氏、Katerina Hristova氏、Henryk Michalewski氏、Jonathan Protzenko氏、George Tsoukalas氏に感謝します。方法論に関するフィードバックをSignalのRolfe Schmidt氏、Michael Rosenberg氏、Ehren Kret氏に感謝します。また、プロジェクトへの支援にTulsee Doshi氏、Four Flynn氏、Kate Olszewska氏、Alicia Huang氏、Andy Liu氏、Benoit Schillings氏、Raluca Ada Popa氏、Melvin Johnson氏、Koray Kavukcuoglu氏、Demis Hassabis氏、Sundar Pichai氏に感謝します。

---