Anthropic、暗号学的なAI推論証明に向けたFlashProveを公開

Anthropicは2026年11月2日、FlashProveを公開した。これは、言語モデルの応答が、秘密を明かすことなく、コミットメントで指定された重みに基づいて生成されたと示す暗号学的証明を利用する、オープンソースの研究用プロトタイプだ。同社によると、MetaのLlama 4 Maverickでは、証明の生成速度は毎秒110トークンだった。

この研究は、ホスト型AIにおける検証の課題に取り組むものだ。回答の品質が高くても、それを生成したモデルは特定できない。ルーティングサービスが別のシステムに差し替えたり、評価者にテスト対象として意図したものとは異なるモデルが提供されたり、攻撃者がトークン列を改ざんしたりする可能性がある。重みが非公開で、必要なハードウェアも相当なものになる場合、ユーザーがモデルを再実行して確認するのは現実的ではない。

非公開の重みに応答を結び付ける

FlashProveは、信頼できるハードウェアに依存せず、ソフトウェアのみで構成する設計で、ゼロ知識簡潔知識証明（zkSNARK）を採用している。オフライン段階では、プロバイダーが、重みを秘密に保ったまま特定の重み一式を一意に識別する短いコミットメントを公開する。完了したプロンプトと応答の各ペアについて、出力トークンがコミットメントで指定されたモデルの出力であることを示す証明を生成する。コミットメント、プロンプト、応答を持つ人は誰でも、重みにアクセスせずに証明を検証できる。

この方式が目指す性質は、完全性、健全性、ゼロ知識性、簡潔性だ。誠実に生成された証明は受理される一方、偽の命題を証明するには、広く信頼されている暗号学的仮定を破る必要があるとされる。証明を検証しても、重みや中間計算値が明らかにならないことが求められる。また、この設計では、モデルのアーキテクチャ自体は公開されたまま、各トークンの生成にどの混合エキスパート・サブネットワークが使われたかを隠す。

この実装は、Maverickの混合エキスパート構造を活用している。証明者の計算量は、全4,000億個ではなく、トークンごとに有効化される約170億個のパラメーターに応じて増減する一方、どのエキスパートが選択されたかは隠される。分割された重みをホストメモリーからストリーミングすることで、約290 GBのホストメモリーと併用し、80 GBのGPU 1基で証明者を動作させられる。

Anthropicは、顧客の完全性確認、独立評価、規制対応ツール、承認済みモデルの要件の徹底などを、想定される用途として挙げている。推論証明書があれば、リクエストに対して申告されたモデルが応答したことを証明できる可能性がある。ただし、同じハードウェアが別のモデルの学習にも使われていなかったことまでは証明できない。この違いにより、計算資源の利用方法に基づくコンプライアンス要件について、こうした証明書が示せる範囲には限界がある。

証明の性能と推論への負荷

Anthropicの評価では、一般公開されているモデルの4ビット変換版を使用した。H100を1基、CPUコアを24基搭載したサーバーで、24件のリクエストからなるバッチを約223秒で証明し、各リクエストについて18.78 MBの証明を生成した。オフラインのコミットメント生成には約39分かかった。

検証側では、クライアントが約6.5 MBのコミットメントをダウンロードし、GPUを使わずにCPUで証明を検証する。Anthropicの測定では、オフライン段階の検証も含め、24スレッドで17秒、1スレッドで21秒かかった。

これらの測定値は、CPUのみで行う検証と、はるかに負荷の大きい証明生成を区別して示している。vLLMを実行するH100 8基でのFP8推論と比較すると、Anthropicによれば、同じバッチの処理に必要なGPUあたりの時間は、証明生成のほうが約72倍だった。また、テストしたvLLMの最大負荷時には約94倍に達した。したがって、このスループットには、証明なしでモデルを提供する場合に比べて相当なコストが伴う。

形式検証と実用上の限界

FlashProveのリポジトリには、証明者、高速なC++検証器、より低速なLean検証器、最上位の数学的命題に関するLeanによる証明、対話型定理ビジュアライザーが含まれており、Apache 2.0ライセンスで公開されている。バージョン0.16.0については、メンテナンスされておらず、コントリビューションも受け付けていない研究成果物と記されている。

Leanによる検証作業では、ランダムオラクルモデルにおける完全性、健全性、ゼロ知識性を扱っている。ただし、形式化された命題が意図した保証を実際に表現しているかを確認するには、依然として人手によるレビューが必要だ。Lean検証器は健全性定理と形式的に結び付けられているが、日常的な利用を想定したC++検証器には形式的な保証がなく、代わりにLean検証器との一致がテストされている。

プロジェクトの既知の制限に関する文書によると、人間の指示のもとで動作するAIシステムが、ソフトウェア、Leanによる証明、文書のほぼすべてを作成し、報告されたテストも実行した。独立したセキュリティ監査は行われておらず、重みの秘匿性や敵対的な証明に関するテストも限られている。

証明の対象となるのは、貪欲デコードのもとでの重みの厳密な整数版だ。浮動小数点推論やサンプリングデコードでは、証明対象の計算から外れる場合があり、一般的なエラーテストでは、敵対的に設計されたプロンプトを網羅していない。コンテキストは1,024トークンに制限され、タイミング攻撃などのサイドチャネル攻撃も保証の対象外だ。また、推論と並行して証明を生成する場合と比べ、事後的な証明では再計算が必要になり、保証が遅れ、非決定性も生じる。

証明可能な推論を、実際に提供されるトラフィックに対する日常的なチェックとして定着させるには、このリリースで明らかになった課題に取り組む必要がある。具体的には、証明コストの削減、より制約の少ないデコード方式とより長いコンテキストへの対応、そして高速な実装と形式的なプロトコルとの結び付きをさらに強めることだ。