AnthropicのFlashProve：証明可能な推論が証明すること、しないこと

2026年11月2日、AnthropicのFrontier Red Teamは、同社が「証明可能な推論（provable inference）」と呼ぶもののオープンソースのプロトタイプ、FlashProveを公開しました。AIの提供元が、ある応答が特定の1組のモデルの重みから生成されたことを、重みを見せずに証明する方法です。¹提供元のコミットメント、プロンプト、応答を持っていれば、誰でも普通のコンピュータで、GPUなしに、数秒で証明を確認できます。

デモに使われているのは、Metaのオープンウェイトのモデルで、パラメータ数4,000億のLlama 4 Maverickです。H100 GPU 1台で毎秒約110トークン分の証明を作り、1,024トークンのリクエストで証明は約19 MB、確認には約17秒かかります。Anthropicは今回の公開を「中間的な進展であり、完成した研究計画ではない」と位置づけ、コードのリポジトリは自らを、保守されない研究成果物としています。³

以下では、証明可能な推論が扱う問題、FlashProveのコミット、証明、検証の各ステップの仕組み、そのコスト、以前のシステムとの比較、証明が正確に何を述べ、何を述べないのか、現時点で実行できること、そして結果の背後にあるAIモデルを明記する研究の記録にとって何が変わりうるのかを順に紹介します。出典はすべて2026年11月3日に確認しました。

証明可能な推論はどんな問題を解決するのか#

AIモデルにプロンプトを送ると、応答と、サービスが表示するモデル名が見えます。その2つが本当に対応しているかは確かめられません。Anthropicの記事はこう述べています。「現在、モデルに問い合わせるユーザーは、応答が開発者の言う特定のモデルから来たものであって、ルーティングのサービスがコストの理由でひそかに差し替えたモデルや、トークンの流れを改ざんした攻撃者によるものではないことを確かめられない」。¹そして、「モデルの出力だけから判断するのは、たとえ質の高い応答を返していても信頼できない」。

すぐに思いつく確認方法も使えません。最先端のモデルの多くは重みが非公開で、重みがあったとしても、大きなモデルを再び実行して出力を比べるには、ほとんどのユーザー、さらには評価者でさえ持っていないハードウェアが必要です。記事の言葉では、証明可能な推論の目標は「計算資源が限られ、重みについての情報を一切持たないユーザーが、応答が要求したモデルから来たことを検証できるようにする」ことです。

記事は、それが重要になる4つの場面を挙げています。

• ペースの管理（pacing）。 提供元のチップを、新しいモデルの訓練ではなく、モデルの提供（サービング）に使わせたい規制当局は、ある期間に処理したリクエストを網羅する証明を求めることができます。Anthropic自身が限界を述べています。これは「ハードウェアが、たとえば裏で訓練をしていないことを立証するものではない」。
• 改ざんの検出。 推論サーバーを乗っ取った攻撃者や、弱いモデルになりすました強いモデルは、見つからずにいるためには、想定された重みについて有効な証明を作らなければなりませんが、それはできません。
• テキストの来歴。 開発者が、あるソフトウェアのライブラリを最先端のセキュリティ用モデルで検査したと言う。あるいは企業が、ある計画を特定のモデルが承認したと言う。記事は「チャットのログを公開しても、絶対的な保証にはならない」としています。ログは、より安いモデルや性能を落としたモデルで作れるからです。
• モデルの承認。 安全と承認されたモデルだけを提供してよいというルールがあれば、各応答に付けた証明が、どのモデルが答えたかを示します。

研究に最も近いのは3つ目の場面です。ある分析を特定のモデルで行ったと書く論文、開示文、記録は、現状では著者の言葉にすぎません。

この取り組みは、公に掲げた目標にも応えるものです。AnthropicのFrontier Safety Roadmapは、2026年9月30日までに「AIモデルの出力を、特定の1組のモデルの重みに帰属できる形で、確実かつ証明可能に『署名』する技術」のプロトタイプを作ると約束していました。記事によれば、Anthropicはこの目標を別のプロジェクトで達成しました。そのプロジェクトは「推論のトラフィックに署名し、信頼できるサーバーで推論を再計算する」もので、FlashProveは同じ目的を別の方法で追うものだとしています。2026年10月19日の更新で、目標は「推論の検証（inference verification）」と改名されました。トークンの流れについての高い保証は「いくつかの方法で達成できる」からです。

FlashProveはどう動くのか#

FlashProveには2つの当事者がいます。提供元（証明者）とユーザー（検証者）です。そして2つの段階と、確認から成ります。¹

証明はzkSNARKです。zero-knowledge succinct argument of knowledge（ゼロ知識の簡潔な知識の論証）の略です。Anthropicは4つの性質を挙げています。

• 完全性（completeness）。 正直な証明者の証明は受理されます。
• 健全性（soundness）。 「偽の命題について有効な証明を作ることは事実上不可能（つまり、広く信じられている暗号学的な仮定を破るのに等しい）であり、そのため検証者は証明者を信頼する必要がない」。
• ゼロ知識性（zero knowledge）。 検証者は「重み、計算の中間値、各層でどのエキスパートが動いたかについて、何も知ることがない」。モデルのアーキテクチャは隠されません。
• 簡潔性（succinctness）。 量子化した形で約232 GBのモデルの実行が、約19 MBの証明から数秒で確認されます。

構成はよく知られた手順に従っています。対話型オラクル証明（interactive oracle proof）を、ハッシュ関数を使って1つの証明ファイルに変えるもので、StarknetなどのEthereumのレイヤー2ネットワークが使うのと同じ系統の証明システムです。技術報告書は、これがハッシュ関数の安全性に依拠しており、そのため量子コンピュータに対しても安全だと考えられることを付け加えています。²信頼できるハードウェアは使いません。Anthropicは、何を実行したかを保証するチップである信頼できる実行環境（trusted execution environment）を、補完的な手法と位置づけています。その保証は製造元に依拠するのに対し、zkSNARKの保証は、解くことが不可能だと信じられている問題に依拠します。

速さの一部はモデルの設計によります。Maverickは混合エキスパート（mixture-of-experts）モデルです。各トークンは少数のエキスパートのサブネットワーク、つまり4,000億のパラメータのうち約170億だけを通り、FlashProveのトークンごとの作業もそれに沿います。それでも証明は、どのエキスパートが動いたかを隠します。証明プログラムは重みを通常のメモリから順次読み込む（ストリーミングする）ので、80 GBのGPU 1台と、その横にある約290 GBのホストメモリで足ります。

FlashProveはどのくらい速く、コストはどのくらいか#

Anthropicは、Llama 4 Maverickの重みの公開されている4ビット版を使い、1リクエストあたり1,024トークンのウィンドウ1つでFlashProveを測定しました。¹

証明には、応答を提供するより約2桁多いGPU時間がかかります。以前のシステムが必要としたよりはるかに少ないものの（次の節）、提供に比べればまだずっと多く、Anthropicは自らの手法を、提供するそばからすべてのトークンを証明するのではなく、事後の証明（post-hoc proving）、つまり「トークンの一部について、事後に証明する」ものと説明しています。技術報告書はその意味をはっきり書いています。事後の証明は「ユーザーが誤った応答を受け取ることを防ぐものではなく、改ざんが検出されることを保証するだけだ」。²

以前の推論の証明と比べてどうか#

ニューラルネットワークが正しく実行されたことを証明する分野には、暗号学でzkMLという名前があり、非常に遅い結果の短い歴史があります。Anthropicの記事はそれらを挙げています。¹

最も分かりやすい比較は、同じモデルでのものです。VerInfはMaverickを毎秒約0.02トークンで証明し、証明は93.6 GBでした。FlashProveは毎秒約110トークンで証明し、証明は19 MBです。Anthropicの結論は、証明のオーバーヘッドは「おおよそ2桁」で、「以前に予想されていたよりはるかに小さい」こと、そしてこの進歩は「より多くのモデルとアーキテクチャに移せるはずだ」ということです。最後の点は見込みです。FlashProveが示されたのは1つのモデルだけです。

FlashProveの証明は何を述べ、何を述べないのか#

証明が述べる命題は、意図的に狭くなっています。「コミットしたモデルを評価すると、これらの出力トークンが生じる」。¹これに頼ろうと考える人にとっては、速さと同じくらい限界が重要です。

示すこと。 コミットメントの背後にある重みをこのプロンプトで実行すると、まさにこれらのトークンが得られることです。正確には、公開された重みの厳密な整数版についての証明で、確認される各トークンは、そのモデルが次に出す可能性が最も高いトークンです。「証明は、貪欲デコーディング（greedy decoding）のもとでの整数モデルについてのものだ」。リポジトリの健全性定理では、q回のハッシュの問い合わせの後、偽の主張の証明が受理される確率は最大で約q/2^124 + 2^-101です。そしてLeanで書かれた検証プログラムについて、Leanがこの定理を機械で確認しています。⁴

示さないこと。

• 応答が正しいこと。 証明が扱うのは、どの計算がそのテキストを生んだかであり、テキストが真実か、筋が通っているか、安全かではありません。
• モデルの名前。 証明は応答をコミットメントに、コミットメントを1組の重みに結び付けます。その重みがどのモデルなのかは、コミットメントを公開した側がそう言っているだけです。重みが秘密なら、ほかの誰も確かめられません。
• サンプリングや浮動小数点による応答。 モデルは通常、浮動小数点で、サンプリングを使って提供されます。そうした応答は「ある位置でずれ、証明された計算と厳密には一致しなくなりうる」。整数モデルは浮動小数点の推論と「小さな誤差率の範囲に収まることが経験的に確かめられている」ものの、「これは敵対的に設計されたプロンプトを対象としていない」。技術報告書は、害のない数値的なノイズを改ざんと区別する統計的な手法を示しています。²
• 長い会話。 コンテキストは1,024トークンに限られ、「チャットで蓄積されるコンテキストと比べると、かなり短い」。
• ハードウェアがしたほかのすべてのこと。 先に述べたとおり、提供の証明は、同じチップが訓練もしていなかったことを示しません。
• アーキテクチャ。 隠されるのは重みだけです。
• 時間。 「証明の作成にかかる時間を測るような」サイドチャネル攻撃は、「今回の公開の対象外」です。
• 高速なコードが、証明されたコードであること。 Leanが健全性を証明しているのは、Leanの検証プログラムについてです。ユーザーが実行するC++の検証プログラムと、CUDAの証明プログラムは、「同じプロトコルに従うように書かれ、それに照らして試験されているが、それ自体は証明されていない」。重みを隠すことについて、リポジトリは率直です。「プログラムが重みを隠すことは、知っているのではなく、そう期待している」。⁴

AnthropicはFlashProveを作るのにAIをどう使ったのか#

今回の公開は、AIがどの部分を担ったかを明記したAI支援の研究の例でもあります。記事は「Claudeは推論のためのzkSNARKに改良をもたらした」とし、安全策をこう説明しています。「Claudeは最適化が得意だが、特に大規模で複雑なシステムでは、評価の難しい判断をすることが多い。私たちはこれに対し、主張する安全性の保証について、Lean（形式検証の言語）で監査可能な最上位の命題を示すことで対処している」。¹

技術報告書はさらに踏み込んでいます。²

• C++の証明プログラムと検証プログラムは「AIエージェントがLeanでの表現から作ったもの」で、「C++のコードとLeanの仕様の形式的な等価性は証明されていない」。
• リポジトリにある長いプロトコルの説明は「AIが生成したもので、私たちは詳しくは確認していない。入念に確認した論文を後で出す。これに対し、この報告書は著者たちが書いた」。
• 形式的な命題は「手作業とAIエージェントの両方で正しさを確認した。専門家が独立に監査するのに、数時間以上はかからないはずだと考えている」。

リポジトリのREADMEには「Built to be run by an agent」（エージェントが実行するために作られている）という見出しの節があり、コーディングエージェントに渡すプロンプトが載っています。検証プログラムをビルドし、保存された証明を確認し、結果を報告し、より重い作業を始める前には尋ねる、という内容です。³これは、ハーバード大学CMSAの報告書がAI支援の数学に求めている種類の、誰が何をしたかの記述です（AI時代の数学研究：ハーバード大学CMSAの報告書が勧めることを参照）。AIが担った部分、人間が担った部分、そして読者がなお確かめなければならないことです。

FlashProveは今使えるのか#

サービスとしては使えません。今回の公開にはAPIがなく、証明できるのは、証明プログラムを動かす人自身が実行するLlama 4 Maverickだけで、Claude、ChatGPT、Geminiの応答の証明は作りません。FlashProveはApache 2.0ライセンスのコードで、バージョンは0.16.0、「研究成果物：保守されず、貢献も受け付けない」と説明されています。³モデルの重みは含まれていません。読者が自分で、Metaのライセンスのもと、Hugging FaceからMaverickをダウンロードします。¹

リポジトリは4つのルートを示しています。

ルート1は手軽ですが、その例は合成の重みを持つ小さなモデルです。「検証プログラムが動くことを示すだけで、提供されているモデルについては何も示さない」。実際のものを証明するには、専用のH100と数百ギガバイトのメモリが必要です。自社のモデルにコミットして提供したい提供元は、リポジトリの提供のガイドと、運用者の責務の一覧に案内されます。後者は「秘密にしなければならない重みを使う前に、必ず読むべきもの」です。

研究の記録にとって何が変わりうるのか#

学術誌や助成機関のAIに関する方針は、著者に、使ったツールとモデルの名前を挙げるよう求めています（論文・レポートで生成AIの使用を明記する方法を参照）。それらの名前は申告です。論文の中に、読者がそれを確かめられるものは何もありません。現在のPapexの研究の記録も同じです。記録には、研究者本人またはそのAIアプリが報告したAIアプリとモデルが載り、Papexはそれらの名前を自己申告として扱います。確かめる方法がないからです。

推論の証明は、それが対象とする工程については、この状況を変えうる種類の証拠です。提供元のコミットメント、プロンプト、応答、証明はファイルです。記録と一緒に保存すれば、提供元も記録の著者も信頼することなく、何年も後に誰でも検証プログラムを再実行できるでしょう。署名と独立したタイムスタンプが示すのは、誰がある版の責任を引き受け、その版がいつ存在したかです。推論の証明なら、どの重みがあるテキストを生んだかを示すでしょう。

それでも範囲は狭いままです。証明が示すのはどの重みがどのテキストを生んだかで、分析が妥当か、人が確認したか、結果が成り立つかではありません。それらは人の仕事のままです。査読、追試、そして数学では形式証明です。さらに、現状では3つのことが妨げになります。AIアプリを使った研究のセッションは1,024トークンをはるかに超え、サンプリングを使います。ほとんどの研究者が使うモデルはクローズドで、応答にこうした証明を付けているクローズドなモデルの提供元を、私たちは知りません。そして、証明には応答の約70〜95倍のGPU時間がかかります。

Anthropicの記事にある1つのアイデアは、科学の側からも改めて見る価値があります。提供元は開発者に、「モデルの提供元が特定のモデルで少なくともXトークンを費やし、特定の結果を得られなかったという失敗の証明（Proof-of-Failure）」を渡せるかもしれません。たとえば、少なくとも100万トークンを費やしても、モデルがあるパッチにバグを見つけなかった、というものです。¹失敗した試みこそ、AIエージェントが報告から省きがちなものです（AI研究エージェントは否定的な結果を隠すのかを参照）。うまくいかなかった試みの、確かめられる記録があれば、それは新しいものになるでしょう。

主な用語#

出典#

1. Progress on provable inference for large language models（Anthropic、Frontier Red Team、2026年11月2日）、2026年11月3日確認 ↩ a b c d e f g h i
2. FlashProve: an open-source library for provable inference（Roy Rinberg、Alex Allain、Alessandro Chiesa、Miranda Christ、Rahul Dalal、Giacomo Fenzi、Ben Mayer、Guy Weissenberg、技術報告書、2026年11月）、全23ページ、2026年11月3日確認 ↩ a b c d
3. anthropics/FlashProve（GitHub）、README（バージョン0.16.0）、2026年11月3日確認 ↩ a b c
4. What is proved, and of what（FlashProveのガイド）、2026年11月3日確認 ↩ a b