SkillEvoLean：面向 Lean 证明器的变异增强技能演化

arXiv:2610.01799v1 发布类型：新 摘要：技能演化为在不更新参数的情况下改进大型语言模型智能体提供了一种很有前景的方法，但其在形式化定理证明中的应用仍未得到充分探索。现有方法主要面向自然语言推理，通过分析成功和失败的轨迹，并逐步修订求解策略来改进技能。尽管 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 上均多解决了一道题。