SkillEvoLean：Lean证明者的变异增强技能进化

技能进化提供了一种在不更新参数的情况下改进大语言模型智能体的有前途的方法，但其在形式定理证明中的应用仍未得到充分探索。现有方法主要针对自然语言推理，通过分析成功和失败的轨迹并逐步修改解决策略来提高技能。尽管Lean验证器提供了可靠的执行反馈，但当所有采样轨迹都失败时，现有的技能进化方法缺乏成功的轨迹来推断有效的更新方向。此外，这些方法也主要关注根指令文件，因此没有充分探索包括数学概念和证明技术在内的参考知识的演变。为了解决这些限制，我们提出了一个突变增强技能自我进化框架，用于构建技能增强的Lean证明者。该框架通过渐进式和基于突变的更新，共同演化出高级解决策略及其参考知识。渐进进化从成功和失败的轨迹中获得局部改进，而当无法生成完整的证明时，就会触发突变，对数学概念进行采样，以在验证者的反馈下产生和选择新的候选技能。我们在 MiniF2F、PutnamBench、2025 年国际数学奥林匹克 (IMO 2025) 和 2026 年美国数学奥林匹克 (USAMO 2026) 上评估我们的方法。在相同的主干模型、轨迹采样预算和测试时间计算下，我们的方法在 GPT-5.5 上分别实现了 100.0%、90.6%、4/6 和 4/6 的证明成功率，优于基线方法。进一步分析表明，概念引导突变在 MiniF2F 和 PutnamBench 上分别优于随机文本引导突变 6.9 和 8.2 个百分点，同时在 IMO 2025 和 USAMO 2026 上解决了一个额外问题。