PaperlayerView exact revision on arXiv

Source-linked AI summary

Leanabell-Prover: Posttraining Scaling in Formal Reasoning

Jingyuan Zhang, Qi Wang, Xingguang Ji, Yahui Liu, Yang Yue, Fuzheng Zhang, Di Zhang, Guorui Zhou, Kun Gai

arXiv:2504.06122v3cs.AI

TL;DR

Lean proof generation has not yet seen the posttraining gains achieved in natural-language reasoning, and existing formal-reasoning RL results have been modest. The paper combines continual training with synthetic self-reflection data and Lean-verifier-rewarded RL. It reports improved whole-proof provers, including a 59.8% pass@32 result on MiniF2F.

  • Problem

    Lean proof generation remains challenging, and formal-reasoning RL has shown only modest gains compared with natural-language reasoning.

    Source: §1 · p. 2

  • Method

    The authors continue training whole-proof provers on statement-proof and synthetic self-reflection data, then apply GRPO using Lean 4 verification feedback as reward.

    Source: §1 · p. 2

  • Results

    Leanabell-Prover-GD-RL reaches 59.8% pass@32 on MiniF2F, 2.2 percentage points above Goedel-Prover-SFT's 57.6%.

    Source: §4 · p. 9

  • Takeaways & Limitations

    The authors report that their posttraining framework improves both DeepSeek-Prover-v1.5-SFT and Goedel-Prover-SFT whole-proof models.

    Source: §4 · p. 9, §5 · p. 12

    The expected stronger RL performance did not fully materialize, and self-reflection capacities weakened after RL training.

    Source: §5 · p. 12

Abstract

from arXiv · show

Recent advances in automated theorem proving (ATP) through LLMs have highlighted the potential of formal reasoning with Lean 4 codes. However, ATP has not yet be revolutionized by the recent posttraining scaling as demonstrated by Open AI O1/O3 and Deepseek R1. In this work, we investigate the entire posttraining of ATP, aiming to align it with breakthroughs in reasoning models in natural languages. To begin, we continual train current ATP models with a hybrid dataset, which consists of numerous statement-proof pairs, and additional data aimed at incorporating cognitive behaviors that emulate human reasoning and hypothesis refinement. Next, we explore reinforcement learning with the use of outcome reward returned by Lean 4 compiler. Through our designed continual training and reinforcement learning processes, we have successfully improved existing formal provers, including both DeepSeek-Prover-v1.5 and Goedel-Prover, achieving state-of-the-art performance in the field of whole-proof generation. For example, we achieve a 59.8% pass rate (pass@32) on MiniF2F. This is an on-going project and we will progressively update our findings, release our data and training details.

1. Introduction

Formal theorem proving offers verifiable reasoning, but generating Lean 4 proofs remains harder than solving the same problems in natural language. The paper investigates continual training and reinforcement learning to improve whole-proof generation.

Motivation

  • Lean 4 proof generation remains challenging: DeepSeek-Prover-v1.5-RL reaches 50.0% pass@32 on MiniF2F, while DeepSeek-R1 reaches 100% on the same problems in natural language.Prior work also reports gains from synthetic formal statement-proof data and expert iteration, while some stepwise search approaches use more than two million search steps.Source: §1 · p. 2
  • Formal reasoning has seen only modest RL gains so far: DeepSeek-Prover-v1.5-RL improves its supervised fine-tuned model by 1.8%.Replicating successful natural-language RL approaches, which primarily target Qwen2.5 models, is not straightforward.Source: §1 · p. 2

Approach

  • The approach continues training whole-proof provers on statement-proof data and synthetic self-reflection examples, then applies GRPO reinforcement learning using Lean 4 verification feedback.The reflection behaviors include backtracking and systematic error-checking.Source: §1 · p. 2

Contributions

  • Leanabell-Prover achieves 59.8% pass@32 on MiniF2F-test, and the project reports collecting around 1.52M formal statements and 0.22M statements with detailed informal CoTs and verified proofs.The authors report releasing intermediate models and training data.Source: §1 · p. 3

2. Related Work

Prior Lean theorem-proving work includes stepwise tactic generation and whole-proof generation, while RL methods use either whole-proof verifier feedback or stepwise tactic-state preferences. The paper also situates its approach amid work on cognitive behaviors for reasoning.

Lean4 Theorem Proving using LLMs

  • Proof-step methods iteratively predict tactics from the current proof state and verify each step, while search methods such as MCTS can become computationally expensive as proofs grow.LeanDojo retrieves premises based on the current state and generates the next tactic.Source: §2 · p. 3
  • Whole-proof generation uses supervised training or prompting to generate an entire proof at once, with predictable computation but no intermediate executor feedback.The passage identifies limited formal proof data and the expertise needed to generate it as challenges for this approach.Source: §2 · p. 3

Reinforcement Learning for Lean4 Theorem Proving

  • DeepSeek-Prover-v1.5-RL uses GRPO with whole-proof Lean verifier feedback, whereas Xin et al. (2025) use DPO preference pairs from tree search and tactic states.The passage states that existing methods still need improvement.Source: §2 · p. 3

Cognitive Behaviors

  • Related work argues that verification, backtracking, subgoal setting, and backward chaining may matter for obtaining substantial gains from RL.Other cited work proposes starting from base models already trained with such cognitive behaviors.Source: §2 · p. 4

3. Model Training

The training pipeline builds on two supervised whole-proof provers, adds formalized proof data and synthetic reflection examples, then applies GRPO with Lean 4 verifier feedback. Its data sources cover MiniF2F domains well, while the authors report domain bias in ProofNet.

3.1. Continual Training

  • The base models are 7-billion-parameter DeepSeek-Prover-v1.5-SFT and Goedel-Prover-SFT models trained on proofs with detailed explanatory informal comments.The authors use them as whole-proof generators with an existing alignment between natural-language descriptions and Lean 4 code.Source: §3.1 · p. 4
  • Using a trained formalizer, the authors convert natural-language statements and verify them with the Lean 4 compiler, obtaining 520K formal statements from NuminaMath and 370K from AoPS.PromptCoT synthesizes problems at AMC, AIME, and USAMO levels across algebra, number theory, and calculus.Source: §3.1 · p. 5
  • The continual-training corpus contains around 1.52M formal statements and 0.22M statements with detailed informal comments and verified proofs.Training sources include Mathlib4, Lean Workbook, synthetic Goedel-Prover and STP theorems, and sampled proofs from NuminaMath and AoPS.Source: §3.1 · p. 5, Table 1 · p. 5
  • Lean Workbook, Goedel-Prover, STP Lean, and NuminaMath cover MiniF2F's data distribution well, whereas ProofNet shows domain bias; the authors leave training distributions unadjusted.Figure 2 presents domain distributions for these training sources and the MiniF2F and ProofNet test sets.Source: Figure 2 · p. 4, §3.1 · p. 5

3.2. Integrating Cognitive Behaviors

  • Lean completion examples pair failed proofs and verifier feedback with revised valid proofs so synthetic reflections can identify errors and describe alternatives.The authors sample statements that did not achieve pass@16 and collect replacement valid proofs.Source: §3.2 · p. 6
  • The rewriting strategy evaluates and repairs problem-solving comments, then uses invalid and valid Lean code to generate explanatory CoTs; the authors collect 19K CoT samples.A second continual-training stage on the synthesized data produces Leanabell-Prover-SFT.Source: §3.2 · pp. 6–7

3.3. Reinforcement Learning

  • GRPO samples groups of candidate proofs, assigns rewards from Lean feedback, normalizes group rewards into advantages, and optimizes the policy.Training selects examples with 2–16 successful proofs in pass@32; the authors use 32 candidates per theorem and omit the KL penalty.Source: §3.3 · pp. 7–9
  • RL rewards are based on full-proof compilation: validated proofs receive a terminal reward, critical errors receive a penalty, and warnings are ignored when verification passes.The agent generates whole proofs and receives Lean 4 compiler feedback.Source: §3.3 · pp. 7–8

4. Experiments

On MiniF2F-test, the posttraining framework improves both whole-proof prover lineages, with Leanabell-Prover-GD-RL reaching the reported state of the art. The experiments also examine gains from larger sampling budgets, exploration during RL, and failure patterns across problem sources.

Sampling budget

  • At pass@128, Leanabell-Prover-DS-RL rises from 56.6% to 59.0%, while DeepSeek-Prover-v1.5-RL rises from 50.0% to 51.6%.These are gains as the sampling budget increases from 32 to 128.Source: §4 · p. 9

Exploration Abilities and RL

  • Both SFT models were exploratory by pass@16 across temperatures, and GRPO and Dr. GRPO training dynamics remained largely consistent.The reward curves shown are for Leanabell-Prover-DS-RL and Leanabell-Prover-GD-RL.Source: §4 · pp. 9, 11, Figure 3 · p. 11, Figure 4 · p. 11

Results on MiniF2F

  • 59.8% (pass@32): Leanabell-Prover-GD-RL reaches the reported MiniF2F-test state of the art, up 2.2% from Goedel-Prover-SFT’s 57.6%.The study evaluates MiniF2F-test as its main benchmark.Source: §4 · p. 9, Table 2 · p. 10

Exploration Abilities and RL

  • For DeepSeek-Prover-v1.5-SFT, errors fell across MiniF2F-test source types, especially AMC, MATH, and CUSTOM; the improvement was smaller with Goedel-Prover-SFT.The authors note that statement difficulty, domain coverage, and fit with prover capabilities also matter.Source: §4 · p. 11, Figure 5 · p. 12

5. Conclusion, Limitation, and Future Work

Leanabell-Prover applies continued training with formalized statements and proofs, adds synthetic data intended to embed cognitive behaviors, and then uses RL optimization. The authors report limits tied to weak base models and weakening self-reflection after RL, and identify formal–natural reasoning and whole-proof–proof-step methods as future directions.

5. Conclusion, Limitation, and Future Work

  • The Leanabell-Prover series starts from DeepSeek-Prover-v1.5-SFT and Goedel-Prover-SFT, continues training on formalized statements with proofs, adds synthetic cognitive-behavior data, then applies RL.The cognitive-behavior stage is described as a second-stage continual training step.Source: §5 · p. 12
  • The authors identify weak base models as a limitation: expected stronger RL performance has not fully materialized, and self-reflection capacities weaken after RL.They compare DeepSeek-Prover-v1.5 with stronger models used for natural-language posttraining scaling.Source: §5 · p. 12
  • Future work aims to transfer mathematical knowledge and reasoning from natural language into formal proofs; prompted Deepseek R1 reached 51.6% (pass@32) on MiniF2F-test.The authors state that current formal provers still lag behind natural-language reasoning models.Source: §5 · p. 12
  • The authors also propose proof-step rollouts that still score complete proofs, as a possible way to improve RL training efficiency.This is presented as a future direction for bridging whole-proof generation and proof-step methods.Source: §5 · pp. 12–13

A. Formalizer Details

The formalizer translates natural-language statements into Lean 4 theorem statements, and its quality is assessed with compilation-correctness and faithfulness/completeness tests. It is trained on Goedel-Prover data and performs similarly to Formalizer A.

A. Formalizer Details

  • 29.7K informal/formal statement pairs from Goedel-Prover are used to train the formalizer for two epochs at a fixed learning rate of 5 × 10−6.The formalizer is intended to translate natural-language statements into Lean 4 formal statements.Source: A. Formalizer Details · p. 16
  • The formalizer performs similarly to Formalizer A on the Compiling Correctness and Faithfulness and Completeness tests.Table 4 assesses the formalized statements using these two tests.Source: A. Formalizer Details · p. 16, Table 4 · p. 16
  • Table 3 gives two examples of formalizer inputs and outputs, with prompts requesting a Lean 4 theorem statement rather than proof code or comments.The prompt asks the model to complete a Lean code statement skeleton.Source: Table 3 · p. 16, A. Formalizer Details · p. 16

B.1. Lean Completion Example

The example demonstrates completing Lean code for a trigonometric identity, while its reasoning commentary identifies a mismatch between the inequalities supplied to nonlinear arithmetic and the exact relationships the proof may need.

B.1. Lean Completion Example

  • The example asks Lean to prove that sin(2x) equals 7/25 from the assumption sin(π/4 − x) = 3/5.The accompanying reasoning uses the sine difference identity and the double-angle formula.Source: §B.1 · p. 17
  • The attempted proof first simplifies with trigonometric identities, then uses field_simp and ring_nf before calling nlinarith.The tactic sequence is shown in the Lean code and discussed in the verification commentary.Source: §B.1 · pp. 18–19
  • The commentary flags that nlinarith is given sine and cosine bounds where exact equalities may be needed, and the shown tactic reports failure.The proposed approach instead emphasizes the Pythagorean identity and square-root facts.Source: §B.1 · pp. 18–19

B.2. Rewriting Example

The rewriting example concerns constructing, for every n ≥ 2, a list of distinct integers whose pairwise sums are divisible by their differences. Its commentary highlights that a base-case-only or repeated-element construction does not establish the general claim.

B.2. Rewriting Example

  • The target is a length-n list of distinct integers for every n ≥ 2, with each pairwise sum divisible by the corresponding difference.The Lean theorem states the list-length and divisibility requirements.Source: §B.2 · p. 20
  • A proposed inductive approach adds a new integer using a factorial offset, but its accompanying divisibility justification is not established by the stated argument.The passage claims the offset preserves the property but reasons that 2a_j is always divisible by a_i − a_j, which does not follow from the text's stated conditions.Source: §B.2 · p. 21
  • The commentary notes that using [0, 1] handles only n = 2, while List.replicate n 0 fails the distinctness requirement.It identifies the missing ingredient as a construction that works for arbitrary n or a valid induction step.Source: §B.2 · pp. 21–22

C. RL Details

The section describes the distribution of valid proofs in pass@32 testing for Leanabell-Prover-GD-SFT, using statements for which at least one sampled proof passes Lean 4 verification.

C. RL Details

  • The pass@32 distribution is calculated for Leanabell-Prover-GD-SFT.Figure 6 presents the overall distribution of valid proofs in this testing setting.Source: C. RL Details · p. 22, Figure 6 · p. 23
  • The distribution includes formal statements for which at least one sampled proof is valid according to the Lean 4 compiler.This is the stated criterion for building the set used in the distribution.Source: Figure 6 · p. 23
Loading 2504.06122v3…