Applies LLM self-play to Lean4 theorem proving, using the Lean4 compiler as the verifier and reward for generated proofs and synthetic conjectures.
Abstract
LLM self-play algorithms are notable in that, in principle, nothing bounds their learning: a Conjecturer model creates problems for a Solver, and both improve together. However, in practice, existing LLM self-play methods do not scale well with large amounts of compute, instead hitting learning plateaus. We argue this is because over long training runs, the Conjecturer learns to hack its reward, collapsing to artificially complex problems that do not help the Solver improve. To overcome this, we introduce Self-Guided Self-Play (SGS), a self-play algorithm in which the language model itself guides the Conjecturer away from degeneracy. In SGS, the model takes on three roles: Solver, Conjecturer, and a Guide that scores synthetic problems by their relevance to unsolved target problems and how clean and natural they are, providing supervision against Conjecturer collapse. Our core hypothesis is that language models can assess whether a subproblem is useful for achieving a goal. We evaluate the scaling properties of SGS by running training for significantly longer than prior works and by fitting scaling laws to cumulative solve rate curves. Applying SGS to formal theorem proving in Lean4, we find that it surpasses the asymptotic solve rate of our strongest RL baseline in fewer than 80 rounds of self-play and enables a 7B parameter model, after 200 rounds of self-play, to solve more problems than a 671B parameter model pass@4.
Problem
LLM asymmetric self-play methods plateau over long training runs because the Conjecturer hacks a reward based only on Solver pass rate. It collapses to artificially complex problems that do not help the Solver solve hard target problems.
Approach
Self-Guided Self-Play (SGS) has one LLM act as Solver, Conjecturer and Guide. The Conjecturer is conditioned on each unsolved Lean4 target to propose a simpler related problem. A frozen Guide scores each synthetic problem for relevance, low complexity and non-redundancy, and this score is combined with a difficulty reward. The Solver is trained with RL (REINFORCE^{1/2}) on the 3,323-problem Goedel-Pset subset, with proofs verified by the Lean4 compiler, and scaling laws are fit to cumulative solve-rate curves.
Figure 1: Left: Intuition behind SGS. Bottom, the space of problems solvable over course of SGS, starting as a small area , expanding past asymptotic RL performance , directed towards unsolved target problems ( \blacklozenge ) by synthetic problems ( \bm{\times} ). Top, the Guide score for synthetic problems, which is high along the path to unsolved targets, and low for not related and inelegant pFigure 2: Benefit of Guide component in SGS . Top: Percentage of generated problems with disjunctive conclusions. Without the Guide, this rises to over 80%; SGS stays near the D_{\text{3k}} baseline ( dotted orange ). Bottom: Average conclusion length, confirming that No Guide problems become overly long and complex. Inlaid examples: Problems generated from the same unsolved seed theorem, problem
Results
SGS surpasses the asymptotic solve rate of the strongest RL baseline in under 80 rounds. After 200 rounds, a 7B model solves more problems than a 671B model at pass@4. Ablations show the Guide prevents collapse into disjunctive, overlong conjectures.
Figure 6: Ablation of the SGS components. Left: Cumulative solve rate. The Guide improves performance at all points during training. Freezing the Conjecturer leads to even worse performance, but still above baseline. No Problem Conditioning shows no improvement over baseline. Right: Number of solvable problems used to train the Solver per iteration. Without the Guide, the Conjecturer produces far Figure 12: SGS and STP (Dong & Ma, 2025 ) performance on D_{\text{3k}} . We see that SGS has superior scaling, with a crossover happening at around 1M generations.
