Anthropic 開源 FlashProve：用零知識證明防模型掉包，單卡每秒 110 token

當你跟真人面對面聊天時，你能看見對方的臉、聽見聲音，甚至握個手，很容易確認對方到底是誰。

但當你呼叫一個大模型 API 時，螢幕那頭究竟是正牌的前沿模型，還是中轉服務商為了省成本偷偷掉包的便宜小模型，你其實完全沒法核實。

Anthropic 剛剛開源了一個叫 FlashProve 的原型系統，試圖用密碼學來解決這個「驗明正身」的難題。

這個系統基於零知識證明技術 zkSNARK。簡單來說，模型服務商可以給自己的模型生成一個密碼學承諾，隨後每次吐出回答時，都附帶一份幾十兆大小的數學證明。

任何拿到證明的人，不需要知道模型的具體權重引數，只需要在普通家用電腦的 CPU 上跑幾秒鐘驗證，就能 100% 確認這段話確實來自承諾過的那個模型。

怎麼在不交出底牌的前提下自證清白

可驗證推理最讓人頭疼的地方，在於前沿模型的引數權重是商業機密，絕對不可能公開給使用者去復算。

FlashProve 聰明的地方就在於，它利用 zkSNARK 的隱藏特性，在證明過程中完全隱去了模型權重，只公開證明本身。

雖然模型的網路架構依然是公開的，但核心的權重引數不會洩露半點。

為了展示這套系統在超大模型上的可行性，Anthropic 在一塊輝達 H100 顯示卡上，運行了 4000 億引數的混合專家模型 Llama 4 Maverick。

在 4-bit 量化和 1024 token 的上下文設定下，FlashProve 生成證明的吞吐量達到了每秒 110 個 token，每次請求生成的證明檔案大約 19 MB。

當然，安全是有代價的。生成這份密碼學證明所耗費的 GPU 算力，大約是在常見推理框架 vLLM 上原生跑同一模型的 70 到 95 倍。

不過，這個速度已經比以往同類開源方案快了幾個數量級。

更硬核的是，Anthropic 不僅寫了程式碼，還拉來了 EPFL、MIT 等高校學者合作，用形式化驗證語言 Lean 4 把整套系統的安全性在數學上證明了一遍，偽造成功的機率被壓低到了微乎其微的級別。

防中轉商偷梁換柱，也防 AI 裝傻逃避監管

這項技術能解決的問題，比防範 API 代理商偷工減料要深刻得多。

一個直接的應用是安全評測。第三方評測機構在測試模型安全性或對齊水平時，必須確保自己正在打分的系統，跟服務商公開上線的是同一套權重。

另一個更大的隱患來自模型自身或者駭客入侵。

如果伺服器被攻破，駭客可能篡改輸出植入惡意程式碼；而未來具備自我部署能力的高階 AI，甚至可能故意把自己偽裝成更弱的模型，從而繞開嚴格的監控和圍欄。

有了 FlashProve，只要每次推理都強制繫結權重證明，任何未授權的權重替換或輸出篡改都會立即導致驗證失敗。

此外，它還能幫監管機構盯著算力。如果法規要求某批晶片只能用於日常推理而不能用於訓練新模型，監管方只要抽查推理證明，就能確保算力沒被挪作他用。

為什麼重要

在我們看來，Anthropic 這次拿出來的雖然只是個標註為「不再維護」的研究原型，但它第一次把大模型的可驗證推理從紙面理論推到了工程可用的門檻邊緣。

對普通使用者來說，你顯然不會為了日常查天氣或寫郵件去承擔 70 倍的算力溢價。但對於安全審計、法律合同、核心程式碼漏洞掃描這類高風險場景，一個帶防偽簽名的回答極具商業價值。

對整個行業而言，可驗證推理會重塑模型分發和聚合平臺的信任鏈條。過去那些號稱轉發頂級模型、實則在後臺搞蒸餾替換的灰色路由中間商，一旦遇上較真的企業級客戶，生存空間將被大幅壓縮。

更值得玩味的是 Anthropic 的開發方式。他們在正文中坦言，FlashProve 的許多最佳化和協議草案其實是由 Claude 協助寫出的，但因為 AI 寫的複雜系統太難人工排查，研究團隊才倒逼自己用 Lean 4 做了嚴密的形式化證明。

讓 AI 參與設計密碼學系統，再用數學證明器去兜底驗證，這種工作流本身可能比單純的速度突破更具前瞻性。

這套系統目前以 Apache 2.0 協議開源。儘管離大規模商業部署還有很長的路要走，但至少它證明了一條路：AI 的透明度，未必要以犧牲商業秘密為代價。