Anthropicは、AIモデルの回答が約束されたモデルから出たかを確認するオープンソースのプロトタイプFlashProveを2026年11月2日に公開した。研究記事、技術報告書、実行コード、セキュリティ特性をまとめたLean証明も併せて公開した。サービス事業者は、モデルが学習した数値である重みを公開せずに推論計算を証明でき、利用者や監査者はGPUや重みなしでCPUで確認できる。
1. 応答が約束されたモデルから出たかを確認する
AIサービスでは、回答内容だけで実際にどのモデルが答えたかを知るのは難しい。要求をモデルに送る仲介サービスが費用削減のために小型モデルへ切り替えたり、サーバーへの侵入者が出力トークンを操作したりしても、利用者が気づきにくい問題を対象とする。
提供者はまず、モデルの重みの短い指紋であるコミットメント、つまり元の情報を隠したまま固定する暗号学的な値を作る。その後、入力と回答トークンに対する証明ファイルを生成し、利用者はそのファイルとコミットメントで回答がその重みから出たかを確認する。証明は、重みや推論の中間値、計算中に生じる一時的な値を明かさないよう設計された。
2. バッチ処理で大規模モデルの証明を試みた
AnthropicはLlama 4 Maverickの公開4ビット重みを整数モデルに変換して測定した。このモデルは全4,000億パラメータのうちトークンごとに約170億を使い、複数の計算担当の一部だけを選んで動かす混合エキスパート構造だ。研究記事によると、証明の作業量も全4,000億ではなく実際に使った約170億パラメータに比例するため、この構造が大規模モデルの証明負担を減らす。
Anthropicの技術報告書第6節にある単件と24件バッチの証明結果は次のとおりだ。処理量は、検証した出力トークンだけでなく要求全体のトークンを数える事前処理、つまり入力トークンを先に計算する段階を基準とする。
表：単件と24件バッチの証明生成結果
条件：Llama 4 Maverickの公開4ビット重みによる整数モデル、H100 80GB 1枚とCPU 24コア、要求ごとに1,024トークン、次の1トークンを検証、セキュリティ目標128ビット、同社発表に基づく
単位：所要時間は秒、処理量は要求全体を基準とするトークン/秒、要求ごとの証明サイズはMB
| バッチサイズ（要求数） | バッチ所要時間（秒） | 処理量（トークン/秒） | 要求ごとの証明サイズ（MB） |
|---|---|---|---|
| 1件 | 58 | 17.6 | — |
| 24件 | 223 | 110 | 18.78 |
チャート：バッチサイズ別の証明処理量 条件：上表と同じ整数モデルの測定、要求全体のトークン基準 単位：トークン/秒
単件 ███▌ 17.6
24件バッチ ██████████████████████ 110この数値は、長い入力を再計算する証明処理の速度を示す。技術報告書第6節は、回答の各トークンを検証する別の試験でも速度差は測定されず、検証したトークンだけを数えると毎秒39.1トークンだったと述べた。
研究記事によると、証明の確認にはCPU 24スレッドで17秒、単一スレッドで21秒かかった。
重みのコミットメントはモデルごとに一度生成し、約39分かかり、約1,600万要求に再利用できると、同社は研究記事で述べた。
比較対象のvLLMは、同じモデルのFP8版、つまり8ビット浮動小数点形式版をH100 8枚で実行した。研究記事によると、GPU 1枚換算のFlashProveの24件バッチ証明は、同じサイズのvLLMの事前処理より約72倍長くかかり、実行ごとの差は66~77倍だった。vLLMが試験した最大負荷を基準にすると約94倍だった。
3. 推論後に証明し、リアルタイムの負担を分離する
FlashProveは応答を先に届け、別のサーバーで記録済みの入力と出力から推論を再計算して証明する事後処理、つまり応答後に別途実行する方式だ。トークン生成のたびに証明する代わりに複数の要求をまとめ、GPU作業を並列化して複数の計算を同時に行う。モデルの層を区間に分け、GPUには一度に一部の計算だけを載せ、重みはホストメモリ、つまりCPUが使う主記憶装置から読み込む。
この方式には、証明生成が推論サービスの即時応答経路を妨げない利点がある。一方、同社発表では、証明作業自体は通常の推論の約70~95倍のGPU時間を使い、再計算を含めると証明作業量が約1~1.5%増えると技術報告書の付録は推定する。技術報告書第6節によると、個々の要求はバッチ証明完了まで約5分待つ場合があり、1件ずつ処理すると証明は58秒で準備できるが、処理量は毎秒17.6トークンに下がる。
4. プロトタイプの検証範囲と利用方法
研究記事によると、セキュリティ特性は数学的命題を機械で確認するツールLean 4で形式化され、数学的定義を論理式で表現した。リポジトリには高速なC++検証器と、低速だが形式的な保証を備えるLean検証器がある。
技術報告書第7節によると、高速な実行コードがLeanの定義と同じ動作をすることと、バッチ証明が重みの情報を隠すことは、まだ形式的に証明されていない。研究記事が示す検証対象は、最大1,024トークンの文脈で整数モデルが最高スコアのトークンを選ぶ計算であり、浮動小数点計算や確率に従ってトークンを選ぶ回答は、この結果と異なる場合がある。
開発者はリポジトリの案内に従って検証器をビルドし、試験用の合成重みを使う小型モデルの保存済み証明で動作を確認できる。以下はそのコマンド例であり、実際の証明確認に使うコミットメントIDは、利用者が信頼する経路から入手する必要がある。
bin/cp_verify examples/accepted-proof/config examples/accepted-proof/ivk examples/accepted-proof/example.req examples/accepted-proof/example.y examples/accepted-proof/example.proof -id "$(cat examples/accepted-proof/ID.txt)"FlashProveは、モデルの重みを公開しない推論検証の可能性を大規模モデルで示した研究用プロトタイプであり、計算コストと検証範囲が実用化の鍵となる。