Anthropicのフロンティア・レッドチームは、EPFL、MIT、StarkWareの協力者とともに、「FlashProve」を開発しました。これは、特定の言語モデルが特定の応答を生成したことを暗号学的に証明するプロトタイプです。証明器（prover）、2種類の検証器（verifier）、それらを裏付ける形式証明、そしてプロトコル仕様は、Apache 2.0ライセンスの下でGitHubに公開されています。
出典：Anthropic
ホスト型APIにプロンプトを送っても、どのモデルが応答したのかを確認する手段はありません。プロバイダーがリクエストをより安価なモデルに振り分けたり、推論サーバーにアクセスできる人物がトークンストリームを改ざんしたりしても、応答は一見まともなものに読めてしまいます。外部の評価者も同じ問題に、逆の立場で直面します。テストしたモデルが実際に提供されているモデルと同一かどうかを確かめる方法がないのです。FlashProveは、検証者がこれを確かめるための手段を提供します。
リポジトリの内容
リポジトリには、3つの実行ファイルが含まれています。証明器、C++で書かれた高速な検証器、そしてLeanで書かれたもう1つの検証器です。Leanは証明支援系であり、チームはこれを使って、プロトコルの完全性（completeness）、健全性（soundness）、ゼロ知識性（zero-knowledge）を記述し、証明しました。
Lean版の検証器は動作が遅いものの、それで問題ありません。役割はリファレンスだからです。Leanによって、この検証器が受理するのは健全性定理の対象となる命題だけであることが確立されており、すべてのテスト用証明でC++版の検証器と結果が一致しました。日常的な利用にはC++版を使います。
Anthropicは、各要素が完全には整合していない可能性があると述べています。このシステムには、論文、Leanのプロトコル、実際に動作するコードという3つのバージョンが存在し、3つがすべて同じ内容を示しているとは保証できないとしています。確認するには、Leanの記述を人手で読み通す必要があり、リポジトリにはその助けとなるインタラクティブなビジュアライザーが付属しています。証明器には形式的な裏付けとなるツールがないため、この部分は従来どおりの監査で確認することになります。
モデルの重みはリリースに含まれていません。FlashProveは、4000億パラメータのMixture-of-Experts（MoE）モデルであるLlama 4 Maverickで検証されました。重みはMetaのライセンスに従い、Hugging Faceから各自で取得します。証明器の実行には、80GBのGPU 1基と約290GBのホストメモリがあれば足ります。証明器が扱うのはトークンごとに有効となる約170億パラメータだけで、重みはレイヤー単位のセグメントに分けてストリーミングされます。
性能の数値
24基のCPUコアを備えたH100 1基の環境では、証明器は毎秒約110トークンを処理します。1,024トークンのリクエストに対する証明のサイズは約18.78MBで、その検証には、24個のCPUスレッドで約17秒、シングルスレッドで約21秒かかります。証明器が重みにコミットするオフラインの工程は、モデルごとに1回、約39分かかり、その後は約1,600万件のリクエストをカバーします。クライアントがダウンロードするのは、6.5MBのコミットメントと、リクエストごとの証明1つです。H100を8基使い、同じモデルをFP8でvLLMにより動かした場合と比較すると、オーバーヘッドはGPUあたり、複数回の実行を通じて約72倍、テストした最大負荷時には約94倍でした。
翻訳元: https://www.helpnetsecurity.com/2026/11/04/anthropic-flashprove-provable-inference/
