Source-linked AI summary
SkillEvoLean: Mutation-enhanced skill evolution for Lean provers
Kuo Zhou, ZiXion Yang, Lu Zhang
TL;DR
Skill evolution remains underexplored in formal theorem proving, especially when failed proof trajectories provide little direction for updating skills. SkillEvoLean combines trajectory-based refinement with concept-guided mutation, and reports consistent improvements across four Lean benchmarks over existing baselines.
Problem
Skill evolution remains largely unexplored for formal theorem proving, where all-failed proof trajectories provide little evidence for choosing a new strategy and may leave progressive updates stagnating.
Source: §1 · p. 2, §4.1 · p. 13Method
SkillEvoLean combines trajectory-based progressive refinement with mutation that maps skills into concepts, perturbs them, and realizes them as coherent textual skills.
Source: §2.2 · pp. 5, 7, §5 · p. 13Results
SkillEvoLean reports consistent improvements across MiniF2F, PutnamBench, IMO 2025, and USAMO 2026 over static and existing skill-optimization baselines.
Source: §5 · p. 13Takeaways & Limitations
The findings suggest skill evolution can accumulate and reuse procedural knowledge across theorem-proving tasks through both refinement and broader strategy exploration.
Source: §5 · p. 13Evolved-skill quality depends on training-problem diversity, proof-trajectory informativeness, and skill-evaluation reliability.
Source: §5 · p. 13
Abstract
from arXiv · showhide
Skill evolution offers a promising way to improve large language model agents without updating their parameters, but its use in formal theorem proving remains underexplored. Existing methods mainly target natural-language reasoning, improving skills by analyzing successful and failed trajectories and incrementally revising solving strategies. Although the Lean verifier provides reliable execution feedback, when all sampled trajectories fail, existing skill evolution methods lack successful trajectories from which to infer effective update directions. Furthermore, these methods also focus mainly on the root instruction file, thus underexploring the evolution of reference knowledge including mathematical concepts and proving techniques. To address these limitations, we propose a mutation-enhanced skill self-evolution framework for building skill-augmented Lean provers. The framework jointly evolves a high-level solving policy and its reference knowledge through progressive and mutation-based updates. Progressive evolution derives local improvements from successful and failed trajectories, while mutation is triggered when no complete proof can be generated, sampling mathematical concepts to produce and select new skill candidates under verifier feedback. We evaluate our method on MiniF2F, PutnamBench, the 2025 International Mathematical Olympiad (IMO 2025), and the 2026 USA Mathematical Olympiad (USAMO 2026). Under the same backbone model, trajectorysampling budget, and test-time compute, our method achieves proof success rates of 100.0%, 90.6%, 4/6, and 4/6, respectively, with GPT-5.5, outperforming the baseline methods. Further analysis shows that concept-guided mutation outperforms random-text-guided mutation by 6.9 and 8.2 percentage points on MiniF2F and PutnamBench, respectively, while solving one additional problem on both IMO 2025 and USAMO 2026.
1 INTRODUCTION
Skill evolution is largely unexplored for formal theorem proving, where trajectory-based updates can stagnate when all sampled proofs fail. The paper proposes concept-guided mutation and a unified framework that combines it with progressive refinement.
1 INTRODUCTION
- External skills offer an editable way to acquire task-specific capabilities without additional model training, and can be refined through execution experience..Source: §1 · pp. 1–2
- When all sampled proof trajectories fail, existing trajectory-based evolution lacks successful behavior to guide updates and may stagnate on difficult theorems.Lean can reject invalid proofs, but provides little evidence about which high-level strategy should replace the current one.Source: §1 · p. 2
- Concept-Guided Skill Refinement maps a skill into reasoning and procedural concepts, perturbs those concepts, then maps them back into coherent, behaviorally different instructions.This avoids directly editing the surface text, where arbitrary changes may disrupt syntactic coherence or semantic structure.Source: §1 · p. 2
- The framework combines progressive refinement with mutation-based exploration and reports improvements over existing skill-construction and skill-evolution baselines on challenging Lean benchmarks.The paper frames skill evolution for formal theorem proving and identifies stagnation under all-failed trajectories as a limitation of progressive updates.Source: §1 · p. 2
2 METHOD
The framework evolves Lean-proving skills through trajectory-based local refinement and concept-guided mutation, combining exploration with verifier-checked updates. Skills include a root policy, reference resources, and examples.
2 METHOD
- The framework combines progressive refinement from execution trajectories with mutation-based exploration when all generated trajectories fail, retaining effective updates after Lean-verifier evaluation.Progressive and mutational evolution are complementary: the former uses trajectory feedback for local refinement, while the latter explores new skill variants under stagnation.Source: §2 · p. 2, §2.2 · p. 7
- A skill comprises a root natural-language policy, reference resources, and representative examples; LLM-based operators perform structured transformations of textual instructions.The operators are prompted invocations of a shared backbone model with operator-specific prompts, inputs, and output formats.Source: §2 · pp. 2–3
2.1 PROGRESSIVE SKILL EVOLUTION
- Progressive evolution contrasts successful and failed trajectories for each problem, locates relevant skill positions, generates local updates, and merges updates across problems.The position tree lets the updating model target files, sections, or entries rather than rewrite the entire skill.Source: §2.1 · p. 4
2.2 MUTATIONAL SKILL EVOLUTION
- Mutation maps a skill into a concept representation, perturbs it with sampled concepts, then realizes the result as a coherent textual skill.An LLM-based pruning step removes conflicting or redundant concepts; a candidate is retained only when it improves the current iteration's best evaluation score.Source: §2.2 · pp. 6–7
3 EXPERIMENTS
The experiments compare skill-evolution methods across Lean benchmarks and backbones, then examine component contributions, inference-cost targets, and retention. The main results favor the full method, while the cost and retention analyses are explicitly framed as planning targets.
3 EXPERIMENTS
- Evaluation covers MiniF2F-test, PutnamBench, IMO 2025, and USAMO 2026, comparing skill methods under the same target model, test set, Lean environment, and inference budget.DeepSeek-V4-Pro initializes skills and implements evolution operations; evaluation uses frozen DeepSeek-V4-Pro, DeepSeek-V4-Flash, or GPT-5.5 backbones.Source: §3 · pp. 7–8
3.1 MAIN RESULTS
- Across three backbones, the method leads on all four benchmarks; with GPT-5.5 it scores 100.0% on MiniF2F-test, 90.6% on PutnamBench, and 4/6 on both olympiads.On GPT-5.5, it improves MiniF2F-test from 89.3% to 100.0% and PutnamBench from 78.2% to 90.6%; the strongest baselines solve at most 2/6 on either olympiad benchmark.Source: §3.1 · pp. 8–9
COMPONENT ABLATION.
- Planning targets show removing mutation drops MiniF2F-test from 98.4% to 82.3% and yields no IMO 2025 or USAMO 2026 solves.Removing progressive evolution also lowers the targets; Figure 3 reports that progressive-only updates improve rapidly over four cycles and saturate after the fifth. The component table is labeled a planning scenario, not measured results.Source: Table 3 · p. 8, Figure 3 · p. 8, COMPONENT ABLATION · p. 9
EFFECT OF MUTATION GUIDANCE.
- 6.9 and 8.2 percentage points: CGM's gains over RTGM on MiniF2F and PutnamBench, alongside one additional solve on each olympiad benchmark.These are mutation-guidance targets under matched limits, not measured results.Source: Table 4 · p. 9, EFFECT OF MUTATION GUIDANCE · p. 10
3.3 INFERENCE COST ANALYSIS
- Planning targets reduce average total tokens per PutnamBench problem from 101K to 96K and tokens per solved problem from 151.9K to 117.4K.The target success rate is 81.8%; these are planning arithmetic, not observed improvements, and token counts alone do not represent monetary cost.Source: §3.3 · pp. 10–11, Table 5 · p. 10
3.4 FORGETTING AND KNOWLEDGE RETENTION
- The retention audit uses disjoint problems, fixed checkpoints, and an unchanged initial-skill control to distinguish apparent losses from persistent forgetting.Endpoint metrics track retained, gained, and lost problems; historical forgetting also includes problems solved at intermediate checkpoints but not at the final one, and ratios with empty denominators are undefined.Source: §3.4 · pp. 11–12
- Retention targets are 98.7% on MiniF2F-test and 97.4% on PutnamBench, with net gains of 20.9 and 23.6 percentage points, respectively.The targets include nonzero losses, so aggregate improvement does not imply complete retention; Table 6 is labeled planning targets, not measured results.Source: Table 6 · p. 11, §3.4 · p. 12
4 RELATED WORK
Prior skill-evolution work mainly derives updates from execution feedback or trajectory analysis, which can leave difficult Lean problems without informative update directions when all sampled proofs fail. Existing Lean provers combine language-model reasoning with search and verification, but generally do not explicitly reuse external skills across problems.
4.1 SKILL EVOLUTION
- Skill-evolution approaches use execution feedback or trajectory analysis, but trajectory-derived updates need successful or partly successful behavior, which may be absent when all Lean proof attempts fail.Execution feedback can also be sparse or limited to final correctness.Source: §4.1 · pp. 12–13
4.2 LLM-BASED LEAN PROVERS.
- Lean provers combine language-model reasoning with verification, structured search, and iterative refinement, but generally do not explicitly reuse external skills across problems.Skill evolution treats strategies and recurring failure patterns as procedural knowledge that can be integrated and refined across problems.Source: §4.2 · p. 13
5 CONCLUSION & DISCUSSION
SkillEvoLean combines trajectory-based refinement with concept-guided mutation, and experiments show improvements across benchmarks and backbone models. The authors identify dependencies on problem diversity, trajectory informativeness, and skill-evaluation reliability.
5 CONCLUSION & DISCUSSION
- Experiments show consistent improvements across MiniF2F, PutnamBench, IMO 2025, and USAMO 2026 over static and existing skill-optimization baselines.The experiments also report complementary roles for progressive evolution and mutation, and the effectiveness of mathematical concept guidance.Source: §5 · p. 13
- SkillEvoLean combines trajectory-based progressive refinement with concept-guided mutation to explore new strategies when refinement stagnates.The authors report that this combination supports accumulating and reusing procedural knowledge across theorem-proving tasks.Source: §5 · p. 13
- Evolved-skill quality depends on training-problem diversity, proof-trajectory informativeness, and the reliability of skill evaluation.Suggested future directions include compact skill representations, resolving redundant or conflicting instructions, and transfer across formal libraries, theorem domains, and interactive theorem provers.Source: §5 · p. 13