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.
Figures & tables
Figure 1: Macro-average Pass@8 (%) across six benchmarks among specialized autoformalizers. MathForm -8B achieves the strongest overall performance within this category despite its smaller model size.
Figure 2: Overview of the MathForm data construction and training pipeline. The system combines Mathlib knowledge retrieval, compilation and semantic verification, and iterative refinement to generate reliable formal data, followed by trajectory reconstruction and training of MathForm -8B.
Figure 3: Distribution of natural-language problem sources in FormalVerse .
Figure 4: Numbers of natural-language-to-formal-language pairs accepted in successive refinement rounds. Later rounds contribute an additional 31.0% of all retained pairs.
AVG
FormalMATH
ProverBench
CombiBench
FATE-M
FATE-H
FATE-X
Model
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
Specialized Autoformalizers
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
Table 1: Pass@8 pass rates (%) under Syntax Check (SC) and Consistency Check (CC) for specialized autoformalizers on six benchmarks. AVG is the equally weighted macro-average across all six benchmarks. For each column, the best result is shown in bold and the second best is underlined .
Figure 5: Training dynamics during reinforcement learning. The left panel shows the training reward and its exponential moving average (EMA), while the right panel reports the Mean@3 pass rate on FATE-H over the course of training.
AVG
FATE-M
FATE-H
FATE-X
Method
SC
CC
SC
CC
SC
CC
SC
CC
gpt-oss-120b
Single
27.33
26.43
52.00
51.30
21.00
19.00
9.00
9.00
BoN
42.67
41.10
70.00
69.30
40.00
37.00
18.00
17.00
Feedback
42.57
40.77
68.70
67.30
41.00
38.00
18.00
17.00
Retrieval
32.23
29.00
56.70
52.00
27.00
26.00
13.00
9.00
Table 2: Ablation results for SC and CC pass rates (%) of the refinement pipeline with two generators on the FATE series. Single denotes single-pass generation; BoN denotes Best-of- N ; Feedback denotes feedback-only iteration; and Retrieval denotes retrieval-only single-pass generation. AVG is the equally weighted average over FATE-M, FATE-H, and FATE-X.
AVG
FormalMATH
ProverBench
CombiBench
FATE-M
FATE-H
FATE-X
Training Dataset
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
NuminaMath-LEAN
66.24
41.49
99.53
85.18
96.55
72.41
87.00
25.00
69.33
49.33
35.00
16.00
10.00
1.00
FineLeanCorpus
78.25
46.53
100.00
84.47
98.85
74.71
96.00
29.00
90.67
68.00
53.00
17.00
31.00
6.00
FormalVerse
77.17
60.32
98.82
90.59
98.85
89.66
78.00
36.00
95.33
84.67
62.00
46.00
30.00
15.00
Table 3: Pass@8 SC and CC pass rates (%) of models trained on different datasets across six benchmarks. All models are initialized from Qwen3-8B and trained on 100K examples under the same trajectory reconstruction and training configuration. AVG is the equally weighted macro-average across all six benchmarks. The best result in each column is shown in bold and the second best is underlined .
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
Table 4: Judge-model reliability on the human-annotated semantic-consistency test set (Mean@3).
Appendix figures & tables4 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 6: Category distribution of the natural-language mathematical problems in FormalVerse .
Table 11
AVG
FormalMATH
ProverBench
CombiBench
FATE-M
FATE-H
FATE-X
Model
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
SC
CC
General-Purpose LLMs
DeepSeek-V4-Pro
78.34
76.54
97.88
96.24
94.83
93.68
85.00
81.00
87.33
87.33
70.00
68.00
35.00
33.00
Qwen3.7-Plus
86.33
83.38
99.29
98.59
100.00
97.70
92.00
87.00
94.67
92.00
78.00
77.00
54.00
48.00
Qwen3-235B-A22B-Thinking-2507
58.94
55.37
91.29
88.24
81.03
75.29
59.00
50.00
71.33
70.67
32.00
30.00
19.00
18.00
Qwen3-32B
43.07
36.55
80.94
72.94
61.49
50.00
43.00
27.00
46.00
43.33
20.00
19.00
7.00
7.00
Appendix
Table 7: Pass@8 SC and CC pass rates (%) of general-purpose LLMs and MathForm -8B across six benchmarks. AVG is the equally weighted macro-average across all six benchmarks. The best result in each column is shown in bold and the second best is underlined .
FATE-M
FATE-H
Model
SC
CC
SC
CC
StepFun-Formalizer-32B
42.67
36.00
16.00
12.00
Goedel-Formalizer-V2-32B
75.33
68.00
38.00
27.00
ReForm-32B
78.67
74.00
50.00
41.00
MathForm -8B
86.67
76.67
54.00
42.00
Appendix
Table 8: Human-evaluation results (%) on FATE-M and FATE-H, based on one randomly sampled candidate per problem. The best result in each column is shown in bold .