17秒扒下假模型頭套，驗身速度快5000倍

掏的是頂配旗艦的錢，調的是轉售路由的API，後台真正幹活的，卻可能是個縮水的小模型。

這種「掛羊頭賣狗肉」的暗箱操作，曾是整個大模型API供應鏈最隱秘的灰色地帶。

沒有權重、沒有機房，那怕後台半夜被偷樑換柱、摻水降智，開發者也只能乾瞪眼吃啞巴虧。

今天，這條暗箱鏈條被一劍斬斷！

就在剛剛，Anthropic聯手零知識證明祖師爺級學者，公佈大模型「可證明推理」重磅突破，正式開源密碼學驗真系統FlashProve！

從此，開發者無需信任任何中心化機構，也不用服務商交出半行權重程式碼。大模型每生成一條回答，都會被強制釘上一張數學級「出生證明」。

那怕手頭只有一台普通家用CPU，跑上17秒，就能用純數學方式精準驗出每一個Token是不是目標模型「親生的」，任何偷換模型、半路篡改的把戲都將當場現形！

更絕的是，這次打造出FlashProve的核心主力，竟是Claude自己。

這一次，所有程式碼、Lean 證明、技術文件，全部以Apache 2.0協議開源。

傳送門：https://github.com/anthropics/FlashProve

01. 按手印、開證明、秒級驗真  終結大模型「套殼掉包」

平時覺得大模型突然「變笨了」，很多人會去質問模型「你到底是誰」，或者甩幾道數學題去試探。

可模型自報家門的一句話本身就是後台生成的，算力負載與採樣配置的微小波動也會改變回答，使用者手裡永遠拿不到能把服務商釘死的鐵證。

更讓人後背發涼的場景，Anthropic寫進了部落格——

隨著模型越來越強、能自我部署，一個更高級的模型完全可能頂替獲批的弱模型上崗，再裝成弱模型的樣子，躲開本該施加在它身上的監控。

想要驗明真偽，傳統路子只有拿到權重自己重跑一遍，可前沿模型的權重是各家的命根子，普通人也根本養不起4000億參數模型的機房。

為了在不看權重、不重跑模型的條件下解開這個死結，FlashProve把驗真流程拆成了環環相扣的三步。

模型上線前，服務商在單張H100上花約39分鐘，用零知識編碼給模型權重生成一串唯一的承諾ID並向全網公開。這串ID就像權重的數字DNA指紋，那怕偷偷改掉一個參數都對不上；但外界光看指紋，絕無可能反推出權重長什麼樣。

每處理完一次對話請求，服務商的GPU就會順手生成一份約19MB的密碼學證明，用來證實這段輸出確實是由那個按過手印的模型算出來的。

任何使用者或審計機構拿到回答後，在普通CPU上運行驗證程序cp_verify，17秒就能拿到「真」或「假」的判決，全程既不要權重，也不要GPU。

撐起這套魔法的底層引擎，正是密碼學界大名鼎鼎的zkSNARK（零知識簡潔非互動式知識論證）。

驗證者只需要像老師抽查作業一樣，隨機翻看幾處，就能以極高機率抓到破綻。

為了把一次推理拆成能抽查的形式，每個請求背後要跑大約2000個名為sumcheck的子協議。

更硬核的是，它的安全性只依賴雜湊函數BLAKE2，不靠橢圓曲線這類代數結構，甚至被認為能扛住未來的量子電腦攻擊。這套密碼學路線，也早已在Starknet這類以太坊二層網路裡久經實戰。

原理說通了，真正的難關在後面：這麼重的證明，能不能在一個4000億參數的大模型上跑得動？

02. 單張H100狂飆5500倍  80GB視訊記憶體吞下4000億巨獸

答案是：能，而且只用一張H100。

團隊測試對像是Meta的Llama 4 Maverick，4000億參數的混合專家（MoE）模型，每個Token實際啟動約170億參數。

FlashProve充分利用了這一特性：證明器在生成計算軌跡時，工作量只跟那170億真正幹活的參數成正比，省去了95%以上的無效陪跑。

更妙的是，為了防止外界通過「那幾個專家被啟動」反推出模型權重的秘密，系統用零知識編碼把路由選擇藏進了一個指示向量裡，驗證器在核對時是對所有專家做加權求和，既省下了海量算力，又能保密模型內部的運轉路徑。

模型4-bit量化後的權重足足有232GB，而單張H100的視訊記憶體只有80GB，硬塞肯定當場爆視訊記憶體。

如果把整個推理過程的計算軌跡一次性打包，再豪華的顯示卡也扛不住。

於是，團隊把權重放在主機記憶體裡，分段送進GPU，逐段完成計算與證明。

H100在工作時像流水線一樣，每次只從記憶體裡流式讀取一個片段的權重，算完立刻在視訊記憶體裡完成編碼、雜湊與歸約，只把極少量需要傳遞給下一段的資料留存下來。

靠著這種「吃完一段、消化一段」的流式接力，單張80GB顯示卡硬是把232 GB的龐然大物啃了下來。

03. 114頁論文無人通讀  Claude包攬400MB數學證明

看到這裡你大概會好奇，如此精密繁複的密碼學協議與GPU加速工程，究竟耗費了多少名密碼學博士的心血。

點開FlashProve的GitHub開源首頁，右側的語言統計欄立刻暴露出這個項目的反常之處。

整個倉庫裡，C++程式碼只佔1.4%，Python佔1.3%，CUDA佔0.9%，而高達95.2%的程式碼（足足398MB）全部是用Lean 4數學證明語言寫成的。

一個大模型推理倉庫裡為什麼會塞滿近400MB的數學證明，隨倉附帶的114頁協議規範論文在第51頁給出了答案。

人類學者在這項工程裡只負責指明方向，從這篇114頁的密碼學論文、23頁技術報告，到C++與CUDA底層程式碼，再到近400MB的Lean形式化證明，幾乎全部出自Claude之手。

不光是寫程式碼和寫論文，項目裡每一次測試、運行、對比、推算和程式碼審校，也全都由AI包攬；凡是文中出現「經閱讀」「手工算得」「據匯報」的地方，那個讀者、計算者和匯報者全都是AI。

密碼學程式碼向來是軟體工程裡最脆弱的禁區，那怕一個符號寫反、一處隨機數掩碼漏掉，整座安全大廈就會瞬間坍塌。

Claude很擅長在龐大的系統裡尋找最佳化路徑，但它在底層做出的成千上萬個複雜決策，人類專家根本不可能靠肉眼逐行審完。

既然人類審不過來，Anthropic乾脆請出數學界的鐵面判官Lean 4。

在這裡，寫進去的每一步數學推導都要經過編譯器核心逐行核對，錯一處都過不了關。

在整個項目裡，人類科學家省去了稽核上億行中間推導的苦功，只跟AI一起敲定了最頂層的6條安全定義，把三件事釘成了鐵律。

完備性。只要服務商老老實實按承諾的權重跑模型，生成的證明就一定能通過核驗，被誤傷拒絕的機率不到兆分之一。知識可靠性。如果服務商拿假模型冒充、或者偷改了一個Token，造假矇混過關的機率不到2的100次方分之一，在數學上等同於不可能。零知識。不管客戶端拿著證明核驗多少次，證明檔案都不會向外洩露半點模型權重。只要這幾條頂層定理「說的是對的」，中間那近400MB的繁瑣歸約那怕人類一眼不看，Lean 4的核心也已經替人類把住了關。

更有趣的是，就連這個倉庫的打開方式，也告別了傳統的人類程式設計師手冊。

README開篇寫明「專為Agent運行而建」，並附上了現成的提示詞與AGENTS.md規範。

04. 密碼學祖師爺下場，AI跨入「數學鐵律」紀元

站在更高的時間坐標上回望，FlashProve的誕生引爆了深遠的技術合流。

它帶來的是「AI造系統、Lean保真偽」的全新工程範式。

面對近400MB證明程式碼、114頁公式推導的密碼學工程，碳基大腦的閱讀極限已經被擊穿。

在FlashProve裡，人類省去了逐行審讀C++最佳化和繁瑣引理的苦功，只死守那6條頂層定理的定義權，讓AI去攀登最險峻的工程與數學絕壁，再讓形式化驗證器做鐵面無私的守門人。

人類定下公理的邊界，AI窮盡推理的迷宮，數學給出終極的審判。這正是人類通往超級智能之路上，最硬核的一張安全契約。  (新智元)

彙整鉅亨號中所有使用「FlashProve」關鍵字，所發布的內容 (依照時間排序，最新在前，舊的在後)`

Anthropic親手終結「套殼AI」！17秒扒下假模型頭套，驗身速度快5000倍