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

> MathForm's retrieval-augmented, verification-guided iterative refinement framework produces an 8B model that outperforms 32B baselines, achieving 72.37% average semantic consistency on autoformalization benchmarks.

- **Source:** [arXiv](https://arxiv.org/abs/2608.14221)
- **Published:** 2026-08-29
- **Permalink:** https://picx.dev/p/jGff22
- **Whiteboard:** https://picx.dev/p/jGff22/image

## Summary

## Summary (Overview)

- **MathForm** introduces a knowledge-augmented autoformalization framework that combines Mathlib knowledge retrieval with compiler- and semantics-guided iterative refinement, moving beyond reliance on parametric memory for translating natural-language mathematics into Lean 4 formal statements.
- The framework is used to construct **FormalVerse**, a large-scale Lean 4 dataset containing approximately **367K verified examples** spanning diverse mathematical domains and problem sources.
- The resulting **MathForm-8B** model, trained via supervised fine-tuning (SFT) followed by reinforcement learning (RL), achieves average **Pass@8 rates of 88.06% under Syntax Check (SC)** and **72.37% under Consistency Check (CC)** across six benchmarks, outperforming multiple specialized 32B autoformalizers.
- On the challenging FATE-H and FATE-X subsets, MathForm-8B attains CC pass rates of **63% and 37%**, exceeding the strongest specialized baselines by 10 and 12 percentage points respectively.
- Ablations demonstrate that knowledge retrieval, verification-guided iterative refinement, and reinforcement learning each contribute meaningfully to the final performance, with gains concentrated on high-abstraction statements requiring deep Mathlib knowledge.

---

## Introduction and Theoretical Foundation

### Background and Motivation

Autoformalization—translating natural-language mathematical statements into machine-verifiable formal languages such as Lean 4—is a critical bottleneck for scaling formal theorem proving. While systems like AlphaProof, DeepSeek-Prover-V2, and Goedel-Prover-V2 have advanced formal proof generation, they require large corpora of machine-checkable statements that remain scarce. Much mathematical knowledge exists only in natural language, and manual formal encoding demands both precise mathematical interpretation and expertise with proof assistants.

### Two Key Limitations of Existing Approaches

1. **Over-reliance on parametric memory**: Existing methods (e.g., TheoremLlama, Herald, Kimina-Autoformalizer, Mathesis) depend primarily on knowledge stored in model parameters. However, formalization in Lean requires familiarity with Mathlib's definitions, type system, notational conventions, and existing structures—knowledge that is highly specific and evolves as the library develops, making it difficult to fully internalize in model parameters.

2. **Best-of-N (BoN) filtering without feedback**: Many existing data-construction pipelines adopt a Best-of-N strategy where a model samples a large pool of candidates and a discriminator filters post hoc. This approach:
   - Merely selects from the model's existing output distribution
   - Cannot indicate *where* semantic deviations occur or *how* to repair them
   - Caps data difficulty at the model's current single-pass capability

### Theoretical Perspective

The authors argue that faithful formalization is better understood as a **knowledge-grounded process that converges through repeated verification**, rather than a one-shot translation judged after the fact. Because a single mathematical object may correspond to a complex hierarchy of types and definitions in Mathlib, a plausible-looking statement can compile yet still strengthen a condition or drop a key assumption—rendering it useless downstream.

---

## Methodology

### 3.1 Autoformalization Framework

#### 3.1.1 Problem Collection and Normalization

Problems are collected from diverse natural-language mathematics datasets including:
- **DeepTheorem**, **NuminaMath**, **AceReason-Math**, **Lean Workbook**, **Principia-Collection**, **DeepMath**, **OpenR1-Math**
- Supplemented with theorems and exercises from classical mathematics textbooks

Non-mathematical content, purely numerical computation exercises, and problems that cannot be naturally expressed as theorem statements are filtered out. Redundant answer-format instructions or extraneous context are rewritten.

#### 3.1.2 Knowledge Retrieval and Formalization Generation

The pipeline consists of two components:

- **Retrieval Planner**: Analyzes the mathematical objects, relations, and type constraints in a natural-language statement, and judges whether additional Mathlib knowledge is needed. When needed, it issues targeted queries and collects relevant definitions, theorems, notations, and existing formalizations from Mathlib via **LeanExplore** (top-2 results per query).
- **Formalization Generator**: Conditions on both the original statement and retrieved results, identifies the corresponding Mathlib types and definitions, and produces the Lean 4 formal statement.

Both modules are driven by **gpt-oss-120b** for fast, inexpensive inference. Separating retrieval planning from code generation reduces reliance on parametric memory.

#### 3.1.3 Verification-Guided Iterative Refinement

The generation loop proceeds as follows:

1. **Format Check**: Discards outputs containing proof steps, tactics, or solution procedures beyond the formal statement itself.
2. **Compilation**: Candidates are compiled with Lean 4; failures are recorded with compiler diagnostics (syntax errors, undeclared identifiers, missing dependencies, type mismatches).
3. **Semantic Consistency Check**: Successfully compiled candidates are assessed by **QwQ-32B** as judge, flagging errors such as omitted assumptions, strengthened/weakened conditions, incorrect quantifier order, extraneous constraints, and mismatched conclusions.

Each sample undergoes at most **three rounds**; generation stops as soon as a candidate passes both checks. The first round yields ~69% of all retained pairs, with the second and third rounds adding ~20% and ~11% respectively—recovering **31% of data** that single-pass generation would not have produced.

#### 3.1.4 Trajectory Reconstruction

Since raw trajectories span multiple rounds with interleaved retrieved context, compiler errors, and failed attempts (unsuitable as training targets), the authors synthesize a **clean, structured formalization trajectory** for each verified pair. The model reconstructs the intermediate analysis mapping the natural-language statement to its Lean 4 formalization, explicitly excluding proof strategies and problem-solving procedures.

#### 3.1.5 Data Decontamination

Training data is decontaminated against all evaluation benchmarks by removing any example sharing at least one **13-gram** with an evaluation example.

### 3.2 Training MathForm-8B

#### 3.2.1 Supervised Fine-Tuning

SFT is performed on **Qwen3-8B** using the **LLaMA-Factory** framework, training the model to identify mathematical objects, logical structures, variable dependencies, and implicit type constraints.

#### 3.2.2 RL Data Selection

RL data consists of ~20,000 statements that **never passed validation** during iterative refinement (unsolved by the construction pipeline). After offline difficulty filtering and removing ambiguous statements, **3,000 examples** remain.

#### 3.2.3 Reward Function

Training uses **DAPO (Decoupled Clip and Dynamic sAmpling Policy Optimization)** with the verl framework. The token-level objective is:

$$
J_{\mathrm{DAPO}}(\theta) = \mathbb{E} \left[ \frac{1}{\sum_{i=1}^{G} |y_i|} \sum_{i=1}^{G} \sum_{t=1}^{|y_i|} \min \left(\rho_{i,t} A_i, \operatorname{clip}\left(\rho_{i,t}, 1 - \epsilon_{\text{low}}, 1 + \epsilon_{\text{high}}\right) A_i\right) \right].\tag{1}
$$

where $\rho_{i,t}$ is the token-level policy ratio and $A_i$ the group-normalized advantage.

The binary reward jointly considers compilation success and semantic consistency:

$$
r(x, y) = \left\{ \begin{array}{ll} 1, & C(y) = 1 \text{ and } S(x, y) = 1, \\ 0, & \text{otherwise}. \end{array} \right.\tag{2}
$$

where $C(y)$ denotes Lean 4 compilation success and $S(x,y)$ the semantic-consistency judgment from gpt-oss-20b.

---

## Empirical Validation / Results

### 4.1 Benchmarks and Evaluation

**Benchmarks**: FormalMATH-Lite, DeepSeek-ProverBench (ProverBench), CombiBench, and the FATE series (FATE-M, FATE-H, FATE-X)—covering competition mathematics, combinatorics, and algebraic reasoning from elementary abstract algebra to advanced commutative algebra, homological algebra, and foundations of algebraic geometry.

**Evaluation Protocol**: Pass@k rates with k=8, temperature 0.6, under two criteria:

$$
\begin{array}{l} \text{SC@k(x) = }\max_{1\leq i\leq k} C(y_{i}), \\ \text{CC@k(x) = }\max_{1\leq i\leq k} C(y_{i})S(x,y_{i}). \end{array}\tag{3}
$$

### 4.2 Main Results

**Table 1: Pass@8 pass rates (%) under SC and CC for specialized autoformalizers**

| Model | AVG SC | AVG CC | FormalMATH SC/CC | ProverBench SC/CC | CombiBench SC/CC | FATE-M SC/CC | FATE-H SC/CC | FATE-X SC/CC |
|---|---|---|---|---|---|---|---|---|
| Herald Translator-7B | 64.12 | 27.63 | 95.29/47.76 | 78.74/37.36 | 77.00/5.00 | 70.67/54.67 | 42.00/15.00 | 21.00/6.00 |
| Kimina-Autoformalizer-7B | 73.20 | 34.37 | 99.29/76.24 | 96.55/56.32 | 95.00/16.00 | 77.33/44.67 | 43.00/8.00 | 28.00/5.00 |
| Mathesis-HPO-7B | 76.20 | 34.96 | 99.06/79.29 | 97.13/59.77 | 96.00/15.00 | 84.00/48.67 | 50.00/4.00 | 31.00/3.00 |
| StepFun-Formalizer-7B | 58.12 | 39.55 | 97.41/81.41 | 89.66/59.20 | 79.00/28.00 | 60.67/52.67 | 17.00/12.00 | 5.00/4.00 |
| StepFun-Formalizer-32B | 63.65 | 44.47 | 99.06/85.88 | 92.53/64.94 | 86.00/32.00 | 71.33/60.00 | 23.00/17.00 | 10.00/7.00 |
| Goedel-Formalizer-V2-8B | 78.24 | 60.08 | 98.82/94.12 | 98.28/89.66 | 89.00/42.00 | 87.33/82.67 | 62.00/44.00 | 34.00/8.00 |
| Goedel-Formalizer-V2-32B | 78.28 | 63.74 | 99.06/94.59 | 98.28/92.53 | 91.00/49.00 | 89.33/85.33 | 63.00/48.00 | 29.00/13.00 |
| ReForm-8B | 81.76 | 66.21 | 99.06/94.12 | 98.85/90.80 | 86.00/47.00 | 94.67/91.33 | 67.00/53.00 | 45.00/21.00 |
| ReForm-32B | 81.61 | 68.41 | 99.06/95.53 | 98.28/94.25 | 93.00/55.00 | 91.33/88.67 | 69.00/52.00 | 39.00/25.00 |
| **MathForm-8B-SFT** | 84.38 | 66.53 | 99.29/91.06 | 100.00/90.80 | 83.00/43.00 | 98.00/91.33 | 80.00/58.00 | 46.00/25.00 |
| **MathForm-8B** | **88.06** | **72.37** | **100.00/95.06** | **100.00/94.83** | 93.00/47.00 | **99.33/97.33** | **82.00/63.00** | **54.00/37.00** |

**Key findings**:
- MathForm-8B achieves the best average SC (88.06%) and CC (72.37%) pass rates, with absolute gains of **6.45 and 3.96 percentage points** over ReForm-32B (81.61/68.41).
- RL raises average SC from 84.38% to 88.06% and CC from 66.53% to 72.37%; the larger CC gain indicates improved semantic alignment beyond compilability.
- Gains concentrate on high-abstraction statements: on FATE-X, MathForm-8B exceeds the strongest baseline by **12 percentage points** in CC.

### 4.3 Ablation Studies

#### 4.3.1 Refinement Pipeline Ablation

**Table 2: Ablation results on FATE series with two generators**

| Method | AVG SC/CC (gpt-oss-120b) | AVG SC/CC (Qwen3-235B) |
|---|---|---|
| Single | 27.33/26.43 | 7.43/7.43 |
| BoN (N=3) | 42.67/41.10 | 18.77/18.77 |
| Feedback-only | 42.57/40.77 | 28.77/28.77 |
| Retrieval-only | 32.23/29.00 | 9.90/8.57 |
| **MathForm (full)** | **49.67/48.00** | **37.57/36.23** |

The full pipeline yields additional gains of **7.00/6.90** (gpt-oss-120b) and **8.80/7.46** (Qwen3-235B) SC/CC percentage points over the strongest single-component configuration, demonstrating that retrieval and refinement are complementary.

#### 4.3.2 Data Quality Comparison

**Table 3: Models trained on different datasets (Qwen3-8B, 100K examples)**

| Training Dataset | AVG SC/CC | FormalMATH CC | ProverBench CC | CombiBench CC | FATE-M CC | FATE-H CC | FATE-X CC |
|---|---|---|---|---|---|---|---|
| NuminaMath-LEAN | 66.24/41.49 | 85.18 | 72.41 | 25.00 | 49.33 | 16.00 | 1.00 |
| FineLeanCorpus | 78.25/46.53 | 84.47 | 74.71 | 29.00 | 68.00 | 17.00 | 6.00 |
| **FormalVerse** | 77.17/**60.32** | **90.59** | **89.66** | **36.00** | **84.67** | **46.00** | **15.00** |

FormalVerse attains the highest average CC pass rate (60.32%), exceeding FineLeanCorpus by **13.79** and NuminaMath-LEAN by **18.83** percentage points, and ranks first in CC on **every** benchmark. The difference lies almost entirely in semantic fidelity rather than compilability.

#### 4.3.3 Judge-Model Reliability

**Table 4: Judge-model reliability on human-annotated test set (Mean@3)**

| Judge Model | Accuracy | Precision | Recall | F1 |
|---|---|---|---|---|
| gpt-oss-120b | **0.8917** | **0.8755** | **0.9133** | **0.8940** |
| QwQ-32B | 0.8567 | 0.8367 | 0.8867 | 0.8609 |
| gpt-oss-20b | 0.8500 | 0.8142 | 0.9067 | 0.8579 |

---

## Theoretical and Practical Implications

### Theoretical Implications

1. **Autoformalization as a process, not a one-shot translation**: The results validate the view that faithful formalization is a knowledge-grounded, iterative process converging through repeated verification—challenging the prevailing Best-of-N paradigm.

2. **Parametric memory is insufficient**: The strong gains on high-abstraction domains (FATE series) demonstrate that retrieval-augmented formalization is essential for statements requiring deep Mathlib type-hierarchy knowledge that cannot be fully internalized in model parameters.

3. **Data–model co-evolution**: Training on data produced by the full pipeline (including refinement rounds) compresses the pipeline's capability into the model's single-pass generation, realizing a form of capability transfer from the construction pipeline to the model.

### Practical Implications

1. **Scaling formal data construction**: The framework enables reliable large-scale NL-to-Lean data construction (367K verified examples) that would be infeasible with manual formalization or single-pass generation alone.

2. **Compact models can compete**: An 8B model outperforms multiple specialized 32B autoformalizers, demonstrating that high-quality training data can compensate for model scale.

3. **Verification-driven RL**: The binary reward jointly considering compilability and semantic consistency provides an effective learning signal that improves semantic alignment beyond what compilation alone can achieve.

---

## Conclusion

### Main Takeaways

- **MathForm** combines Mathlib knowledge retrieval with compiler- and semantics-guided iterative refinement, enabling reliable autoformalization data construction beyond parametric memory.
- **FormalVerse** provides ~367K verified Lean 4 examples spanning diverse mathematical domains—a significant resource for the community.
- **MathForm-8B** achieves state-of-the-art results among specialized autoformalizers (88.06% SC / 72.37% CC average Pass@8), outperforming multiple 32B baselines.
- Knowledge retrieval and verification-guided refinement are **complementary** and jointly improve data quality, with gains concentrating on high-abstraction statements requiring deep library knowledge.

### Future Directions

The authors plan to explore **larger-scale test-time scaling methods** to further strengthen formalization on complex problems, potentially extending the framework to even more advanced mathematical domains and more challenging formalization tasks.

---

_Markdown view of https://picx.dev/p/jGff22, served by PicX — AI-generated visual whiteboard summaries of research papers._