arXiv 论文提出 LLM 智能体在 Lean 中设计进化算法并证明运行时上界

查看 PDF HTML（实验性）

摘要：LLM 现在能在 Lean 中证明困难的定理。它们能否也能设计算法并证明其正确性与效率？LLM 引导的优化启发式设计（如 AlphaEvolve）纯粹是经验性的。结合 LLM 的自动定理证明器证明给定的命题。迄今为止，几乎没有证据表明 LLM 能同时做到两者：设计一个算法并通过数学证明保证其效率。我们提出了一个分阶段流水线，模仿进化算法设计与分析中的研究方法。智能体提出黑盒优化算法，Lean 守卫过滤掉有缺陷的设计。随后智能体定义一个势函数并证明漂移界限，从而保证相对基线算法的期望运行时间改进。在整个流水线中，算法从不进行经验比较。该智能体生成了一个在 CycleUncover 问题上的期望运行时间为 $O(n^2)$ 的黑盒优化算法，而经典的 (1+1) EA 需要运行时间 $e^{\Omega(n)}$。该流水线还设计并分析了一个用于整数 valued 次模最小化的黑盒优化算法，期望运行时间为 $O(n^{2+2c})$，并且在 LeadingOnes 上达到了最优阶 $O(n^2)$。在 8 类问题上，15 次使用前沿模型的运行中有 12 次完成了整条流水线，并得到机器验证的期望运行时间界限。消融实验表明，去掉分阶段过程并要求智能体零样本完成带运行时间保证的算法设计，会导致对预设基线算法（随机搜索）的复制或不完整的证明。我们的研究表明，Lean 中机器验证的规约可以取代开放式算法发现中的经验评估。据我们所知，这是首个能在 Lean 中设计高效黑盒优化算法并附带机器验证运行时间界限的自动化流水线示例。

提交历史

来自：Per Kristian Lehre [查看邮件]
[v1] 2026年10月26日 周一 15:22:04 UTC（557 KB）