Tech Teardown 041｜FlashProve：AI推論にZK証明、コードはClaude、保証はLean

背景と現象：選んだモデルが実際に返信しているか確認できない

2026年11月4日、Anthropicは研究ブログ「Progress on provable inference for large language models」を公開し、FlashProveというシステムを発表した。同時に、ブログ本体、技術レポート、プロトコル仕様、実行可能なコード（証明器1つと検証器2つ）、Lean証明、および定理インタラクティブビジュアライゼーションツールの5つのファイルをオープンソース化した。コード、証明、ドキュメントはすべてApache 2.0ライセンスで提供される。それに伴うリポジトリanthropics/FlashProveは2026年10月30日に作成され、11月5日時点で781★の評価を受けており、バージョンファイルには0.16.0と記載されている。ブログのHNエントリーは155▲、コメントは77件。

ブログで提起された問題は非常に直接的である：ユーザーがモデルにリクエストを送信する際、実際に選んだモデルが返信しているかを確認する方法がない。ルーティングサービスはコスト削減のために安価なモデルに切り替える可能性があり、攻撃者はトークンフローを改ざんする可能性がある。出力の品質から推測すると信頼性が低く、どんなに美しい回答でも自分の出自を証明することはできない。独立した評価機関は、オンラインで動作するモデルを評価している必要があり、第三者のルーティングを利用するユーザーは、トークンが実際に自分が支払った料金で購入したものであることを確認する必要がある。

2つ目の分解ポイントは、著者陣とClaudeの役割である。ブログの署名には、学界と暗号学の起業家コミュニティからの人々が混在している：Anthropicの2人、EPFLの3人、さらにMIT、StarkWare、Succinct、RESI出身の研究者も含まれている。さらに目を引くのはブログの自己紹介である：「Claudeは推論用のzkSNARKを改善し、既存のオープンソースシステムよりもはるかに高速なシステムを構築した」と述べている。5つのファイルの中で、プロトコル仕様のドキュメントにはClaudeが書いたと明確に記載されている。Anthropicは同時に、このような書き方のリスクと対策についても説明している：Claudeは最適化に長けているが、大規模で複雑なシステム内での意思決定はしばしば評価が困難であるため、対策として、安全保証をLean（形式化検証言語）で監査可能なトップレベルの命題として記述することを提案している。

READMEの最初の行には自己位置づけが記されている：「研究ファイル：メンテナンスせず、コントリビューションを受け付けない」。ブログでは、これが進行中の研究であり、完成した研究プログラムではないことも明言しており、公開の目的は他者に改善を提供することである。

アーキテクチャと技術原理：commit、prove、verifyの3ステップ

FlashProveの核心はzkSNARK式の証明可能な推論であり、メカニズムは3ステップで構成されている（READMEの文言による）。第1ステップcommit：サービスプロバイダーはコミットIDを発行し、一連の重みを結びつける。重み自体は秘密にされ、すべての依存する重みの公開値はマスクされており、docs/what-is-not-hidden.mdで宣言されているリストを除いている。設計目標は明確に記されている。重みを隠すことが目的であり、アーキテクチャを隠すことは目的ではない。第2ステップprove：各返信はサービスプロバイダーのGPUによって証明される。第3ステップverify：誰でもC++の検証器cp_verifyを使用して、通常のCPUで数秒で「この返信が実際にコミットされたモデルから来たものである」ことを確認できる。このプロセスでは重みは必要とされない。

Lean部分はコレクションのもう一方の重点です。ローカルクローンには合計30,902ファイルがあり、そのうち.leanファイルが29,563件、.pyファイルは185件で、総サイズは723MBです。ディレクトリにはprover、verifier、lean、paper（技術報告のPDF）、docs（19件）、guide（8件）、tests、toy、scalesなどが含まれています。lean/THEOREM.mdには6つの定理が記載されており、すべて同じコミッター/prover/verifierに対して適用されます。各公開セットにおいて成立します：sound（不正行為者がq回のハッシュ検索で検証者を欺く確率は約q/2^124 + 2^-101以下、原稿には「これは境界であり、安全度ではない」と注記されています）；soundAndBinding（誰も約束された重みを別のセットに変えることはできず、確率は約q/2^124 + 2^-100です）；completeOnCanServe（サービス要求に対する誠実な証明が誤って拒否される確率は2^-40以下です）；zeroKnowledgeOnCanServe（2^64回のハッシュ検索と688,127件の返信の中で境界を漏らすことは2^-154以下であり、シミュレーターは重みを得ることができません）；refusedHandsOutNoProof（拒否された要求には空の証明しか返されませんが、「正しく拒否されるかどうか」は証明の範囲外です）；repliesFit（688,127件の返信と表列数の一致度のカウント）。

2つの境界は特筆に値します。それぞれ、コレクションの自己宣言です。一つ目は、6つの定理は「正確なマッチング」を要求しており、検証者はこの点を検出しません：サービス提供者が要求を見た後に公開ファイルの戦略を変更した場合、定理は適用されません。二つ目は、テストセットはすべて合成重みを使用しています。SUITE.mdの原文には「通過したテストはプログラムが合成入力に対して期待される答えを提供していることを示すだけであり、信頼性や隠蔽性については何も説明できない」と記されています。

重要データ：110 tok/s、93倍のコストと6つの確率境界

性能数値はすべてコレクションのguide/performance.mdおよびREADMEから得られており、公式の自己報告です。独立した再現はまだありません。

実行対象：Llama 4 Maverickフルサイズ（400BパラメータMoE）、第三者が公開した4ビット変換を使用して（ダウンロード量232GB）、1,024-tokenのコンテキストウィンドウ、1枚のH100は80GBです。速度：prefillのバッチでは24時間で111.23±0.92 tokens/s、READMEでは約110；1バッチでは17.41；64バッチでは123.31に達しますが、コレクション自体は80GBのハードドライブでは64バッチは信頼性がないと評価しており、メモリは80,629/81,559 MiBまで使用され、合成重みの下での8回の試行でCUDA呼び出しはすべて失敗しました。

コストも同様にコレクションの自己宣言です：各GPUあたり、vLLMのネイティブprefillより93.0倍遅い（最高負荷時）、vLLMの24バッチより71.4倍遅いです。また、これは「計算された最適な状況」であり、起動時間や約束時間を含まず、ベースラインマシンでは依然として8×H100でFP8を実行しています。

証明と保存容量：単一の証明は平均で18.78MB；クライアント側での各コミットは一度に6.24MBをダウンロード；サービスプロバイダーは各コミットで2.15GBを保存する必要がある。コミットには約39分かかり、一度のコミットを複数回使用できる；サービスプロバイダーのホストメモリは330GB以上、ディスクは245GB以上必要である。検証コストはシステム全体の中で最も非対称な数字であり、cp_verifyは単一スレッドで約21秒、メモリは最大3.53GB、GPUは不要である；Lean版の「可証正確検証器」は全サイズの証明を約24分かかり、メモリは最大14.13GBである。

ワークスペースは自身の弱点をかなり正直に説明している：起動には68〜79秒かかる；前1,000回のリクエストにコミットコストを分散させた後の安定速度は88.81 tok/sで、設定した100 tok/sの目標には達していない。performance.mdでは直接、基準に達していないと認めている。

影響と意義：「どのモデルが言っているか」を検証可能な属性に変える

第一に、コンプライアンスと監査のシナリオ。ブログではzkSNARKがAIのコンプライアンス要件を検証するツールとして利用できると明確に述べられている：規制当局はサービスプロバイダーに特定の期間の推論リクエストをカバーする証明書を提供するよう要求しており、サービスプロバイダーはハードウェアが実際に公称のモデルを実行している場合を除き、偽造することはできない。同時に、規制当局は権利情報を得ることができない。HNの高評価コメントも同じ意味である：コンプライアンス監査、エージェントチェーン、規制シナリオにおいて、「どのモデルが言っているか」自体が重要な属性である。

第二に、集約ルーティングの信頼問題。あるコメントではOpenRouterのような集約器がリクエストを他のモデルにルーティングすることが指摘されており、このメカニズムは有効である。別のコメントでは、より具体的な詐欺シナリオが挙げられている。一部の市場でClaudeの転売業者がアクセスを提供すると約束しながら、実際にはモデルを偽装している。これは推論防止の対象となる。また、一部のホスト上で同名のモデルが明らかに性能が悪いとされること、未公開の量化版が実行されているという噂がある（コメント者はそれを噂だと認めている）。このメカニズムがこれを捕捉できるかどうかが問われている。

第三に、オープンソースの重みモデルも同様に自己証明が可能である。ワークスペースのドキュメントを読んだ高評価コメントによると、公開された重みを使用してコミットを行い、シードを公開することで、誰でもHugging Faceのファイルからコミットを再計算し、サービスプロバイダーが公称のチェックポイントや量化ビットワイドを実行しているかを確認できる。つまり、このメカニズムは閉源製品だけでなく、コミュニティに自己検査ツールを提供するものである。

第四に、Claudeが暗号学のコードを書き、Leanがそれを補うという方法論的意義は、システム自体よりも大きい可能性がある。 「評価が困難なAIの決定」を形式化言語で検証可能なトップレベルの命題に変えることで、機械が人間が書いたコードをチェックすることを可能にする。これはAIが重要なインフラ開発に参加する際の再利用可能なエンジニアリングパラダイムである（これが私の判断である）。

議論とリスク：PR行動か、それとも空虚な空白を埋めることか

HNのコメントセクションで最も大きな声を上げたのは皮肉であった。最高評価コメントはこれがPR行動であるとし、以前の報道を引用して、同じ会社がML関連のリクエストを弱いモデルに静的ルーティングすることがニュースになったことを指摘した（コメント者は指摘しているが、独立した確認はされていない）。しかし、同じく高評価のコメントでは反論されている：モデルが偽装されることは、ユーザーが最もよく抱える不満であり、以前には何の検証メカニズムも存在しなかった。このメカニズムが成功すれば、その意義は非常に大きい。

価値の議論はさらに深くなる。ある人々は、それが証明する属性が「最低限の要件」だと考えている：ただし、安価なモデルに置き換えられていないこと、仲介者を通じていないことを示すだけで、それ以外にはあまり有用な情報を提供していないと言う。また、ある人々はまず「出力が正しい」ことを証明するつもりだったが、実際には「どのモデルが使用されているか」のみを証明していることに気づき、もし本来からサービスプロバイダを信頼していなければ、ゲームはとっくに終わっていたと述べている。反対側の意見では、顧客は出力が正しいことを気にかけ、メーカーは自社のモデルから出力されることを気にかける。この解決策は後者に関するものだ。また、あるコメントでは、最終的にそれが安価なルーティングに対するFUD（これはコメント者の推測による動機）として使用されると予測している。私の見解では、実際には両者は衝突していない。「出力が正しい」と「宣言されたモデルから出力される」は二つの独立した検証問題であり、前者はまだ解決されておらず、後者には現在、暗号学のみが実行可能な方法がある（これが私の判断）。

技術的リスクには三つの明確な境界がある。一つ目は、正確なマッチングの問題：六つの定理はすべて、公開されたファイルが約束された内容と正確に一致することを要求しているが、検証者が検査しないため、サービスプロバイダがリクエストを見て戦略を変更すると、保証範囲外になる。これは倉庫自身が指摘した既知の欠陥である。二つ目は、デプロイメントのハードル：GPUスタックにはx86-64 Linux 4.14+、SHA拡張機能を持つCPU、H100 80GBの独占使用、CUDA 13.2 Update 2（更新されたツールキットは明確にサポートされていない）が必要であり、真のモデルを使用する場合は330GBのメモリと245GBのディスクが必要で、個人や小規模なチームにはほぼ手に入らない。三つ目は、すべての性能数値は公式からの報告であり、第三者による再現はない。93倍の速度低下は、短期間では監査ツールのように見え、常に動作する生産特性ではないことを意味している。

結論と展望：倉庫自体が第二の実験である

核心の一言：FlashProveはzkSNARKを使用して、「この回答が約束された重みから来ている」という事実を、普通のCPUで数十秒で検証可能な命題に変える。その代償は、70-95倍のGPU時間と330GBのメモリレベルのデプロイメントハードルである。同時に、29,563個のLeanファイルを使用して、「Claudeが書いた暗号コードが信頼できるか」という問題を六つの監査可能な定理に変換している。

特筆すべき現象がある：READMEには「Agentによって実行されるように構築された」というセクションがあり、著者は読者が自分のCoding Agentをこの倉庫に向けることを前提としており、直接貼り付け可能なコマンドテキストを提供している。また、検証ルートをハードウェアに応じて四つに分けて説明している：ルート1はLinuxとg++13、2GBのメモリがあれば1-2分で構築でき、2秒で既存の証明を検証できる。ルート2はCPU上でおもちゃの証明を約1分間実行する。ルート3の八層の合成小モデルにはH100の完全スタックが必要で、約29分かかる。ルート4が本物のLlama 4 Maverickであり、時間は数時間に及ぶ。セキュリティ対策も適切である：常にroot/sudoを禁止し、サブマシンにはLandlockを使用している。これらの設計自体が「Agentが安全に未知の倉庫を実行する」という実験であり、倉庫のドキュメントの最初の読者は人からAgentへと変わっているかもしれない。

今後注目すべき二つの点があります。一つは、READMEの声明によるとメンテナンスやコントリビューションを行わないこと、ブログで他者に改善を求めることです。Apache 2.0の5つの成果物は、おそらく学界や暗号学の起業家たちが引き継ぐでしょう。独立した再実装が可能かどうかは、星印よりも厳しい検証です。二つ目は、正確な境界条件が補完されるかどうかです。これにより、このメカニズムが監査シーンから一般的な生産プロセスに導入されるかどうかが決まります。

私の結論は一言で言えば：FlashProveは分解する価値があります。それは、推理の信頼性問題を解決したからではありません（実際には解決しておらず、公式もそれを認めています）。むしろ、これまで口頭での保証しかできなかった二つの事柄を、証明可能な命題に変えたからです。すなわち、モデルのアイデンティティと、AIが書いた暗号学コードの正確性です。前者は推理市場の信頼基盤を指し、後者はAIプログラミング時代の品質保証方法を指します。

参考資料

• Anthropicの研究ブログ「Progress on provable inference for large language models」：anthropic.com/research/provable-inference（2026-11-04に公開；Claudeに関する記述はすべてブログの自己声明）
• HNの記事：story 50368626（155▲ / 77コメント、2026-11-05のスナップ）
• リポジトリ：github.com/anthropics/FlashProve（781★ / Apache 2.0 / 2026-10-30に作成 / VERSION 0.16.0、2026-11-05のスナップ）
• ローカルでの簡易なクローン確認（2026-11-05に実施、リポジトリのコードは実行していません）：README.md、guide/performance.md、lean/THEOREM.md、SUITE.md、docs/、AGENTS.md；30,902ファイル / 723MBがローカルでの統計値
• HNのコメント集：hn-provable.json（47件の証拠、本文はすべて転述され、直接引用されていません）

署名：永亮