Provable inference: FlashProveで推論の出どころを証明する仕組み

要点

2026年11月2日、AnthropicのFrontier Red Teamが、AIの応答が「約束どおりのモデル」から出たことを暗号で証明する研究を公開しました。名前はFlashProve。Meta製の4000億パラメーター級モデルLlama 4 Maverickを対象に、H100 1枚で毎秒110トークンの速さで証明を作り、証明1件は約19MBに収まります。

先に断っておくと、これは研究の途中経過を示す試作です。Claudeの配信にすぐ入る話ではなく、証明できるのは1,024トークンまでの文脈、しかも欲張りデコーディング(確率的に選ばず常に最有力を選ぶ生成)に限られます。この記事では、何を解決しようとしているのか、数字をどう読むか、どこが未解決かを順に追います。

背景 — 応答だけでは「どのモデルか」を見分けられない

人と会うときは顔も声も手がかりになります。AIモデルとのやり取りには、それがほとんどありません。ユーザーは、開発元が名乗るモデルが応答したのか、費用を抑えるために仲介サービスがこっそり差し替えた別のモデルなのか、通信路でトークン列を書き換えた攻撃者なのかを、出力だけでは判別できません。出力の質が高くても同じです。

発表は、この確認が欲しくなる場面を4つ挙げています。

想定用途

出どころの証明が効く4つの場面

• ペース調整(pacing)

  規制当局が、事業者の計算資源が推論に使われていることを確かめる場面です。証明の提出で推論の実行は確かめられますが、推論と並行して訓練していないことまでは示せません。

• 改ざん検知

  推論サーバーが侵害され、重みの持ち出しや悪意ある応答の混入が起きる場面です。より高度なモデルが、監視の緩い弱いモデルのふりをして動く事態にも触れています。

• 文章の来歴

  「このコードは先端のセキュリティ用モデルで脆弱性を調べた」といった主張の裏づけです。チャットログの公開だけでは偽造を排除できません。

• モデルの承認

  安全と認められたモデルだけを提供させる場面です。承認外のモデルを使えば、証明が検証を通りません。

どれも、重みを持たず計算資源も乏しい検証側が、重みを見ずに確かめられる必要があります。重みは多くの先端モデルで非公開であり、仮に手元にあっても再実行には大きな計算資源が要るからです。これが、検証可能推論(provable inference、略してPI)の課題設定です。

Frontier Red Teamの役割についてはClaudeのレッドチームの解説に、同チームが暗号分野で続けてきた成果は暗号方式の弱点の発見とECDSA曲線のシードの解明にまとめています。今回は、攻める側ではなく証明する側の仕事です。

zkSNARKは何を保証するのか

FlashProveが使うのは、ゼロ知識で簡潔な論証(zkSNARK)という暗号の道具です。証明する側(prover)が短い証明書を渡し、検証する側(verifier)が「この計算は正しく実行された」と納得できる仕組みを指します。

保証は4つの性質に分かれています。

前の2つだけなら、重みを持つ側が自分で再計算すれば済みます。ゼロ知識と簡潔性が加わって初めて、「重みを見せずに、軽い計算で確かめる」という要件が満たされます。ただし隠れるのは重みであり、モデルの構造(アーキテクチャ)は隠れません。証明はハッシュ関数に依拠する方式で、発表はポスト量子安全性(量子計算機に対する耐性)も得られるとしています。

ハードウェアの隔離環境(TEE)に頼る方式もありますが、発表は今回、計算問題の困難さだけに安全性を預ける純粋なソフトウェア方式に絞ったと書いています。両者は補い合う関係で、どちらか一方で全課題が片づくわけではない、という立場です。

FlashProveの2段階 — 重みの指紋と、トークンごとの証明

仕組みはオフラインとオンラインの2段階です。

手順

FlashProveの流れ

1. 1

   オフライン: 重みへのコミットメントを公開

   証明側が、重みを隠したまま1通りの重みを特定する短い指紋(コミットメント)を公開します。モデル1つにつき1回で、約39分かかります。

2. 2

   オンライン: 応答ごとに証明ファイルを作る

   プロンプトと出力トークンを受け取り、「コミットしたモデルがこの出力を生成する」という主張の証明を作ります。

3. 3

   検証: 手元のCPUで確認

   コミットメントとプロンプトと応答を持つ人が、GPUなしで証明を確認します。

注目は、証明を応答と同時に作らない設計です。応答を返し終えたあとで、完成した文章を並列に読み直す形(プレフィルに近い処理)で、事後に証明を作ります。コミットメントを開く作業も、リクエストごとではなくバッチごとに1回です。

事後方式には利点と代償があります。インライン方式は非常に速くできる反面、効率と引き換えに安全性を削る恐れがあります。事後方式は遅くてもよいので、その引き換えを避けられます。代償として、再計算の複雑さ、保証を得るまでの遅れ、非決定性が残ります。

数字で読む性能

数字

Llama 4 Maverick(4ビット量子化)での実測

• 証明の生成速度

  約110 tok/s

  24件を約223秒で処理

• 証明1件のサイズ

  18.78 MB

  1,024トークンの要求あたり

• 検証時間

  17秒

  24スレッド。1スレッドでは21秒

• vLLM比のGPU時間

  約70〜95倍

  24件まとめて約72倍(実行ごとに66〜77倍)、最大負荷で約94倍

検証側が最初に受け取るコミットメントは約6.5MBです。コミットメントの有効範囲は約1,600万リクエストで、超えたらコミットし直します。処理対象のモデルは4000億パラメーターで、量子化版でも約232GBあります。それでも証明は19MB、確認は秒単位で済みます。これが簡潔性の効き目です。

比較対象のvLLMは、同じモデルのFP8版を8枚のH100で動かした結果です。1枚あたりに直すと、24件をまとめて処理する時間の約72倍、負荷を最大にした条件では約94倍になります。証明を付けると、GPU時間は2桁ほど増えます。

先行研究との距離

発表は、zkML(機械学習の推論をゼロ知識で証明する研究)の流れの中に今回の成果を置いています。数字が揃うところだけを並べます。

同じ4000億パラメーターのモデルで比べられるのはVerInfだけです。そのVerInfが毎秒0.02トークン、証明が93.6GBで検証に約1日かかったのに対し、FlashProveは毎秒110トークン、証明19MB、検証17秒です。桁がいくつも動いています。

Attestableは密モデルなので、条件が違います。比較は「方向が同じ」という程度に読むのが安全です。

70〜95倍のコストをどう受け止めるか

毎秒110トークンは、配信速度ではありません。証明を作る処理が、通常の推論に対して70〜95倍のGPU時間を要するという意味です。全リクエストに証明を付けるには、推論と同じ規模の設備が数十倍必要になります。

そのため現実的なのは、全件ではなく一部を事後に証明する使い方です。事後方式で、一部のトークンだけを対象にできる設計は、この使い方と噛み合います。上の4場面のうち、規制当局への提出や文章の来歴のように、あとから示せることに価値がある用途が候補になります。

効率の工夫は3点あります。

• 証明の作業量が、実際に動いた専門家の分に比例する(1トークンあたり約170億パラメーター分。ただしどの専門家が選ばれたかは隠れたまま)
• 要求をバッチにして事後に証明する
• 層ごとの重みを区切り、順にホストメモリから流し込むことで、80GBのGPU 1枚と約290GBのホストメモリで収める

混合専門家(MoE)という構造に乗った最適化です。著者は進歩が他のモデルや構造にも移せると見ていますが、密モデルへそのまま移せるかは別の話になります。

Leanで検証可能推論のどこまでが保証されるか

暗号のコードは壊れやすく、誤りを生みやすいものです。この研究では、Claudeが推論向けzkSNARKの改良を出し、最先端の手法の新しい適用方法も見つけています。Claudeは最適化に強い一方、評価しにくい判断をすることも多いため、Leanという形式検証言語で最上位の主張を機械検証する方針が取られました。Leanで証明されるのは、完全性、健全性、ゼロ知識の3つです。前提はランダムオラクルモデル(ハッシュ関数を理想化した解析の枠組み)です。

形式検証でも残る穴は2つあります。1つは、Leanで書いた主張が意図と合っているかの確認で、人手で読むしかありません。そのために対話式の可視化ツールが付きました。もう1つは、実際に動くコードが形式化したプロトコルと一致するかです。

ここで検証側のコードの扱いが分かれます。

• 健全性は検証側のコードだけが正しければ成り立つ。証明側を疑ってよいのが証明の価値そのものだから
• 公開された検証器は2つ。1つは遅いLean製で、定理の検証器が受理するものだけを受理することが証明されている。もう1つは日常用のC++製
• C++製の検証器に形式的な保証はなく、テストではLean製の検証器と全証明で結果が一致した
• ゼロ知識は証明側のコードだけが正しければ成り立つ。ただしLeanで書いた証明側は現実的に動かせないため、一致の確認は人間やエージェントによる監査に委ねる

つまり「全部が数学的に保証された」わけではありません。論文、Lean、高速な実行コードの三者が一致する保証はない、と制限事項に明記されています。ここを理解せずに「証明済み」と受け取ると、過大評価になります。

使えない条件 — 研究プロトタイプの限界

対象のLlama 4 Maverickは、Meta製のモデルをサードパーティーが4ビットに変換した公開版です。重みはリリースに含まれず、利用者がHugging Faceから自分で取得し、Metaのライセンスに従います。ClaudeのモデルがFlashProveで証明される、という話ではありません。

呼び名の変更 — provable inferenceからinference verificationへ

もう1点、読み落としやすい経緯があります。AnthropicはFrontier Safety Roadmapで、2026年9月30日までに「出力を特定のモデル重みに帰属できる形で署名する」検証可能推論の試作を作る、と公開目標を掲げていました。

10月19日の更新で、目標の名前は「inference verification(推論の検証)」に変わっています。理由は、元の狙いがトークン列の完全性に対する高い確信であり、それを得る道は複数あるのに、「provable inference」だと暗号による証明に狭く聞こえるためです。目標自体は、ここで取り上げたものとは別の、推論トラフィックに署名して信頼できるサーバーで再計算する取り組みで達成した、とRSPの更新で述べられています。

今回のFlashProveは、同じ目的に別の方法で迫る並行研究です。Roadmapの目標の経緯はFrontier Safety Roadmapの進捗に、方針文書の改定の流れはResponsible Scaling Policyの変遷にあります。

影響 — 当面の利用者と研究側に何が変わるか

この研究の核心は、速さの桁が動いたことです。4000億パラメーターのモデルで、先行の報告より何桁も速くなりました。ゼロ知識の証明が、先端規模のモデルでも検討の土俵に乗る水準に来た、という意味です。

一方で、日常の推論に付けて回れる段階ではありません。「使えない条件」の節で挙げた限界に加えて、形式検証も、高速な実行コードが形式化したプロトコルと一致することまでは覆っていません。公開された成果物は、ブログ記事、技術報告、プロトコル記述、実行コード(証明器と検証器2つ)、Leanの証明と可視化ツールの5点で、コードとLeanの証明、文書はApache 2.0です。他の研究者がこれを検証し、改良することが、発表の狙いそのものです。

利用者にとって当面の意味は、「応答の出どころを確かめる手段が、暗号の側から現実味を帯びてきた」という点にあります。仲介サービス越しにモデルを使う場合や、評価者が公開前後のモデルを確認する場合に効く話で、普段の対話の使い方が変わる段階にはまだありません。