TwIL-LM3-Pro 與 MathForm 8B：陳述與蘊含是形式化的不同兩半

TwIL-LM3-Pro與MathForm-8B鎖定的是同一個宏觀問題——讓機器產出形式化、可供檢核的文字，而非看似合理的散文——而它們各自解決這個問題的不同一半。MathForm-8B 是 OpenBMB 的 80 億參數自動形式化器，於 2026 年 8 月發布：只要給它一個以自然語言表述的數學問題，它就會輸出該問題的 Lean 4 陳述，並把證明義務留給編譯器檢查。TwIL-LM3-Pro 則是 webAI 於 2026 年 9 月推出的 36.6 億參數形式邏輯模型，其目標輸出包括蘊含標籤、一階邏輯翻譯、語意剖析與 Lean 證明評論。一個產出待檢查的對象。另一個則告訴你，你手上的東西是否蘊含你所宣稱的內容。

因為這兩者恰好只在一個賽道上重疊——Lean 形式化——所以做一張比較頁面既誘人又容易誤導。更有用的問題是，它們各自被訓練成要因什麼而獲得獎勵，因為獎勵訊號正是這兩種設計分歧最為尖銳的地方，也是更明智選擇真正所在之處。

陳述與蘊涵

MathForm-8B 是以 FormalVerse 訓練而成，這是一個 Lean 語料庫，OpenBMB 的論文將其描述為約 367,000 個已驗證範例，並在監督式微調後接續強化學習。此流程會在生成前從 Mathlib 檢索相關定義與既有形式化，接著利用編譯器診斷與語意一致性檢查進行精煉。其輸出是一則形式陳述——匯入、型別、定理標頭——由外部編譯器決定接受或拒絕。模型卡明確表示它不會解決問題，也未宣稱會這麼做；證明是別人的工作。

TwIL-LM3-Pro 則是從邏輯這一側切入同一個領域。它的流程管線鎖定六項目標：一階邏輯翻譯、蘊含標註、語意剖析、Lean 形式化、Lean 證明批判，以及規則歸納。MathForm 的設計是為了產出陳述，而 TwIL-LM3-Pro 的設計則是為了對陳述作出判斷——這個是否被蘊含、這個剖析是否正確、這個證明嘗試是否嚴謹。它也會進行形式化，而這正是這兩個模型真正可資比較、而不僅僅是彼此相鄰的唯一之處。

來自編譯器的獎勵與來自評分器的獎勵對比

這是至關重要的設計差異，而且兩家廠商都有記載。

MathForm 的訓練獎勵來自 Lean 編譯與語意一致性回饋。編譯器就是個神諭：它要麼接受該形式化，要麼不接受，沒有部分分數，也沒有任何可爭論的餘地。那是機器學習這個領域裡最乾淨的獎勵訊號，也是為什麼自動形式化基準會以通過率來呈報——這項指標位於一個不在乎任何人相信什麼的程式下游。

TwIL-LM3-Pro 的最終階段，是一次熵加權的 GRPO 執行，對抗程式化驗證器，而模型自身的卡片描述了對寬鬆匹配的部分給分以及 token-F1，使即使全部失敗的提示群組仍能產生梯度。其主打巨觀閘門是四個有界分類通道加上規則歸納的等權平均，而在該閘門中，多選題與程序性通道被計為 `max(exact_match, loose_match)`——這是卡片明白陳述的規則，因為格式不同的正確答案是格式假象，而非推理失敗。

兩種設計都沒有比較差。它們是為了不同的後果而調校的。以編譯器評分的獎勵會產生一個模型，你可以把它指向一個困難的形式化問題，並信任它的輸出，因為輸出是可驗證的。帶有部分分數的評分器評分獎勵會產生一個模型，可以用更模糊的判斷來訓練——蘊含、批判、規則歸納——在這些領域中沒有編譯器可以裁決，而替代方案就是完全不在這些路線上訓練。代價是，所得的數字只跟評測框架一樣好，而 webAI 也這麼說：它的 strict-7 那一列剝除了所有寬鬆匹配分數的痕跡，存在的目的正是讓讀者能在主要數字旁看到更嚴苛的數字。

這些分數不在同一把尺上

兩個模型都公布了與 Lean 相關的數字，而這些數字無法相減。MathForm 的論文報告：在六個 Lean 基準測試中，Syntax Check 下的平均 Pass@8 為 88.06%，Consistency Check 下為 72.37%；在較難的 FATE-H 與 FATE-X 子集上，一致性檢查通過率分別為 63% 與 37%，並宣稱其表現優於數個專門化的 32B 自動形式化器。TwIL-LM3-Pro 的模型卡報告，在其自家的 Track A 評測框架上，`lean_formalize` 的 token-F1 為 0.5092，`lean_critic` 準確率為 0.7950。

在編譯器檢查下的 Pass@8，以及對照參考字串的 token-F1，衡量的是不同的事情。Pass@8 給模型八次嘗試，並詢問其中是否有一次成功編譯且保持一致；token-F1 則評估單次生成與參考的接近程度。一個模型可能在其中一項得分高、在另一項得分低，而這兩份文件都沒有任何內容允許將兩者並列解讀。

對於基準測試紀錄，誠實的總結是：MathForm-8B 的證據來自一篇有編譯器參與其中的論文，而 TwIL-LM3-Pro 的證據則來自一套有評分器參與其中的廠商測試框架，且沒有第三方用同一套評分規準跑過這兩者。任何把「88.06%」與「0.5092」並列、彷彿那是一條比分的頁面，都應被視為還沒讀過定義的頁面。

規格，並排對照

• 參數 — TwIL-LM3-Pro 3.66B 稠密版 對比 MathForm-8B 8B，大約是 2.2 倍大小。

• 基礎模型 — `ibm-granite/granite-4.2-3b` 對比 `Qwen/Qwen3-8B`。

• 訓練資料 — 一個合成的形式邏輯語料庫，涵蓋六個目標 vs FormalVerse，約 367,000 個已驗證的 Lean 4 範例。

• 獎勵 — 一種程式化驗證器，具備部分給分與寬鬆比對容錯，相對於 Lean 編譯與語意一致性回饋。

• 主要輸出 — 蘊含標籤、FOL 翻譯、語意剖析、Lean 陳述，以及對照供編譯器檢查的 Lean 4 陳述之證明評論。

• 上下文視窗 — TwIL-LM3-Pro 為 131,072 個 token，是在 8,192 個 token 內測得；MathForm-8B 在其自身的使用範例中，以最高達 16,384 個 token 的生成預算提供服務。

• 授權條款 — webAI 非商業授權條款 1.0 版 與 Apache 2.0。

• 量化佔用空間——TwIL-LM3-Pro 提供 2.09 GiB 的 Q4_K_M GGUF，可在 CPU 或 4 GB VRAM 上執行；MathForm-8B 則未在其自己的儲存庫中發布任何 GGUF。

許可證再次決定了生產問題。

MathForm-8B 採用 Apache 2.0 授權。你可以對其進行微調、重新發佈，並在商業產品中提供服務。TwIL-LM3-Pro 屬於非商業授權：允許研究與個人使用，而產生收益的部署則需與 webAI 另行簽訂協議；webAI 的商業途徑是企業合作安排，而非公開的價目表。

對於研究團隊或學生來說，這個差異無關緊要——兩者在 Hugging Face 上都是無限制下載。對於一家公司來說，這是決定性的，並且它指向 MathForm-8B，作為任何生產級自動形式化工作的選擇，無論哪個模型在一個兩家廠商都沒有以相同方式衡量的賽道上得分更高。

路由器在此流程中的位置

TwIL-LM3-Pro 與 MathForm-8B 都不是 OrcaRouter 目錄中的路由，而原因各不相同：前者採用非商業授權，且沒有代管端點；後者則是以開放檢查點的形式發佈，供自行託管之用。在形式化流程中，路由問題的關鍵其實在於它們外圍的那一層。一個相容 OpenAI 的端點，背後串接 200 多個模型，以供應商定價、加價 0% 提供，在這種情況下，替換不過是改一項設定，而生成模型若遇供應商降價，當天就能反映。自動容錯移轉在語料庫建置中之所以是關鍵支柱，正因為一項工作在生成回合進行到三分之二時中斷，就得賠上整輪的代價。

勞動分工

如果任務是把教科書數學大規模轉換成可編譯的 Lean 陳述，而且成果必須搭載於商業產品中推出，那麼 MathForm-8B 就是該工具，而 Apache 2.0 授權條款正是原因所在。如果任務是判斷一段文本是否蘊含某項主張、標註蘊含關係、解析語意，或評論某個證明嘗試，那麼 TwIL-LM3-Pro 涵蓋了 MathForm 從未瞄準的領域——而它的非商業授權條款是對該能力可用範圍的一道界線，並不是對該能力本身的負面評價。

合理的組合是兩階段流程，而不是二選一：一個模型產出形式化陳述，另一個對其進行評判。兩者都公開了產出它們的流程，這在這樣的規模下並不尋常，也是這次比較得以進行的原因。