在現代數學與人工智能的交叉領域中，如何讓機器準確“讀懂”並通過形式化驗證數學定理，一直是攻克通用人工智能（AGI）的核心挑戰之一。OpenBMB團隊近日正式開源了全新的數學自動形式化開源框架、數據集與模型——MathForm。

長期以來，數學形式化（例如基於 Lean4語言）不僅是把自然語言翻譯成代碼那麼簡單。一個嚴謹的模型必須將每一個數學概念精準映射到 Mathlib 庫中正確的類型和定義上。行業內常常面臨一個痛點:形式化語句即使能夠順利通過編譯器編譯，也可能在語義上無法準確描述原始問題。

image.png

爲了攻克這一難題，MathForm 框架創新性地引入了檢索增強與驗證引導的數據構建機制。其核心邏輯在於，系統首先會通過檢索規劃器提取語句所需的 Mathlib 定義和現有形式化模型;隨後，生成器會根據 Lean 編譯器的診斷結果以及語義一致性反饋，對輸出內容進行最多三輪的修正，從而大幅保障了代碼質量與數學語義的統一。

在數據與模型層面，OpenBMB 推出了包含超過36.7萬個已驗證 Lean4示例的 FormalVerse 數據集，涵蓋了多元化的數學領域和來源。實驗結果表明，在同等訓練預算和初始條件下，基於 FormalVerse 訓練的模型一致性檢查率達到了60.32%，遠超 FineLeanCorpus 的46.53% 和 NuminaMath-LEAN 的41.49%。

作爲核心成果之一，MathForm-8B 模型在六項基準測試中交出了亮眼答卷，實現了88.06% 的語法檢查通過率和72.37% 的一致性檢查通過率（8分制）。尤爲引人注目的是，它以僅爲對手四分之一的參數體量，反超了 ReForm-32B 和 Goedel-Formalizer-V2-32B 等更大體量的模型。特別是在難度最高的 FATE-H 和 FATE-X 子集中，其一致性檢查成功率分別達到了63% 和37%，比最強的專項基準分別高出10和12個百分點，展現出極強的推理與形式化糾錯能力。

項目地址:https://github.com/openbmb/MathForm