Autoformalization - automatically translating natural language mathematical texts into formal proof language such as Lean4 - can help accelerate AI-assisted mathematical research, be it via proof verification or proof search. I fine-tune Qwen3.5-2B with LoRA for natural language to Lean4 formalization on FineLeanCorpus and consider three training regimes: supervised fine-tuning (SFT) with curriculum learning (difficulty 1 to 10), SFT without curriculum ordering, and reinforcement learning using group relative policy optimization (GRPO) with a cycle consistency reward. Cycle consistency measures how well the meaning of a statement is preserved through a NL to Lean4 to NL' loop, computed as cosine similarity of off-the-shelf sentence embeddings. On an unseen subset of FineLeanCorpus (FLC) and on PutnamBench, RL substantially outperforms both SFT variants (mean cycle consistency 0.669 vs. 0.513 on FLC; 0.561 vs. 0.422 on PutnamBench), while increasing cross-entropy loss by only 0.011 nats, with minimal impact on formalization quality. Curriculum ordering provides no measurable benefit over shuffled training.
Figures & tables
Figure 1: Training pipeline. Phase 1: fθ and gϕ are fine-tuned independently via SFT on FineLeanCorpus, on the NL → Lean4 and Lean4 → NL directions respectively. Phase 2: fθ is further fine-tuned via GRPO with gϕ frozen. The reward is the cosine similarity between the original statement s and the back-translated NL′ ; both live in the same natural language space S .
Model
FLC Cˉ
PB Cˉ
CE loss
Base 2B (few-shot)
0.093
0.034
-
SFT No-Curriculum 2B
0.519
0.432
0.640
SFT Curriculum 2B
0.513
0.422
0.680
RL (GRPO) 2B
0.669
0.561
0.691
Base 9B (few-shot)
0.029
− 0.004
-
SFT Curriculum 9B
0.585
0.548
-
Table 1: Mean cycle consistency ( ↑ ) on FLC held-out (700 problems) and PutnamBench (PB, 660 problems). Cross-entropy evaluation loss ( ↓ ) on FLC validation split (3,932 examples).
Figure 2: Mean cycle consistency by model and evaluation set. Error bars show ±1 std.
Figure 3: Score vs. difficulty (FLC held-out, 100 problems per difficulty level).
Figure 4: RL improvement over SFT curriculum by difficulty level (FLC held-out). The gain decreases monotonically from 0.208 at difficulty 1 to 0.126 at difficulty 7.
Figure 5: Cycle consistency by mathematical domain on FLC held-out. Error bars show ±1 std. Domains with n<10 excluded.
Figure 6: Cycle consistency by mathematical domain on PutnamBench. Error bars show ±1 std. Domains with n<10 excluded.
Figure 7: Score distributions: SFT Curriculum 2B vs RL (GRPO) 2B. On FLC, RL reshapes the distribution creating a high-score tail above 0.8. On PutnamBench, RL produces a more uniform rightward shift, suggesting less exploitation of dataset structure.
Figure 8: GRPO training reward over the full RL run. Dashed red line marks the checkpoint resume point.
Figure 9: SFT training token accuracy: curriculum (solid) vs. no-curriculum (dashed). Dotted red vertical lines mark difficulty transitions in the curriculum run. No-curriculum x-axis is scaled to match curriculum total steps for comparison.
Figure 10: Cross-entropy loss vs. difficulty on FLC val split. All three 2B models track closely.
Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@k and refine@k metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of <\0.01$ per correct proof.
Tyson Klingner, Drew Bladek, Escher Crawford +6
Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA
While Large Language Models (LLMs) have demonstrated exceptional capabilities in mathematical reasoning, they frequently produce subtle errors that evade human detection. Formal mathematical languages like Lean 4 offer mechanical proof checking, strongly motivating the need for autoformalization: the automatic translation of natural language mathematics into verifiable code. Recent trends indicate that general-purpose LLMs, heavily optimized for standard programming, now outperform smaller models explicitly fine-tuned for Lean. Leveraging this shift, we introduce an agentic autoformalization framework powered by general coding LLMs. At the core of our system is an orchestrator that manages a multi-agent pipeline tailored for research-level mathematics. Because cutting-edge research frequently relies on concepts outside the scope of existing libraries like Mathlib, our system dynamically extends necessary type definitions and validates them via a novel Auxiliary Lemma technique before formalizing the primary theorems. We applied our approach to PutnamBench, producing machine-checked Lean proofs for a random sample of 32 problems. Furthermore, we evaluate our system on five papers from the ACM Symposium on Theory of Computing (STOC) spanning combinatorics, communication complexity, mechanism design, and learning theory, successfully formalizing their main theorems and validating the generated formalizations with human experts; for all five we also formalize the proofs alongside the statements, and notably two of them are proved with no axioms beyond Lean's kernel. All of our formalizations are available at https://beyondthelibrary.github.io/formal_arxiv .
Arshia Soltani Moakhar, Iman Gholami, Max Springer +2
Proof autoformalization aims to translate a mathematical informal proof written in natural language into a formal proof in a formal language such as Lean~4. Several works have developed LLM-based models for proof autoformalization. However, existing evaluations have typically focused on translating well-formed informal proofs from curated datasets. We argue that a robust proof autoformalizer must remain faithful even for informal proofs that diverge from these idealized ones, and we present the first study on the robustness of proof autoformalization models. We formulate two categories of perturbations and evaluate robustness under each: a global perturbation paraphrases the informal proof in a different style, under which the formalization should remain consistent; a local perturbation alters a value, symbol, or proof step, possibly in a counterfactual way, and a robust formalization should faithfully reflect the perturbation rather than reverting to the original one or inferring a different one on its own. We build a benchmark with both perturbations on miniF2F and MATH-500, and automatically measure how stable a proof autoformalization's correctness is under global perturbations and how faithfully its output reflects local perturbations. We evaluate seven recent models, all of which are sensitive to global perturbations and mostly fail to remain faithful under local perturbations. Code and data are available via https://github.com/ucr-rai/robust-proof-autoformalization.
Zhengtao Gui, Sheng Yang, Zhouxing Shi
University of California, Irvine · University of California, Riverside