OpenBMB把MathForm這套數學自動形式化方案整體開源：8B模型權重、約36.7萬筆已驗證的Lean 4資料集、評測程式碼與Pass@k腳本一併釋出。模型放在Hugging Face上，授權採用Apache 2.0，基礎模型是Qwen3-8B，權重精度為BF16。專案由清華大學自然語言處理實驗室與面壁智能(ModelBest)共同支持的OpenBMB團隊完成，同名論文已於本月中旬送交arXiv，作者共10人。
自動形式化指的是把自然語言寫成的數學命題，轉換成Lean 4這類機器可驗證的形式語言。難處不在字面翻譯。Mathlib的型別層級與定義體系極其龐大，一個命題裡的「連續函數」「有限群」必須精確對應到函式庫裡那個定義，同時要確保形式化之後的命題和原命題講的還是同一件事。這兩件事只要有一項出錯，編譯器仍有可能照樣放行。
資料是怎麼做出來的
MathForm的流程分四個步驟。規劃器先針對命題裡的數學概念查詢Mathlib，檢索工具LeanExplore每次回傳前22筆結果；模型在這批檢索內容的條件下生成Lean 4命題；候選依序經過格式檢查、編譯測試，再由大型模型擔任裁判做語意一致性判定；通過的路徑會被回溯重建成乾淨的訓練軌跡。
論文裡有個數字說明了反覆修正的必要性：後續回合貢獻了所有保留樣本中額外的31.0%。也就是說，如果只做單一輪次生成、不合格就直接丟棄，接近三分之一的可用資料會白白流失。
檢索這一步是整套方案裡最省成本的設計。要模型單靠記憶去回想Mathlib裡某個定義的精確名稱與簽章，本質上是在考它有沒有背下一個還在持續更新的函式庫。把函式庫交給檢索工具、只讓模型負責組裝，所需的參數量自然就降下來了。這也說明了為什麼8B能和32B較量：兩邊比的根本不是同一件事。
產出的資料集叫做FormalVerse，約有36.7萬筆已驗證樣本，來源橫跨DeepTheorem、NuminaMath、AceReason-Math、Lean Workbook、Principia-Collection、DeepMath、OpenR1-Math，再補上經典教科書內容。這份資料集在Hugging Face上已經拿到358個讚。
成績單與它的兩種讀法
訓練路徑是先做監督式微調，再接強化學習。評測涵蓋六個基準：FormalMATH-Lite與DeepSeek-ProverBench走競賽數學路線，CombiBench測組合數學，FATE系列則依代數難度分成M、H、X三個等級。
MathForm-8B的語法檢查平均Pass@8為88.06%，一致性檢查平均為72.37%；FATE三個等級的一致性通過率依序為97.33%、63.00%與37.00%。對照組包括Herald Translator-7B、Kimina-Autoformalizer-7B、Mathesis-HPO-7B，以及StepFun-Formalizer、Goedel-Formalizer-V2、ReForm各自的7B/8B與32B版本。8B在多項測試集上超越了32B專用形式化模型。
兩種指標之間的落差，比絕對分數本身更有意思。語法檢查只問編譯過不過，一致性檢查問的則是形式化後的命題和原題是不是同一個意思——88%對72%，中間那十幾個百分點，正是這條產線目前真正的瓶頸所在。編譯得過，不代表就是你想證明的那條定理。
門檻降到了一台工作站的等級
本站先前寫過陶哲軒的警告：AI產出的證明會多到沒人讀得完。形式化恰好是這個問題的另一半答案——只要證明能通過Lean編譯器，讀不讀得懂就不再是接受它的前提。前提是命題本身要翻對，FATE-X上37%這個數字說明，離這一步還有不小的距離。
粗略估算，8B模型以BF16載入大約需要16GB顯示卡記憶體，32B同精度則要64GB上下。前者一張24GB的消費級顯卡就能跑起來，後者得靠多卡或專業級顯卡。對大學數學系、證明輔助工具社群和小型團隊來說，跑一條形式化流程的硬體門檻，從叢集等級掉到了單機等級。資料集與評測腳本同步開源，別人要複現或挑毛病，成本也跟著降下來。
對照表裡那一排名字，也說明了這個賽道現在有多擁擠：Herald、Kimina、Mathesis、StepFun-Formalizer、Goedel-Formalizer-V2、ReForm，全是近一兩年冒出來的專用形式化模型，而且清一色開源。形式化不像通用對話那樣靠燒算力拉開差距，比的是資料建構的功夫和驗證迴圈的完整度，參數規模在這裡反而成了次要變數。從論文展示推進到能開源交付，這個節奏比多數人預期得快。
參考來源：OpenBMB專案儲存庫與模型卡、CocoLoop、arXiv預印本2608.14221、Hugging Face資料集頁面；已核實參數規模、授權條款、FormalVerse樣本量與各測試集Pass@8計算口徑。