自进化 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」频道最新

• 观点：Agent 真正的瓶颈是企业数据工程能力 — dhruv2038 · 2026-09-11
• François Fleuret:人类只有「留在幼儿园」和与人机融合两条路 — francoisfleuret · 2026-09-11
• 「AI 竞赛中国论」遭反弹：一条 IG Reels 点出谬误获 50 万赞 — louisvarge · 2026-09-11
• 后 AI 时代没有边做边学,智能廉价到该提前学完 — rachittshah · 2026-09-11
• AI 风险评测遭质疑：研究者称评估方安全监控“草率得离谱” — Kyrannio · 2026-09-11
• AI 圈梗:改果蝇和 agent 集群也「值得冒险」吗 — dejavucoder · 2026-09-11

更多「漫话AGI」频道 AI 资讯 →