自进化 Lean 证明代理靠基准共演化，miniF2F 达到 45.1%

omarsar0 · x · 2026-07-22

这篇论文讨论的是可自修改的 Lean 证明代理，核心观点是：如果代理会自我进化，基准也应该一起进化，而不是永远盯着固定测试集优化。

系统用一个很小的可信运行时包住整个可变工作区，包括 workflow、prompt 和工具。
每一代里，当前冠军会通过 mastery-throttled curriculum 调整任务分布：只有当当前难度被掌握后，才加入更难的证明义务。
为了让不同阶段的分数还能比较，系统会做一次 single-anchor recalibration，在更新后的基准上重跑冠军。
所有成功都必须经过 Lean 验证器确认：只有在可信快照下产出可验证证明，结果才算数。
在 15 代之后，最佳共演化代理在 miniF2F 的 held-out solve rate 达到 45.1%，明显高于 seed 的 12.7% 和固定基准方案中的最佳 32.0%。

论文的结论是：把自我修改放进验证器约束的闭环里，同时让课程难度共演化，能显著抬高形式化证明代理的上限。

「漫话AGI」频道最新