MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

Hugging Face Daily Papers Papers
autoformalization mathematical-reasoning knowledge-retrieval verification lean4 fine-tuning dataset

Summary

MathForm introduces a framework for mathematical autoformalization using knowledge retrieval and verification-guided refinement, yielding the FormalVerse dataset and an 8B model that outperforms specialized baselines.

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.
Original Article
View Cached Full Text

Cached at: 08/19/26, 07:57 AM

Paper page - MathForm: Scaling Mathematical Autoformalization with Knowledge Retrieval and Verification-Guided Refinement

Source: https://huggingface.co/papers/2608.14221

Abstract

MathForm improves autoformalization by retrieving Mathlib knowledge and iteratively refining outputs with verification feedback, yielding a large verified dataset and a high-performing 8B model.

Autoformalizationis 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 asMathlib, 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, anautoformalizationframework for constructing verified training data throughMathlibknowledge retrieval andverification-guided iterative refinement. Before generation, aretrieval plannergathers relevant definitions and existing formalizations fromMathlibto guide the formalization generator. Generated statements are then revised usingcompiler diagnosticsandsemantic-consistency feedback. Using this framework, we constructFormalVerse, a Lean 4 dataset containing approximately 367K verified examples across diverse mathematical domains and sources. We then train MathForm-8B throughsupervised fine-tuningfollowed byreinforcement learning. Across six benchmarks, MathForm-8B achieves averagePass@8rates 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.

View arXiv pageView PDFGitHub3Add to collection

Get this paper in your agent:

hf papers read 2608\.14221

Don’t have the latest CLI?curl \-LsSf https://hf\.co/cli/install\.sh \| bash

Models citing this paper1

#### openbmb/MathForm-8B Text Generation• 8B• Updated2 days ago • 516 • 4

Datasets citing this paper1

#### openbmb/FormalVerse Viewer• Updated2 days ago • 367k • 162 • 6

Spaces citing this paper0

No Space linking this paper

Cite arxiv.org/abs/2608.14221 in a Space README.md to link it from this page.

Collections including this paper0

No Collection including this paper

Add this paper to acollectionto link it from this page.

Similar Articles

MathAtlas: A Benchmark for Autoformalization in the Wild

arXiv cs.AI

MathAtlas is a large-scale benchmark for autoformalization of graduate-level mathematics, containing ~52k theorems and definitions extracted from 103 textbooks, with a mathematical dependency graph of ~178k relations. Experiments show state-of-the-art models achieve at most 9.8% correctness, highlighting the difficulty.