LLMの応答は本物だと証明できるか：FlashProveの保証と限界

出力だけではモデルを特定できない

APIから高品質な文章が返ってきても、利用者は、その文章が契約したモデルから出たのかを出力だけでは確かめられない。第三者のルーターが安価なモデルへ切り替えた可能性や、侵害された推論サーバーがtoken列を差し替えた可能性を、文章の自然さだけで除外することは難しい。

モデルの重みを公開し、利用者が同じ計算を再実行すれば確認できる。しかし、非公開モデルでは重みを渡せず、400B級モデルを各利用者が動かすのも現実的ではない。FlashProveは、提供者が重みを明かさず、利用者も推論をやり直さずに、所定の計算が行われたことを検証する試みである。

使うのはzkSNARKと呼ばれる暗号学的な証明である。証明が正しければ、利用者は「公開された短い指紋に結び付いた重みが、この入力に対して、このtokenを出した」という主張を確認できる。重みや中間計算は隠したまま、誤った計算の証明を作ることは計算上困難だという性質を利用する。

ここでいう証明は、回答内容の保証ではない。モデルが誤情報を生成していても、その誤情報が確かに当該モデルの計算結果なら証明は通る。モデル同一性と計算完全性を確かめる層として位置付ける必要がある。

Commit・Prove・Verifyの流れ

最初のCommitでは、提供者がモデル重みから短いcommitment IDを作り、公開する。このIDは一組の重みに結び付き、重みそのものは隠す。利用者は検証したいモデルのIDを、推論サーバーとは別の信頼できる経路から取得しなければならない。サーバーが送ったIDをそのまま信用すると、差し替え検知の出発点を失う。

Proveでは、提供者が入力、出力token、確定済みの重みに対する計算記録から証明を作る。FlashProveはMixture-of-Expertsの疎な構造を利用し、400B全体ではなく、tokenごとに実際に使う約17Bの重みに比例する作業へ抑える。どの専門家を選んだかも証明の外からは見えない。

Verifyでは、利用者がcommitment、入力、出力token、証明ファイルをCPUで検査する。検証器は重みを持たず、モデルを再実行しない。証明が受理されれば、commitmentに対応する整数モデルが、その入力から指定tokenを計算したという主張に暗号学的な裏付けが付く。

FlashProveは推論と同時に証明する方式ではなく、完了したtokenを後からまとめて証明するpost-hoc方式である。バッチ化で効率を上げられる反面、応答を受け取った時点では保証がまだ届いていない。即時ブロックが必要な制御と、後日の監査に使う証跡では、求める設計が異なる。

110 token/sの測定条件

評価対象はLlama 4 Maverickで、総パラメータ400B、tokenごとに約17Bを使うMoEである。重みは公開された4-bit量子化版を使い、各要求は1,024 tokenの窓、各証明は1 tokenを検査する。証明側はH100 1枚とCPU 24コア、利用者側はCPUで測った。

110 token/sは会話の逐次生成速度ではない。完成済みの24要求をprefillのように並列処理し、1 tokenずつ証明したときの合計処理量である。証明ファイルも「1,024 tokenの回答全体で18.78 MB」ではなく、1 tokenを検査する単位で示されている。長い回答の全tokenを覆えば、証明量と検証作業は増える。

通常推論との比較では、同じモデルのFP8版をvLLMで8枚のH100に載せた。GPUあたりに換算した証明処理は、24要求を同時処理するvLLMより約72倍遅く、測定範囲は66〜77倍だった。vLLMの最大負荷時との比較では約94倍である。量子化方式、GPU数、post-hoc処理が異なるため、利用者が感じる応答遅延の倍率として読んではいけない。

実装は1枚の80 GB H100へ収めるため、約232 GBの量子化重みをレイヤー単位で分割し、約290 GBのホストメモリから順に転送する。リポジトリの実機手順はH100、CUDA 13.2、330 GB RAM、245 GBディスクを要求する。オープンソースであっても、個人が気軽に再現できる規模ではない。

証明が覆う範囲と覆わない範囲

証明対象は、公開設定に従う整数版モデルとgreedy decodingである。各位置では、モデルが最も高く評価したtokenと、提示されたtokenが一致することを検査する。浮動小数点の通常推論や確率的なsamplingでは、丸めや乱数によって途中のtokenが変わり、その後の列も一致しなくなる。

整数版が浮動小数点版へ概ね近いことは経験的に確認したとされるが、敵対的に作ったpromptまで同じとは保証されない。また、モデルのアーキテクチャは公開され、隠れるのは重みと中間値である。MoEの専門家選択は隠す一方、モデルがMoEであること自体は隠さない。

1,024 tokenという上限も実用上は大きい。長いチャット履歴、検索結果、ツール実行ログを含むエージェントでは、どの範囲を証明対象にしたかを明示しなければならない。文脈の一部を落とした証明が正しくても、利用者が見た会話全体を検証したことにはならない。

証明生成時間の差から重みの情報が漏れるside channelも対象外である。暗号学的なzero-knowledgeは証明ファイルの内容に対する保証であり、サーバーの応答時間、電力、アクセスパターンまで隠すわけではない。

Lean形式化にも残る信頼の隙間

FlashProveは、完全性、健全性、zero-knowledgeという上位の性質をLeanで記述する。特に健全性は、Lean製の検証器が誤った主張を受理する確率を、hash query数をqとして概ねq/2^124 + 2^-101以下とする形で機械検査されている。ただし、この数値はrandom oracle modelとexact-match条件における確率上限であり、実際の失敗率を測った統計ではない。

日常利用向けの高速C++検証器とCUDA証明器そのものが、Leanの定理で証明されているわけではない。両者はLeanのプロトコルに合わせて実装され、テストで一致を確認した段階である。Lean検証器は形式保証を持つが遅い。高速実装が仕様と同じであることを監査する作業が残る。

形式化した定理が、人が意図した安全性を正しく表しているかも別問題である。証明支援系は、書かれた定義から定理が導けることを検査する。定義そのものが利用者の期待とずれていれば、機械検査が通っても運用上の保証はずれる。Anthropicは上位statementのvisualizerを用意し、人が定義を監査する必要を明記している。

zero-knowledgeについては、Lean上の理想的なproverに対する証明であり、公開CUDA proverが重みを漏らさないことはテストと監査へ依存する。実装ガイドは、重み秘匿について攻撃探索が少なく、公開プログラムの漏えいを探す試験もないと注意する。形式証明の存在だけを見て、本番の秘密重みを直ちに預けるべきではない。

導入を考えるための判断軸

FlashProveが特に適するのは、後日の監査で「承認済みの重みが使われた」と確認したい場面である。第三者ルーター、独立評価、規制報告、重要な推論ログの抜き取り検査では、post-hocでも価値がある。一方、各tokenを即時に止める安全ゲートや、回答内容の正しさを判定する用途には、それだけでは足りない。

利用者側の最初の課題はcommitment IDの配布である。証明と同じサーバーからIDを受け取ると、攻撃者が重みとIDを同時に差し替えられる。モデル版、量子化方式、公開設定、ID、有効期間を署名付きの別経路で管理し、どの版を承認したかを記録する必要がある。

公開リポジトリはVersion 0.16.0の研究成果で、「not maintained」「not accepting contributions」と明記される。Apache 2.0で読めることと、継続的に脆弱性修正される製品であることは同じではない。本番採用には独立監査、保守主体、更新手順、失効したcommitmentの扱いが必要である。

今回の成果は、400B級MoEでも暗号学的な推論証明が実行可能な速度へ近づいたことを示す。一方で、通常推論の約70〜95倍のGPU時間、短い文脈、整数・greedy条件、実装と形式仕様の隔たりが残る。現段階では「すべてのAI応答へ署名を付けられる完成技術」ではなく、監査用途を絞って評価すべき公開プロトタイプである。

この記事の限界

• GGWSはFlashProveをH100で再現しておらず、性能値は公開報告の条件を分解して整理したものです
• 技術報告は研究チームによる公開資料で、独立した査読や第三者再現を確認していません
• 暗号プロトコルの数式証明を独自監査しておらず、上位statementと公開された限界を基準にしています
• 通常推論との比較は量子化、GPU数、バッチ条件が異なり、製品の待ち時間や費用を直接示しません
• リポジトリは公開時点で保守対象外とされ、将来の脆弱性対応や互換性は保証されません