MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
| Source: arXiv AI
Tags: mathematical AI, Lean 4, autoformalization, Mathlib, formal verification, FormalVerse
MathForm-8B, trained on FormalVerse (a new dataset of 367K verified Lean 4 examples), achieves 72.37% Pass@8 on mathematical autoformalization and outperforms specialized 32B models — showing that retrieval-guided training and verification-driven refinement can close the scale gap in formal mathematics.
Details
Autoformalization — translating natural-language math into machine-verifiable formal proofs in languages like Lean 4 — has historically required massive models because they must map concepts to the complex hierarchy of Mathlib's definitions and types. MathForm challenges this assumption with a smaller but better-trained model. The framework has three components: a retrieval planner that gathers relevant Mathlib definitions and existing formalizations before generation, a formalization generator that uses this context, and a verification-guided refinement loop that revises outputs using Lean compiler diagnostics and semantic consistency checks. This pipeline constructs FormalVerse: 367K verified Lean 4 examples across diverse mathematical domains and sources. MathForm-8B is trained on FormalVerse via supervised fine-tuning followed by RL. Across six benchmarks it achieves 88.06% Pass@8 under Syntax Check and 72.37% under Consistency Check — outperforming multiple specialized 32B models. On the harder FATE-H and FATE-X subsets it reaches 63% and 37% CC pass rates, exceeding the strongest 32B baselines. These results suggest that a well-designed data pipeline with retrieval augmentation and verification feedback can substitute for scale. The FormalVerse dataset itself is a contribution for the community.