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

The Core Challenge

Turning mathematical statements written in English into machine-verifiable code (like Lean 4) is harder than simple translation. The problem isn't just rewording—it's mapping informal math concepts to a library's complex type system and definitions while preserving meaning. Existing models fail because they try to memorize library details internally and lack feedback mechanisms to catch errors. The result: brittle systems that can't scale.

How MathForm Works

The authors introduce a two-stage pipeline that treats formalization as a guided retrieval and refinement problem rather than pure generation.

Stage One: Retrieval-Guided Generation. Before attempting formalization, a "retrieval planner" queries Mathlib (the formal mathematics library for Lean 4) to pull relevant type definitions, lemmas, and existing formalizations. This external knowledge—rather than relying on what the model memorized—is passed to a 8-billion-parameter generator as context. Think of it like giving a translator a reference manual before translating a document.

Stage Two: Verification-Guided Refinement. Generated Lean code almost never works on the first pass. Instead of discarding failures, MathForm iteratively revises using two feedback signals: (1) compiler diagnostics (syntax and type errors), and (2) semantic-consistency checks (does the formalized statement match the original meaning?). This loop continues until either the code verifies or iterations exhaust—creating a feedback-driven pipeline that mirrors how humans debug proofs.

The authors used this framework to build FormalVerse, a dataset of ~367K verified Lean 4 examples across diverse math domains. They then trained MathForm-8B via supervised fine-tuning on this data, followed by reinforcement learning to maximize verification success.

Why It Matters

The results are striking: an 8-billion-parameter model outperforms specialized 32-billion-parameter baselines. Under "Syntax Check" (does the code parse?), MathForm-8B achieves 88% Pass@8. Under "Consistency Check" (is the meaning preserved?), it reaches 72%—the harder metric that measures true correctness. On extremely difficult benchmarks (FATE-H and FATE-X subsets), it hits 63% and 37% consistency, exceeding all prior baselines.

This matters because autoformalization unlocks a bottleneck in formal mathematics: bridging the gap between the informal proofs mathematicians write and the machine-checked proofs needed for absolute certainty. At scale, verified formalizations could accelerate proof verification and enable new kinds of mathematical AI systems.

The key insight is architectural: retrieval + iterative refinement beats memorization + single-pass generation. By treating the formal library as an external knowledge source and treating errors as teaching signals, the approach scales more efficiently and generalizes better than prior work. The framework itself—beyond this specific model—suggests how to build other autoformalization systems with better feedback loops.