SkillEvoLean 让 Lean prover 在没有成功轨迹时也能通过数学概念驱动 mutation 自我演化

Zhou、Yang 与 Zhang 提出 mutation-enhanced skill self-evolution framework，同时演化 Lean prover 的高层 solving policy 与 reference knowledge。普通 skill evolution 往往依赖成功/失败轨迹对比；SkillEvoLean 在所有 sampled trajectories 都失败时，会采样数学概念生成新的 skill candidates，并用 Lean verifier feedback 选择 mutation。论文在相同 backbone、trajectory budget 与 test-time compute 下，使用 GPT-5.5 报告 MiniF2F 100.0%、PutnamBench 90.6%、IMO 2025 4/6、USAMO 2026 4/6；concept-guided mutation 相比 random-text mutation 在 MiniF2F 和 PutnamBench 分别提高 6.9 与 8.2 个百分点。