SkillEvoLean: Mutation-enhanced skill evolution for Lean provers

Kuo Zhou; ZiXion Yang; Lu Zhang

cs.LGOct 1, 2026

SkillEvoLean: Mutation-enhanced skill evolution for Lean provers

Authors: Kuo Zhou, ZiXion Yang, Lu Zhang

Organizations: Peking University

Abstract

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.

Figures & tables

Operator	Function
$\operatorname{LLMInitialize}$	Generates the initial high-level solving policy stored in SKILL.md .
$\operatorname{LLMConsolidate}$	Merges, deduplicates, and filters candidate proof patterns.
$\operatorname{LLMCompare}$	Compares successful and failed trajectories to identify behavioral differences and possible causes of failure.
$\operatorname{LLMLocate}$	Locates the skill component or reference entry that should be updated.
$\operatorname{LLMSuggest}$	Generates concrete modification suggestions from trajectory analysis and verifier feedback.
$\operatorname{LLMRewrite}$	Rewrites the current skill according to the generated suggestions while preserving its overall structure.

Table 1: Summary of the LLM-based operators used in our framework.

Backbone Model	Method	MiniF2F	PutnamBench	IMO 2025	USAMO 2026
DeepSeek-V4-flash	No Skill	61.5	55.3	0/6	0/6
	Human Skill	82.0	58.2	1/6	1/6
	LLM Skill	70.5	51.8	0/6	0/6
	Trace2Skill	77.0	55.3	0/6	0/6
	SkillOpt	77.9	58.8	0/6	1/6
	Ours	94.7	77.1	2/6	3/6

Table 2: Planning scenario, not measured results. Provisional success-rate targets and baseline assumptions across agent backbone models. MiniF2F and PutnamBench entries are percentages; competition entries are solved problems out of six. The planned comparison uses the same Claude Code harness, Lean environment, and inference limits within each backbone.

Figure 3: Progressive evolution converges without mutation. Without mutation-based exploration, progressive updates gradually saturate.

Variant	MiniF2F	PutnamBench	IMO	USAMO
Full Method	98.4	81.8	2/6	3/6
w/o Prog.	92.1	74.5	1/6	2/6
w/o Mut	82.3	63.5	0/6	0/6

Table 3: Planning scenario, not measured results. Component ablation targets with DeepSeek-V4-Pro. Prog. and Mut. denote progressive and mutation-based evolution. All variants are to use the same initial skill and evaluation limits.

Strategy	MiniF2F	PutnamBench	IMO	USAMO
UM	83.7	62.4	0/6	1/6
RTGM	91.5	73.6	1/6	2/6
CGM (Ours)	98.4	81.8	2/6	3/6

Table 4: Planning scenario, not measured results. Mutation-guidance targets with DeepSeek-V4-Pro under matched evaluation limits.

Method	Success rate (%) $\uparrow$	Input tokens (K/problem) $\downarrow$	Output tokens (K/problem) $\downarrow$	Lean calls /problem $\downarrow$	Time (min/problem) $\downarrow$	Tokens/solved problem (K) $\downarrow$
No Skill	61.2	80.0	20.0	10.0	20.0	163.4
Human Skill	64.1	88.0	18.0	9.0	19.5	165.4
LLM Skill	58.2	92.0	22.0	11.0	22.0	195.9
Trace2Skill	61.8	90.0	18.0	9.5	20.0	174.8
SkillOpt	66.5	84.0	17.0	8.5	18.0	151.9
Ours	81.8	82.0	14.0	8.0	17.0	117.4

Table 5: Planning targets, not measured results. Proof success and inference cost on PutnamBench with DeepSeek-V4-Pro. Success rates match the provisional main table. Cost targets concern test-time execution after skills have been finalized and frozen. Per-problem averages include successful, failed, and timed-out attempts. Tokens per solved problem divide total test tokens by the number of solved problems. K denotes thousands of tokens. No token usage, timing, or variability has been measured for this scenario.

MiniF2F-test (initial success assumption: 77.5%)
Method	Retained (per 100)	Gained (per 100) $\uparrow$	Lost (per 100) $\downarrow$	Retention (%) $\uparrow$	Net gain (pp) $\uparrow$	Historical forgetting (%) $\downarrow$
Frozen $S_{0}$ (control)	76.5	1.0	1.0	98.7	0.0	3.1
w/o Prog.	73.5	18.6	4.0	94.8	14.6	5.6
w/o Mut.	76.0	6.3	1.5	98.1	4.8	2.9
Full Method	76.5	21.9	1.0	98.7	20.9	1.4
PutnamBench (initial success assumption: 58.2%)

Table 6: Planning targets, not measured results. Forgetting and retention with DeepSeek-V4-Pro. Retained, gained, and lost are normalized per 100 audit problems, not raw counts. The initial skill is assumed to match the LLM Skill row in the main table; retained plus gained matches the component-ablation targets. Historical forgetting includes problems first solved at intermediate checkpoints. The frozen control allows sampling losses without an update. pp denotes percentage points. No standard deviations are assumed; independent runs must supply them.

Explore similar work

Jul 19, 2026cs.AI

Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution

Designing effective Lean proof agents is a central challenge in formal mathematical reasoning. Beyond building stronger provers, recent work emphasizes the workflow around Lean: how an agent decomposes proof obligations, uses tools and compiler feedback, diagnoses failures, repairs proofs, and maintains structured proof context. Motivated by code-level self-evolving agents, we study whether such workflows can be evolved rather than hand-designed. We present a self-evolving Lean proof agent in which a small fixed, trusted runtime wraps a fully mutable workspace: the proof workflow, prompts, and tools. Unlike most self-evolving systems, which optimize against a fixed external benchmark, our system coevolves the agent and its benchmark. Between generations, the highest-scoring agent (the champion) revises the active task distribution through a mastery-throttled curriculum update that introduces harder proof obligations only after the current level is mastered, and a single-anchor recalibration re-runs the champion on the updated benchmark to keep scores comparable as difficulty rises. All evolution stays inside a Lean-grounded verification loop: however the agent rewrites itself, a success counts only when its behavior yields Lean-verified proofs under a trusted snapshot, and each attempt must emit a machine-readable, Lean-grounded proof context whose representation may evolve but whose groundedness is enforced. We run the coevolving trajectory and a fixed-benchmark baseline for 15 active generations and compare them on a held-out miniF2F test split. The best coevolving agent reaches a 45.1% held-out solve rate, versus 12.7% for the seed and 32.0% for the best fixed-benchmark agent, showing that verifier-grounded self-evolution can improve Lean proof workflows under a coevolving benchmark.

Yuqing Li, Zeguan Wu, Yu Gan +1

University of Pittsburgh

Theorem Proving Agentic Workflow Design

Ask PDF

Jul 30, 2026cs.AI

VeriSkill: A Self-Evolution Framework for Program Verification Skills

Automating program verification with LLM agents requires generating specifications, annotations, auxiliary lemmas, and tool invocations, all of which depend on reusable skills. A natural remedy is skill self-evolution: distilling skills from trajectories and refining them through feedback. However, existing evolution methods struggle with program verification tasks because they cannot reliably identify skill-specific failures or extract actionable signals from opaque verifier feedback. In this paper, we propose VeriSkill, a self-evolution framework built for program verification. It attributes verification failures to skill deficiencies, distills diagnostic signatures into reusable lessons, and iteratively refines candidate skills, admitting only revisions that improve verification performance while preserving program semantics. Experiments show that VeriSkill consistently outperforms all baselines across multiple verification tools, agent frameworks, and LLM backends.

Changguo Jia, Tianqi Zhao, Zhiyou Xiao +2

Peking University, Beijing, China · Zhongguancun Laboratory, Beijing, China · Shanghai Jiao Tong University, Shanghai, China

Skill Evolution Skills Self-Evolution Large Language Model Backbones

Ask PDF

Aug 6, 2026cs.AI

SkillHEX: Improving Agent Skills via Hypothesis-Driven Autonomous Exploration and Exploitation

Although agent skills equip LLMs with reusable procedural knowledge, manual maintenance suffers from high costs, unscalability, and misalignment. Real-world deployments thus require autonomous, on-demand skill evolution at test time, constrained by limited interaction budgets and a lack of training or validation sets. This setting introduces a severe sparse reward challenge, where outcomes conflate multiple latent failure causes. Under such ambiguity, existing methods that greedily refine a single incumbent skill are particularly vulnerable to an exploitation trap, allowing early misdiagnoses to exhaust limited trials along unproductive trajectories. To address this, we introduce SkillHEX, a closed-loop framework coupling hypothesis-driven self-verification with evidence-guided tree search. SkillHEX translates falsifiable failure hypotheses into executable tests, producing diagnostic evidence as dense reward without additional environment attempts. This evidence guides a search over persistent skill-revision branches, dynamically balancing the exploitation of supported edits with the exploration of plausible alternatives. Evaluated on 87 tasks from SkillsBench, SkillHEX outperforms existing self-evolving methods and achieves an average pass rate of 55.9% and 57.9% using GPT-5.3-Codex and Claude Opus 4.7 under a five-iteration budget, respectively.

Yuru Feng, Yaoqi Chen, Beidi Zhao +7

Microsoft · University of California, San Diego · University of Science and Technology of China +1

Self-Evolving Skill Libraries Skills Exploitation Exploration

Ask PDF