SkillEvoLean: Mutation-enhanced skill evolution for Lean provers
作者: Kuo Zhou, ZiXion Yang, Lu Zhang
分类: cs.LG
发布日期: 2026-10-01
💡 一句话要点
提出Mutation增强的技能自演化框架以提升Lean证明器
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 技能演化 形式化定理证明 Lean验证器 突变机制 自动推理 数学教育 大型语言模型
📋 核心要点
- 现有技能演化方法在形式化定理证明中的应用不足，尤其是在所有轨迹失败时缺乏有效的更新方向。
- 本文提出了一种基于突变的技能自演化框架，通过渐进和突变更新共同演化解决策略和参考知识。
- 在MiniF2F和PutnamBench等基准测试中，本文方法在成功率上显著超越了基线方法，表现出更强的解决能力。
📝 摘要（中文）
技能演化为提升大型语言模型代理提供了一种有前景的方法，但在形式化定理证明中的应用仍然未被充分探索。现有方法主要针对自然语言推理，通过分析成功和失败的轨迹来改进技能。然而，当所有采样轨迹失败时，现有技能演化方法缺乏成功轨迹以推断有效的更新方向。为了解决这些限制，本文提出了一种基于突变的技能自演化框架，旨在构建技能增强的Lean证明器。该框架通过渐进和基于突变的更新共同演化高层解决策略及其参考知识。我们在多个基准测试中评估了该方法，结果显示其在多个任务上超越了基线方法。
🔬 方法详解
问题定义：本文旨在解决现有技能演化方法在形式化定理证明中的不足，尤其是在所有轨迹失败时缺乏成功轨迹以推断有效的更新方向。现有方法主要集中于自然语言推理，未能充分利用Lean验证器的反馈。
核心思路：提出的框架通过渐进演化和突变机制共同演化高层解决策略及其参考知识。当无法生成完整证明时，突变机制会被触发，以采样数学概念并生成新的技能候选。
技术框架：该框架包括两个主要模块：渐进演化模块和突变模块。渐进演化模块从成功和失败的轨迹中提取局部改进，而突变模块则在失败时生成新的技能候选。
关键创新：最重要的技术创新在于引入了突变机制，使得在缺乏成功轨迹时仍能生成有效的技能候选，显著提升了技能演化的灵活性和有效性。
关键设计：在参数设置上，框架使用了与GPT-5.5相同的基础模型，并在轨迹采样预算和测试时间计算上保持一致，确保了实验的公平性和可比性。
🖼️ 关键图片
📊 实验亮点
在MiniF2F和PutnamBench上，本文方法的证明成功率分别达到了100.0%和90.6%，在IMO 2025和USAMO 2026上也解决了额外的问题，显示出相较于基线方法的显著提升，尤其是概念引导的突变相较于随机文本引导的突变提升了6.9和8.2个百分点。
🎯 应用场景
该研究具有广泛的应用潜力，尤其是在形式化定理证明、自动推理和数学教育等领域。通过提升Lean证明器的能力，能够更有效地辅助数学问题的解决，推动相关领域的研究与发展。
📄 摘要（原文）
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.