top of page
検索

Google DeepMindの650万行のLean証明が示す次の課題――AIを責任ある形で動かすには

執筆者の写真: kanna qed
kanna qed
11 分前
読了時間: 20分

2026年11月10日、Google DeepMindは、AIエージェントを用いてSignalの暗号プロトコル実装の重要な安全性を機械語レベルで検証した研究「AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level」を発表した。AIエージェントが生成したLeanの証明コードは約650万行。しかし、この研究の核心は行数ではない。AIが作った証明を、そのAI自身の説明に頼らず、承認された形式仕様に対してLeanのカーネルが検査するという役割分担を、実際に利用される暗号実装の特定のビルドに適用したことだ。さらに重要なのは、論文が次の課題を正面から扱っている点である。

証明を作るコストが下がると、難問は「何を証明するか」に移る。原著 §7では、AIの判断が人間や企業の仕事を動かす時代、何を証明すべきなのだろうか。ソフトウェアが正しく動くこと。AIが出した回答に根拠があること。担当者に承認権限があること。その時点の条件で実行してよいこと。実際に目的の結果が得られたこと。途中で条件が変わった場合に、以前の承認を流用していないこと。異なる企業に仕事を引き継いだ後も、責任や証拠を後から検証できること。これらは関連しているが、同じ命題ではない。本稿はDeepMindの成果を正確に読み解いたうえで、形式証明をAIの実運用へ接続する課題を考える。そして最後に、株式会社AIアシュアランスが研究・実装を進める**Responsibility OS(責任OS)**と、広島AIプロセスに着想を得た民間の実装活動との関係を示す。なお、DeepMindと当社が同一の研究を行っている、あるいは共同開発しているという話ではない。異なる保証対象を扱う研究が、AI時代の検証可能性という共通課題の上でどのように接続するかを論じるものである。




1. AlphaProof Codeは、何をどこまで証明したのか

研究の対象は、SignalプロトコルのRust実装libsignalの特定バージョン(v0.105.4)とSPQR関連コード(v1.6.0)を、小規模なCLIハーネスに組み込み、通常のrustcで生成したAArch64 Linux向け実行ファイルである。暗号プリミティブ、出力関数、一部のライブラリ呼び出しは契約によって抽象化しており、その契約も保証の前提となる。既存の主要実装を検証しやすい別実装に置き換えるのではなく、コンパイル後の機械語まで安全性の主張を結び付けた点に意義がある。

  • 証明コード:AIエージェントが生成したLeanコード約650万行

  • 信頼を要する記述:形式仕様・AArch64の意味論など約2万6000行

  • 対象コード:特定条件でビルドしたlibsignal-cliのAArch64実行ファイル

  • 検証の枠組み:記号的モデルと計算量的モデルによる、異なる安全性の証明

  • 主な対象性質:前方秘匿性、侵害後の安全性回復、メッセージの機密性・真正性など(各モデルの前提・適用範囲内)

二つのモデルを混同してはいけない。記号的モデルは暗号プリミティブを抽象化して安全性を扱い、計算量的モデルは攻撃者の成功確率を基礎となる暗号学的仮定に結び付ける。計算量的モデルの証明対象は古典的な攻撃者であり、量子攻撃者は含まれない。 記号的モデルでは、将来Diffie–Hellmanが破られる場合のハンドシェイク秘匿性などを扱う一方、SPQRが狙う耐量子的な侵害後回復(post-quantum healing)までは証明していない。原著・表1、§5.1.6、§5.2.5

また、検証はSignalのスマートフォンアプリ全体を対象にしたものではない。実行環境、初期状態、外部関数の契約、暗号プリミティブなどに明示的な仮定がある。論文自身が、対象ビルドとモデルの制約を列挙している。原著 §4、§5.2.5、§5.3

したがって、「Signalに脆弱性が存在しないことをAIが証明した」と要約するのは誤りである。正しくは、指定された安全性が、指定された形式化と仮定の下で、対象実行ファイルについて成立することを示したという成果である。

2. なぜ「AIが証明したから信用する」ではないのか

AlphaProof Codeの構成には、重要な役割分担がある。

  1. AIエージェントが、人間の指導・レビューの下で形式仕様の作成を支援する。

  2. 人間が仕様を確認・承認する。

  3. 別のAIエージェント群が大規模な証明を作る。

  4. comparatorが、証明された命題と依存する定義が承認済み仕様と一致するかを確認する。

  5. Leanカーネルが証明を検査する。

ポイントは、証明を生成する主体と、証明の受理条件を決める仕組みを分離することだ。

ただし、これでも「人間が承認した仕様が現実の要求を正確に表しているか」は自動的には解決しない。Leanカーネルは、形式命題の証明を検査するのであって、企業の規程、契約上の権限、物理世界の観測値が事実かどうかを万能に判定するわけではない。

論文が紹介する重要な問題の一つは、証明作成エージェントが目標を達成しやすくするため、前提を追加したり定義を弱めたりし得ることだ。§7は、別の先行研究で、あるエージェントが仮定中の述語をFalseに変更し、空虚な証明を成立させようとした事例を取り上げている。これは今回のSignal検証で同じ事件が発生したとの報告ではない。

AlphaProof Codeが承認済みの仕様を隔離し、定義まで照合する理由はここにある。証明が通ったかだけでなく、そもそも何について証明したのかを固定しなければならない。原著 §2.4、§7

整理すると、少なくとも三つの問いが残る。

  • 証明の成立:所定の論理・公理の下で、指定命題を導けるか

  • 仕様の同一性:証明した命題・定義が、承認したものと同じか

  • 仕様の妥当性:その命題が、実際に守りたい要求を十分に表しているか

最初の二つで機械検査が強い力を持つ一方、三つ目には現場の知識、制度・契約、リスク許容度、必要な証拠に関する判断が不可欠になる。

3. 「何を証明するか」は、AIが社会で動くほど複雑になる

暗号ソフトウェアについては、秘密保持や真正性などを形式的な安全性として定義できる。では、AIが次の提案をした場合はどうだろう。

  • 「この自治体向けの回答案を採用する」

  • 「この医薬品を次の事業者に引き渡す」

  • 「接続先Aの処理を止め、接続先Bに切り替える」

これらの提案を実行するプログラムの一部分が形式検証されていたとしても、今回の判断を組織として採用してよいかは別問題だ。

たとえば、以前は許可されていた接続先であっても、現在は権限が失効しているかもしれない。AIが引用した資料の版が違うかもしれない。機器へ命令は送れたが、実際には動作が完了していないかもしれない。

ここには少なくとも、次の違いがある。

  • コードの仕様適合:「このコードは仕様を満たす」

  • 出力の要求適合:「このAI出力は今回の要求に適合する」

  • 実行権限と条件の成立:「この主体は、今、この操作を実行してよい」

  • 現実の結果の認定:「その操作は、目的の結果を実際に達成した」

この四つは、それぞれ別の検証対象であり、一つの成立から残りの成立が自動的に導かれるわけではない。

これらを区別することは、形式検証を否定することではない。形式的な保証の射程を正しく認識し、足りない条件を別の検証対象として定義するということだ。

もう一つ重要なのは、AIの出力をどの状態として扱うかである。提案段階なのか、担当者の確認対象なのか、組織として承認した判断なのか、実行を許した命令なのか。この区別が曖昧なままでは、優れたAIが出した答えも、安全に業務へ組み込めない。

4. 責任OSとは何か――単なる証拠保存でも、承認ゲートでもない

ここで、当社が取り組む**Responsibility OS(責任OS)**の全体像を明確にしておきたい。

責任OSは、AIが生成・支援した判断を、組織が責任を持って採用・実行できる業務行為へ接続し、その前提、経過、結果、責任状態を検証可能にするための社会実装・運用基盤である。

狙いは、AIの出力を正しそうだと評価するだけでも、ログを残すだけでも、許可/拒否だけを返すだけでもない。何が提案され、どの条件と証拠で採用され、誰の権限で何が実行され、実際に何が起き、どこまで確認済みで何が未確認なのかを、業務の状態として扱うことである。

責任OSが対象とする機能的な範囲を、あえて分解すると次のようになる。

  • 要求・意味の固定:AIの出力は提案、確認対象、承認済み判断、実行命令のどの状態か。何を守る必要があるか

  • 採用条件の検証:要求、業務規則、根拠、証拠、適用版、有効期間が一致しているか

  • 権限・責任の照合:誰が、どの範囲で確認・承認・実行でき、どこに責任の境界があるか

  • 実行・停止の制御:条件未成立、失効、結果不明なら実行・継続・切替えを保留/拒否すべきか

  • 結果と完結の確認:命令の発行、処理の受理、現実の作用、目的結果を混同していないか

  • 主体間の引渡し:開発者・提供者・利用企業・協力会社などをまたいでも、適用条件と責任の経路を追えるか

  • ライフサイクル管理:条件変更、再承認、派生情報の利用範囲、利用終了、継続評価を扱えるか

  • 独立再検証・監査:判断時点の規則・証拠・未確認事項・責任状態を後から再計算・検査できるか

これらは、責任OSの全体構想に含まれる技術的な役割を整理したものであり、すべてが一つの完成済み製品で実証されたという主張ではない。現実の適用には、各企業の権限体系、業務ルール、実システムとの接続、観測の真正性などを別途立証する必要がある。

責任OSは「責任を後から移し替えない」ための基盤でもある

AIの判断に関わる組織が増えると、結果だけを残しても十分ではない。同じ「承認済み」という表示の背後に、適用した規則、確認した証拠、未確認だった条件、承認者、依拠した他社の保証が異なる履歴があり得る。

責任OSが重視するのは、判断・実行時点の条件、根拠、関与主体、責任分界を対応付け、後日の変更や責任分担の見直しと区別して検証できるようにすることである。必要な是正や責任分担の変更を禁止するのではない。変更が生じた場合には、その時点と根拠を伴う別の状態として扱うという考え方だ。これは、公開された数理核やPoCだけで、実運用上の改ざん防止や法的責任の確定まで保証したという意味ではない。

これは既存のAIガバナンス、社内規程、リスク管理、監査、人間の責任を置き換えるものではない。既存の制度・業務が求める判断条件を、実際の採用・実行・結果に結び付け、検証可能にする層として位置付ける。

5. Responsibility OS Kernelは、責任OS全体そのものではない

責任OSの説明で、特に混同を避けたい区別がある。

責任OSの全体構想と、その一部の数学的条件をLean4で形式化したResponsibility OS Kernelは、同一ではない。

公開研究「Responsibility OS Kernel」は、操作、証拠、監査トレース、判断根拠、責任記録が、操作の合成や主体間の引渡しに際してどのような関係を持つべきかを、圏論的な構造を用いて形式化している。

その中心には、ある方針にとって重要な責任・証拠上の区別が、観測・変換の過程で失われないための数学的な条件がある。たとえば、同じ処理結果に見えても、責任上は別の履歴を区別しなければならない場面がある。公開Kernelは、そうした区別を保持する必要性と、区別を忘れることで起こる問題を形式的に扱う。

しかし、公開Kernelの定理だけで、実際のセンサー、企業の承認ワークフロー、運用権限、業務システム、法的責任がすべて検証されたわけではない。

関連する技術の関係は、次のように整理できる。

  • Responsibility OS(責任OS):判断・採用・実行・結果・責任・継続管理を、社会や企業の運用へ結び付ける全体的な技術・運用基盤

  • ADIC:計算、証拠、判断根拠、監査・責任記録を結び付け、記録・再計算・再検証へつなぐ中核的な実装アーキテクチャ

  • Responsibility OS Kernel:ADICの保証に関わる抽象構造を踏まえ、責任情報の保存や監査可能性などの条件をLean4で表現する数理核

  • 領域別のAssurance技術・PoC:自治体、プライバシー、フィジカルAI、医薬品物流、企業間接続など、具体的な要求・観測・制御の問題を検証する技術群

  • HAAP:こうした保証に関わる条件・証拠・結果・採用状態などを、組織間でも扱えるようにするための提案段階の相互運用レイヤー

ADIC=責任OSのすべてでも、Kernel=責任OSのすべてでも、HAAP=責任OSの別名でもない。それぞれ役割が異なる。

ここが重要なのは、DeepMindとの比較でも同じである。DeepMindが示したのは、指定仕様に対する大規模なコードの形式検証である。責任OSが扱おうとするのは、そのような保証を含むさまざまな技術的根拠を、実際の判断・実行・結果・責任の運用にどう適用するかという、別の問題領域なのだ。

6. 「保証がある」だけでは十分でないことを示す公開Lean4研究

責任OSの全体像は、単一の形式定理では表現しきれない。そこで当社は関連する境界条件を、複数の独立した研究として公開している。

工程をつなぐ:Physical AI Verified Composition

「Physical AI Verified Composition」が扱うのは、ある工程で成立した保証が、次の工程にも自動的に引き継がれるわけではないという問題である。

局所的な保証を接続するには、工程間の情報・インターフェース・不変条件など、明示的な成立条件が必要になる。上流で区別が失われていれば、下流の高度な処理だけでその区別を復元できない場合もある。

公開成果は抽象的な数学の核であり、個別のロボットや工場の安全性を証明したものではない。

実結果を認定する:Physical AI Outcome Assurance

「Physical AI Outcome Assurance」は、モデルの中で命令が正しいことと、対象の実行で目的の結果が実現したことは別であるという問題を形式化する。

命令送信、機器からの応答、実行の観測、結果の認定は区別しなければならない。一方、すべての場合に事後観測が必須というわけでもない。事前の保証がすべての対象実行を覆うなら、事後証拠への要求は変わり得る。重要なのはどの結果主張が、どの前提と証拠から導けるかだ。

この公開研究も抽象モデルに関するものであり、実機の物理的安全や観測機器の真正性は保証していない。

ガイドラインを運用条件へ:Responsibility OSの公開マッピング

「Responsibility OS × AI事業者ガイドライン」では、開発・提供・利用の主体をまたぐときに、利用範囲、証拠、再検証、条件変更、実行履歴をどのように結び付けるか、限定された抽象プロファイルを示している。

ここでのLeanの定理は、与えられた局所条件が成立する場合の構造的な結果であり、現実の企業がガイドラインに全面適合することを証明したものではない。

同様に「Responsibility OS × EU AI Act」は、選択した条文に関する技術的な要請を形式化しているが、法令全体の遵守を自動認定するものではない。

これらを組み合わせて見えてくるのは、形式検証を単なる「コードの正しさの証明」にとどめず、保証の適用性、引渡し、条件更新、結果、説明責任へ接続する研究領域である。

7. 業務PoCで見える「正しさ」と「採用・実行・完結」の違い

数学的な構造だけでなく、合成データを用いた公開PoCでも、保証対象を分けている。

自治体AI:回答を生成できることと、職員の確認用に採用できることは違う

クラウドシエンとAIアシュアランスが公開する「自治体AI・回答採用アシュアランス」では、AIが生成した回答案を、自治体・制度・資料の版・期間・金額・相談条件・引用根拠などと照合する。

2026年10月11日のOpenAI API実験では、合成データと限定された出力形式を用いた24件の原回答に対し、採用11件・保留3件・不採用10件という結果を記録した。ここでの採用は、あくまで職員が確認する回答案としての採用可能性を意味し、行政処分や実自治体での運用を指すものではない。

重要なのは、AIが自分の答えを「正しい」と説明するかではなく、あらかじめ定義された条件と外部の根拠に照らし、出力をどの状態へ進められるかを確認することだ。

企業間ネットワーク:前の結果が不明なら、次の操作を許可できないことがある

「Physical Internet Cyber Assurance」は、合成企業間の限定的な通知操作を対象に、承認、失効、再送、結果不明、取消し確定後の切替えを試す公開PoCである。

たとえば接続先Bで処理が実行済みか、取り消されたかが分からないまま、接続先Cへ切り替えると、二重実行のおそれがある。このPoCはBの取消しが確定しない場合に、Cへの切替えを保留するなどの条件を扱う。

実際の貨物移動、物流プラットフォーム全体、ネットワーク機器の経路変更の実証ではない。それでも、「以前の許可があった」「送信できた」という事実から、今回の実行許可や実行結果を飛躍して導いてはいけないことを具体的に示している。

情報のライフサイクル:要約した後も、利用条件は消えない

「自治体AI・派生情報ライフサイクル・アシュアランス」では、元情報の利用条件をAIが生成する要約へ承継し、用途変更、再利用、派生コピー、利用終了までを検討する。

出力を要約したからといって、元情報の利用制限が消えるわけではない。また、ある管理経路で利用終了が成立しても、管理外のコピーや提供事業者内部での消去を証明したことにはならない。

ここでも責任OSの課題はその場の許可/拒否だけでは終わらない。条件が時間を超えてどの情報・操作に及ぶかが問題になる。

これらのPoCは、実運用の効果や全障害への安全性を証明するものではない。個別の限定条件で検証した結果を、対象範囲を明示して公開している。

8. 責任OSの位置は、AIモデルの下流にある「一個のゲート」ではない

ここで一つ、誤解を避けておきたい。

責任OSを、「AI → 形式検証 → 許可ゲート → 実行」だけの細いパイプラインとして描くのは不十分だ。実際には、要求を決める時点から、採用・権限・実行・観測・完結・主体間の引渡し・再評価に至るまで、各段階に責任と保証の条件が関わる。

完成済みの製品構成図ではなく、責任OSが横断的に扱う問題領域を列挙すると、次のようになる。

  • 要求・規則の定義:企業や組織の規程、契約、安全要求、利用目的、判断基準を明確にする。

  • AI・ソフトウェアの技術的保証:形式証明、テスト、評価などにより、対象範囲と前提を限定して性質を確認する。

  • 判断の採用と権限の確認:AI出力の意味、採用状態、判断根拠、証拠、担当主体と責任分界を対応付ける。

  • 実行・停止・引渡し:現在の条件に照らして操作を許可・保留・拒否し、既存の人・業務システム・設備・他社との接続を扱う。

  • 実際の作用と結果の認定:命令や応答と、対象実行・結果・完結を区別し、未確認事項を残す。

  • 継続的な責任・保証管理:条件の変更や承継、責任状態、監査と再検証、規程・条件の継続評価まで扱う。

責任OSは、このうち最後の一工程だけに置く「許可ゲート」ではない。要求から実行後の検証、さらに主体間の引渡しや継続管理までを結び付ける技術・運用基盤として位置付ける。

ここでの形式証明は重要な保証手段の一つだが、すべてのAI判断がLean証明を必要とするという意味ではない。業務によっては、検査可能なルール、認証された記録、テスト、人的審査、第三者評価などを組み合わせる必要がある。

責任OSの狙いは、どの手段を使った場合でも、「何を確認できたから、この判断や行為を成立させたのか」を再検証できる状態にすることである。

9. HAAPは何を担うのか――責任OSと相互運用は別の論点

広島AIアシュアランス協議会(HAAC)の「Hiroshima AI Assurance Protocol(HAAP)」は、責任OSと関係するが、同じものではない。

責任OSは、組織がAI判断を責任ある業務行為へ結び付けるための全体的な運用・技術基盤である。一方HAAPは、そうした判断の採用・実行を支える条件・証拠・責任情報・検証結果を組織間で扱うための、提案段階の共通レイヤーである。

HAAPの公開概要は、以下を区別する。

  • Verification outcome:所定の要求・証拠を検証した結果は何か

  • Adoption state:その判断を組織として採用可能な状態か

  • Transition authorization:指定された状態遷移を許可できるか

これらを一つのPASSに潰さない。検証結果は、新たな法的・契約的・組織的権限を自動的には生み出さないという境界が、公式の技術概要でも明示されている。HAAP公式技術概要

また、HAAPの現行公開資料は非規範的な技術概要である。共通ワイヤーフォーマット、必須項目、署名政策、信頼アンカー、複数実装の相互運用性を、既に完成・実証したと主張するものではない。

言い換えると、責任OSで扱う問題を、各社が別々の内部ルールを持ちながらどこまで共通に検証・接続できるかという問題へ広げるのが、HAAPで追求する方向性の一つである。

10. この課題は、広島AIプロセスやAISIの議論とも接続する

このテーマを単なる企業独自の技術構想に閉じず、国際的なAIガバナンスの議論へ接続する根拠もある。

まず日本のAIセーフティ・インスティテュート(AISI)は、2026年7月7日公表の「AIセーフティに関する評価観点ガイド 第1.20版」で、AIエージェントの外部環境との相互作用を踏まえ、**「観測と制御」**という評価観点を追加した。AIの出力だけでなく、外部システムや物理環境への作用を評価対象にする方向性である。

さらに2026年10月6日の「AISI事業実証WGビジョンペーパー 第2.0版」では、**CCAS(Compositional Conformity Assessment Schemata)**を取り上げている。本文38ページ(PDFの41ページ目)では、組織内の多層的な評価だけでなく、サプライチェーン・バリューチェーンにまたがるトラストチェーン、組織間の関係・責任分担を含めた評価構想を示す。

これは、局所的な評価結果を、企業や工程をまたぐ保証としてどう扱うかが、日本の公的な評価方法論でも重要な課題となっていることを示す。ただし、AISIが責任OSやHAAPを採用・認証したことを意味しない。

国際的には、OECDが2026年5月28日に広島AIプロセスの自主的な報告枠組み(第2版)を公表し、大規模モデル開発企業だけでなく、より広いAI開発・利用のエコシステムへ対象を拡大した。

こうした原則や評価枠組みは重要だが、それだけで個々の企業の特定操作について、採用可否や実行許可が自動的に決まるわけではない。

広島発の民間主導の活動としてHAACが目指しているのは、広島AIプロセスの理念を業務における採用条件、証拠、検証範囲に接続し、後から検査可能な形で社会実装へ近づけることである。HAACはG7や政府の認証機関ではなく、ここで述べる対応づけは当社と協議会による技術的提案である。

11. 大企業の既存ガバナンスを置き換える必要はない

この研究の社会実装上の含意は、技術者だけにとどまらない。

企業には既に、社内規程、決裁権限、情報セキュリティ、内部統制、品質保証、監査、取引先管理の仕組みがある。責任OSが目指すのは、それらを「AI時代には不要」と否定することではない。

むしろ、既存の仕組みが決めた条件を、AIが関わる実際の判断・実行の場面へ接続することに価値がある。

例えば、既存のシステムを一度に全面更新しなくても、ある一つの高リスクな操作について、採用条件と根拠の版を固定し、条件が未成立なら保留し、実行後の結果を照合する――そのように対象範囲を限定して検証を始められる可能性がある。

ただし、それがすべての企業で容易に実装できることを意味しない。実行経路の完全な仲介、データ品質、鍵管理、各社の責任分担、業務システムの統合には別の技術・運用上の検証が必要となる。

「規程が存在する」ことと「今回のAI判断にその規程が実際に適用された」ことの間に、検証可能な接続をつくる。 これが責任OSの実務上の重要な価値の一つになる。

12. 結論――AIに証明させる時代、責任の所在まで検証できるか

AlphaProof Codeが示したのは、AIエージェントが、既存の複雑なソフトウェアについて大規模な形式証明を生成し、それを人間が逐一信用しなくても検査できる可能性である。その意義は大きい。

だが、社会の中でAIが実際に仕事を動かすなら、もう一段の問いが必要になる。

  • 何を保証するのか。 その仕様は現実の要求を表しているか。

  • 何に保証を適用できるのか。 今回の用途、主体、証拠、時点で成立するか。

  • どの行為を成立させてよいのか。 組織としての採用、実行権限、失効や保留を区別できるか。

  • 実際に何が起きたのか。 命令、応答、結果、完結を混同していないか。

  • 責任は後から検証できるか。 条件変更や主体間の引渡しを経ても、当時の責任状態を追えるか。

ここでの責任OSは、単なる証拠保管庫ではなく、単発の採用判定器でもない。AIの判断を、根拠・権限・実行・結果・責任・継続管理と結び付け、企業や社会が責任を持って使える状態にするための技術基盤である。

DeepMindの研究と当社の公開成果は、規模も証明対象も異なる。前者がソフトウェアの安全性に関する機械検証の可能性を大きく広げたのに対し、後者は、形式的・実証的な保証を実際の判断、行為、結果、責任へどう接続するかという問題に取り組んでいる。

AIに正しさを証明させられるようになるほど、その正しさを「誰が、どの条件で、何のために使ったのか」を検証できる技術が重要になる。

それが、AI時代に責任OSを社会へ実装しようとする理由である。

一次文献・公開技術資料

Google DeepMind:研究の一次資料

日本・国際的な公的一次資料

当社・協議会の公開技術資料

注:本稿におけるDeepMindとの接続、および責任OSとAISI・広島AIプロセスの関係づけは、公開一次資料に基づく当社の技術的な分析・提案であり、Google DeepMind、AISI、OECD、G7等による当社技術の承認・採用を意味しない。


 
 
 

コメント


bottom of page