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

该论文提出 SkillEvoLean，一种面向 Lean 证明器的突变增强技能自演化框架。针对现有技能演化方法依赖成功轨迹、只关注根指令文件的问题，该框架同时演化高层求解策略与其参考知识：渐进演化从成功与失败轨迹中提取局部改进，当无法生成完整证明时触发突变，采样数学概念并在验证器反馈下生成、筛选新的技能候选。在 MiniF2F、PutnamBench、IMO 2025 与 USAMO 2026 上，相同骨干模型、采样预算与测试时算力下，证明成功率分别为 100.0%、90.6%、4/6、4/6。

此前技能演化多用于自然语言推理，且在形式化定理证明中，一旦所有采样轨迹都失败，就缺少成功轨迹来推断更新方向。该工作把演化对象从单一指令文件扩展到数学概念与证明技巧等参考知识，并在无完整证明时用突变机制继续搜索改进方向，给出了可比条件下的多基准成功率。

机制分两条路径：渐进演化在有成功或失败轨迹时做局部策略修订；当没有任何完整证明时触发突变，通过采样数学概念生成新技能候选，并依据 Lean 验证器的执行反馈筛选保留。高层求解策略与参考知识被联合演化，从而在不更新模型参数的条件下改变 agent 的解题行为。

对构建 Lean 或形式化证明类 agent 的产品而言，该方法把验证器反馈转化为可积累的技能资产，而非一次性提示，可能降低对模型微调的依赖；但报告中的成功率依赖特定骨干模型、采样预算与测试时算力，工程落地时需先复现这些约束下的成本与收益。

• 在 Lean 证明 agent 产品中引入技能库版本管理，把渐进演化与突变产生的技能候选作为可审计、可回滚的资产。
• 针对全失败轨迹场景设计独立触发流程，用验证器反馈筛选突变生成的数学概念候选，避免演化停滞。
• 在 MiniF2F、PutnamBench 等基准上搭建与论文对齐的评测配置，验证相同算力预算下的成功率提升是否可复现。

• 论文中突变生成数学概念的具体采样与筛选策略细节未在证据中给出。
• 成功率结果是否依赖特定骨干模型，换用其他模型后是否保持。
• 该方法与参数微调、其他技能演化方法的直接对比结果未在证据中说明。
• 多基准上达到该成功率的实际算力与时间成本未被披露。