arXiv：cs.LG（机器学习，全量分类）· Kuo Zhou, ZiXion Yang, Lu Zhang·· 14 小时前AI 评分40
SkillEvoLean：面向 Lean 证明器的变异增强技能进化
SkillEvoLean: Mutation-enhanced skill evolution for Lean provers
AI 导读
研究者提出 SkillEvoLean，一个面向 Lean 证明器的变异增强技能自进化框架，在不更新模型参数的前提下联合进化高层求解策略与参考知识。在 GPT-5.5 上，该方法于 MiniF2F、PutnamBench、IMO 2025 和 USAMO 2026 分别取得 100.0%、90.6%、4/6 和 4/6 的证明成功率，优于基线。
正文
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.
| Subjects: | Machine Learning (cs.LG) |
| Cite as: | arXiv:2610.01799 [cs.LG] |
| (or arXiv:2610.01799v1 [cs.LG] for this version) | |
| https://doi.org/10.48550/arXiv.2610.01799 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Kuo Zhou [view email]
[v1]
Thu, 1 Oct 2026 14:42:54 UTC (217 KB)
来源：arXiv：cs.LG（机器学习，全量分类） · arxiv.org