Anthropic FlashProve: 110トークン/秒を実現するzkSNARK証明可能推論
Anthropicは、特定のコミット済みモデルが特定の出力を生成したことをzkSNARKを用いて証明する、証明可能推論のためのオープンソース研究プロトタイプ「FlashProve」を公開しました。400Bパラメータの混合エキスパート（MoE）モデルであるLlama 4 Maverickにおいて、Anthropicは単一のH100 GPU上で約110トークン/秒の証明生成速度を報告しています。生成される証明は約19 MBで、CPU上で数秒以内に検証可能です。この成果は、モデルの同一性や出力の来歴に関する暗号学的証明を、ルーティングの整合性、改ざん検知、監査ツール、AIのペース調整といった用途で検討できるほど実用的なものにするため重要ですが、Anthropicはこれを完成したシステムではなく、中間的な研究の進捗として明示的に位置づけています。
Anthropicが公開したもの
Anthropicは研究ブログ記事と併せて、ブログ記事本体、技術レポート、プロトコル記述、実行可能コード、Leanによる証明という5つの成果物を公開しました。コードには、証明器（prover）、高速なC++検証器（verifier）、および証明可能に正しいLean検証器が含まれています。Leanの資料には、最上位の数学的ステートメントの証明と、監査を支援するためのLean定理の対話型ビジュアライザーが含まれています。Anthropicは、コード、Lean証明、およびドキュメントをApache 2.0ライセンスの下で公開しました。
ブログ記事では、FlashProveを証明可能推論のためのオープンソースの高性能プロトタイプと説明しています。Anthropicによると、その目的は「証明可能推論の開発を加速・促進すること」と「ゼロ知識簡潔引数がこの問題に対して実用的であることを示すこと」の2点です。また、この記事は完成した研究アジェンダではなく中間的な進捗を共有するものであり、他者がこの成果を取り入れて改善することを歓迎するとしています。
なぜ証明可能推論が重要なのか
証明可能推論は、単純な信頼のギャップに対処します。現在、モデルにクエリを投げるユーザーは、その応答が開発者が主張する特定のモデルから得られたものかどうかを確認できません。応答は、ルーティングサービスによって密かに差し替えられた安価なモデルから来ている可能性もあれば、トークンストリームを改ざんした攻撃者から来ている可能性もあります。出力の品質だけで判断するのは信頼性に欠けます。
zkSNARK（ゼロ知識簡潔知識引数）を用いると、証明者は計算が正しく実行されたことを短い証明書を使って検証者に納得させることができます。この証明書は、計算の正しさ以外の情報を一切明かさないため「ゼロ知識」であり、証明よりも検証の方が指数関数的に高速であるため「簡潔」です。証明可能推論において、モデル提供者は重みセットにコミットし、各応答がそのコミット済みモデルによって生成されたことを証明します。証明は重みに関する情報を一切明かさず、検証者は重みや提供者のハードウェアを必要としません。
Anthropicは、この動機を4つの信頼の課題に整理しています。
課題1：AI開発のペース調整
AI開発を規制・調整するための提案の中には、ハードウェアとその使用状況の監視に依存するものがあります。提供者は、強力な新しいモデルのトレーニングではなく、推論にハードウェアを割くことを義務付けられる可能性があります。提供者は、より安価なモデルを提供したり、計算リソースを予期せぬ方法で使用したりして、トレーニングのためのリソースを確保しようとするかもしれません。
zkSNARKを使用すれば、規制当局は一定期間に行われた推論リクエストをカバーする証明書を要求できます。証明書は、リクエストが主張されたモデルによって生成されたことを示す必要があります。悪意のある提供者は、ハードウェアが実際に正しいモデルを提供していない限り、その要求を満たすことはできません。規制当局は提供者のハードウェア構成なしで主張を確認でき、提供者は規制当局がモデルの独自情報を知ることはないという保証を得られます。Anthropicは重要な制限として、これはハードウェアが推論を提供していることを検証するものであり、そのハードウェアが裏でトレーニングを行っていないことまでは証明できないと指摘しています。
課題2：改ざん検知
モデルの価値が高まるにつれ、推論サーバーは標的となります。攻撃者や不正なエージェントがサーバーを侵害し、重みを流出させたり、悪意のある応答を提供したり、本物の応答に紛れ込んだりする可能性があります。敵対者は外部からとは限りません。より高度なモデルが認可された弱いモデルの代わりとして実行され、分類器や監視を回避するために弱いモデルを装うことも考えられます。
zkSNARKを使用すれば、提供者はすべての応答に対して有効な証明を要求できます。証明は重みへの特定のコミットメントに結びついているため、単に「何らかのモデル」が生成したのではなく、「コミットされたモデル」が生成したことを証明します。サーバーを侵害した攻撃者や、別のモデルに成りすましたモデルは、検知を回避するために期待される重みに対する有効な証明を生成しなければなりませんが、それは不可能です。ユーザーもまた、内部情報を漏らさず、かつ検証が安価であるため、証明を受け取ることができます。
Anthropicはこれを「Frontier Safety Roadmap」に関連付けています。同ロードマップでは、2026年9月30日までに、AIモデルの出力を確実に署名し、特定のモデル重みセットに帰属させることができる証明可能推論のプロトタイプを開発するという公的な目標を掲げています。Anthropicは、推論トラフィックに署名し、信頼されたサーバー上で推論を再計算する別の関連プロジェクトを通じてその目標を達成したと述べており、FlashProveは異なる手法で同じ目的を追求しています。
課題3：テキストの来歴
開発者が「ソフトウェアライブラリがフロンティアサイバーセキュリティモデルによって脆弱性スキャンを受けた」と主張したり、企業が「ビジネスプランが適切なモデルによって承認された」と主張したりする場合があります。ユーザーはモデルを実行するためのリソースや権限を持っていない可能性があり、チャットログを公開しても、ログは安価なモデルや劣化したモデルで偽造できるため、絶対的な保証にはなりません。
zkSNARKを使用すれば、提供者は「出力が与えられた入力に対して主張されたモデルによって生成された」という証明を付加できます。簡潔性により、ユーザーは特殊なハードウェアなしで迅速に証明書を確認でき、ゼロ知識により、提供者はユーザーが独自の重みについて何も学ばないことを確信できます。Anthropicは「Proof-of-Failure（失敗の証明）」の例を挙げています。コードをリリースする前に、モデル提供者は開発者に対して、「特定のモデルで少なくとも一定数のトークンを消費したが、特定の成果（例えば、少なくとも100万トークン試行してもパッチにバグが見つからなかったなど）を得られなかった」という証明を提供できます。
課題4：モデルの承認
規制により、提供者は安全と承認されたモデルのみを提供することが義務付けられる可能性があります。リスクの高いモデルの方が競合他社より優れていたり、提供コストが安かったりする場合、提供者はこれを回避するインセンティブを持つかもしれません。規制当局は、承認されたモデルのみが提供されていることを確認する方法を必要としています。
zkSNARKを使用すれば、規制当局は提供者に対し、承認されたモデルの使用を強制する証明を応答に添付するよう要求できます。証明は各リクエストを使用されたモデルに結びつけるため、提供者が未承認のモデルを使用した場合、検証は通りません。規制当局は、各リクエストを再実行することなく、軽量な方法でこれを確認できます。
Anthropicは、このソフトウェアのみの暗号学的アプローチと、メーカーが耐タンパー性のあるハードウェアを製造することに依存するハードウェアベースのソリューションである「信頼された実行環境（TEE）」を対比させています。Anthropicは、信頼されたハードウェアと暗号学は異なる保証とトレードオフを持つ補完的なアプローチであり、両者が役割を果たすだろうと述べています。
FlashProveの仕組み
FlashProveは、大規模な混合エキスパート言語モデルのための証明可能推論システムです。これには、証明者としてのモデル提供者と、検証者としてのユーザーという2つの当事者が関与します。プロトコルには2つのフェーズがあります。
オフラインフェーズでは、証明者がモデルの重みへのコミットメントを公開します。コミットメントは、重みを隠したまま、重みの選択を正確に固定する短い指紋のようなものです。その後の推論の主張は、このコミットメントに対してチェックされます。
オンラインフェーズでは、証明者がリクエスト（プロンプトと対応する出力トークン）を受け取り、「コミットされたモデルを評価すると、これらの出力トークンが生成される」というステートメントを証明する証明ファイルを作成します。コミットメント、プロンプト、および返答を保持している人は誰でも、重みなしで、かつ限られた計算量で証明を確認できます。
この証明システムには4つの関連する特性があります。完全性（Completeness）とは、正直な証明者の証明は検証者に受け入れられることを意味します。健全性（Soundness）とは、偽のステートメントに対する有効な証明を生成することは事実上不可能であり、検証者は証明者を信頼する必要がないことを意味します。ゼロ知識（Zero-knowledge）とは、検証者は重み、中間計算値、各層でどのアキスパートが実行されたかについて何も学ばないことを意味します（重みを除くモデルアーキテクチャは隠されません）。簡潔性（Succinctness）とは、証明が小さく、チェックが安価であることを意味します。証明対象の計算は400Bパラメータモデル（量子化版で約232 GB）のH100 GPU上での実行ですが、検証者は約19 MBの証明ファイルを受け取り、24コアCPU上で数秒でチェックできます。
Llama 4 Maverickでのパフォーマンス
Anthropicは、公開されている4ビット重みを使用した、トークンあたり約17Bパラメータを使用する400Bパラメータの混合エキスパートモデル「Llama 4 Maverick」で実装を評価しました。各検証リクエストは1,024トークンのウィンドウであり、各証明は1トークンをチェックします。証明者は単一のH100と24個のCPUコアを備えたサーバー上で実行され、検証者はCPU上で実行されます。
オフラインフェーズはモデルごとに1回実行され、約39分かかります。技術レポートで議論されている技術的な理由により、結果として得られるコミットメントは約1,600万リクエストまで有効で、その後は提供者が再度コミットする必要があります。24リクエストのバッチに対するオンラインフェーズは、証明者にとって約223秒かかり、これは110トークン/秒に相当し、各証明は18.78 MBです。
検証者はGPUを必要とせず、重みへのコミットメントにのみアクセスできます。クライアントは合計約6.5 MBのコミットメントをダウンロードし、その後リクエストごとに1つの証明をダウンロードします。証明のチェックには、オフラインフェーズのチェックを含めて、24スレッドで17秒、シングルスレッドで21秒かかります。
Anthropicはこれを、広く使用されている推論エンジンであるvLLMを用いた、同じモデルのFP8版を8台のH100で実行する通常の推論と比較しています。GPUあたりで見ると、24リクエストのバッチを証明するのにかかる時間は、vLLMが同じ24リクエストを一度に処理する時間の約72倍（実行間で66〜77倍の範囲）であり、Anthropicが試した最高負荷でvLLMが実行された場合は約94倍でした。
FlashProveを実用的にするエンジニアリングの選択
FlashProveは、証明コストを管理可能な範囲に抑えるためにいくつかのアーキテクチャ上の決定を行っています。証明者の作業量は、実際に実行されたエキスパートに比例します。混合エキスパートモデルでは、1トークンあたり400Bパラメータのうち約17Bが使用されるため、トークンあたりの証明者の作業量は全パラメータではなくその17Bに比例し、証明はどのエキスパートが選択されたかを隠したままにします。
リクエストは事後的にバッチで証明されます。証明者はプリフィルのように1回の並列パスで完了したテキストを読み取り、リクエストごとではなくバッチごとに1回、重みへのコミットメントを開きます。
システムは単一のGPUに収まるように設計されています。各層のモデル重みはセグメントに分割され、層のセグメントごとに証明されます。重みは通常のメモリに保持され、ストリーミングされるため、約290 GBのホストメモリを備えた単一の80 GB GPUで十分です。
Anthropicは、インライン証明と事後証明を区別しています。インライン証明は推論と並行して行われ、超高速であることが期待されますが、効率のためにセキュリティを犠牲にする可能性があります。事後証明は事後的にトークンのサブセットに対して行われ、そのトレードオフなしで低速であることが許容されます。FlashProveは事後アプローチを採用しています。Anthropicは、事後証明の制限として、再計算の複雑さの増加、トラフィックに関する保証を得るまでの遅延、および本質的な非決定性を指摘しています。
暗号学的構成
FlashProveは、Ethereumのレイヤー2ネットワークなどのピアツーピアシステムで展開されている種類のzkSNARKを使用しています。Anthropicによると、このzkSNARKは確立されたレシピに従っています。対話型オラクル証明（IOP）と呼ばれる基礎となる情報理論的オブジェクトが、ハッシュ関数を使用して暗号学的証明にコンパイルされ、耐量子セキュリティさえ提供します。IOPは、線形制約を持つコード近接性テストやルックアップ引数など、符号理論や計算複雑性理論の技術に基づいた最先端のビルディングブロックから組み立てられています。Anthropicは、これらのピースを推論のための特注のIOPに組み合わせることは繊細な作業であると説明し、詳細は技術レポートを参照するよう促しています。
Leanによる形式検証
Anthropicは、形式検証を通じて暗号学的コードへの信頼に対処しています。チームはLean証明アシスタントを使用してプロトコルと望ましいセキュリティ特性を記述し、機械チェック可能な形式で特性を証明しています。3つの最上位特性は、完全性、健全性、ゼロ知識です。これらの特性は、ハッシュ関数に依存する暗号プロトコルを分析するための情報理論的な方法である「ランダムオラクルモデル」で記述されています。
Anthropicは、残る2つの信頼のギャップを特定しています。第一に、形式的なステートメントが意図と一致していることを確認するために監査される必要があります。これは手動で行う必要がありますが、Anthropicは証明を監査するよりも劇的に負担が少ないと述べており、支援のためにインタラクティブなビジュアライザーを提供しています。第二に、実行可能コードが、セキュリティ特性が証明されている形式的に定義されたプロトコルと一致していることを確認するために監査される必要があります。
監査アプローチは特性によって異なります。健全性は検証者にのみ依存するため、AnthropicはC++検証器と並んで実行可能なLean検証器を提供しています。Lean検証器は動作が遅いですが、健全性定理の検証者が受け入れるものだけを受け入れることがLeanによって証明されています。C++検証器は日常的なツールであり、形式的な保証はありませんが、Anthropicのテストにおけるすべての証明でLean検証器と一致しています。完全性は正直な証明者と検証者を想定しているため、Lean検証器により、チームは標準的なソフトウェアテストを通じて、正直な証明者が受け入れられる証明を生成することへの確信を得ることができます。ゼロ知識は証明者にのみ依存しますが、証明者は高コストであり、Lean証明者を実行することは非現実的です。Anthropicはそのための機能を提供しておらず、重みを隠したい証明者は、Lean証明者との等価性を確保するために、慎重なエージェント的または人間によるセキュリティ監査を行うための十分なリソースを持っている必要があると考えています。
また、Anthropicは、Claudeが推論のためのzkSNARKの改善を生み出し、既存のオープンソースシステムよりも大幅に高速なシステムを構築したと述べています。ブログ記事では、Claudeは最適化が得意だが、特に大規模で複雑なシステムでは評価が難しい決定を下すことが多く、Anthropicはこれに対抗するために、主張されるセキュリティ保証についてLeanで監査可能な最上位のステートメントを提供していると指摘しています。
FlashProveと従来の研究の比較
Anthropicは、FlashProveを俗に「zkML」と呼ばれる研究の系譜に位置づけています。初期のシステムは小規模でした。2017年のSafetyNetsは2層の畳み込みMNIST CNNと小さな全結合音声モデルを検証し、2021年のzkCNNは15MパラメータのVGG-16に88.3秒/証明で到達し、2022年のKangらはフル解像度のImageNetでMobileNet v2を証明しました。
続いてTransformerの証明が登場しました。ZKMLのGPT-2は117Mパラメータでトークンあたり約159秒（約0.006トークン/秒）かかりました。Modulus Labsの1.5BパラメータのGPT-2 XLは90時間以上を要しました。2024年のzkLLMは、GPU上で2,048トークンの入力に対してLLaMA-2-13Bを約15分で証明しました。これはAnthropicの表現では新しいトークンあたり約0.001トークン/秒、バッチ内では約2.5トークン/秒です。2025年には、zkGPTがGPT-2を21.8秒（約0.05トークン/秒）に短縮し、zkPyTorchは1つのCPUコアでLlama-3 8Bをトークンあたり約150秒（約0.007トークン/秒）で証明し、ZKTorchはGPT-J 6Bを約20分（約0.001トークン/秒）で証明しました。VerInfは、FlashProveがターゲットとするのと同じ400Bパラメータの混合エキスパートモデルであるLlama 4 Maverickを約0.02トークン/秒で証明しました。Anthropicが現在の査読済み最先端技術と呼ぶDeepProveは、単一のフォワードパスで生成されたシーケンス全体を認証し、1台のマシンでGPT-2に対して約2.9トークン/秒、Gemma 3に対して1.4トークン/秒、分散環境で31トークン/秒に達します。
Anthropicは商用的な取り組みにも言及しています。Attestableは、単一のH100でGemma 4 31Bを53〜77トークン/秒で証明したと報告していますが、執筆時点でAttestableは対応するオープンソースライブラリを公開していません。
Anthropicは進歩の規模を強調しています。2024年には、zkLLMが1台のA100で13Bモデルを約2.5トークン/秒で証明しました。Anthropicが知る限り、Llama 4 Maverickの唯一の以前の証明であるVerInfは、DGX Spark上で1,000トークンに14.3時間を要し、検証にほぼ1日かかる93.6 GBの証明を生成しました。FlashProveは、同じモデルを単一のH100上で110トークン/秒で証明し、数秒で検証可能な19 MBの証明を生成します。Anthropicは、この進歩はより多くのモデルやアーキテクチャに転用可能であり、ネイティブ計算に対するオーバーヘッドは測定値で約70〜95倍、つまり約2桁の規模に収まり、以前の予想よりもはるかに小さいと考えています。
Anthropicが文書化している制限
Anthropicはいくつかの技術的な制限を挙げています。第一に、高速な実行可能コードには形式的な保証がありません。Anthropicは、実行可能な低速のLean検証器を含むプロトコルのLean実装と、Leanで証明されたセキュリティ特性を提供しています。論文と高速な実行可能コードはLeanプロトコルから派生していますが、AnthropicはLean、論文、コードのすべてが完全に一致していることを保証していません。
第二に、証明は貪欲法（greedy decoding）による整数モデルに関するものです。Anthropicは公開された重みの正確な整数バージョンを証明しており、証明は各チェックされたトークンがそのモデルの貪欲な選択であることを主張します。浮動小数点実装やサンプリングデコードからの返答は、ある位置で乖離し、証明された計算と正確に一致しなくなる可能性があります。整数バージョンは一般的に、敵対的に設計されたプロンプトを考慮しない場合でも、浮動小数点計算の非決定性を考慮しても、真の浮動小数点推論の小さな誤差範囲内にあることが期待され、経験的にテストされています。
第三に、アーキテクチャの隠蔽は目標ではありません。システムは、各Transformer層のフィードフォワードブロックが複数のエキスパートサブネットワークに置き換えられ、ルーターがトークンごとに少数のエキスパートのみをアクティブにする混合エキスパートアーキテクチャを使用していることを前提としています。FlashProveは効率向上のためにMoE構造を使用しています。密なモデル（dense models）などの他のアーキテクチャも広く使用されており、その記述には提供者が秘密にしておきたい知的財産が含まれている可能性があります。Anthropicは、検証者がコミットされた実行可能ファイルをコミットされたモデル上で実行することをチェックするような、隠蔽コミットメントを通じて重みとアーキテクチャの両方をコミットすることでアーキテクチャも隠蔽するシステムを想像できると述べています。
第四に、サイドチャネル攻撃は範囲外です。プロトコルは、証明自体がコミットされたモデルの重みについて何も明かさないことを保証しますが、証明生成時間を測定するなどのサイドチャネルは、重みに関する情報を潜在的に明らかにする可能性があります。Anthropicはこれを今回のリリースの範囲外としています。
第五に、システムは現在、最大1,024トークンのコンテキストに対する推論を証明します。Anthropicは、これはチャット設定で蓄積されるコンテキストと比較して短いと指摘しており、理想的には、数百数千から数百万トークンのコンテキストウィンドウを定期的に持つフロンティアモデルの完全なコンテキストウィンドウまでコンテキスト長を増やすことであると述べています。
リリースが意味するもの
FlashProveは研究プロトタイプであり、商用の証明可能推論サービスではありません。その重要性は、オープンシステムでは以前は手の届かなかった規模と速度で、ソフトウェアのみの暗号学的アプローチを実証したことにあります。Anthropicは、400Bパラメータの混合エキスパートモデルにおいて、19 MBの証明と秒単位の検証で110トークン/秒を報告しており、これは数桁遅いか、はるかに小さなモデルに限定されていた以前のオープンな結果とは対照的です。
このリリースは、AI生成の暗号システムをより監査可能にするためのパターンも示しています。Leanでの形式検証を最上位のセキュリティステートメントに使用し、高速な検証器と証明可能に正しい検証器の両方を提供し、形式的なステートメント、論文、実行可能コードの間の残りのギャップを文書化することです。Anthropicは、高速なC++検証器には形式的な保証がなく、Lean、論文、コードが完全に一致していない可能性があることを明示的に述べているため、形式検証は信頼の前提を減らしますが、排除するものではありません。
AIガバナンスに関して、ブログ記事は、証明可能推論がペース調整の要件、改ざん検知、テキストの来歴、モデルの承認をサポートできると主張しています。また、制限も明確に述べています。証明はハードウェアが主張されたモデルを提供したことを示せますが、同じハードウェアが裏でトレーニングを行っていないことまでは示せません。証明は重みを隠しますがアーキテクチャは隠しません。現在のシステムは最大1,024トークンのコンテキストを処理します。これらの制限が、有望なプロトタイプと展開可能なコンプライアンスまたはセキュリティメカニズムとの間のギャップを定義しています。