MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

Summary

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 concepts to the complex hierarchy of types and definitions in formal libraries like Mathlib. Existing approaches struggle because they rely heavily on parametric memory and lack feedback-driven revision. To address this, we introduce MathForm, a framework that constructs verified training data through Mathlib knowledge retrieval and verification-guided iterative refinement. Using this framework, we build FormalVerse, a Lean 4 dataset with approximately 367K verified examples, and train MathForm-8B via supervised fine-tuning and 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.