MathForm讓8B勝32B

一套名為 MathForm 的自動形式化框架近期在人工智慧與數學符號處理領域引發關注。該框架透過結合知識檢索與反覆迭代修訂機制，成功讓僅有 8B 參數的輕量級模型，在多項標準化測試中表現超越多個參數規模達 32B 的專用模型。這項成果挑戰了長久以來「參數愈大、效能愈好」的直覺，也為資源受限的環境下發展高效能數學推理模型提供了全新路徑。根據開發團隊公布的技術細節，MathForm 的運作流程始於對 Mathlib 數學知識庫的檢索。Mathlib 是一個以 Lean 4 形式化驗證語言所建構的開源數學定理集合，內容涵蓋從基礎代數到高等分析的大量已驗證命題。

MathForm 並不直接從零開始生成數學敘述，而是先從 Mathlib 中擷取與目標問題相關的既有形式化內容，作為後續生成與修正的基礎。接著，MathForm 採用兩道校驗機制進行反覆修正：編譯診斷（compilation diagnostics）與語義一致性（semantic consistency）。編譯診斷指的是讓模型產出的 Lean 4 程式碼通過編譯器檢查，若出現錯誤訊息則回饋給模型重新調整；語義一致性則確保最終生成的形式化敘述在邏輯上與原始問題對應，避免產生表面正確但實質無關的答案。透過這兩階段的不斷迭代，MathForm 最終建構出約 36.

7 萬條經 Lean 4 編譯器驗證的高品質訓練樣本。這批樣本隨後被用來微調一個基於 Mistral 架構的 8B 參數語言模型，最終產出的模型稱為 MathForm-8B。在評估階段，研究團隊選用了六個不同的基準測試，這些測試都針對語法檢查（Syntax Check）任務設計，要求模型判斷一段 Lean 4 程式碼是否合乎語法規則，並進一步辨識其形式正確性。結果顯示，MathForm-8B 在六項基準的平均分數達到 88.06%，明顯優於多個參數規模高達 32B 的專用模型。

這些 32B 參數的對比模型包括學術界近期推出的幾款專為數學形式化而訓練的大型語言模型，例如某些以 DeepSeek 架構為基礎、參數量達 32B 的版本。儘管這些模型擁有四倍於 MathForm-8B 的參數，但在 Syntax Check 這類需要精確理解形式化語法的任務上，MathForm-8B 仍以顯著差距領先。這項對比凸顯了「資料品質與訓練流程設計」有時比單純擴大模型規模更具影響力。研究團隊進一步指出，MathForm 的成功關鍵在於「形式化驗證資料的閉環反饋」。傳統的語言模型訓練往往依賴人類標註或從網路爬梳的自然語言文本，這類資料容易帶有模糊性與不一致性。

而 Lean 4 編譯器提供的明確錯誤訊息與 Verdict，則使得模型能在每一次迭代中獲得絕對正確的校驗信號，進而快速收斂出高可靠度的數學表達能力。值得注意的是，MathForm 並非從無到有創造新的數學知識，而是專注於將既有的自然語言數學問題轉譯為嚴格的形式化證明程式碼。這個能力對於自動定理證明、智慧型輔助教學系統，以及大型數學軟體的形式化驗證都具有直接應用價值。當前的結果僅限於語法檢查任務，但團隊表示已著手將相同框架延伸至證明完整性的評估，預計後續會公布更多跨任務的測試成果。在學術界，形式化數學一直面臨「高品質資料稀缺」的瓶頸。

即使像 Mathlib 這樣的大型知識庫，其中可供監督學習的完整形式化樣本數量仍遠小於自然語言文本。MathForm 以知識檢索搭配迭代修正的策略，相當於利用少量初始資料加上自動化校驗，自行擴增出數十萬條可靠樣本，這套做法可望被複製到其他形式化語言或特殊領域（如物理學、密碼學）的符號處理模型訓練上。從硬體成本角度來看，訓練一個 8B 參數模型所需的 GPU 記憶體與功耗遠低於訓練 32B 甚至 70B 的模型。這使得中小型研究團隊或缺乏大型算力資源的機構，也能夠嘗試開發具有競爭力的數學推理模型。

MathForm-8B 的展示，等於為 AI for Math 領域的「輕量級方案」背書，未來或許會有更多類似框架出現，以較低的資源門檻達成高水準的形式化驗證能力。此外，這項研究也再次凸顯了 Lean 4 生態系在人工智慧訓練中的獨特價值。Lean 4 不僅是一種證明輔助工具，它所內建的嚴格型別系統與編譯器診斷機制，恰好能為機器學習提供近乎無雜訊的監督訊號。研究者可以將 Lean 4 視為一個「可程式化的數學裁判」，讓模型在不斷試錯中學會正確的數學語言表達，而非僅是模仿人類書寫的統計模式。

目前 MathForm 的相關程式碼與模型權重尚未完全公開，但開發團隊表示將在近期整理後開源，以便社群重現結果並進行改善。若後續更多研究能驗證這套框架在不同數學分支與不同尺寸模型上的通用性，那麼 MathForm 很可能成為「用小模型做大事」的經典案例，並推動形式化資料自動生成技術的標準化。總結來看，MathForm 的問世象徵著一個重要轉折：在數學符號處理這類高度結構化的領域，參數規模不再是唯一的主導因素。透過精準的知識檢索、迭代修正與編譯器驗證，一個僅 8B 參數的模型也能在特定任務上壓過體型四倍於己的專用系統。

這條路徑若能順利擴展，將大幅降低頂級數學 AI 的進入門檻，並讓更多研究者參與形式化數學的自動化進程。