Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study

AI summary

Overview

Research area: Neural theorem proving — specifically, reinforcement-learning-trained language models that write formal proofs in Lean 4, and how their behavior changes at inference time.

Technical level: Advanced. The paper assumes familiarity with reinforcement learning post-training, LLM sampling (temperature, pass@k), and interactive theorem provers, though its central argument is stated in plain terms.

Scope: A single-model diagnostic study on miniF2F-test (244 theorems) probing why RL-trained Lean provers stop finding new proofs as sampling budgets grow, tested with a fixed tactic-skeleton schedule, controlled prompt-diversity ablations, a base-vs-RL contrast, and a cross-model comparison of four provers.

What This Paper Is About

RL-trained theorem provers are supposed to get better as you give them more attempts. This paper shows that on miniF2F-test, DeepSeek-Prover-V1.5-RL stops improving entirely: going from 32 to 64 independent samples yields zero new solved theorems (42/244 both times). The authors' goal is to diagnose this "mode collapse," test whether a fixed schedule of 15 tactic skeletons can break it, and establish whether the phenomenon is specific to reinforcement learning rather than to supervised fine-tuning or to the base language model.

Key Contributions

1. A two-part diagnosis of mode collapse. An i.i.d. sampling plateau on V1.5-RL from k=32 to k=64 that a fixed 15-skeleton schedule breaks, plus a controlled diversity ablation (skeleton vs. paraphrase vs. irrelevant comment) showing the gain comes from structural guidance, not prompt diversity in general.

2. A leave-one-out empirical-difficulty stratification. Grounded in cross-prover baseline solvability rather than mathematical prestige, this localizes the skeleton gain to the easy and trivial buckets where V1.5-RL's gap to other open-source provers concentrates, and reveals a clean structural-content gradient across the three perturbations.

3. RL-specificity established two ways. A within-architecture base-vs-RL contrast on V1.5 (the base model proves zero theorems under every condition), and a cross-model contrast showing the RL-trained DeepSeek-Prover-V2-7B gains +3 frontier theorems unreachable by any i.i.d. baseline despite a flat aggregate, while SFT-trained Goedel-Prover loses 10.0 ± 4.4 theorems across n=3 seeds.

4. A direct distributional measurement of first-tactic collapse. On 13,159 V1.5-RL samples at k=64, three tactic heads account for 65.3% of all strategic openings, and observed per-theorem entropy is at most 8% of the sampling capacity.

Main Findings

• The i.i.d. plateau is total. On miniF2F-test with DeepSeek-Prover-V1.5-RL, i.i.d. sampling solves 38/244 at k=16 (15.6%), 42/244 at k=32 (17.2%), and still 42/244 at k=64 (17.2%). Thirty-two additional stochastic samples find zero new proofs.

• Tactic skeletons break the plateau. The 15-skeleton schedule solves 55/244 (22.5%) at k=16, 58/244 (23.8%) at k=32, and 60/244 (24.6%) at k=64. The absolute gap is +17, +16, and +18 respectively; relative improvement is +44.7%, +38.1%, and +42.9%. The abstract reports +45% relative improvement at k=16 and a mean Δ of +12.3 ± 4.2 theorems across n=3 seeds, with the sign preserved in every seed.

• Diversity is not the mechanism — structure is. At k=16: irrelevant Lean comments solve 25/244 (10.2%), i.i.d. baseline 38/244 (15.6%), instruction paraphrases 38/244 (15.6%), skeletons 55/244 (22.5%). Irrelevant tokens actively degrade performance; paraphrase matches the baseline at the topline.

• A natural-language-only condition recovers most of the gap. A dedicated C3 ablation using empty tactic prefixes and 7 distinct natural-language goal-hint comments solves 48/244 (19.7%), between sample-only A (15.6%) and structured-skeleton B (22.5%). NL hints recover roughly 58% of the A-to-B gap (+10 of the +17 topline), with tactic stems contributing the remaining +7.

• The skeleton gain lands where mode collapse should hurt. With a leave-one-out difficulty score, miniF2F-test splits into frontier (σ=0, 117 theorems, 48% of the set), hard (σ=1, 24), medium (σ=2, 13), easy (σ=3, 53), and trivial (σ=4, 37). The skeleton condition's +17 net is dominated by easy (+9) and trivial (+6) — theorems that three or four of four other-model baselines already solve. Paraphrase nets 0 (a small redistribution: +3 easy, −3 trivial); comments net −13. The easy-plus-trivial column reads +15 / 0 / −14 for skeleton / paraphrase / comment.

• No perturbation touches the frontier. At k=16, 32, and 64, no intervention on V1.5-RL unlocks a single σ=0 frontier theorem.

• The skeleton win decomposes into two additive layers. Of V1.5-RL's 55 structured wins at k=16, attempt 0 (truly empty prompt) contributes 16 wins and 0 NEW; attempt 15 (hint comment only) contributes 9 wins and 8 NEW; tactic prefixes (attempts 1–14) contribute 30 wins and 12 NEW. The 0/16 NEW count for attempt 0 indicates the model is effectively deterministic at these inference settings. Dominant prefixes were intros (+6) and norm_num (+3).

• The skeleton is not just a Mathlib-automation top-up. Of 24 NEW B-RL k=16 solves, only 3 (12.5%) were one-shot closers where the continuation was effectively empty; the other 21 (87.5%) required substantive continuation tactics beyond the skeleton.

• The base model has no proof capability at all. DeepSeek-Prover-V1.5-Base proves 0/244 under i.i.d. and skeleton conditions at k=16, 32, and 64. It emits sorry in 58.8% of outputs or echoes the theorem statement, whereas the RL model produces explicit sorry tokens in under 0.2% of i.i.d. outputs. RL is therefore both the source of the proof capability and the source of its collapse.

• Cross-model pattern is not uniform. At k=16, V1.5-RL goes 38 → 55 (+17); V2-7B goes 126/244 (51.6%) → 127/244 (52.0%), a +1 aggregate; SFT-trained Goedel-Prover goes 90/244 (36.9%) → 85/244 (34.8%), a −5. Goedel also plateaus on k-scaling (pass@16 and pass@32 identical at 36.9% for i.i.d.; structured 34.8% → 36.1%).

• V2's flat aggregate hides frontier solves. Three theorems with σ=0 for V2 — imo_1960_p2, imo_1962_p2, and numbertheory_x5neqy2p4 — are solved by V2 structured at k=16 but by none of the other six sample baselines. Two are IMO problems.

• The intervention is near-Pareto-dominant on V1.5-RL. At k=16, of 38 theorems solved by i.i.d. sampling, skeletons solve 35 and add 20 new ones; only 3 i.i.d. solves are lost. The 20 unique solves concentrate in mathd_algebra and mathd_numbertheory.

• The RL-vs-SFT sign is stable across seeds. Across seeds 1, 2, 3 at k=16: V1.5-RL Δ = +17, +9, +11 (means 36.7 ± 1.5 → 49.0 ± 5.6, Δ = +12.3 ± 4.2); Goedel Δ = −5, −12, −13 (means 97.7 ± 6.7 → 87.7 ± 2.5, Δ = −10.0 ± 4.4). The Δ means separate by +12.3 − (−10.0) = 22.3 theorems against a combined std of roughly 6.1, about a 3.7σ separation.

• Within-model variance flips between the two models. On V1.5-RL the i.i.d. condition is near-deterministic (±1.5) while the structured condition varies (±5.6); on Goedel the pattern reverses (i.i.d. ±6.7, structured ±2.5).

• First-tactic collapse, measured directly. Across 64 i.i.d. V1.5-RL samples per theorem: 120 theorems (49.2%) show exactly 1 unique first-tactic head, 69 (28.3%) show 2, 34 (13.9%) show 3, 12 (4.9%) show 4, and 9 (3.7%) show 5–7. Median is 2, mean 1.9, max 7. Median Shannon entropy is 0.27 bits per theorem (mean 0.48) versus log₂64 = 6.0 bits under uniform sampling — observed entropy is at most 8% of capacity. Across 13,159 samples, have (37.2%), rw (14.1%), and norm_num (14.0%) account for 65.3% of all strategic openings. The structured schedule injects 15 distinct first-tactic heads, so at the same k=64 call budget it explores roughly 7.5× the strategic-opening surface.

• The authors flag a saturation rival explanation. The cross-model Δ ordering is monotone in baseline headroom (A=38 gains +17; A=126 gains +1; A=90 loses −10), and with only one SFT model in the matrix — which is also the highest-baseline prover — "SFT" and "saturated" are not statistically separable. The paper reads the cross-model evidence as compatible with both accounts and rests the RL-specificity claim on the V1.5-Base control.

Methodology in Plain English

The researchers take a theorem prover that has already been trained with reinforcement learning and run it two ways on the same 244 theorems. In the "sample" condition, every attempt uses the same empty prompt and differs only by random seed — the standard way of buying more attempts. In the "structured" condition, the seed is fixed and the prompt changes: a deterministic 15 × 8 = 120 grid of 15 hand-selected Lean tactic skeletons crossed with 8 goal-hint comments, where the first skeleton and first hint are both empty. Both conditions make exactly the same number of model calls, so the comparison is apples-to-apples; budgets tested are k ∈ {16, 32, 64}. Each generated proof is checked by the Lean 4 kernel (lake env lean --json, 120-second per-attempt timeout) with the toolchain pinned to v4.9.0-rc1 and Mathlib pinned to commit 7fa489a5, matching the environment V1.5 was trained in — the authors note this pinning matters because newer Lean versions ship stronger built-in solvers, which would confound the result.

To rule out "any prompt variation helps," two further conditions are added: C1, 16 semantically equivalent rephrasings of the instruction as Lean comments with an empty tactic prefix; and C2, 16 content-free comments prepended to the theorem. A later C3 spends all 16 attempts on natural-language goal hints with no tactic stem at all.

For difficulty analysis, the authors avoid using human judgments of mathematical difficulty, arguing that the formalization itself shifts how hard a theorem is for a machine. Instead they compute a leave-one-out score per theorem: how many of the other models' hint-free baselines solve it. For V1.5-RL that means four baselines (Goedel at k ∈ {16,32} and V2-7B at k ∈ {16,32}), giving buckets from frontier (σ=0, solved by none) to trivial (σ=4, solved by all). They then compare which theorems each intervention newly solves versus which it loses.

Finally, they go back to the raw per-attempt logs and extract the first tactic head of every proof — the leading identifier on the first line — to measure how many distinct strategic openings the model actually tries across 64 samples per theorem. Sampling used temperature 0.6 and top-p 0.95 throughout, with a 1024-token generation budget for completion-mode provers and 8192 tokens for the chain-of-thought reasoning model. Inference ran on a single A100 per experiment (80GB for V1.5, 40GB for V2 and Goedel-Prover), with theorems sharded 8-way.

Why This Matters

Impact on research. The paper reframes a performance result as a diagnostic one. The skeleton schedule is presented not as a new proving architecture but as a probe that exposes how little of the tactic space RL-trained provers actually explore. This bears directly on the common practice of scaling inference compute by increasing k, and it connects to prior work on entropy collapse in RL post-training (Kirk et al., 2024; Yue et al., 2025; Wu et al., 2025) — with the twist that here the verifier is a formal kernel, not string matching, and the base model proves exactly zero theorems. That makes the base-vs-RL contrast unusually clean evidence that RL is both necessary and responsible for the narrowness.

Real-world applications:

• Automated theorem proving and formal verification pipelines, where knowing that extra sampling budget is wasted lets engineers spend compute on structural diversity instead.
• AI-assisted software verification, where proofs of program correctness in Lean-style systems face the same explore/exploit trade-off.
• Agentic proof assistants with compiler feedback loops — the paper's diagnostic measures the underlying model that such harnesses are layered on top of.
• General RL post-training for reasoning tasks, since the collapse signature (near-deterministic openings on a fixed prompt, high variance recovered only when the prompt varies) suggests a measurement any RLVR pipeline could apply.

Industry relevance. Inference-time compute is billed by the call. If a prover's solve rate is flat from k=32 to k=64, the second half of that budget buys nothing. A deterministic prompt schedule is a cheap substitute, and the paper positions structural diversity as orthogonal to scaling model size or training compute.

Future Directions

1. A matched-capability SFT control at lower baseline pass@k. The authors state this is the natural next experiment, because with only one SFT model — which is also the highest-baseline prover — the RL-specific and saturation accounts cannot be statistically separated.

2. Replace the hand-designed 15-skeleton grid with a learned per-theorem skeleton retriever. The difficulty gradient in the stratification suggests this should outperform the fixed schedule.

3. Close the loop at training time. Entropy-regularized or skeleton-conditioned RL is proposed, with the caveat that the V1.5-Base control implies any training-time intervention must contend with RL's dual role in creating and collapsing the proof policy.

4. Extend the measurements. The first-tactic distribution is currently V1.5-RL only; extending it to V2-7B and Goedel would test whether first-tactic concentration tracks the RL-vs-SFT asymmetry. The headline k=32 to k=64 plateau is single-seed and needs replication; V2 has not been tested at k ≥ 32; ProofNet and PutnamBench are untested; and a Kimina-Prover replication was attempted but cut for compute reasons after an output-extractor fix, with only a partial sample baseline of 20/35 trials (57%) deferred to future work.

Target Audience

Researchers and engineers working on neural theorem proving, formal verification, or reinforcement learning with verifiable rewards. It is especially useful for practitioners who design inference-time search or sampling budgets for code and proof models, and for anyone interested in the diversity-versus-accuracy trade-off introduced by RL post-training. Readers without background in Lean or RL fine-tuning will need to read the ablations carefully, but the central plateau result is stated plainly enough to be accessible.

Authors’ abstract

RL-trained Lean theorem provers mode-collapse at inference time: on miniF2F-test with DeepSeek-Prover-V1.5-RL, doubling the i.i.d.\ sampling budget from $k{=}32$ to $k{=}64$ produces zero additional solved theorems (42/244 in both cases). A fixed schedule of 15 tactic skeletons breaks this plateau and recovers a $+45%$ relative improvement at $k{=}16$ (mean $Δ= +12.3 \pm 4.2$ theorems across $n{=}3$ seeds, sign preserved in every seed). A controlled diversity ablation rules out the prompt-diversity confound: tactic skeletons help, paraphrases match the baseline, and irrelevant Lean comments actively degrade. A leave-one-out formalization-difficulty stratification reveals a structural-content gradient across the three perturbations. The phenomenon is RL-specific: V1.5-Base proves zero theorems regardless of intervention, identifying RL as the stage that creates the proof capability which subsequently collapses; extending to two additional 7B Lean provers, RL-trained DeepSeek-Prover-V2-7B contributes $+3$ frontier solves no i.i.d. baseline can reach despite a flat aggregate, while SFT-trained Goedel-Prover does not ( $-10.0$ $\pm 4.4$ theorems, $n{=}3$, sign preserved every seed). Inference-time structural diversity is a cheap, complementary axis for RL-trained provers, orthogonal to scaling model size or training compute.