MathForm Brings Retrieval and Verification into Mathematical Autoformalization

Introduction

Turning a natural-language statement such as “for every real number…” into Lean 4 is not merely a translation task. The model must identify the appropriate types, definitions, and library conventions in Mathlib, while ensuring that the resulting proposition still means what the original statement meant. MathForm addresses this broader problem by combining retrieval, machine verification, and iterative revision.

How the framework works

Many existing pipelines depend heavily on knowledge stored in model parameters. They often generate a formal statement once and retain it if the compiler accepts it. Compilation filtering can remove obvious errors, but it does not by itself solve incorrect library choices, type mismatches that require reformulation, or semantic drift. MathForm introduces a feedback loop with several stages:

• Retrieval before generation: A retrieval planner gathers relevant Mathlib definitions, type information, and existing formalizations before the generator writes Lean code.
• Compiler-guided revision: Generated statements are checked by the Lean compiler. Diagnostic messages are then used to guide subsequent corrections.
• Semantic-consistency feedback: The system also evaluates whether the formal statement remains faithful to the natural-language proposition, rather than treating compilation as the only notion of success.
• Verified data construction: Revised and checked examples are collected into FormalVerse, a Lean 4 dataset spanning multiple mathematical domains and sources.

The authors report approximately 367K verified examples in FormalVerse. They use the dataset for supervised fine-tuning followed by reinforcement learning, producing MathForm-8B.

Reported results

Across six benchmarks, MathForm-8B reaches an average Pass@8 of 88.06% under Syntax Check and 72.37% under Consistency Check. The paper reports that these results outperform multiple specialized 32B autoformalizers. On the more difficult FATE-H and FATE-X subsets, the model obtains Consistency Check pass rates of 63% and 37%, respectively, exceeding the strongest specialized baselines on both subsets.

The main contribution is therefore not simply a smaller model with competitive scores. MathForm treats three issues as parts of one workflow: acquiring library-specific knowledge, producing compilable formal code, and preserving the meaning of the source proposition. In formal mathematics, compilation is necessary but not sufficient. A statement can be accepted by a prover while still failing to capture the intended claim. Retrieval and revision offer a way to reduce that gap.

The supplied material does not include the full experimental protocol, baseline configurations, or details of human semantic evaluation, so the reported comparisons should be read alongside the complete paper. Still, the released code, model, and dataset provide practical starting points for reproduction. More broadly, MathForm points toward a data-generation paradigm in which mathematical models do not rely only on parametric memory, but improve under the combined constraints of a formal library and an interactive verifier.

Source: Hugging Face Daily Papers