大規模言語モデルにおける証明可能な推論の進捗

大規模言語モデルにおける証明可能な推論の進捗

Roy Rinberg (Anthropic), Alex Allain (Anthropic); Alessandro Chiesa (EPFL, StarkWare), Miranda Christ (MIT, RESI), Rahul Dalal (Anthropic STEM Fellows Program, Succinct), Giacomo Fenzi (EPFL), Ben Mayer (Anthropic Fellows Program, MIT), Guy Weissenberg (EPFL)

エグゼクティブサマリー

友人と直接話すとき、それが本当に本人であると知る方法はたくさんあります。相手の姿を見たり、声を聞いたり、握手をしたりできます。しかし、AIモデルと対話するとき、そのような方法はほとんどありません。今日、モデルに問い合わせるユーザーは、応答が、ルーティングサービスによってコスト削減のために秘密裏に置き換えられたものではなく、あるいはトークンストリームを改ざんした攻撃者によるものでもなく、開発者が主張する特定のモデルから生成されたものであることを確認する方法がありません。モデルの出力だけを見て判断するのは、たとえ高品質な応答を生成したとしても、信頼できません。推論の暗号学的証明は、この問題を解決します。これにより、モデルプロバイダーはモデルにコミットし、各応答がそのモデルによって生成されたことを証明できます。このような証明は、消費者向け製品から内部セキュリティに至るまで、さまざまなアプリケーションを可能にし、AIのペース要件への準拠を検証するためのツールキットに貢献する可能性があります。

具体的には、「zkSNARK」として知られる強力な暗号学的証明の一種について進歩を遂げました。これは、その強力な隠蔽性と効率性の特性から、証明可能な推論に特に適しています。この投稿では、主にFlashProveと呼ぶシステムを通じて、その進捗の一部を共有します。簡単な技術的概要は以下の通りです。

1. Claudeは、推論のためのzkSNARKsの改善を達成し、既存のオープンソースシステムよりも大幅に高速なシステムを構築しました。
   1. 大規模モデル（Llama 4 Maverick、400BパラメータのMixture of Experts）の場合、4ビット量子化された重みを使用し、プリフィルで整数演算を使用すると、単一のH100 GPUは約110トークン/秒で証明を生成し、1,024トークンごとのリクエストで約19MBの証明サイズになります。これは、一般的なオープンソースライブラリであるvLLMでモデル自体を実行するGPU時間の約70〜95倍です。
   2. 既存のオープンソースシステムは桁違いに遅いです。これはセクション6で議論しています。Claudeは、暗号学的証明システムの確立された設計原則に依存しながら、暗号およびセキュリティ文献の最先端ツールを適用する新しい方法を見出しました。モデルへのコミットメントとそれに続く推論証明は、モデルの重みを隠蔽します。モデルのアーキテクチャを隠蔽することは、このシステムの目標ではありません。
2. Claudeは最適化に長けていますが、特に大規模で複雑なシステムでは、評価が難しい決定をすることがよくあります。私たちは、主張されるセキュリティ保証について、Lean（形式検証言語）でトップレベルの監査可能なステートメントを提供することで、これに対処します。

本日、私たちは5つの成果物をリリースします。

• 現在のブログ投稿。システムとその潜在的なアプリケーションの概要を説明します。
• システムの詳細を説明する技術レポート。
• (Claudeが作成した) プロトコル仕様ドキュメント。
• 実行可能なコード（以下を含む）：プロバーと2つのベリファイア、C++の高速ベリファイア、およびLeanの証明可能な正しいベリファイア。
• トップレベルの数学的ステートメントに対するLean証明、および監査を支援するためのLean定理のインタラクティブビジュアライザー。

コード、Lean証明、およびドキュメントはApache 2.0ライセンスの下でリリースされます。1 この研究投稿は、中間的な進捗を共有することを目的としており、完了した研究アジェンダではありません。私たちは、他者が私たちの成果を見て、それを活用し、改善することを明確な目標として、これを共有します。

はじめに

ユーザーがAIモデルにリクエストを送信するとき、今日、選択したモデルが応答を生成したモデルであると確信する方法はありません。ユーザーが主に品質だけでなく、どの特定のモデルが生成したかについても気にする日常的な用途では、これはそれほど差し迫った懸念ではありません。しかし、そのような保証が役立ついくつかのケースがあります。たとえば、リリース前後にAIモデルをテストする独立した評価者は、評価しているモデルが提供されているモデルであることを知る必要があります。サードパーティのルーティングサービスを介してモデルを使用するクライアントは、トークンが支払ったモデルから来たという保証を望んでいます。そして、サイバー攻撃者が特定のモデルになりすましてトークンストリームを変更した場合、ユーザーは出力だけではそれを検出する方法がありません。

しかし、モデル応答の検証を可能にすることは困難です。ほとんどの最先端モデルの重みは非公開にされており、ユーザーが重みにアクセスできたとしても、特定の応答がその重みを持つモデルによって生成されたことを確認するには、モデルを実行する必要があります。これは、典型的なユーザー（あるいは評価者でさえ）が費やすことができる計算リソースをはるかに超える計算リソースを必要とします。

証明可能な推論（PI）の目標は、限られた計算リソースを持ち、重みに関する情報を持たないユーザーが、応答が要求されたモデルから来たことを検証できるようにすることです。PIは、AIプロバイダーへの顧客の信頼を高めたいという願望によって動機付けられています。また、独立した評価者に保証を提供し、プロバイダーが特定のコミットメントや法的義務を満たしていることを証明できるようにするため、AI開発の最前線をペース配分し、AI規制のためのツールキットにも影響を与えます。

PIを実装する1つの方法は、ゼロ知識サクシント引数と呼ばれる暗号オブジェクトを介して行われます。モデルプロバイダーは、主張される応答とともに、ユーザーが迅速に（理想的にはCPUで数秒で）検証できる短い証明（たとえば、数メガバイト）を送信します。主張される応答が指定されたモデルから逸脱した場合、ユーザーのチェックは失敗します。重要なことに、暗号技術は、証明がモデルの重みに関する何も明らかにしないことを保証します。

本日、私たちはFlashProveをリリースします。これは、大規模な混合専門家（MoE）言語モデルの証明可能な推論のためのオープンソースの高性能プロトタイプです。400Bパラメータの混合専門家モデル（Llama 4 Maverick、4ビット量子化）について、単一のH100 GPUが100トークン/秒を超える速度で証明を生成し、1,024トークンごとのリクエストで約19MBの証明サイズ（一般的なオープンソースライブラリであるvLLMが同じ長さのプロンプトを処理するのにかかる時間の約70〜95倍）であることを示します。

このリリースには、実行可能なコード、Lean形式化、およびプロトコルの技術的な説明が含まれています。私たちの目標は2つあります。(i) 証明可能な推論の開発を加速および促進すること。(ii) ゼロ知識サクシント引数が証明可能な推論に実用的であることを実証すること。

この進歩は、AI開発のペース配分、AI顧客への整合性保証の提供、監査人および規制当局向けのツールの促進などにおいて、重要な意味を持つと信じています。

AIの普及における信頼性の課題

人工知能の開発と、デジタルインフラストラクチャおよび経済におけるその役割の増大は、AIプロバイダーが回答しなければならない信頼性の課題をもたらします。これらの課題やその他の課題に対処するには、証明可能な推論（PI）のためのツールに依存することが役立ちます。

PIのためのツールには、ハードウェアアプローチ、ソフトウェアアプローチ、またはその両方の組み合わせが含まれます。ここでは、ソフトウェアのみのアプローチに焦点を当てます。それは「zkSNARK」（zero-knowledge succinct argument of knowledge）として知られる暗号ツールです。非公式には、zkSNARKは、プロバーが短い「証明書」を介して、特定の計算が正しく実行されたことをベリファイアに納得させるシステムです。特に、証明書は計算の正しさによって暗示される以上の情報を明らかにしないゼロ知識であり、証明された計算と比較して検証が指数関数的に高速であるためサクシントです。

以下に、いくつかの課題と、zkSNARKがそれらにどのように役立つかを概説します。

課題1：ペース配分

AI開発を規制およびペース配分するためのいくつかの提案は、ハードウェアとその使用方法の監視に依存しています。たとえば、プロバイダーは、強力な新しいモデルをトレーニングするのではなく、ハードウェアを推論に専念させることが要求される場合があります。プロバイダーは、より安価なモデルを提供したり、予期しない方法でコンピューティングを使用したりして、トレーニングのためのリソースを解放することで不正を試みる可能性があります。規制当局は、ハードウェアが推論に使用されていることをどのように確実に保証できるでしょうか？

zkSNARKがどのように役立つか：規制当局は、プロバイダーに、指定された期間に提供された推論リクエストをカバーする証明書を要求できます。証明書は、リクエストが主張されたモデルによって生成されたことを示す必要があります。悪意のあるプロバイダーは、ハードウェアが実際に正しいモデルを提供していない限り、この要求を満たすことができません。zkSNARKを使用すると、規制当局は、プロバイダーが持つ可能性のある複雑なハードウェアセットアップを必要とせずに、プロバイダーの主張が有効であることを確認できます。同時に、プロバイダーは、規制当局が専有的なモデル情報を学習しないという保証を得られます。2 これにより、ハードウェアが推論を提供していることは検証できますが、ハードウェアが側面でトレーニングしていないことなどを確立するものではないことに注意してください。

課題2：改ざん検出

AIモデルがより価値が高まるにつれて、それらを実行するサーバーは主要なターゲットになります。攻撃者または不正なエージェントは、推論サーバーを侵害することで、重みを盗み出したり、ユーザーに悪意のある応答（ユーザーのコンピューターにマルウェアを配信するなど）を提供したりする可能性があります。これらすべては、正規の応答に紛れ込みながら行われます。敵対者は外部である必要はありません。モデルが自己改善および自己展開できるようになるにつれて、より高度なモデルは、それに適用されるであろう分類器や監視を回避するために、承認されたモデルの代わりに実行され、より弱いモデルとして提示される可能性があります。どちらの場合も、質問は同じです。企業は、どの重みが実際にサーバーで実行されていることをどのように確信できるでしょうか？Frontier Safety Roadmapで、Anthropicは、推論トラフィックを検証するためのプロトタイプを作成するという公開目標を設定しました。「私たちは、2026年9月30日までに、証明可能な推論のプロトタイプを開発します。これは、AIモデルの出力を特定の重みセットに帰属させる方法で、信頼性高く、証明可能に「署名」する技術です。」RSPの更新で述べたように、私たちは、推論トラフィックに署名し、信頼されたサーバーで推論を再計算する、別個だが関連するプロジェクトを通じてその目標を達成しました。このブログ投稿での作業は、異なる方法で同じ目的を追求しています。3

zkSNARKがどのように役立つか：プロバイダーは、すべての応答に対してサーバーから有効なzkSNARKを要求できます。証明は重みの特定のコミットメントにバインドされているため、あるモデルが応答を生成したというだけでなく、コミットされたモデルが生成したことを証明します。サーバーを侵害した攻撃者、または別のモデルに置き換わるモデルは、検出を回避するために、期待される重みに対して有効な証明を生成する必要がありますが、それはできません。ユーザーは、証明が内部情報を漏洩せず（ゼロ知識により）、チェックが容易である（サクシント性により）ため、証明を受け取ることもできます。これにより、攻撃者が推論APIを通じて達成できることが制限されます。

課題3：テキストの出所

理解/分析に多大な努力が費やされたことを証明したい場合があります。たとえば、開発者は、ソフトウェアライブラリが最先端のサイバーセキュリティモデルによって脆弱性のスキャンを受けたと主張するかもしれません。または、企業は、ビジネスプランが適切なモデルによって承認されたと主張するかもしれません。ユーザーはこれらをどのように検証できるでしょうか？ユーザーは、モデル自体を実行するリソースを持っていないかもしれません（または実行する権限を持っていないかもしれません）。チャットログを公開しても、絶対的な保証はありません。開発者は理論上、それを偽造し、最先端モデルではなく、より安価なモデルまたは劣化版で生成する可能性があります。一般的に、ユーザーは選択したモデルによってサービスが提供されていることをどのように検証できるでしょうか？

zkSNARKがどのように役立つか：プロバイダーは、各応答とともに、指定された入力に対して主張されたモデルによって出力が生成されたことを証明するzkSNARKを添付できます。サクシント性により、ユーザーは特別なハードウェアなしでこの証明書を迅速にチェックできます。ゼロ知識は、プロバイダーが専有的な重みについて何も学習しないことを保証します。これは、応答を生成したモデルを検証するための既存のメカニズムを補完します。

たとえば、エクスプロイトが定期的に発見される世界では、新しいコードをリリースする前に、モデルプロバイダーはコード開発者に、モデルプロバイダーが特定のモデルに少なくともXトークンを費やし、特定の（たとえば、1Mトークン以上試行した後、この特定のモデルは特定のパッチでバグを見つけられなかった）結果を達成しなかったというProof-of-Failureを提供できます。

課題4：モデル承認

規制により、プロバイダーは、サイバーセキュリティまたは安全性のリスクと見なされるモデルではなく、安全として承認されたモデルのみを提供することが要求される場合があります。プロバイダーはこれを回避するインセンティブを持つ可能性があります。なぜなら、リスクの高いモデルは競合他社よりも優れたパフォーマンスを発揮したり、提供コストが安かったりする可能性があるからです。規制当局は、承認されたモデルのみが提供されていることをどのように保証できるでしょうか？

zkSNARKがどのように役立つか：規制当局は、プロバイダーに、応答にzkSNARKを添付することを要求し、承認されたモデルの使用を強制できます。証明は各リクエストを使用されたモデルにバインドするため、プロバイダーが未承認のモデルを使用している場合、検証されません。規制当局は、サクシント性のおかげで、各リクエストを再実行する必要なく、軽量な方法でこれをチェックできます。

信頼できるハードウェアからのPIに関する注記。以前の研究は、PIを達成するために信頼できる実行環境に焦点を当てることがよくあります。これらは、メーカーが改ざん防止ハードウェアを製造することに依存するプライバシーと証明を提供するハードウェアベースのソリューションです。この研究では、計算問題の困難さに依存するセキュリティとプライバシーを持つ、ソフトウェアのみの暗号ソリューションに焦点を当てています。侵害された環境（ハードウェア、オペレーティングシステムなど）に直面しても、敵対者は計算不可能な問題を壊さずに無効な証明を生成することはできません。信頼できるハードウェアと暗号技術は、異なる保証とトレードオフを持つ補完的なアプローチです。どちらも上記の信頼性の課題に対処する上で役割を果たします。

私たちのシステム：FlashProve

FlashProveは、大規模な混合専門家（MoE）言語モデルの証明可能な推論のためのシステムです。詳細については、技術レポートを参照してください。ここではシステムを概説します。

FlashProveは2つの当事者を含みます：モデルプロバイダー（プロバー）とユーザー（ベリファイア）。これは2つのフェーズに分かれています。

• オフラインフェーズでは、プロバーはモデルの重みに対するコミットメントを公開します。これは、重み自体は隠されたままで、1つの正確な重みの選択を固定するための短いフィンガープリントです。後続の推論主張は、このコミットメント、つまりこのフェーズでコミットされた重みモデルに対してチェックされます。
• オンラインフェーズでは、ベリファイアからのリクエスト（つまり、プロンプトと対応する出力トークン）に応じて、プロバーは次のステートメントを証明する証明ファイルを生成します。

コミットされたモデルが評価時にこれらの出力トークンを生成する

コミットメント、プロンプト、および応答を持つ誰もが、重みなしで、限られた計算能力でそれをチェックし、このプロンプトで実行されたコミットされた重みが正確にこれらのトークンを生成したと確信できます。

保証

証明ファイルは、次の「完全性」と「健全性」のプロパティを満たします。

• 正直な場合、証明ファイルは受け入れられます（完全性）。正直なプロバーの証明は、ベリファイアによって受け入れられます。
• 証明ファイルは偽造できません（健全性）。偽のステートメントの有効な証明を生成することは、事実上不可能です（つまり、広く信じられている暗号学的仮定を破ることに相当します）。したがって、ベリファイアはプロバーを信頼する必要はありません。

完全性と健全性だけでは、モデルの重みを知っている計算能力の高いベリファイア（プロンプトでモデルを評価し、結果が応答と一致するかどうかを確認する）で達成できます。次の2つのプロパティが、このシステムを非自明なものにしています。

• 証明ファイルは、ステートメント以外の何も明らかにしません（ゼロ知識）。ベリファイアは、重み、計算の中間値、または各レイヤーでどの専門家が実行されたかについて何も学習しません。モデルのアーキテクチャ（重みを除く）は隠されていません。
• 証明ファイルは小さく、チェックが容易です（サクシント性）。証明された計算は、400Bパラメータ（量子化バージョンで約232GB）のモデルをH100 GPUで実行することですが、ベリファイアは約19MBの証明ファイルを受け取り、CPUでチェックするのに数秒かかります。監査人、またはプロバイダーよりもはるかに少ないハードウェアを持つユーザーは、複雑なインフラストラクチャにアクセスせずに証明ファイルをチェックできます。

評価

公開されている4ビット重みを使用したLlama 4 Maverick（400Bパラメータの混合専門家、トークンあたり約17Bパラメータを使用）でプロトコルを実装した結果を測定しました。各ベリファイアのリクエストは1,024トークンのウィンドウであり、各証明は1つのトークンをチェックします。プロバーは単一のH100と24個のCPUコアを持つサーバーで実行され、ベリファイアはCPUで実行されます。

• プロバー。プロバーは、単一のH100と24個のCPUコアを持つサーバーで実行されます。オフラインフェーズはモデルごとに1回実行され、約39分かかります。（技術レポートで説明する技術的な理由から、生成されたコミットメントは約1600万リクエストに有効であり、その後プロバイダーは再度コミットする必要があります。）オンラインフェーズは、24リクエストのバッチで、プロバーは約223秒かかります。これは110トークン/秒であり、各証明は18.78MBです。
• ベリファイア。ベリファイアはクライアントのCPUで実行されます。GPUは必要なく、重みのコミットメントにのみアクセスできます。クライアントはコミットメント（合計約6.5MB）をダウンロードし、その後リクエストごとに1つの証明をダウンロードします。証明のチェックは、オフラインフェーズのチェックを含め、24スレッドで17秒（シングルスレッドで21秒）かかります。

プレーン推論との比較：同じモデルのFP8リリースを8つのH100で実行したvLLMを実行し、GPUあたりでは、24リクエストのバッチを証明するのにかかる時間が、vLLMが同じ24リクエストを一度に処理するのにかかる時間の約72倍（実行全体で66〜77倍）、vLLMが試した中で最も高い負荷で実行された場合は約94倍であることを発見しました。

システム内部。FlashProveの背後にあるメカニズムは、ピアツーピアシステム（たとえば、イーサリアムのようなブロックチェーンのStarknetやMantleのようなL2ネットワーク）で展開されている種類のzkSNARKです。私たちのzkSNARKは、確立されたレシピに従って構築されています。インタラクティブオラクル証明（IOP）と呼ばれる情報理論的なオブジェクトが、ハッシュ関数に依存することによって暗号学的証明にコンパイルされます（ポスト量子暗号セキュリティも提供します）。私たちのIOPは、線形制約付きコード近接性テストやルックアップ引数などの最先端のビルディングブロックから組み立てられており、コーディング理論と計算量理論の技術に基づいています。これらのピースを推論のためにカスタムIOPに組み合わせることは繊細な作業です。構築に関する詳細については、技術レポートを参照してください。

システムのエンジニアリング

FlashProveは、技術レポートで詳細に議論されているアーキテクチャ上の決定から恩恵を受けています。ここではいくつか強調します。

• プロバーの作業量は、実際に実行された専門家の数に比例します。MoEモデルでは、トークンは400Bパラメータのうち約17Bを使用し、プロバーのトークンあたりの作業量は、すべてのパラメータではなく、それらの約17Bに比例します（証明はどの専門家が選択されたかを隠蔽します）。
• リクエストは、事後的にバッチで証明されます。プロバーは、完了したテキストを1つの並列パス（プリフィルと同様）で読み取り、リクエストごとではなく、バッチごとに1回コミットメントを開きます。
• システムは単一のGPUに収まるように設計されています。各レイヤーのモデルの重みはセグメントに分割され、一度に1つのセグメントのレイヤーごとに証明されます。重みは通常のメモリに保持され、ストリーミングされるため、約290GBのホストメモリを備えた単一の80GB GPUで十分です。

事後検証対インライン検証

推論サーバーに証明メカニズムを統合する際には、選択肢があります。インライン証明（つまり、推論と並行して証明する）対事後証明（つまり、トークンの一部に対して事後的に証明する）です。私たちのシステムは後者に従います。インラインソリューションは超高速であることが期待され、効率のためにセキュリティを犠牲にする可能性があります。一方、事後証明は遅くても許容され、そのようなトレードオフに苦しむ必要がないかもしれません。一方で、事後証明には制限があります。再計算の複雑さの増加、トラフィックに関する保証を得るまでの遅延、および固有の「非決定性」です。事後証明の動機と影響については、技術レポートで詳しく説明します。

形式検証による信頼性

暗号コードは、非常に壊れやすく、エラーが発生しやすいことで有名です。ユーザーは、今日リリースされるコードをどのように信頼できるでしょうか？

答えは形式検証です。Lean証明アシスタントを使用して、プロトコルと望ましいセキュリティプロパティを指定します。機械的にチェック可能で、正しいことが保証される形式でこれらのプロパティを証明します（コンパイラエラーを除く）。私たちは3つのトップレベルのプロパティを対象としています。

1. 完全性：ステートメントが正しい場合、生成された証明はベリファイアによって受け入れられます。
2. 健全性：偽の証明はベリファイアによって拒否されます（無視できる確率を除く）。
3. ゼロ知識：証明は、ベリファイアが応答自体から推測できること以上の、モデルの重みに関する情報を明らかにしません。4

これらのプロパティは、いわゆるランダムオラクルモデルで記述されています。これは、ハッシュ関数に依存する暗号プロトコルを分析するための情報理論的な方法です。

形式検証は、2つの重要な信頼のギャップを残します。第一に、形式ステートメントは、意図と一致していることを確認するために監査される必要があります。これは手動で行う必要があります（ただし、証明の監査よりもはるかに負担が少ないです）。監査を支援するためにインタラクティブビジュアライザーを提供します。

第二に、実行可能なコードは、セキュリティプロパティが証明されている形式的に定義されたプロトコルと一致していることを確認するために監査される必要があります。これに最も役立つ方法は、プロパティによって異なります。なぜなら、健全性はベリファイアのみに依存し、ゼロ知識はプロバーのみに依存し、完全性はそれらの相互作用に依存するからです。

• 健全性については、ベリファイアコードが正しいだけで十分です（「証明」を持つことの価値は、ベリファイアを信頼すればプロバーを完全に信頼しなくてよいことです）。実行可能なLeanベリファイアとC++ベリファイアを提供します。Leanベリファイアはより遅く実行されますが、Leanはそれが私たちの健全性定理のベリファイアが受け入れるものだけを受け入れることを証明します。それにもかかわらず、C++ベリファイアは日常的に使用されるものです。正式な保証はありませんが、テストではLeanベリファイアとすべての証明で一致しています。
• 完全性については、脅威モデルは敵対的な攻撃を想定していません（プロバーとベリファイアは正直です）。したがって、Leanベリファイアを使用すると、標準的なソフトウェアテストを通じて、正直なプロバーが受け入れられる証明を生成することに自信を得ることができます。正しいステートメントでプロバーを実行し、次に生成された証明でLeanベリファイアを実行します。
• ゼロ知識については、プロバーが正しいだけで十分です。しかし、ベリファイアとは異なり、プロバーは高価な手順であり、Leanプロバーを実行することは実用的ではありません。ここでは支援を提供していません。モデルの重みを隠したいプロバーは、Leanプロバーとの同等性を確保するために、慎重なエージェントおよび/または人間のセキュリティ監査に十分なリソースにアクセスできると予想しています。

先行研究

証明可能な推論の達成は、一般に「zkML」と呼ばれる一連の研究の目標です。初期の研究としては、SafetyNets（2017）は2つの畳み込み層を持つMNIST CNNと小さな全結合音声モデルを検証し、zkCNN（2021）はVGG-16（1500万パラメータ）を88.3秒/証明で達成し、Kangら（2022）はフル解像度のImageNetでMobileNet v2を証明しました。

Transformerの証明が続きました。ZKMLのGPT-2は、1億1700万パラメータでトークンあたり約159秒（≈0.006トークン/秒）かかり、Modulus Labsの15億パラメータGPT-2 XLは90時間以上かかりました。EZKL（2023）は、約966秒/トークン（≈0.001トークン/秒）で100万パラメータのGPTスタイルTransformerを証明しました。パフォーマンスは徐々に向上しました。zkLLM（2024）は、GPU上で約15分で2,048トークンの入力を持つLLaMA-2-13Bを証明しました。これは、新しいトークンあたり約0.001トークン/秒、またはバッチで約2.5トークン/秒です。2025年には、zkGPTはGPT-2を21.8秒（≈0.05トークン/秒）に、zkPyTorchは単一CPUコアで約150秒/トークン（≈0.007トークン/秒）でLlama-3 8Bを証明し、ZKTorchはGPT-J（6B）を約20分（≈0.001トークン/秒）で証明しました。VerInfは、約0.02トークン/秒でLlama 4 Maverick（私たちが証明するのと同じ400BパラメータのMoEモデル）を証明しました。DeepProveは、現在の査読付き最先端技術であり、単一のフォワードパスで生成されたシーケンス全体を証明します。これは、単一マシンでGPT-2で約2.9トークン/秒、Gemma 3で1.4トークン/秒、分散環境で31トークン/秒に達します。SASHのプロバー（2026）は、単一H100でLlama 3.1 8Bで約1.25トークン/秒を達成しました。

最近の商業的な取り組みは印象的な数字を達成しており、Attestableは単一H100でGemma 4 31Bを53〜77トークン/秒で証明しています。執筆時点では、Attestableは対応するオープンソースライブラリをリリースしていません。

上記の数字は、過去数年間の証明可能な推論の急激な進歩を示しています。これらは、ゼロ知識で証明できることについての私たちの事前確率を更新するはずです。

• 2024年、zkLLMは13Bモデルを1つのA100で約2.5トークン/秒で証明しました。私たちが知る限り、Llama 4 Maverickの最初の証明であるVerInfは、DGX Sparkで1,000トークンを14.3時間で処理し、検証にほぼ1日かかった93.6GBの証明を報告しています。
• FlashProveは、同じモデルを単一H100で110トークン/秒で証明し、19MBの証明は数秒で検証できます。Attestableは独立して、密な31Bモデルで53〜77トークン/秒を報告しています。

この進歩は、より多くのモデルとアーキテクチャに転移し、ネイティブ計算に対するオーバーヘッドが約2桁（私たちの測定では約70〜95倍）の柔軟で強力なツールをもたらし、以前予想されていたよりもはるかに少ないものになると信じています。

制限事項

このリリースは研究プロトタイプであり、以下の技術的な制限があります。

• 高速実行可能コードに対する正式な保証はありません。プロトコル（実行可能な「低速」Leanベリファイアを含む）のLean実装と、Leanで証明されたセキュリティプロパティを提供します。論文と高速実行可能コードはLeanプロトコルから派生していますが、3つすべて（Lean、論文、コード）が互いに一致することを保証するものではありません。
• 証明は、貪欲デコーディング下の整数モデルに関するものです。公開された重みの正確な整数バージョンを証明し、証明はチェックされた各トークンがそのモデルの貪欲な選択であることを主張します。浮動小数点実装からの応答、またはサンプリングデコーディングは、ある位置で逸脱する可能性があり、証明された計算と正確に一致しなくなる可能性があります。整数バージョンは、一般的に、浮動小数点計算の非決定性を考慮しても、汎用的に真の浮動小数点推論との小さなエラー率の範囲内にあると期待され、経験的にテストされています。ただし、これは敵対的に設計されたプロンプトをカバーするものではありません。
• アーキテクチャの隠蔽。私たちのシステムは、提供されるモデルが混合専門家（MoE）アーキテクチャを使用していると仮定しています。このアーキテクチャでは、各トランスフォーマーレイヤーのフィードフォワードブロックは、複数の専門家サブネットワークと、各トークンに対して少数の専門家のみをアクティブ化するルーターに置き換えられ、私たちのシステムは効率向上のためにMoE構造を使用します。密モデルなどの他のアーキテクチャも広く使用されており、その説明にはモデルプロバイダーが秘密にしておきたい知的財産が含まれている可能性があります。実際、アーキテクチャをさらに隠蔽するシステムを想像することもできます。プロバーは、重みとアーキテクチャ（つまり、推論のための「実行可能コード」）の両方を隠蔽コミットメントによってコミットし、ベリファイアの主張は、コミットされた実行可能コードのそのコミットメントモデル上での実行をチェックすることに関するものになります。
• サイドチャネル攻撃。プロトコルの現在の保証は、証明自体がコミットされたモデルの重みに関する情報を明らかにしないということです。しかし、「サイドチャネル攻撃」、たとえば証明の生成にかかる時間を測定するなど、重みに関する情報を明らかに可能性があります。これはこのリリースでは範囲外と見なします。
• より長いコンテキスト。システムは現在、最大1,024トークンのコンテキストでの推論を証明します。これは、チャット設定で蓄積されるコンテキストと比較すると非常に短いです。理想的には、このコンテキスト長は、最先端モデルの完全なコンテキストウィンドウ（数万から数百万トークンを定期的に持つ）にまで拡張できる可能性があります。

---