Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

Arsen Shebzukhov

cs.CLMar 25, 2026

Improving Lean4 Autoformalization via Cycle Consistency Fine-tuning

Authors: Arsen Shebzukhov

Organizations: Department of Computer Science, Stanford University

Abstract

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

Panel of Figure 1 — Figure 1: Training pipeline. Phase 1: $f_{\theta}$ and $g_{\phi}$ are fine-tuned independently via SFT on FineLeanCorpus, on the NL $\to$ Lean4 and Lean4 $\to$ NL directions respectively. Phase 2: $f_{\theta}$ is further fine-tuned via GRPO with $g_{\phi}$ frozen. The reward is the cosine similarity between the original statement $s$ and the back-translated $\text{NL}^{\prime}$ ; both live in the same natural language space $\mathcal{S}$ .

Model	FLC $\bar{\mathcal{C}}$	PB $\bar{\mathcal{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 (

\uparrow

) on FLC held-out (700 problems) and PutnamBench (PB, 660 problems). Cross-entropy evaluation loss (

\downarrow

) on FLC validation split (3,932 examples).

Figure 2: Mean cycle consistency by model and evaluation set. Error bars show $\pm 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 $\pm 1$ std. Domains with $n<10$ excluded.

Figure 6: Cycle consistency by mathematical domain on PutnamBench. Error bars show $\pm 1$ std. Domains with $n<10$ excluded.

Panel of Figure 7 — 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.

Explore similar work

Evaluation of LLMs for Mathematical Formalization in Lean
Jun 4, 2026Tyson Klingner, Drew Bladek, Escher Crawford +6LLM Evaluation Lean Theorem Proving
Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA
Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
Jun 30, 2026Arshia Soltani Moakhar, Iman Gholami, Max Springer +2Multi-Agent LLM Systems Automated Theorem Proving
Evaluating the Robustness of Proof Autoformalization in Lean 4
Jun 12, 2026Zhengtao Gui, Sheng Yang, Zhouxing ShiLean Theorem Proving Autoformalization
University of California, Irvine · University of California, Riverside

Jun 4, 2026J/K move · Enter open · S save

Evaluation of LLMs for Mathematical Formalization in Lean

Tyson Klingner, Drew Bladek, Escher Crawford, Bohao Chen+5

Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA

LLM Evaluation Lean Theorem Proving LLM Mathematical Reasoning

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

Evaluation of LLMs for Mathematical Formalization in Lean

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

Evaluating the Robustness of Proof Autoformalization in Lean 4