LLM 在 Lean 中设计并证明算法运行时间界

LLM 流水线在 Lean 中设计算法并机器校验其运行时间界。

资讯摘要

论文提出一条分阶段流水线，让 LLM 智能体提出黑盒优化算法，由 Lean 校验过滤有缺陷的设计，再定义势函数并证明漂移界，从而给出期望运行时间保证，全程不做经验对比。作者报告：在 CycleUncover 上生成的算法期望运行时间为 O(n²)，而经典 (1+1) EA 需 e^(Ω(n))；另为整数子模最小化设计算法，期望运行时间 O(n^(2+2c))，在 LeadingOnes 上匹配经典 O(n²)。8 类问题、15 次运行中 12 次完成机器校验的运行时间界。

要点速读

1. 流水线分阶段：智能体提出算法，Lean 过滤缺陷设计，再证明漂移界给出期望运行时间保证，不做经验对比。
2. CycleUncover 上生成算法期望运行时间 O(n²)，经典 (1+1) EA 为 e^(Ω(n))；整数子模最小化为 O(n^(2+2c))，LeadingOnes 匹配 O(n²)。
3. 8 类问题 15 次运行中 12 次完成机器校验界；消融显示零样本直接要求设计会退化为随机搜索或证明不完整。

中文摘要由 AI 根据公开来源生成，可能存在理解偏差；具体能力、数字、开放时间等信息请以原文为准。
采集于 2026/10/29 08:00:21（北京时间）。 arXiv 日期为本次公告时间，论文初次投稿日期请查看原文版本记录。