MathForm：利用知識檢索與驗證引導精化擴展數學自動形式化

摘要

自動形式化通常被描述為將自然語言數學陳述轉換為機器可驗證的形式語言（如 Lean 4）的過程。然而，忠實的形式化不僅僅是翻譯。模型必須將數學概念映射到形式化程式庫（如 Mathlib）中複雜的類型與定義階層，同時確保生成的陳述保留原始命題的意義。現有方法之所以困難，是因為它們高度依賴模型的參數化記憶來獲取程式庫特定知識，而常見的資料建構流程往往僅對單次輸出進行篩選，缺乏回饋驅動的修訂機制。為了解決這些挑戰，我們提出了 MathForm，這是一個自動形式化框架，透過 Mathlib 知識檢索與驗證引導的迭代精煉來建構經過驗證的訓練資料。在生成之前，檢索規劃器從 Mathlib 收集相關定義與現有形式化，以引導形式化生成器。隨後，生成的陳述會利用編譯器診斷訊息與語義一致性回饋進行修訂。利用此框架，我們建構了 FormalVerse，這是一個 Lean 4 資料集，包含來自不同數學領域與來源的約 367,000 個已驗證範例。接著，我們透過監督式微調與後續的強化學習來訓練 MathForm-8B。在六個基準測試中，MathForm-8B 在語法檢查（SC）下的平均 Pass@8 率達到 88.06%，在一致性檢查（CC）下達到 72.37%，優於多個專門化的 32B 自動形式化模型。在具有挑戰性的 FATE-H 與 FATE-X 子集上，其 CC 通過率分別達到 63% 與 37%，在兩種情況下均超過最強的專門化基準模型。

English

Autoformalization is commonly framed as translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4. However, faithful formalization requires more than translation. Models must map mathematical concepts to the complex hierarchy of types and definitions in formal libraries such as Mathlib, while ensuring that generated statements preserve the meaning of the source propositions. Existing approaches struggle because they rely heavily on the model's parametric memory for library-specific knowledge, while common data construction pipelines often resort to filtering single-pass outputs and lack mechanisms for feedback-driven revision. To address these challenges, we introduce MathForm, an autoformalization framework for constructing verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Before generation, a retrieval planner gathers relevant definitions and existing formalizations from Mathlib to guide the formalization generator. Generated statements are then revised using compiler diagnostics and semantic-consistency feedback. Using this framework, we construct FormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B through supervised fine-tuning followed by reinforcement learning. Across six benchmarks, MathForm-8B achieves average Pass@8 rates of 88.06% under Syntax Check (SC) and 72.37% under Consistency Check (CC), outperforming multiple specialized 32B autoformalizers. On the challenging FATE-H and FATE-X subsets, it attains CC pass rates of 63% and 37%, exceeding the strongest specialized baselines in both cases.