MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement
MathForm-8B beats larger specialized autoformalizers by pairing Mathlib retrieval with verifier-driven revision.
The framework retrieves relevant Mathlib definitions and prior formalizations before generating Lean 4 statements, then revises outputs using compiler diagnostics and semantic-consistency feedback. The authors use it to build FormalVerse, a dataset of about 367,000 verified Lean 4 examples. After supervised fine-tuning and reinforcement learning, MathForm-8B reaches average Pass@8 rates of 88.06% under syntax check and 72.37% under consistency check across six benchmarks. On FATE-H and FATE-X, it reports consistency-check pass rates of 63% and 37%. HF Daily Papers' note
The framework retrieves relevant Mathlib definitions and prior formalizations before generating Lean 4 statements, then revises outputs using compiler diagnostics and semantic-consistency feedback. The authors use it to build FormalVerse, a dataset of about 367,000 verified Lean 4 examples. After supervised fine-tuning and reinforcement learning, MathForm-8B reaches average Pass@8 rates of 88.06% under syntax check and 72.37% under consistency check across six benchmarks. On FATE-H and FATE-X, it reports consistency-check pass rates of 63% and 37%. HF Daily Papers' note
score 5