LLM 在 Lean 中设计算法并证明进化算法运行时上界

查看 PDF HTML（实验性）

摘要：LLM 如今能在 Lean 中证明困难定理。它们是否也能设计算法并证明其正确性与效率？由 LLM 引导的优化启发式设计（如 AlphaEvolve）纯属经验性。结合 LLM 的自动定理证明器只能证明给定命题。迄今为止，几乎没有证据表明 LLM 能同时做到这两点：设计算法并通过数学证明保证其效率。我们提出一个分阶段流水线，其建模参照了进化算法设计与分析的研究方法。智能体提出黑盒优化算法，Lean 守卫过滤掉有缺陷的设计。随后智能体定义一个势函数并证明漂移界，以保证相对于基线算法的期望运行时间改进。在流水线的任何阶段，算法都没有经过经验性比较。智能体生成了一种黑盒优化算法，在 CycleUncover 问题上期望运行时间为 $O(n^2)$，而经典 (1+1) EA 需要运行时间 $e^{\Omega(n)}$。该流水线还为整数值子模最小化设计并分析了一种黑盒优化算法，期望运行时间为 $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）