OpenBMB 團隊近日釋出 MathForm-8B，一個專門用於數學自動形式化的 8B 引數模型，能夠將自然語言描述的數學命題轉換為 Lean 4 形式化程式碼。該模型基於 Qwen3-8B 底座，採用 Apache 2.0 許可開源，並隨附論文《MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement》。

MathForm-8B 的訓練資料來自團隊構建的 FormalVerse 資料集，訓練流程分為兩個階段：先進行監督微調，再通過強化學習最佳化，其中強化學習的獎勵訊號來自 Lean 編譯檢查和語義一致性反饋。這種“驗證引導”的機制旨在減少形式化過程中的錯誤，提高生成程式碼的可靠性。

在技術架構上，MathForm 系統整合了 Mathlib 知識檢索、編譯與語義驗證，以及迭代精煉三個環節，以生成高質量的形式化資料，隨後通過軌跡重建訓練出 MathForm-8B。論文報告了模型在六個基準上的 Pass@8 通過率（分別經過語法檢查和一致性檢查），並給出了平均成績，但摘要中未列出具體數值。

模型的使用方式較為靈活，支援 Transformers、vLLM 和 SGLang 三種推理框架，並可通過 OpenAI 相容 API 呼叫。官方推薦設定溫度為 0.6、top_p 為 0.95，最大生成長度為 16384 token。評估程式碼、基準檔案和指令碼均已公開在 MathForm 倉庫中，編譯檢查依賴 Kimina Lean Server，實驗基於 Lean 4.21.0。

從產業角度看，MathForm-8B 的釋出是自動形式化領域的一次開源嘗試，其“檢索+驗證”的範式可能為 AI 在數學推理、定理證明乃至安全關鍵程式碼生成方面提供新思路。對於關注 AI 模型應用層的投資者而言，這類模型展示了將大語言模型與形式驗證工具結合的可能性，或可推動 AI 在科研、教育等場景的落地，但當前仍處於研究階段，實際應用效果有待觀察。