チャットボットが返した回答が、本当に指定されたAIモデルによって生成されたものなのか。現在のAIサービスでは、利用者がこれを独立して検証するのは難しい。事業者が裏側で安価なモデルに切り替えたり、出力を改ざんしたりしても、回答の文章だけから見抜くことはできない。この問題に対し、暗号技術を使ってAIの計算結果を数学的に検証する研究が進んでいる。
Anthropicの研究チームは2026年11月2日、大規模言語モデル（LLM）の推論結果をゼロ知識証明（zkSNARK）によって検証できるシステム「FlashProve」を公開した。Metaの「Llama 4 Maverick」（4,000億パラメータ、128エキスパート構成）の4ビット量子化モデルを対象に、単一のNVIDIA H100 GPUで証明書を生成できることを実証した。成果は査読済み論文ではなく、AIが生成した記述やコードを含む研究プロトタイプであり、詳細な検証は完了していない。それでも、従来は膨大な計算資源を必要としていた大規模LLMの推論検証に、具体的な性能指標を示した点で重要な進展といえる。
モデルの重みを公開せずに計算結果を証明する仕組み
FlashProveが採用する「証明可能推論（Provable Inference）」は、検証者がモデルの重みを入手したり、同じ計算を再実行したりすることなく、回答が指定されたモデルの計算結果と一致するかを確認する技術だ。商用AIモデルの重みは通常公開されず、仮に入手できても数千億パラメータ規模のモデルを一般の利用者が実行するのは現実的ではない。ゼロ知識証明を利用すれば、モデルの内部情報を明かさずに計算の正しさだけを証明できる。
FlashProveは、処理をオフラインとオンラインの2段階に分けている。オフライン段階では、モデル提供者が重み全体に対応する暗号学的な「コミットメント」を作成する。これはモデルの重みを特定するための暗号学的な値で、約6.24MBのデータとして公開されるが、重みそのものは復元できない。オンライン段階では、提供者がプロンプトと応答トークンに対応する約18.78MBの証明書を生成し、検証者はコミットメントと照合することで計算結果の正しさを確認する。
この仕組みは、正しい計算なら証明が受理される「完全性」、不正な計算の証明を偽造することが計算量的に困難である「健全性」、モデルの重みや中間計算を明かさない「ゼロ知識性」、そして巨大な計算でも証明書と検証処理を小さく抑える「簡潔性」を目指して設計されている。ゼロ知識性によって、Mixture-of-Experts（MoE）モデルでどのエキスパートが選択されたかも秘匿される。ただし、モデルのアーキテクチャ自体は隠されない。また、健全性は暗号学的な計算困難性の仮定に依存しており、無条件の数学的保証ではない。
重要なのは、今回の検証対象が通常のLLM推論とは異なる点だ。FlashProveは、公開された4ビット量子化重みを整数化したモデルを使用し、各ステップで最も確率の高いトークンを選ぶ「貪欲法（Greedy Decoding）」による決定論的な計算を証明する。一般的なAIサービスで利用される浮動小数点演算や確率的サンプリングを、そのまま検証できるわけではない。
MoEの疎な計算構造を利用し、単一GPUで証明を生成
大規模LLMのゼロ知識証明が難しい理由は、通常の推論よりもはるかに多くの計算とメモリを必要とするためだ。数千億パラメータの計算をそのまま暗号回路に変換すれば、巨大なGPUクラスタでもメモリ不足に陥りかねない。FlashProveは、暗号プロトコルの最適化とMoEモデルの構造を組み合わせることで、この問題に対処している。
暗号技術の基盤には、対話型オラクル証明（IOP）を採用した。符号近接性テストやルックアップ引数などの手法を組み合わせ、ハッシュ関数によって非対話型のzkSNARKへ変換する。ハッシュ関数の安全性に依存する構成のため、耐量子性も期待されるが、これは暗号学的な仮定に基づく理論上の性質であり、量子コンピュータによる実証を意味するものではない。
計算量の削減で特に重要なのが、MoEの疎（スパース）な構造だ。Llama 4 Maverickは総パラメータ数が4,000億に達する一方、各トークンの計算で実際に使われるのは約170億パラメータに限られる。FlashProveは、モデル全体ではなく実際に活性化されたパラメータの計算量に応じて証明処理が増えるよう設計されている。エキスパートの選択情報も検証者には公開されない。
ハードウェア面では、約232GBの量子化重みをGPUのVRAMではなく、約290GBのCPU側メモリに保持する。モデルを層ごとに分割し、必要な重みを80GBのVRAMを備えるH100へ順次転送することで、単一GPUの容量を超えるモデルを扱えるようにした。
さらに、FlashProveは回答の生成と証明処理を分離する「事後証明（Post-hoc Proving）」を採用している。回答を生成した後、複数リクエストの計算をまとめて処理し、重みの読み込みやコミットメント関連処理を共有することで効率を高めた。回答の送出を証明処理で遅らせずに済む一方、証明書の発行には別途待ち時間が発生し、計算のやり直しも必要になる。なお、現時点の実装はMoEモデル向けに最適化されており、複数GPUへの証明処理の分散には対応していない。
毎秒110トークンを達成、ただし通常推論の約72倍の計算負荷
研究チームは、4ビット整数化したLlama 4 Maverickを単一のH100 GPUと24 CPUコアで評価した。セキュリティパラメータは128ビット安全性を目標としており、モデル導入時のオフライン処理には約39分を要した。この処理で作成したコミットメントは、レポートによれば約1,600万件のリクエスト検証に再利用できる。
オンライン証明では、各1,024トークンのコンテキストを持つ24件のリクエストを一括処理し、約223秒で証明を生成した。総処理トークン数を所要時間で割ったスループットは毎秒110トークンとなる。
ただし、この数値は毎秒110個の新しい回答トークンを生成・証明できるという意味ではない。1,024トークンの入力文脈全体を含めた処理速度であり、標準的な測定条件で実際に証明しているのは各リクエストの末尾1トークンだけだ。すべてのトークンを証明対象にした場合の検証トークンスループットは、毎秒39.1トークンだった。
| 処理条件 | 測定結果 | 備考 |
|---|---|---|
| 24件のバッチ証明 | 約223秒、110トークン/秒 | 文脈全体の処理速度。証明対象は末尾1トークン |
| 単一リクエストの証明 | 58秒、17.6トークン/秒 | 1,024トークンの文脈を処理 |
| 全トークン検証 | 39.1トークン/秒 | 文脈内の全トークンを証明対象とする |
| CPUによる証明書の検証 | 17秒（24スレッド）、21秒（1スレッド） | GPU不要 |
| 証明書サイズ | 約18.78MB/リクエスト | コミットメント関連データは約6.24MB |
| 通常推論とのGPU時間比較 | 約72倍（66〜77倍） | vLLMによるFP8推論との比較 |
バッチ化によって処理効率は向上したものの、証明書の発行には約223秒を要する。一方、証明書を受け取った検証者は、GPUを使わずCPUだけで17〜21秒で検証を完了できた。計算負荷の大部分を証明書の生成側に集中させ、検証側を軽量にしている。
研究チームは、FP8版のLlama 4 Maverickを8基のH100で動かす推論エンジン「vLLM」とも比較した。単一GPUあたりの処理時間に換算すると、FlashProveの証明生成には通常推論の約72倍（66〜77倍）のGPU時間が必要で、vLLMを最大負荷で動かした場合との差は約94倍に達した。ただし、比較対象は数値形式や実行構成が異なり、倍率を算出するための絶対的なGPU時間も公表資料から確認できないため、単純な同条件比較ではない。
先行研究「VerInf」が同モデルの1,000トークンの証明に約14.3時間を要し、約93.6GBの証明書を生成していたことを考えると、FlashProveは処理時間とデータ量を大幅に削減したことになる。それでも通常推論と比べれば計算負荷は依然として大きい。これらの性能値は研究チーム自身の測定結果であり、独立した第三者による追試も完了していない。
Leanによる形式検証と、実装に残る安全性の課題
FlashProveは暗号プロトコルの正しさを確認するため、定理証明支援系「Lean」を採用している。ランダムオラクルモデルの下で、完全性、健全性、ゼロ知識性という主要な性質を形式的に証明した。ただし、数学的なプロトコルが検証されていることと、実際に動作するソフトウェア全体の安全性が証明されていることは別問題だ。
公開コードには、定理と直接対応するLean製の検証器と、実用的な速度で動作するC++製の検証器が含まれる。両者はテストで同じ判定結果を返しているものの、数学的に完全な同値性が証明されているのはまだ先の課題だ。また、CUDAとC++で実装された高速証明器はAIを利用して生成されたコードを含んでおり、Lean側の仕様と完全に一致する保証はない。
実装上の欠陥は、正しい計算の証明に失敗する原因になるほか、ゼロ知識性が損なわれればモデルの重みなどが漏洩する危険性もある。検証器側が正しければ、不正な証明を受け入れない健全性は維持されるが、証明器の安全性まで保証されるわけではない。さらに、公開時点でLeanによるゼロ知識性の完全な形式証明が完了していたのは個別リクエストの証明に限られ、バッチ証明には未解決の部分が残っている。
形式検証にはほかにも境界がある。Leanで記述した仕様が実際に必要なセキュリティ要件を正確に表しているかは人間による精査が必要であり、実行環境やコンパイラへの信頼も前提となる。また、厳密一致を検証する場合と、誤差を許容する「Clipped-gap acceptance」では保証の範囲が異なる。後者が保証するのは設定された許容値の範囲内であり、任意の計算結果が完全一致すると証明するものではない。
モデルのすり替え防止や第三者監査への応用
FlashProveが実用化されれば、AIサービスの透明性を高める手段になり得る。例えば、仲介事業者が指定されたモデルを安価なモデルに無断で切り替えていないかの確認や、外部の評価機関による独立したモデル評価に利用できる。また、セキュリティスキャンや業務分析が指定モデルで実行されたことの証明、規制当局が認可済みモデルの使用を確認する仕組みへの応用も想定されている。
研究チームは、AI開発の進展を管理する「ペーシング（Pacing）」への活用も提案している。事業者に定期的な推論証明の提出を求めれば、指定モデルの推論が実行されていたことを確認できる。ただし、同じ計算設備でモデルの学習が並行して行われていないことまでは証明できない。
セキュリティ上の限界も明確だ。事後証明は不正な計算や改ざんを後から発見する仕組みであり、誤った回答や悪意ある出力が利用者に届くことをリアルタイムで防ぐものではない。モデルの重みの窃取などを防止するには、セキュアブートや隔離実行環境、監査ログといった従来の対策も引き続き必要となる。
何より、暗号学的に証明できるのは「指定されたモデルが、その計算結果を出したこと」であり、「回答内容が正しいこと」ではない。 事実誤認や有害な内容を含む回答であっても、モデルが正しく計算した結果なら証明は成立する。
実用化に向けては、一般的なAIサービスで使われる浮動小数点演算や確率的サンプリングへの対応が必要になる。今回の整数量子化モデルと実際の浮動小数点推論は、通常のプロンプトでは経験的に近い結果を示すものの、意図的に差を引き起こす敵対的なプロンプトに対して一致は保証されない。検証可能なコンテキスト長が最大1,024トークンに限られることや、証明生成時間から内部情報を推測するサイドチャネル攻撃が対策範囲外であることも課題だ。
FlashProveは、Anthropicの商用AIサービス「Claude」に導入された機能ではなく、Apache 2.0ライセンスで公開された研究プロトタイプである。今回の成果は、数千億パラメータ規模のLLMでも、数分程度の事後バッチ処理によって暗号学的な推論検証が可能になることを示した。ただし、通常推論に対する大きな計算負荷や実装の安全性、実際のAIサービスとの数値的な互換性には課題が残る。今後は、形式検証された理論と高速な実行コードの隔たりを埋め、実運用でどこまで効率よく検証できるかが焦点となる。
