MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
AuthorsLushi Pu, Weiming Zhang, Xinheng Xie, Zixuan Fu, Bingxiang He, Hengyu Zhao, Hongya Lyu, Xin Li, Jie Zhou, Yudong Wang
Resources
MathForm helps language models turn informal mathematics into reliable Lean proofs by retrieving library knowledge and repeatedly refining outputs against formal verification feedback.
Key results
Lean 4 natural-language-to-formalization pairs used for training
MathForm-8B average across six benchmarks
MathForm-8B average across six benchmarks
Pass@8 rate on the challenging abstract-algebra subset
Pass@8 rate on the most challenging subset
What the paper found
MathForm treats mathematical autoformalization as a retrieval-and-verification loop rather than one-shot translation into Lean 4. A retrieval planner uses OpenAI’s gpt-oss-120b to query Mathlib through LeanExplore for definitions, types, notation, and existing formalizations; generated statements are then compiled and checked for semantic fidelity, with compiler diagnostics and feedback from QwQ-32B guiding up to three refinement rounds. This process produces FormalVerse, a decontaminated dataset of approximately 367K verified natural-language-to-Lean pairs spanning competition mathematics through advanced algebra. Training Qwen3-8B with supervised fine-tuning and DAPO reinforcement learning yields MathForm-8B, which reaches average Pass@8 rates of 88.06% on Syntax Check and 72.37% on Consistency Check across six benchmarks, surpassing specialized 32B autoformalizers. The largest gains appear on abstract algebra: Consistency Check reaches 63% on FATE-H and 37% on FATE-X, exceeding the strongest specialized baselines by 10 and 12 percentage points. Ablations show retrieval and feedback-driven refinement are complementary, while reinforcement learning raises average Consistency Check from 66.53% after supervised fine-tuning to 72.37%, indicating that optimization against compilation and semantic-consistency rewards improves faithful formalization, not merely syntactic validity.
Original abstract
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.
Read the original paperMore in AI Reasoning
Browse all 39 papers →Knowing When Thinking Is Not Enough: Teaching Small Reasoning Models to Reason Beyond Their Parametric Knowledge
Chanuk Lee, Minki Kang, Sangwoo Park, Woongyeong Yeo, Jinheon Baek, Sung Ju Hwang
FlyBy teaches small reasoning models to recognize when more internal thinking will not help and instead ask a stronger model for missing knowledge.
On Language Drift during RLVR Post-Training
Michael Sullivan, Alexander Koller
RLVR can make reasoning models increasingly use strange internal languages, and preventing that drift may require sacrificing some performance.
Principled Thoughts for Latent Recursive LLM Systems
Fahd Seddik, Fatemeh Fard
REST teaches latent LLM agents to form more causal, minimal, separable, and stable internal thoughts, improving reasoning accuracy and interpretability.