Kolibri 與 MathForm-8B：其中一項準確度宣稱可由編譯器驗證

Kolibri 與 MathForm-8B 共用一份授權條款，除此之外幾乎沒有其他共同點。兩者皆為 Apache 2.0，皆為開放權重，且都在過去三個月內發布——Aleph Alpha 的 Kolibri 於 2026 年 10 月 3 日，OpenBMB 的 MathForm-8B 於 2026 年 8 月 14 日——而兩者也都把模型卡的一大部分篇幅花在數學上。相似之處到此為止。Kolibri 是一個 781 億參數的德英混合專家模型，每個 token 啟用 34.6 億參數，且旨在置於受監管的文件工作流程中。MathForm-8B 則是一個 80 億參數的稠密模型，從 Qwen3-8B 微調而來，只有一項任務：接收以普通英文撰寫的數學問題，並輸出其形式正確的 Lean 4 陳述。對任何評估這兩者之一的人來說，真正重要的差異並不是參數數量，而在於 MathForm-8B 的準確率主張是可執行的。你可以用編譯器檢查它的輸出。Kolibri 的輸出則只能靠另一次基準測試來檢查。

那種不對稱就是整篇文章的重點，而且它遠不止適用於這兩個模型。廠商的基準測試表是一種宣稱。證明輔助器接受一項形式化，則是一項結果。當一個模型的整個輸出空間都是機器可驗證的東西時，行銷那一層就消失了——Lean 編譯器要嘛接受該陳述，要嘛不接受，而無論再怎麼用發布貼文包裝，都改變不了這一點。

MathForm-8B 實際上產出什麼

自動形式化是一項狹隘、不吸引人且著實困難的任務，而模型卡對於其設定則有令人耳目一新的具體說明。

• 輸入與輸出——輸入自然語言數學陳述，輸出 Lean 4 形式化，並包含完整的定理標頭。

• 基礎模型 — Qwen/Qwen3-8B，經微調；與 OpenBMB 其餘發布內容相同，採用 Apache 2.0 授權。

• 訓練 — 在 FormalVerse 資料集上進行監督式微調，接著進行強化學習，並以 Lean 編譯與語意一致性回饋驅動強化訊號。

• 資料管線——Mathlib 知識檢索、編譯與語意驗證、迭代精煉，接著是軌跡重建。模型卡上的管線圖是這次發布中最具資訊量的部分。

• 評估 — Pass@8 通過率在兩項獨立檢查（語法檢查與一致性檢查）下，橫跨六項基準測試，在卡片上的圖表中以等權重巨集平均報告，而非以我們能逐行引用的表格形式。

• 工具鏈 —— 用於編譯檢查的執行中 Kimina Lean Server、用於實驗的 Lean 4.21.0，以及最大 16,384 個 token 的序列，溫度 0.6、top-p 0.95。

• 服務 — 以 16,384 個 token 的上下文，透過 OpenAI 相容的聊天介面提供。最後這個細節比表面上看起來更重要，因為這意味著模型能像一般端點那樣直接放入既有管線中。

請注意這兩項彼此獨立的檢查。語法檢查（Syntax Check）看的是 Lean 語句究竟能否剖析並通過型別檢查。一致性檢查（Consistency Check）則是看形式化語句的意義是否與自然語言問題相同——這是一項困難得多的性質，因為一個語法上有效、卻形式化了錯誤定理的 Lean 語句，比編譯錯誤還糟。OpenBMB 兩者都回報，這正是正確的做法，也是這項任務具備通用推理所沒有的驗證方案的原因。

Kolibri 如何運用數學，以及為何它是一種不同種類的數

Kolibri 在基準測試意義上擅長數學。在 Aleph Alpha 自家的後訓練測試框架中，當推理強度設為高時，它在 AIME 2025 的英文成績為 96.9、德文為 87.5，在 AIME 2026 為 96.0 與 90.0，並在其數學測試套件中取得 96.5 的英文平均，對比德文的 88.8。就同一張表而言，Kolibri 在 AIME 2025 英文的 96.9 高於 Nemotron 3 Super 120B-A12B 的 91.7 與 Qwen3.6 35B-A3B 的 84.6，且略低於 Qwen3.8 27B 的 97.9。

那些數字每一個都是廠商自行回報的，是在廠商自家的測試框架上得出的，沒有經過獨立重現，而且沒有 Artificial Analysis 頁面可供 Kolibri 交叉查核。這不是對那些數字的批評；而是在說明它們是哪一種性質的東西。AIME 分數是選擇題考試中正確最終答案的百分比。它只告訴你模型能得出一個整數。它完全不會告訴你得出該答案的推理是否嚴謹，也沒有留下任何可供第三方檢視的產物。

把 MathForm-8B 的輸出放在旁邊一比，那個差異非常明顯。Kolibri 對 AIME 問題的答案是一個數字。MathForm-8B 的輸出則是一段 Lean 4 定理陳述，它要嘛能對 Mathlib 編譯通過，要嘛不能。如果你正在建構的系統中，數學主張必須站得住腳——形式驗證流程、證明助理工作流程、稽核軌跡——那麼第二種產物遠比第一種有價值，而沒有任何基準測試列能表達這一點。

兩者實際上會在哪裡交會

若把它框定為一場對決，這個對戰組合其實沒什麼意思：一個 8B 專家模型在數學形式化上勝過 78B 的通用模型，卻在其他所有方面落敗，包括德語行政文書、長上下文文件推理，以及跨越上百步代理軌跡的工具呼叫。但這兩者並非彼此的替代品，真正有用的問題是：由兩者共同建構的管線會是什麼樣子。

這種自然的組合方式屬於路由式架構。由一個具備強大推理與工具呼叫能力的一般型模型負責資料匯入、消歧與檢索；而那百分之二需要正式成品的案例，則呼叫專家型模型來處理。若要靠人工完成這件事，就代表得用兩家供應商、兩份合約、兩套 SDK、兩組憑證，還有一個得由專人維護的派送層。這正是單一端點能夠值回票價的情況：一組相容於 OpenAI 的金鑰，一條路由規則把數學形態的請求送往形式化端點，其餘一切全交給一般型模型，並在其中一方速度變慢時進行容錯切換。這正是路由 DSL 的職責——把數個模型組合成單一次呼叫，而不是在開發階段就把選擇硬性寫死——而當一組模型共同作答能派上用場時，模型融合便能涵蓋這一點。Kolibri 與 MathForm-8B 目前都不在目前的 OrcaRouter；我們用各種供應商名稱與模型名稱的拼法搜尋了整個型錄，兩者都不在其中。這套組合的論證談的是問題的形態，而不是這兩個特定的端點。

價目表上所列的，是那個模式中通才的那一半，而且價格可以量化。Qwen3.8-27B 的定價為每百萬輸入 token 0.33 美元、每百萬輸出 token 2.40 美元，並提供 262,144 個 token 的視窗；Qwen3.8-Max 則為 2.00 美元與 6.00 美元，視窗為 100 萬個 token。對於正在評估是否值得在文件處理流程中加入形式化步驟的團隊來說，成本低廉的實驗做法是把通才型工作導向那裡，衡量真正需要 Lean 成品的請求量，然後再決定是否值得佈建一個 16,384-token 的專家端點。供應商的定價是原樣轉嫁，每個 token 都沒有額外加價，因此廠商一調價，這些數字當天就會跟著變動。

授權條款是他們唯一完全相同的一點

兩者皆採用 Apache 2.0，而在這個客製化研究授權與可接受使用附加條款十分常見的類別中，這是一項真正值得指出的對等點——這意味著這兩個模型無論是要商業使用、修改或再散布，都不需要先經過法律審查。

在其他方面，兩者的要求則有所不同。Kolibri 帶來約 78 GB 的權重佔用空間，以及兩張 A100 80 GB 加速卡、兩張 H100 SXM5、一張 H200、一張 B200 或一張 B300 的硬體門檻，另外還需要廠商的 aleph-alpha-inference 套件與 vLLM 外掛。MathForm-8B 在 bfloat16 下約有 16 GB 的權重，並可在單一現代加速器上以 16,384 個 token 的上下文提供服務；其相依項目是 Lean 工具鏈，而就評估流程而言，還需要一個執行中的 Kimina Lean Server。其中一種部署能裝進工作站，另一種則否。

這些上下文數字則指向相反方向，而且差距懸殊。Kolibri 的原生上下文視窗為 262,144 個 token，並已驗證可達 1,048,576 個 token，這正是它成為文件模型的原因：一份完整的德國監管申報文件或航太維修手冊，都能在一次呼叫中容納。MathForm-8B 則在設計上將上限設為 16,384 個 token，因為形式化請求就是單一問題陳述，沒有理由需要更長。這兩個數字都不是缺陷。它們只是描述不同的工作。

選擇，以及下方的驗證問題

• 若你的輸出必須可檢查，就選 MathForm-8B。如果下游系統會取用 Lean 4，或者重點在於讓證明助理對結果背書，那就沒有通用模型能取代它；該深究的是 Syntax Check 與 Consistency Check 下的 Pass@8 數字，而不是任何 AIME 列。

• 如果你需要一個模型，能在長上下文下閱讀德文與英文文件、在這些文件之間推理、呼叫工具、在上下文不足以支持答案時拒絕作答，並且能在你自己的環境邊界內、依你能用一行說明的授權條款部署，那就選 Kolibri。數學是它具備的一項能力，而不是它所代表的產品。

• 如果你正在建構形式化流程，請同時考慮兩者。不是把它們當作替代方案，而是當作同一條路由規則背後的兩個端點，並只在少數需要專門處理的請求時才呼叫該專門元件。

如果你要單憑某個基準測試數字來評估其中任何一個，請先做一項檢驗：問那個數字留下了什麼產物。對 MathForm-8B 來說，有一個 Lean 檔案，以及一個要嘛接受、要嘛不接受它的編譯器，而且你今天下午就能自己把兩者都跑一遍。對 Kolibri 來說，則只有發布表格裡的一個百分比，由廠商自行報告、未經重現，也沒有可資對照的獨立索引頁——而唯一能否證它的方法，就是下載 78 GB 的權重、租用硬體，然後重新執行一遍測試框架。當你在決定要把什麼投入正式環境時，這種不對稱性比那個分數本身更有價值。