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

概要

友人と対面で話すとき、相手が本人であることを確かめる手段はいくつもある。姿が見え、声が聞こえ、握手もできる。AIモデルとの対話では、そのどれもがほぼ使えない。今日、ユーザーはモデルにリクエストを送っても、返ってきた応答が開発者の名乗るモデルから出たものかを検証できない。ルーティングサービスがコスト削減のために別のモデルへ密かに差し替えているかもしれないし、攻撃者がトークンストリームを改ざんしているかもしれない。モデルの出力だけを見ても信頼できない。出力の品質がどれほど高くても同じだ。推論の暗号学的証明がこの問題を解決する。モデル提供者がまずあるモデルへのコミットメントを作り、そのうえで各応答がそのモデルによって生成されたことを証明する。この種の証明はコンシューマー向け製品から社内のセキュリティまで幅広い用途を支え、AI開発のペーシング（pacing）のコンプライアンスを検証するツールの一助にもなる。

具体的には、zkSNARKと呼ばれる暗号学的証明で進展を得た。隠蔽性と効率の高さから、証明可能な推論に特に向いている。本記事ではその一部を、私たちがFlashProveと呼ぶシステムを中心に紹介する。技術的な要点は次のとおりだ。

Claudeは推論向けzkSNARKに改良を加え、これまでのオープンソースシステムよりはるかに高速なシステムを構築した。大規模モデルの一例（Llama 4 Maverick、400BパラメータのMoEモデル）で、4-bit量子化重み、prefill段階で整数演算を使う条件のもと、H100 GPU 1枚あたりの証明生成速度は約110 tokens/秒、1,024トークンのリクエストあたりの証明サイズは約19 MBだった。これはvLLM（よく使われるオープンソースライブラリ）でモデル自体を動かすのに必要なGPU時間のおよそ70〜95倍にあたる。
従来のオープンソースシステムは数桁遅い。詳細は第6節を参照してほしい。Claudeは新しい手法を見つけ、暗号学とセキュリティの文献にある最先端のツールを活用しつつ、暗号学的証明システムの成熟した設計原則に依拠した。モデルへのコミットメントと、それに続く推論の証明はいずれもモデルの重みを隠す。モデルアーキテクチャの隠蔽は本システムの目的ではない。

Claudeは最適化が得意だが、評価の難しい判断を下すことが多い。大規模で複雑なシステムではとりわけそうだ。私たちはこれに対して、主張する安全性保証を Lean（形式検証言語）でトップレベルの監査可能な記述としてまとめる形で対処した。

本日、5つの成果を公開する。

本ブログ記事：私たちのシステムとその潜在的用途の概要
技術レポート：システムの詳細
（Claudeが執筆した）プロトコル仕様書
実行可能なコード：証明器と2つの検証器、C++で書かれた高速検証器と、証明可能な正しさを持つ検証器（Leanで記述）を含む
トップレベルの数学的命題に対するLean証明と、監査を補助するLean定理の対話的可視化ツール

コード、Lean証明、ドキュメントはApache 2.0ライセンスで公開する。¹ この研究記事は完成した研究アジェンダではなく、途中経過の共有を目的としている。公開するのは、私たちの成果を見て、使って、改良してくれる人が現れることを期待しているからだ。

はじめに

ユーザーがAIモデルにリクエストを送るとき、自分が選んだモデルがその応答を生成したモデルであることを今は確かめられない。日常的な利用では、ユーザーは出力だけを気にかけ、どのモデルが生成したかまでは気にしないことが多く、この問題は差し迫ったものではない。だが、いくつかの場面ではこの保証が役に立つ。たとえば、モデルのリリース前後にテストする独立評価者は、評価しているモデルが実際にサービスを提供しているモデルであることを知る必要がある。サードパーティのルーティングサービス経由でモデルを呼ぶ顧客は、トークンが自分が料金を払っているモデルから来たという保証を望む。そして、ネットワーク上の攻撃者がトークンストリームを改ざんしてあるモデルを装った場合、ユーザーは出力だけからはまったく気づけない。

しかし、モデル応答の検証を実現するのは容易ではない。ほとんどのフロンティアモデルの重みは非公開だ。仮にユーザーが重みを入手できたとしても、ある応答がその重みを持つモデルによって生成されたことを確かめるにはモデルを一度動かす必要があり、それに必要な計算資源は一般のユーザー（評価者であっても）が負担できる範囲をはるかに超える。

証明可能な推論（provable inference、PI）が目指すのは、計算資源が限られ、モデルの重みを一切知らないユーザーでも、ある回答がリクエストしたモデルから出たものだと検証できるようにすることだ。PIを後押しする動機は2つある。1つはAIプロバイダーに対する顧客の信頼を高めること。もう1つは、独立評価者に保証を提供し、プロバイダーがいくつかの約束や法的義務を果たしたことを証明できるようにすることだ。したがってPIは、AIフロンティア開発のペース配分とAI規制にも関わる。

PIを実現する道の1つは、ゼロ知識簡潔引数と呼ばれる暗号学的対象を使うものだ。モデル提供者は主張する回答とともに短い証明（たとえば数MB）を添え、ユーザーはそれを高速に検証できる（理想的にはCPUで数秒）。主張する回答が指定されたモデルから出たものでなければ、検証は失敗する。重要なのは、この証明がモデルの重みに関するいかなる情報も漏らさないことを暗号学が保証する点だ。

本日公開するFlashProveは、証明可能な推論に向けた、オープンソースで高性能なプロトタイプだ。400BパラメータのMoEモデル（Llama 4 Maverick、4-bit量子化）に対して、H100 GPU 1枚で毎秒100トークンを超える速度で証明を生成し、1,024トークンのリクエストあたりの証明サイズは約19 MBであることを示す（GPU時間は、同じ長さのプロンプトを処理する常用オープンソースライブラリvLLMのおよそ70〜95倍）。

今回のリリースには、実行可能なコード、Lean による形式化、プロトコルの技術的な説明が含まれる。目的は二つある。(i) 証明可能な推論の開発を加速させ、後押しすること。(ii) ゼロ知識簡潔引数が証明可能な推論に実用できることを示すこと。

この進展は、安全性、AI 開発のペース配分、AI 顧客へのインテグリティ保証、監査者や規制者に渡すツールといった点で重要だと考える。

AI の普及に伴う信頼の課題

人工知能の発展、そしてデジタルインフラと経済におけるその役割の拡大は、AI プロバイダーが応答を迫られる信頼の課題を生んでいる。証明可能な推論（PI）に関するツールは、こうした課題への対処に役立つ。

PI のツールにはハードウェアによるもの、ソフトウェアによるもの、両者を組み合わせたものがある。ここではソフトウェアによるものだけを扱う。zkSNARK（ゼロ知識簡潔知識引数）と呼ばれる暗号技術だ。平たく言えば、zkSNARK とは、証明者が短い「証明書」によって検証者に計算が正しく実行されたことを納得させる仕組みである。重要なのは、この証明書がゼロ知識であること、つまり計算が正しいという事実から導かれる以上の情報を何も漏らさないこと、そして簡潔であること、つまり検証が証明対象の計算より指数関数的に速いことだ。

以下ではいくつかの課題と、zkSNARK がそれらへの対処にどう役立つかを挙げる。

課題 1：ペース配分

AI 開発のペースを規制したり制御したりする提案の中には、ハードウェアとその使われ方を監視することに頼るものがある。たとえば、強力な新しいモデルの訓練ではなく推論専用にハードウェアを使うことをプロバイダーに求める場合だ。プロバイダーは、より安価なモデルを提供したり、想定外の方法で計算資源を使ったりして、訓練用のリソースを捻出しようとするかもしれない。規制者は、ハードウェアが実際に推論に使われていることをどう確実に確かめられるのか。

zkSNARK がどう役立つか： 規制者は、一定期間に処理した推論リクエストを対象とする証明書の提出をプロバイダーに求められる。証明書は、それらのリクエストが申告どおりのモデルによって生成されたことを示さなければならない。悪意あるプロバイダーは、ハードウェアが実際に正しいモデルを動かしていない限り、この要求を満たせない。zkSNARK があれば、規制者はプロバイダーが持つかもしれない複雑なハードウェア環境を用意することなく、プロバイダーの主張が成り立つかを検証できる。プロバイダー側も、規制者にモデルの専有情報が渡らないことを確信できる。² ただしこれが検証するのは、ハードウェアが推論を処理していることであって、裏で訓練をしていないことまでは証明しない。

課題 2：改ざんの検知

AI モデルの価値が上がるほど、それを動かすサーバーは格好の攻撃対象になりやすい。攻撃者や制御を失った agent は推論サーバーを侵害し、重みを窃取したり、ユーザーに悪意ある応答を返したり（ユーザーの端末にマルウェアを送り込むなど）できる。しかもそのすべてを正規の応答に紛れ込ませられる。敵は外部にいるとは限らない。モデルが自らを改良して配備できるようになるにつれ、より高性能なモデルが、稼働を許可されたモデルに取って代わり、本来なら自分を対象とする分類器や監視を逃れるために、弱いモデルを装うかもしれない。どちらの場合も問題は同じだ。企業は、サーバー上で実際に動いているのがどの重みなのかをどう確定するのか。Anthropic は Frontier Safety Roadmap の中で、推論トラフィックの検証の試作について公約を掲げている。「2026 年 9 月 30 日までに、推論を証明する試作品を開発する。これは AI モデルの出力に確実かつ証明可能な形で「署名」を付ける技術であり、出力を特定のモデルの重みに帰属させられるようにする。」RSP の更新で述べたとおり、私たちは独立したものの関連する別の取り組みでこの目標を達成した。推論トラフィックへの署名と、信頼できるサーバー上での推論の再計算である。本稿の成果は、別の手法で同じ目標を追うものだ。³

zkSNARK がどう役立つか： サービス提供者は、応答ごとに有効な zkSNARK を添付するようサーバーに要求できる。証明は重みへの特定のコミットメントに束縛されるため、応答が何らかのモデルから出たことだけでなく、コミットされたモデルから出たことを示す。サーバーを侵害した攻撃者や、別のモデルになりすまそうとするモデルは、期待される重みに対して有効な証明を出さなければ露見を避けられないが、それはできない。ユーザーもこの証明を受け取れる。ゼロ知識性により証明から内部情報は漏れず、簡潔性により検証の負担は小さい。これにより、攻撃者が推論 API を通じて達成できることが制限される。

課題 3：テキストの出所

人は、ある事柄を理解し分析するために実際に多大な労力を費やしたことを示したい場合がある。たとえば、開発者が自分のソフトウェアライブラリの脆弱性をあるフロンティア級のサイバーセキュリティモデルにスキャンさせたと主張したり、企業が自社の事業計画を適切なモデルに承認させたと主張したりする場合だ。ユーザーはこうした主張をどう確かめられるのか。モデルを動かすためのリソースも、その権限も持たないかもしれない。チャット履歴を公開しても絶対的な保証にはならない。開発者は理論上、フロンティアモデルではなくより安価なモデルや性能を落とした版を使って履歴を偽造できる。要するに、ユーザーは自分が選んだまさにそのモデルを使っていることをどう確認するのか。

zkSNARK がどう役立つか： サービス提供者は、各応答に zkSNARK を添付し、その出力が申告どおりのモデルによって与えられた入力から生成されたことを示せる。簡潔性により、ユーザーは専用ハードウェアなしで証明書をすばやく検証できる。ゼロ知識性により、サービス提供者は専有の重みに関する情報がユーザーに渡らないことを確信できる。これは、ある応答がどのモデルから出たかを検証する既存の仕組みを補完するものだ。

たとえば、脆弱性が頻繁に見つかる環境では、モデル提供者は新しいコードをリリースする前に、コード開発者へ失敗証明（Proof-of-Failure）を発行できる。特定のモデルにある結果を出させるために少なくとも X トークンを使い、それでも目的の結果が得られなかったことを示す証明だ。具体的には、少なくとも 100 万トークンを試した後も、そのモデルが特定のパッチの中にバグを 1 つも見つけられなかった、という内容になる。

課題 4：モデルの承認

規制当局は、サービス提供者に対し、安全と承認されたモデルだけを提供することを求めるかもしれない。サイバーセキュリティや安全性のリスクがあると判断されたモデルの提供は認めない、というわけだ。提供者側にはこの要件を回避する動機があり得る。リスクの高いモデルのほうが競合より性能が高かったり、提供コストが低かったりするからだ。規制当局は、承認済みのモデルだけが提供されていることをどうやって保証するのか。

zkSNARK がどう役立つか： 規制当局は、応答に zkSNARK を添付するよう提供者に義務づけることで、承認済みモデルの使用を強制できる。証明は各リクエストを使用したモデルに結びつけるので、提供者が未承認のモデルを使えば証明は検証を通らない。簡潔性のおかげで、規制当局はリクエストを 1 件ずつ再実行することなく、軽い負荷で検査を済ませられる。

信頼できるハードウェアと PI についての補足。 従来の研究では PI の実現に トラステッド実行環境（TEE）をよく用いてきた。こうしたハードウェアベースの方式はプライバシーとリモート認証を提供するが、前提として製造元が改ざん耐性のあるハードウェアを作れる必要がある。本研究は純粋にソフトウェアの暗号方式に焦点を当てており、その安全性とプライバシーは計算問題の困難性に依存する。ハードウェアや OS など環境がすでに侵害されていても、攻撃者は計算上実行不可能な問題を破らない限り、有効な証明を偽造できない。信頼できるハードウェアと暗号は補完し合う 2 つのアプローチであり、与える保証もトレードオフもそれぞれ異なる。上述の信頼に関する課題に対しては、どちらも役割を果たす。

私たちのシステム：FlashProve

FlashProve は、大規模な Mixture-of-Experts（MoE）言語モデル向けの証明可能な推論システムである。詳細は技術レポートを参照してほしい。ここでは概要を述べる。

FlashProve には 2 つの当事者がいる。モデル提供者（証明者）とユーザー（検証者）だ。システムは 2 つの段階に分かれる。

オフライン段階では、証明者がモデルの重みへのコミットメントを公開する。重みそのものは隠したまま、ある特定の重みの組を固定する短い指紋だ。以降の推論に関する主張はすべてこのコミットメント、すなわちこの段階でコミットした重みのモデルに対して検査される。
オンライン段階では、検証者からリクエスト（プロンプトと対応する出力トークン）を受け取ると、証明者が証明ファイルを生成し、次の命題を証明する。

コミットしたモデルが評価時に生成した出力トークンであること。

コミットメント、prompt、応答のすべてを持つ者なら誰でも、重みなしで、しかもわずかな計算量で検証でき、コミットした重みがこの prompt 上で実行された結果としてまさにこれらのトークンが得られたと確信できること。

保証

証明ファイルは次の 2 つの性質、すなわち「完全性」と「健全性」を満たす。

正直な証明ファイルは受理される（完全性）。 正直な証明者が生成した証明は検証者に受理される。
証明ファイルは偽造できない（健全性）。 誤った主張に対して有効な証明を生成することは事実上不可能であり（確立された暗号学的仮定を破ることに等しい）、検証者は証明者を信頼する必要がない。

モデルの重みを知る強力な検証者だけであれば、完全性と健全性は実現できる（prompt 上でモデルを実行し、結果が応答と一致するか確認すればよい）。このシステムを本当に価値あるものにするのは、次の 2 つの性質だ。

証明ファイルは主張以外の情報を漏らさない（ゼロ知識）。 検証者は重み、計算の中間値、各層でどのエキスパートが動いたかを一切知らない。モデルアーキテクチャ（重みを除く）は隠さない。
証明ファイルは小さく、検証コストが低い（簡潔性）。 証明対象の計算は 400B パラメータモデル（量子化版で約 232 GB）を H100 GPU 1 枚で 1 回実行したもので、検証者が受け取る証明ファイルは約 19 MB、24 コアの CPU なら数秒で検証が終わる。監査者や、サービス提供者よりはるかに貧弱なハードウェアしか持たないユーザーでも、複雑なインフラなしに証明ファイルを検証できる。

評価

Llama 4 Maverick（400B パラメータの MoE モデルで、トークンあたり約 17B のパラメータを使用）上で、公開されている 4-bit 重みを使ってこのプロトコルを実装し、測定した。検証リクエスト 1 件は 1,024 トークンのウィンドウで、証明 1 件がトークン 1 個を検証する。証明者は H100 1 枚と CPU 24 コアを備えたサーバー上で、検証者は CPU 上で動作する。

証明者。 証明者は H100 1 枚と CPU 24 コアを備えたサーバー上で動作する。オフライン段階はモデルごとに 1 回だけ実行し、約 39 分かかる。（技術レポートで論じているいくつかの技術的な理由により、生成されるコミットメントはおよそ 1,600 万リクエストまで利用でき、その後は提供者がコミットメントを再生成する必要がある。）オンライン段階で 24 リクエストのバッチを処理するのに証明者は約 223 秒を要する。毎秒 110 トークン、証明 1 件あたり 18.78 MB である。
検証者。 検証者はクライアント側の CPU 上で動作し、GPU を必要とせず、重みへのコミットメントにしかアクセスできない。クライアントはまずコミットメント（合計約 6.5 MB）をダウンロードし、その後はリクエストごとに証明を 1 つダウンロードする。24 スレッドで証明 1 件を検証するのに 17 秒（シングルスレッドでは 21 秒）かかり、これにはオフライン段階の検証も含まれる。

通常の推論との比較。 広く使われている推論エンジン vLLM で同じモデルの FP8 版を 8 枚の H100 上で動かしたところ、GPU 1 枚あたりに換算して、24 リクエストのバッチを証明するのに要する時間は、vLLM が同じ 24 リクエストを一度に処理する時間の約 72 倍だった（複数回の実行で 66 倍から 77 倍）。試した中で最も高い負荷では、この倍率は約 94 倍になる。

システムの内部。 FlashProve を支える仕組みは zkSNARK で、ピアツーピアシステムに導入されているものと同じ種類だ（例えば Ethereum などのブロックチェーンにサービスを提供する Starknet や Mantle といった L2 ネットワーク）。私たちの zkSNARK は確立された手法に沿って構築している。まず対話型オラクル証明（IOP）と呼ばれる情報理論的な対象があり、これをハッシュ関数によって暗号学的証明へとコンパイルする（したがって耐量子安全性も備える）。IOP は最先端の部品を組み合わせて作っており、線形制約付き符号近接性テストやルックアップ引数といったツールを使っている。これらは符号理論と計算複雑性理論の技術に基づく。これらの部品を組み合わせ、推論向けに仕立てた IOP を作るのは繊細な作業だ。構成の詳細は技術レポートを参照してほしい。

システム設計

FlashProve は私たちが下したアーキテクチャ上の判断に支えられている。個々の判断については技術レポートで詳しく論じている。ここではそのうちいくつかを取り上げる。

prover の作業量は、実際に計算に関与するエキスパートに比例する。MoE モデルでは、1 トークンが使うのは 400B パラメータのうち約 17B だけなので、prover が 1 トークンあたりに処理する作業量は全パラメータではなくこの約 17B に比例する（証明自体は、どのエキスパートが選ばれたかを依然として明かさない）。
リクエストは事後にバッチ単位で証明する。prover は生成済みのテキストを 1 回の並列走査で読み（prefill と同じ）、重みのコミットメントはリクエストごとではなくバッチごとに 1 回だけ開く。
システムは GPU 1 枚を前提に設計している。各層のモデル重みは複数のセグメントに分割し、一度に 1 セグメントずつ証明する。重みは通常のメモリに置き、必要に応じてストリーミングで読み込む。そのため 80 GB の GPU と、隣接する約 290 GB のホストメモリがあれば足りる。

事後証明とオンライン証明

証明の仕組みを推論サーバーに組み込む際には選択肢がある。オンライン証明（推論と同時に証明する）か、事後証明（後から一部のトークンについて証明する）かだ。私たちのシステムは後者を採る。オンライン方式は極端な速度を要求され、効率のために安全性を犠牲にするかもしれない。事後方式なら速度は遅くてよく、そのようなトレードオフを迫られない。一方で事後証明には限界もある。再計算に伴う余分な複雑さ、トラフィックを確保したうえでの遅延、そして本質的な「非決定性」だ。事後証明を選ぶ動機と影響については、技術レポートでさらに掘り下げている。

形式検証がもたらす信頼性

暗号コードは脆く、間違えやすいことで知られている。今日リリースするコードを、ユーザーはなぜ信頼できるのか。

答えは形式検証だ。私たちは Lean 証明支援系を使ってプロトコルと、期待されるセキュリティ性質を記述する。そしてこれらの性質を、機械的に検査でき、正しさが保証された形（コンパイラが正しい限りにおいて）で証明する。対象とするトップレベルの性質は 3 つある。

完全性：命題が真なら、生成された証明は検証器に受理される。
健全性：偽造された証明は、確率が無視できる場合を除いて検証器に拒否される。
ゼロ知識性：証明はモデル重みに関する情報を一切漏らさない。検証器が応答そのものから推論できる内容を除いて。⁴

これらの性質はランダムオラクルモデルの下で述べている。ランダムオラクルモデルとは、ハッシュ関数に依存する暗号プロトコルを解析するための情報理論的な手法だ。

形式検証には、重要な信頼のギャップが 2 つ残る。第一に、形式化された命題が意図と合っているかを監査しなければならない。これは人手でしかできない（とはいえ証明の監査よりはずっと楽だ）。補助として対話的な可視化ツールを用意している。

第二に、実行されるコードが、セキュリティ性質の証明に用いた形式化されたプロトコルと一致するかを監査しなければならない。この監査をどう支援するのが最善かは性質によって変わる。健全性は検証器だけに、ゼロ知識性は証明者だけに、完全性は両者のやり取りにかかっているからだ。

健全性については、検証器のコードが正しいことだけを確かめればよい（「証明」の価値はまさにここにある。検証器を信頼しさえすれば、証明者はまったく信頼しなくてよい）。私たちは C++ の検証器と並べて、実行可能な Lean の検証器を提供している。Lean の検証器は動作が遅いが、健全性定理における検証器が受理するものだけを受理することは Lean が証明済みだ。とはいえ日常的な利用には C++ の検証器を勧める。形式的な保証は一切付かないが、私たちが試したすべての証明で Lean の検証器と一致した。
完全性については、脅威モデルが敵対的攻撃を想定していない（証明者も検証器も正直である）。したがって Lean の検証器があれば、正直な証明者が受理される証明を生成することを、通常のソフトウェアテストで確信できる。正しい命題に対して証明者を走らせ、生成された証明に対して Lean の検証器を走らせればよい。
ゼロ知識性については、証明者が正しいことだけを確かめればよい。だが検証器と違い、証明者はコストの大きい処理であり、Lean の証明者を走らせるのは現実的でない。ここでは補助を提供しない。提供するモデルの重みを隠そうとする証明者なら、Lean の証明者との等価性を確かめるための入念なエージェントによる監査や人手によるセキュリティ監査を行うだけのリソースはあるはずだ、というのが私たちの考えだ。

先行研究

証明可能な推論の実装は、一般に「zkML」と呼ばれる研究方向の目標である。初期の研究として、SafetyNets（2017）は2層畳み込みの MNIST CNN と小規模な全結合音声モデルを検証し、zkCNN（2021）は VGG-16（1500万パラメータ）に到達して証明1回あたり88.3秒、Kang et al（2022）はフル解像度の ImageNet 上で MobileNet v2 を証明した。

続いて Transformer の証明が登場した。ZKML の GPT-2 は1億1700万パラメータでトークンあたり約159秒（≈0.006 tok/s）を要し、Modulus Labs の15億パラメータの GPT-2 XL では90時間以上かかった。EZKL（2023）は100万パラメータの GPT 系 transformer を証明し、トークンあたり約966秒（≈0.001 tok/s）だった。性能は徐々に向上している。zkLLM（2024）は GPU 上で2048トークン入力の LLaMA-2-13B の証明を約15分で完了する。新しいトークン1個あたり ≈0.001 tok/s、バッチ処理では約2.5 tok/s だ。2025年には、zkGPT が GPT-2 を21.8秒（≈0.05 tok/s）に短縮し、zkPyTorch は単一 CPU コア上で Llama-3 8B をトークンあたり約150秒で証明し（≈0.007 tok/s）、ZKTorch は GPT-J（6B）を約20分で証明した（≈0.001 tok/s）。VerInf は Llama 4 Maverick（私たちが証明したのと同じ400Bパラメータの MoE モデル）を ≈0.02 tok/s で証明している。DeepProve は現在の査読済み最先端研究であり、単一のフォワードパスで生成系列全体の証明を出力する。単一マシン上で GPT-2 は約2.9 tok/s、Gemma 3 は1.4 tok/s、分散環境では31 tok/s に達する。SASH の prover（2026）は H100 1枚で Llama 3.1 8B を ≈1.25 tok/s で証明する。

最近の商用の取り組みも目覚ましい数字を出している。Attestable は H100 1枚で Gemma 4 31B を53〜77 tok/s で証明する。本稿執筆時点で、Attestable は対応するオープンソースライブラリを公開していない。

以上の数字は、ここ数年の証明可能な推論の進歩がいかに急峻かを示している。ゼロ知識証明の能力の限界についての私たちの事前判断は、これらによって更新されるべきだろう。

2024年、zkLLM は A100 1枚で13Bモデルを約2.5 tokens/秒で証明した。私たちの知る限り、Llama 4 Maverick の証明はこれまで VerInf だけであり、DGX Spark 上で1000トークンに14.3時間、証明サイズ93.6 GB、検証に丸1日近くを要すると報告している。
FlashProve は H100 1枚で同じモデルを110 tokens/秒で証明し、証明サイズは19 MB、検証は数秒で終わる。Attestable は稠密31Bモデルで53〜77 tokens/秒という結果を独立に報告している。

こうした進歩はより多くのモデルやアーキテクチャに広げられるべきであり、そうすればネイティブ計算の約2桁（私たちの測定では約70〜95倍）のオーバーヘッドで動く柔軟かつ強力なツールとなり、従来の予想をはるかに下回る水準になる。

限界

今回公開するのは研究用プロトタイプであり、以下の技術的限界がある。

高速な実行コードに対する形式保証はない。 私たちはプロトコルの Lean 実装（実行可能な「低速」Lean 検証器を含む）と、Lean で証明した安全性の性質を提供する。論文と高速な実行コードはいずれも Lean プロトコルから導出したものだが、三者（Lean、論文、コード）が互いに一致することは保証しない。
証明の対象は貪欲デコード下の整数モデルである。 私たちは公開重みの正確な整数版を証明し、証明は検査された各トークンがそのモデルの貪欲な選択であることを主張する。浮動小数点実装やサンプリングデコードが返す応答は、ある位置でずれて、証明された計算と完全には一致しなくなる可能性がある。整数版と実際の浮動小数点推論の間には、通常ごく小さな誤差率しかないと考えられており、経験的なテストでもそう確認されている（浮動小数点計算の非決定性を考慮に入れても）。ただしこれは、敵対的に設計されたプロンプトを対象とするものではない。
アーキテクチャの隠蔽。 私たちのシステムは、提供するモデルが混合エキスパート（MoE）アーキテクチャであることを前提とする。すなわち、各 transformer 層のフィードフォワードブロックが複数のエキスパートサブネットワークと router に置き換わり、router がトークンごとにごく一部のエキスパートだけを活性化する構造であり、私たちのシステムはこの MoE 構造を利用して効率を高める。稠密モデルなど他のアーキテクチャも広く使われており、その記述にはモデル提供者が秘匿したい知的財産が含まれうる。実際、モデルアーキテクチャをさらに隠すシステムも考えられる。証明者は重みとアーキテクチャ（つまり推論の「実行コード」）を隠蔽コミットメントで同時にコミットし、検証者の主張は、コミットされた実行コードをコミットされたモデル上で実行した結果を検査することになる。
サイドチャネル攻撃。 現時点のプロトコルの保証は、証明そのものがコミットされたモデルの重みの情報を漏らさないことである。しかし、証明の生成にかかる時間を測定するといった「サイドチャネル攻撃」によって、重みに関する情報が漏れる可能性がある。今回の公開はこの問題を対象としていない。
より長いコンテキスト。 現状のシステムが証明できるのは、最長1,024トークンのコンテキスト上の推論である。チャットで蓄積されるコンテキストに比べるとかなり短い。理想的には、コンテキスト長はフロンティアモデルの完全なコンテキストウィンドウ（通常、数十万から数百万トークン）まで拡張できるべきである。

私たちのオープンソース研究では、Meta の Llama 4 Maverick（400B パラメータ）を使っている。Hugging Face で第三者が公開している 4-bit 変換版を採用した。今回のリリースに重みは含まれない。読者自身が Hugging Face からダウンロードし、Meta の Llama 4 ライセンスに従う必要がある。今回のリリースでは、このモデルが計算した小容量の内容、たとえばコミット ID、チェックサム、性能データ、一部のパラメータ設定を公開している（完全な一覧は THIRD_PARTY.md を参照）。読者自身による結果の検証や、この作業を他のモデルへ適用することも歓迎する。完全なサンプルを動かすには、大型の GPU マシンと Meta のトークナイザーへのアクセス権が必要になる。 ↩
どの情報を隠すかはシステムの設計次第だ。私たちの作業では重みを隠し、アーキテクチャは隠していない。今後の作業では、アーキテクチャの詳細も隠す予定だ。（原理上はモデルのあらゆる詳細を隠せる。問題は、それをどれだけ効率的に実現できるかにある。） ↩
2026 年 10 月 19 日の更新では、目標の名称も変更した。現在は「証明可能な推論」（provable inference）ではなく「推論の検証」（inference verification）を使っている。当初の目標は、トークンストリームの完全性に対して高い保証を与えることであり、それは複数の方法で実現できる。「証明可能な推論」という呼び方は、私たちが必要と考えているよりも狭い道筋を暗示していた。このプロトタイプとは別に進めているのが、推論に対する暗号学的証明の研究であり、これはトークンストリームに高い保証を与える方法の一つそのものだ。 ↩
モデルのアーキテクチャは隠していない。アーキテクチャの詳細をさらに隠すことは今後の作業に委ねる。 ↩

概要