Lushi Pu, Weiming Zhang, Xinheng Xie, Zixuan Fu, Bingxiang He, Hengyu Zhao, Hongya Lyu, Xin Li, Jie Zhou, Yudong Wang
5 min
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.
Sam: So retrieval isn't just background context. It can actively fix a mistake that compilation alone would never catch.
Alex: Exactly. And that distinction — between "does it compile" and "does it mean the right thing" — is what makes the two checkers doing different jobs so useful. They catch different kinds of errors.
Sam: Where does the training data come into this?
Alex: So using this pipeline, the authors build a large dataset of verified Lean 4 examples — examples that have already survived both kinds of checking. They call it FormalVerse. That dataset is then used to train a model called MathForm-8B. The idea is that the model learns from outputs the pipeline itself can trust, rather than from raw guesses.
Sam: So the pipeline produces good examples, and those examples teach the model to do better on its own.
Alex: That's the idea. The paper describes it as a kind of co-evolution: the pipeline generates checked examples, and those examples help train a stronger model that can eventually handle more in a single pass. You're trying to compress a careful multi-step process into something the model internalizes.
Sam: Did that actually help on harder problems?
Alex: The evidence points that way. On the more difficult benchmarks — particularly in algebra, where Lean's type structure and existing library formalizations matter most — the full method outperformed simpler approaches. Human reviewers also confirmed the same overall ranking, which matters because it suggests the improvement wasn't just an artifact of one automatic checker being easy to fool.
Sam: What are the limits? Where does this still struggle?
Alex: The sober takeaway is that the approach depends heavily on good retrieval and good checking. If the library search misses the right concept, or if the original statement is genuinely ambiguous, the pipeline can still produce an incorrect formalization. It's not a solution to every problem — it's a meaningful reduction in avoidable mistakes.
Sam: So it's less about replacing human judgment and more about building a system that fails less often on the kinds of errors that are preventable.
Alex: That's a fair summary. The contribution is a careful way to connect informal mathematics, library knowledge, and verified Lean output — and to use that connection both to build better training data and to train a stronger model. It's a practical step forward, and an honest one about where the limits still are. Thanks for listening to ResearchPod.