arXiv · cs.AI· Per Kristian Lehre·· 15 小时前精选AI 评分57
arXiv 论文提出 Agentic Algorithm Design：LLM 在 Lean 中设计进化算法并证明运行时界
Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean
来源与原文
arXiv · cs.AI
作者：Per Kristian Lehre
发布时间：（北京时间）
阅读原始来源 · arxiv.org ↗完整链接与内容说明
https://arxiv.org/abs/2610.35595v1
本站目前仅有 AI 导读与摘要，未展示原文正文；技术细节、代码和完整结论请查看原始来源。
AI 导读
Per Kristian Lehre 等提出分阶段管线，让智能体提出黑盒优化算法，用 Lean 证明期望运行时界并过滤缺陷设计。智能体给出的算法在 CycleUncover 问题达 O(n²)，而经典 (1+1) EA 需 e^Ω(n)；在 8 个问题类上，15 次运行中 12 次用前沿模型完成机器验证的运行时证明，消融显示去掉分阶段会导致照抄基线或证明不完整。
推荐理由
论文展示了分阶段管线让智能体在 Lean 中机器验证算法运行时证明，为无实证评估的开放式算法发现提供了可检验的替代路径。
来源：arXiv · cs.AI · arxiv.org