Search papers, labs, and topics across Lattice.
This paper introduces MathForm, an innovative framework for autoformalization that enhances the translation of natural-language mathematical statements into machine-verifiable formal languages by integrating knowledge retrieval and verification-guided refinement. By leveraging a retrieval planner to gather relevant definitions from Mathlib and employing iterative feedback for revision, MathForm constructs a comprehensive dataset, FormalVerse, containing 367K verified examples. The results show that MathForm-8B significantly outperforms existing specialized models, achieving high pass rates on various benchmarks, particularly in challenging subsets like FATE-H and FATE-X.
MathForm-8B not only outperforms specialized autoformalizers but also sets a new standard for verified mathematical formalization with an impressive 88.06% pass rate on syntax checks.
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.
