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

原標題：Anthropic親手終結「套殼AI」，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規範。

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

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

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

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

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

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