Anthropic 開源 FlashProve 原型 以密碼學證明回覆出自指定模型
Anthropic 近日發表研究文章，公布名為 FlashProve 的開源原型，利用 zkSNARK（零知識簡潔論證）為大型語言模型的輸出生成密碼學證明，讓使用者在完全不知道模型權重的情況下，仍可核對一段回覆是否確實由指定模型產生。團隊以 Meta 的 Llama 4 Maverick（400B 參數混合專家模型）配合 4-bit 量化進行測試，單張 H100 顯示卡每秒可生成約 110 個 token 的證明，每個 1,024-token 請求的證明大小約 19MB。
為何需要可證明的推理
Anthropic 指出，使用者今日與模型對話時，幾乎無法確認回覆來自哪一個模型。當模型經第三方路由服務提供，服務商可能為節省成本而暗中換上較便宜的模型；攻擊者亦可篡改 token 串流，冒充某個模型作答。單憑輸出品質判斷並不可靠，因為即使換上能力較弱的模型，回覆表面上仍然合理。
密碼學證明可以填補這個信任缺口。模型供應商先對一組權重作出承諾，之後為每個回覆附上一份短小證明，使用者只需在一般處理器上快速驗證，即可確認回覆與該組權重相符，而證明本身不會洩露權重內容[1]。
Anthropic 列出多個應用場景：監管機構可核查供應商是否真的把算力用於推理，而非暗中訓練更強模型；企業可偵測伺服器被入侵或模型被替換；開發者可證明某段程式碼曾由前沿網絡安全模型檢查；監管機構亦可確認平台只提供已核准的模型。
速度與形式化驗證
團隊量度的證明生成速度約為每秒 110 個 token，成本相當於以 vLLM 直接執行同一模型的 70 至 95 倍 GPU 時間。Anthropic 承認這個開銷仍然可觀，但強調比以往開源系統快上幾個數量級，令「可證明推理」由理論可行變成工程上可測試。
研究過程中有兩點值得注意。其一，Anthropic 表示系統的優化由 Claude 參與完成，但同時指出 Claude 在大型複雜系統中的決策難以評估，因此團隊以 Lean 形式化驗證語言，為聲稱的安全保證撰寫可供審核的頂層陳述。其二，證明只隱藏權重，並不隱藏模型架構，這一點在混合專家模型以外仍有待處理。
開源的五項產物
Anthropic 同日發布五項產物：研究文章本身、技術報告、協議規格文件、可執行程式碼，以及 Lean 證明與互動式視覺化工具。程式碼包含一個證明器與兩個驗證器，其中快速驗證器以 C++ 撰寫，另一個「可證明正確」的驗證器則以 Lean 實作。程式碼、Lean 證明與文件一律以 Apache 2.0 授權釋出。
團隊表明無意在短期內部署，而是希望其他人接手改進。文章將此定位為階段性進度，而非完成的研究議程。
距離實用仍有的距離
FlashProve 目前只覆蓋 1,024 token 的上下文，與聊天場景累積的長對話相差甚遠。證明針對的是整數版本的模型配合貪心解碼，若實際服務使用浮點運算或抽樣解碼，某些位置的輸出可能與被證明的計算不一致。此外，團隊並未保證 Lean 規格、論文與快速程式碼三者完全對應，量度證明生成時間等側通道攻擊亦不在本次範圍之內[1]。
Anthropic 在負責任擴展政策的路線圖中，原定於 2026 年 9 月 30 日前完成可證明推理原型。該目標已透過另一項計劃達成，做法是為推理流量簽署並在受信任伺服器上重算；10 月 19 日的更新亦把名稱由「可證明推理」改為「推理驗證」，以涵蓋多種達到同等保證的方法。FlashProve 則是同一目標下以密碼學為主的另一條路線。
參考資料
[1] Progress on provable inference for large language models（2026年11月）
[2] FlashProve 技術報告