---
author: Best Partners TV
date: '2026-11-07'
guest: ''
layout: post.njk
source: https://www.youtube.com/watch?v=9LhMsk6_1JU
speaker: Best Partners TV
tags:
  - provable-inference
  - zk-snark
  - formal-verification
  - model-auditing
title: Frontier Red Team 開源可證明推理系統 FlashPro
summary: 介紹 Frontier Red Team 團隊發布的開源可證明推理系統 FlashPro。該系統基於 zk-SNARKs、雜湊函數及 Lean 形式化驗證，旨在不洩漏模型權重的前提下驗證大模型推理計算的正確性與模型真實性，並分析了其性能開銷、工程權衡、局限性及監管合規等應用場景。
insight: ''
draft: true
series: ''
category: ai-application
area: tech-engineering
project: []
people:
  - Roy Rinberg
companies_orgs:
  - Frontier Red Team
  - 宾州大学
  - 麻省理工学院
  - SocketBear
  - Meta
products_models:
  - FlashPro
  - Lean
  - Llama-3-Maverick
media_books: []
status: evergreen
---
大家好，這裡是最佳夥伴，我是大飛。當我們與朋友面對面交談時，我們可以看到他們的臉，聽到他們的聲音，並與他們握手；基本上沒有理由懷疑他們的身份。但是，當面對螢幕上的大型模型時，這些驗證方法都不存在了。你付費後，選擇一位模特兒的名字，但沒有人能真正證明後台是誰在回答你的問題。許多第三方路由平台可能會將你選擇的昂貴型號替換為更便宜的型號以節省成本，或者有人可能會篡改傳輸以改變回應。無論哪種情況，我們僅僅透過觀察答案的質量，都無法區分二者之間的差異。

### FlashPro 系統發布與開源內容

11 月 2 日，Frontier Red Team 開源了一個名為 FlashPro 的系統。它的核心重點是可證明推理。該計畫的主要作者是 Roy Rinberg，團隊成員包括來自賓州大學、麻省理工學院和 SocketBear 的學者。他們一次發布了五項內容：一篇部落格文章、一份技術報告、一份協議規範、可執行程式碼和精益驗證原始碼。程式碼包含一個用 C++ 寫的快速驗證器和一個完全用 Lean 寫的、經過定理證明的驗證器。所有內容均以 Apache 2.0 授權發布。今天，我們將向大家介紹這個系統。

### 傳統驗證的困境與 zk-SNARKs 原理

那麼，為什麼之前沒能實現這一點呢？要驗證一個模型，最簡單的方法是獲取權重並重新運行相同的查詢，看看結果是否匹配，但是前沿模型的權重可能有數百 GB，需要 H100 卡才能運行。一般使用者沒有這些資源，甚至獨立的評估機構也未必有；此外，有些模型的重量根本不是公開的。因此，這始終依賴信任；我們只是相信平台所說的使用哪種模型。

然而，FlashPro 使用的是零知識簡潔論證（簡稱 zk-SNARKs）。這個名稱很複雜，但它必須滿足兩件事：首先，證明本身不能洩露權重，也不能洩露中間計算的內容，或者在哪一層激活了哪些專家。其次，證明必須足夠小，驗證必須足夠快，以至於不需要 GPU。第一種稱為零知識，第二種稱為簡潔性。

這兩點其實有點違反直覺，因為證明計算正確性最直接的方法就是自己再運行一次。然而，再次運行恰恰是最昂貴的方法，因此 FlashPro 的具體解決方案分為兩個階段。

首先是離線階段，在此階段，提供者將權重壓縮到一個較短的承諾中；你可以把它想像成給這組參數留下一個數字指紋。權重本身是私密的，但此指紋鎖定了一組特定的參數，所有後續檢查都將以此為依據進行。此步驟每個模型只需運行一次，大約需要 30 分鐘。

接下來是線上階段，用戶發送請求，提供者返回答案以及證明。這個證明只需要說明一件事：由該指紋鎖定的特定權重確實為該輸入產生了該輸出。這樣一來，使用者就掌握了四樣東西：承諾、投入、產出和證明。依靠這些，他們可以自行進行驗證，而無需權重或計算能力。

值得注意的是承諾步驟：對於一次性證明，您只需計算並提供一個，下次則需要重新開始。但推理則不同；數百萬次請求都需要重複引用同一組權重。因此，該結構是先進行提交，鎖定權重一次，然後為每個請求產生單獨的證明。這裡有一個容易被忽略的細節：承諾必須具有約束力，因此提供者不能交換不同的權重，這在密碼學中被稱為約束屬性；另一方則隱藏了屬性，這意味著承諾書沒有透露權重是什麼。這套工具在密碼學領域並非一項新發明。

### 密碼學構造與矩陣運算

這個構造可分為三個步驟：第一步使用一種稱為互動式預言機證明（IOP）的機制，將這種龐大的計算壓縮成幾個點。第二步使用雜湊函數，特別是梅克爾承諾，來縮短冗長的證明，以便驗證者只需要檢查幾個位置。最後，使用 Fiat-Shamir 啟發式演算法將互動式輪次壓縮成一則訊息，從而產生非互動式證明文件。整個系統僅依賴雜湊函數，而不是橢圓曲線等代數結構，其優點在於可以應對來自量子電腦的未來威脅。這種設計被稱為後量子安全，他們使用的雜湊函數是 BLAKE2。

更深入地來看，最複雜的部分是逐層矩陣乘法和非線性函數。矩陣乘法是可控的，可以寫成多項式限制；問題在於像 softmax 這樣的運算，在有限領域中表示這些運算的成本非常高。此方法涉及預先編寫一個公共查找表，證明者只需要證明每個輸入輸出對都可以在該表中找到。「查找參數」這個名稱指的正是這個意思；在整個證明過程中，一次請求涉及大約 2,000 次查找，佔交互輪數的 90% 到 95%。

### 測試配置與基準數據

首先，讓我們來看看他們用於測試的模型：該模型是 Meta 的 Llama-3-Maverick，而不是他們自己的雲模型。這是一個包含 4000 億個參數的專家混合模型，使用來自 Hugging Face 的第三方 4 位元量化版本，並將其轉換為整數模型。雖然將浮點權重轉換為整數會引入誤差，但測量結果顯示這些誤差非常小。每個請求使用 1,024 個令牌的窗口，安全目標為 128 位元。這裡值得注意的一點是，此版本不包含權重；你需要自行從 Hugging Face 下載並按照其許可證運行它們。這樣一來，至少其他人可以重現並驗證結果，對吧？

在驗證器方面，它使用一個 H100 和 24 個 CPU 核心，批次大小為 64 個請求。使用 24 個核心進行測量耗時 223 秒，相當於每秒 110 個代幣，每個證明檔案大小為 18.78 MB。驗證程式不需要 GPU；使用 24 個執行緒時，驗證需要 17 秒；而使用單一執行緒時，驗證需要 21 秒。客戶端需要下載約 6.5 MB 的數據，然後每次請求接收一個證明。

這裡有一個統計學上的細微差別需要澄清：每個證明只能驗證每 1,024 個代幣中的一個。然而，證明器已經計算出了全部 1,024 個令牌。所以，每秒 110 個令牌指的是它的令牌處理速度。此外，他們還嘗試驗證整個回應中的每個代幣；速度幾乎沒有變化，相當於每秒只有 39.1 個已驗證的代幣。

成本如何？我們還要明確一點，基於單 GPU 時間，產生證明比標準 VLM 推理慢約 70 到 95 倍。對照組使用 vLLM 版本，運行在 8 台 H100 上。以卡片計算，一批 24 個請求的處理速度比 VLM 一次處理相同的 24 個請求慢約 72 倍。如果逐一驗證，單一請求可以在 58 秒內獲得一個證明。但吞吐量將下降到每秒 17.6 個令牌。因此，他們選擇分批處理。一批訂單從請求到校樣大約需要 5 分鐘；相比之下，逐一進行實際上更慢。

### 歷史方案對比與工程權衡

實際上，這個數字聽起來可能有點嚇人；2017 年，SafetyNet 驗證了一個兩層 MNIST 小型網路。2021 年，ZKCNN 達到了 VGG16 的水平，擁有 1500 萬個參數，每次推理耗時 88.3 秒。ZKML 的 GPT-2 有 1.17 億個參數，每次推理需要 159 秒。對於 15 億 GPT-2 XL，Modulus Labs 花了 90 多個小時，而 ZKLLM 在 2024 年在 A100 上驗證了具有 130 億個參數的 LLaMA-2。吞吐速度為每秒 2.5 次推理。2025 年，ZK-GPT 將 GPT-2 的推理時間縮短至 21.8 秒；唯一公開的 LLaMA 驗證系統是 WINF。產生 1,000 個代幣需要 14.3 小時，證明檔案大小為 93.6 GB，僅驗證就需要近一天的時間。

FlashPro 每秒可進行 110 次推理，產生證明只需數十秒；此外，還有一個名為 Attestable 的商業解決方案。在單一 H100 上，它證明了一個 301 億參數的密集模型，每秒可進行 53 到 77 次推理。然而，該程式碼並非開源，且兩者的模型架構也不同。對於 FlashPro 而言，每次推理僅啟動 170 億個參數。因此，這兩個數字不能直接比較；只有與先前的方案相比，這種「70 倍」的速度提升才有意義。

實際上，達到這種水準的工程壯舉依賴於幾個關鍵的權衡取捨。最經濟實惠的方案就是教育部本身；在 4000 億個參數中，每次推理只使用 128 位專家中的一位加上一位共享專家，總共約 170 億個參數。證明工作量只涉及這 170 億個參數；空閒的專家不消耗運算資源，零知識編碼隱藏了實際啟動的是哪個專家。

接下來是推理後批次證明。該系統在推理過程中無法證明；它會等待伺服器產生整個回應，然後再進行並行批量處理，就像預填充階段一樣。由於每個批次只需拆包一次重量承諾，因此可以消除冗餘開銷。代價是，證明過程不在關鍵路徑上，因為在證明完成前你就能得到答案。

在硬體方面，它採用單卡工作流程；232GB 的權重資料儲存在主機記憶體中，並進行分段處理，只有在需要時才將每一部分發送到 80GB 的 VRAM 卡。所以，一個 H100 就足夠了；無需使用多卡集群，也無需在卡之間來回傳輸數據。

此外，還有一點與承諾的期限有關；一次承諾必須支援大約 1600 萬次請求，但每次證明都需要讀取編碼，而讀取次數是有限制的——讀取過多會洩露資訊。因此，他們採用的方法被稱為連結證明。首先，證明初始編碼是正確的，然後每次都使用一組新的隨機數對同一組權重進行重新編碼。然後，提供連結證明，證明這些權重仍然是同一批權重，因此任何單一編碼都不能被篡改。

哈希本身還會帶來另一個問題。Fiat-Shamir 變換是一個哈希鏈，其中每一輪都必須等待前一輪哈希完成後才能開始，這是嚴格串行的。然而，他們的方法是同時驗證一批請求；每個請求都有自己的鏈，最後這些鏈合併成一個共享鏈，然後再分支出去。從數學角度來看，這是一個有向無環圖，正是因為串列部分被並行部分覆蓋，所以單張卡才能以全容量運作。

### Lean 形式化驗證與安全性保證

我們都知道，加密程式碼極其脆弱，一個看似微不足道的實作細節都可能導致重大漏洞。因此，在這個版本中，團隊使用 Lean 將協定和安全屬性編寫為機器可驗證的定理，總共三個：完備性、可靠性和零知識。

完備性意味著有效的證明總是可以通過；可靠性意味著偽造的證據永遠無法通過；零知識意味著除了證明本身之外，不會透露任何其他資訊。何必這麼麻煩呢？因為該系統的大部分程式碼都是借助人工智慧優化產生的，導致程式碼複雜，人類很難逐行審核。具體方法是以可審計的形式編寫頂層描述，這樣人們只需要驗證定理是否表達了他們想要證明的內容，而無需逐行驗證過程。

接下來，他們如何解釋自己的不足之處，這更有意思。他們非常坦誠地承認，日常使用的 C++ 驗證器缺乏形式化保證，而經過驗證的驗證器是速度較慢的 Lean 驗證器。它只接受符合可靠性定理的內容。然而，Lean 只在一次只證明一個請求的情況下才能證明零知識；批量證明的零知識證明尚未建立。GPU 的證明代碼由 AI 生成，沒有證據表明它與 Lean 描述等價。這種主動揭露資訊的方式比掩蓋細節值得信賴得多。

此外，他們劃清了界限：如果證明器程式碼失敗，最多只會影響完備性和零知識，但不會影響可靠性，因為可靠性完全取決於驗證者，而驗證者只需要信任自己。

### 系統限制與邊界條件

然而，還有一個比數字更重要的限制：目標是使用貪婪解碼的基於整數的模型，其中每個位置都選擇得分最高的標記。然而，線上服務通常使用浮點運算，並且在生成文字時經常應用隨機抽樣。因此，對於同一個提示，兩者的結果可能會有所不同，他們對此也毫不避諱。

整數版本和浮點版本之間的輸出差異通常很小，但這僅適用於正常輸入；精心設計的對抗性輸入並不能保證一定有效。因此，這證明了計算是使用一組特定的權重執行的，但不能證明輸出是否是模型自然給出的結果。

還有一些其他的限制，我們簡單概括一下。首先，上下文長度上限為 1,024 個標記，而聊天場景通常需要數十萬個標記。其次，雖然系統可以隱藏權重，但無法隱藏架構，而架構本身可能屬於商業機密。第三，側通道攻擊無法緩解；例如，產生證明所需時間的細微差別，理論上都可能洩漏資訊。最後，此證明器僅支援單一 GPU，不支援張量並行。

關於事後驗證的概念，我們需要詳細說明：它保證篡改行為會被偵測到，而不是保證篡改行為不會發生。如果攻擊者劫持推理伺服器竊取權重，他們可能會在證明失敗觸發警報之前透過篡改回應洩露資訊。操作員也必須信任他們的日誌；能夠修改日誌的攻擊者可以在日誌中保留正確的輸出，同時將篡改後的版本傳送給使用者。這是一種縱深防禦，而不是單一防線。

然而，重新計算的成本並不高，大致相當於一次前向傳播，而證明產生的成本是其 70 到 95 倍，因此重新計算只會增加證明器 1% 到 1.5% 的工作量。

### 應用場景與未來展望

那麼，它實際應用於哪些領域呢？論文中提到了幾個應用案例。

其中之一是運算資源監管，監管機構可以要求提供者在一段時間內提交推理請求的證明，以確認硬體正在運行推理而不是訓練下一代模型。然而，這個證明只能證實它正在進行推理；它無法證明它是否在暗中進行秘密訓練。

其中一種類型是防篡改。一旦推理伺服器被攻破，如果更強大的模型試圖替換以逃避監控，它將無法提供相應權重的有效證明，篡改行為將立即暴露出來。公司也可以在內部使用此方法來確認其伺服器上正在運行的確切版本。

還有一類是與文字來源有關。假設一家企業聲稱該程式碼通過了前沿模型的安全掃描；買家可以使用該證明進行核實。反之，他們也可以提供「失敗證明」，表明他們花費了數百萬美元進行漏洞研究，但模型沒有發現任何缺陷。

最後一個類別是合規性。監管機構要求在某些情況下只能使用註冊模型。透過使用證明將請求綁定到模型，它從機制上阻止了秘密運行未經授權的模型的路徑。

實際上，實現可證明推理有兩種方法。依賴可信硬件，特別是可信執行環境，前提是晶片供應商確實製造了防篡改硬體。另一種方法是依靠純軟體密碼學，其安全性基於計算難度。即使機器和作業系統完全被攻破，攻擊者也無法偽造有效證據。這兩種方法保證的是不同的結果：一種依賴晶片信任，而另一種依賴數學。

他們也有自己的時間表。在他們的前沿路線圖中，他們設定了一個目標，在 2026 年 9 月 30 日之前建立一個可證明的推理原型。在 2026 年 10 月 19 日的更新中，官方立場從「可證明的推理」變為「推理驗證」，理由是「可證明的」聽起來比實際路徑更狹窄。

因此，它目前仍是一個研究原型，而不是一個即買即用的產品。至於讓每個 API 回應都附帶可驗證的證書，那還是一個更遙遠的目標。

總而言之，僅就這一點而言，我認為它的意義在於「可證明的」這個詞，而速度只是實現這一目標的前提條件。此前，該生產線的瓶頸在於效能，因此無法實現。現在，經過多次嘗試，次數已降至 70 到 95 次，終於達到了實際部署的範圍。那麼，這個數字背後的概念是什麼呢？在標準推理服務中，成本翻倍已經令人難以承受；每天撥打 70 次電話仍然是不可接受的。所以，它的真正用途不在於我們每天使用的任務，而是那些需要驗證的場景。剩下的問題就從性能轉移到如何彌合可靠性方面的差距。對於從事翻譯和評估的人員來說，這還不能立即使用，但將來在討論這個問題時，至少我們可以自己測試一下這個工具。

感謝觀看，我們將