AlphaProof Code 與 MathForm-8B：同一條 Lean 流程的兩個階段，而非兩個競爭對手

仔細閱讀 AlphaProof Code 論文，會有一個公告並未強調的數字特別醒目：在 DeepMind 五名研究人員耗費四週驗證 Signal 的過程中，無法自動化的部分是最前端。人類專家與多種模型共同合作，把 Signal 的安全目標轉譯成正式的 Lean 規格，而且在任何證明工作開始之前，每一項都由專家審查過。這就是瓶頸。OpenBMB 於 2026 年 8 月 14 日在 Hugging Face 發布的 80 億參數自動形式化模型 MathForm-8B，正是直接嘗試自動化這一步——將自然語言數學陳述轉成可供他人證明的 Lean 4 定理陳述。將兩者並列，你比較的並不是兩個產品。你看到的是同一條流程中前後相連的兩個階段，而隔開它們的，是數學與協定安全之間的差異。

流程，依工作發生的順序

真實軟體的形式驗證有三項任務。首先，決定什麼必須成立，並用形式語言寫下來。其次，證明實作滿足它。第三，以機械方式檢查證明，因為錯誤的證明比沒有證明更糟。

MathForm-8B 只做第一項工作，而且僅限於一類狹窄的輸入：教科書式的數學陳述。給它「對每個實數 x，x² 皆為非負」，它會回傳 Lean 4 中的 import、型別與定理標頭。它不會回傳的是證明，而其作者明白表示，證明搜尋是別人的問題。它公布的數字全為廠商自行提報且未經重現：在六項基準測試中，語法檢查下的平均 Pass@8 為 88.06%，較嚴格的一致性檢查下則為 72.37%——這兩個數字之間的落差，才是誠實衡量「語法上有效的陳述有多常表達出與要求不同的意思」的尺度。

AlphaProof Code 負責第二與第三項工作，外加一個 MathForm-8B 無法觸及的規格階段。Signal 的安全目標並非 MathForm 所受訓練那種意義下的數學命題；它們是關於協定的陳述——訊息在裝置暫時遭入侵之前與之後都持續受到保護，發起方與回應方確實是他們所宣稱的身分。要將這些轉換成 Lean，需要的是任何 8B 自動形式化器都不具備的協定專業知識。規格一旦存在，證明工作便完全交給代理，而檢查工作則交給 Lean 的 kernel，外加一個把關代理，使用comparator對照一份保留的規格副本。

每一個實際使用起來要花你多少成本

• 權重 — MathForm-8B：可下載、Apache 2.0、四個 BF16 格式的 safetensors 分片，從 Qwen3-8B 微調而成。AlphaProof Code：無。本次釋出內容包含 Lean 開發、AArch64 語意，以及位於 github.com/google-deepmind/code-verification 的 libsignal 繫結。

• 執行方式 — MathForm-8B：Transformers、vLLM 或 SGLang，全都提供 OpenAI 相容端點，且在你自己的硬體上執行。AlphaProof Code：沒有端點、沒有 API、沒有候補名單、沒有價格；它是一個研究框架，DeepMind 表示在它規模化之前需要「持續研究」。

• 輸入 — MathForm-8B：以自然語言表示的數學陳述。AlphaProof Code：一份形式化規格，加上你想據此證明的二進位檔。

• 輸出 — MathForm-8B：一個 Lean 4 定理陳述，尚未證明。AlphaProof Code：一個經機器檢驗的證明，或在程式碼有誤時的反駁。

• 人工審查 — MathForm-8B：你審查輸出的陳述，而在 72.37% 一致性下，你會審查很多這類陳述。AlphaProof Code：專家在證明工作開始前審查每一份規格，接著代理會標記約 1% 的程式碼庫以供再次檢視。

• 已知限制 — MathForm-8B：僅限數學陳述，不產生證明，且其 README 中連結的程式碼儲存庫在發佈時仍是佔位符。AlphaProof Code：SPQR healing 沒有後量子保證、沒有載荷隱私、每次提升僅限一個工作階段，且 MAC 偽造界限在單一工作階段中接近 25,000 則訊息時會變得空洞無效。

MathForm-8B 必須縮小的差距

很容易會說，自動形式化器說不定早就寫得出 Signal 的規格，替研究人員省下一開始得先投入的那幾週。但論文本身的說法並非如此，而且原因很具體。協定的規格並不是把某個主張換句話說；它是在選擇對手模型。Signal 這項工作有一條 Dolev–Yao 符號軌，其中包含一位在握手後破解 Diffie–Hellman 的量子攻擊者；還有一條計算軌，採用古典對手與具體界線。這兩條軌對同一份程式碼陳述不同的定理，而從中擇一是有安全後果的工程決策。沒有任何一個被訓練來把「證明 x² ≥ 0」轉成 Lean 的模型，會做出那個決定。

自動形式化器理論上能做的是那項工作中機械性的部分：給定一個以文字描述的安全目標，以及一個既有 Lean 定義的函式庫，依專案自身的慣用語法產出陳述的初稿，供專家修正。這是實質的節省，但遠比標題所暗示的小得多。該論文報告了一份規格偏差目錄，包含超過 200 個計算性條目與約 35 個符號性條目——其中十五項是 Double Ratchet 分析中的缺漏或錯誤——而這正是人工審查步驟所發現的內容。會起草陳述的模型必須以該目錄為衡量基準，而不是以數學基準測試上的 Pass@8 分數來衡量。

在兩個數字完全無法比較的情況下

MathForm-8B 的 88.06% 與 AlphaProof Code 的 650 萬行程式碼衡量的是不同事物，絕不應放在同一欄。前者是作者自建基準套件上的命中率；後者是為單一目標產出的證明數量。廠商坦承，88.06% 採用語法檢查，而這是個薄弱的判準——陳述可以編譯通過，卻仍形式化了錯誤的主張，這就是為何一致性數字低了 16 個百分點。

AlphaProof Code 中具有類似風格的一環，是驗證工作：兩個先前已修復的 Signal 錯誤——一個弱狀態錯誤和一個小子群錯誤——被重新引入到一個隔離副本中，而在這兩種情況下，系統都產生了經機器檢查的證明，證明有錯誤的版本無法通過安全定理。那是一項負向測試，而負向測試正是自動形式化器基準測試完全缺失的東西。MathForm-8B 沒有報告任何形式為「給定一個故意錯誤的陳述，模型指出它錯了」的結果。

實際上你會如何將它們搭配在一起使用

具體來說，而且這是整個比較中唯一有近期可行路徑的部分：使用自動形式化器起草、由強大的通用模型評論草稿，並由證明代理嘗試完成證明。每個階段都有不同的失敗模式，而將三者都透過同一把金鑰路由是實務上的便利。在 OrcaRouter 上，超過 200 個模型位於單一 API 之後，以供應商定價且 0% 加價，因此，一個會將同一陳述傳給兩個模型並比對其 Lean 輸出的規格草擬迴圈，是一次 routing-DSL 呼叫，而不是三份合約和三套 SDK。自動容錯移轉可涵蓋你所選模型正值狀態不佳的情況。

上述種種都提供不了那項保證。MathForm-8B 給你一個陳述，模型給你一份評析，而仍然得有某個東西來證明它。目前，唯一能在真實部署的程式碼上閉合這個迴路的已發表系統是 AlphaProof Code，而且它並不出售。

閱讀這兩篇論文，而不是從中選出一個贏家的原因

MathForm-8B 是一個有用的產物，職責範圍狹窄，並有真實且經實測的準確率上限。AlphaProof Code 則是一項工作流程示範，其最具可移轉性的發現不是證明量，而是分工：規格工作需要人類與強大的通用模型，證明工作需要代理團隊與核心，而兩者之間的界線正是所有困難所在。任何在建置驗證管線的人，都應認真看待這個分工，並把自動形式化視為降低第一階段成本的環節——而不是取代它的環節。

對今年這個月正在決定要下載什麼的團隊，誠實的總結是：MathForm-8B，可以，如果你使用 Lean 並想要一個起草輔助工具。AlphaProof Code 的話，請閱讀其產物儲存庫與規格偏差目錄，因為這份目錄比任何公告都更能告訴你，生產程式碼的形式驗證仍無法觸及什麼。