11月4日、Help Net Securityが「Anthropic open-sources FlashProve, its provable inference prototype for MoE models」と題した記事を公開した。この記事では、Anthropicが暗号学的証明によってLLMの推論結果の同一性を検証するOSSプロトタイプ「FlashProve」を公開したことが詳しく紹介されている。
「本当にそのモデルが答えたのか」を証明する
ホストされたAPIにプロンプトを送る際、ユーザーは実際にどのモデルが応答したかを確認する手段を持っていない。プロバイダがコスト削減のために安価な別モデルにリクエストをルーティングしても、推論サーバーへのアクセス権を持つ何者かがトークンストリームを改ざんしても、返ってくる回答は「それらしい回答」として見える。外部の評価者も同じ問題に直面する——自分がテストしたモデルが、実際に本番でサービスされているモデルと同じかどうかを確かめる方法がない。
FlashProveはその問題に対するアプローチだ。Anthropicと、EPFL・MIT・StarkWareの研究者が共同で開発した本プロトタイプは、「特定の言語モデルが特定の返答を生成した」ことを示す暗号学的証明（cryptographic proof）を生成する。ゼロ知識証明（ZKP）を活用し、モデルの重みそのものを開示せずに同一性を証明できる点が技術的な核心だ。
リポジトリはApache 2.0ライセンスでGitHubに公開されている。
リポジトリの中身
リポジトリには3つの実行可能ファイルが含まれる。
- プルーバー（Prover）：証明を生成する
- C++製の高速ベリファイアー（Verifier）：日常的な検証用途向け
- Lean製のリファレンスベリファイアー：プロトコルの完全性（completeness）・健全性（soundness）・ゼロ知識性（zero-knowledge）をフォーマルに証明するために使用
Leanは定理証明支援系と呼ばれるツールで、数学的命題をコードとして記述・検証できる。Leanベースのベリファイアーは動作は遅いが、「健全性定理が対象とする文のみを受理する」ことを形式的に保証する役割を担う。すべてのテストケースでC++ベリファイアーと一致したことが確認されている。
ただし、Anthropicは3つのレイヤー（論文・Leanプロトコル・実際のコード）が必ずしも一致しているとは保証しないと明言している。Leanの記述との整合性は人手での確認が必要であり、リポジトリにはそのためのインタラクティブなビジュアライザーが同梱されている。プルーバー自体にはフォーマルな検証ツールがないため、従来通りのコード監査が必要になる。
動作モデルと必要なハードウェア
FlashProveはLlama 4 Maverick（Metaの4000億パラメータのMixture-of-Expertsモデル）でテストされている。重みはHugging FaceからMetaのライセンスに従って自分でダウンロードする必要があり、リリースには含まれていない。
MoE（Mixture-of-Experts）モデルはトークンごとに一部のエキスパート（部分ネットワーク）しかアクティベートしない構造を持つ。FlashProveはこの特性を活かし、1トークンあたり約170億パラメータのみを処理し、重みをレイヤー単位でストリーミングする。これにより、80GBのGPU 1枚＋約290GBのホストメモリという構成で動作する。
実測値
H100 1枚＋CPUコア24基の環境での実測値は以下の通りだ。
| 項目 | 値 |
|---|---|
| 生成速度 | 約110トークン/秒 |
| 1,024トークンリクエストの証明サイズ | 約18.78 MB |
| 証明の検証時間（24スレッド） | 約17秒 |
| 証明の検証時間（シングルスレッド） | 約21秒 |
| 重みのコミットメント生成（オフライン・1回のみ） | 約39分 |
| 1コミットメントがカバーするリクエスト数 | 約1600万件 |
| クライアントのダウンロード量 | コミットメント6.5 MB＋リクエストごとに証明1件 |
ベースラインとの比較として、同じモデルをFP8でH100 8枚上で動かしたvLLMと比較した場合、GPUあたり約72倍のオーバーヘッド（最高負荷時は約94倍）が生じる。現時点でプロダクション用途には遠い数字だが、プロトタイプとしての位置づけであり、改善の余地を探るための数値として公開されている。
技術的な意義
LLMが社会インフラとして普及するにつれ、「サービスされているモデルの同一性をどう検証するか」は監査・コンプライアンス・セキュリティの観点から重要度が増している。
この問いへの暗号学的アプローチとしては、機械学習モデルへのゼロ知識証明適用を扱うzkML（zero-knowledge machine learning）と呼ばれる研究領域が先行して存在する。zkMLは主に小規模モデルの推論結果を証明対象としており、大規模LLMへの適用はスケール上の課題から研究段階にとどまっていた。FlashProveはMoEアーキテクチャの「トークンごとにアクティベートされるパラメータが限定される」という特性を利用することで、400億パラメータ級モデルへの適用を現実的なハードウェア構成で実現した点で、先行研究との差別化が図られている。
ゼロ知識証明とフォーマル検証（Lean）を組み合わせた設計は、今後のprovable inference研究の参照実装として機能する可能性がある。オーバーヘッドの大きさは課題として残るが、コミットメントが約1600万リクエストをカバーするという構造は、実用化に向けたコスト分散の方向性を示唆している。
詳細はAnthropic open-sources FlashProve, its provable inference prototype for MoE modelsを参照していただきたい。
