arXiv 论文提出 LLM 智能体在 Lean 中设计进化算法并证明运行时上界
Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean
AI 导读
Per Kristian Lehre 等提出分阶段流水线，LLM 智能体提出黑盒优化算法，由 Lean 守卫过滤缺陷设计，再定义势函数并证明漂移上界，全程不做经验比较。
推荐理由
论文展示了 LLM 在 Lean 中设计优化算法并机器检查运行时证明的分阶段流程，为算法自动发现替代经验评估提供了实例。
正文 · 原文
Abstract:LLMs now prove hard theorems in Lean. Can they also design algorithms and prove their correctness and efficiency? LLM-guided design of optimisation heuristics (such as AlphaEvolve) is purely empirical. Automated theorem provers with LLMs prove given statements. So far, there has been little evidence that LLMs can do both: design an algorithm and guarantee its efficiency by a mathematical proof. We present a staged pipeline modelled after research methodology in design and analysis of evolutionary algorithms. The agent proposes black-box optimisation algorithms, and Lean guards filter out flawed designs. The agent then defines a potential function and proves drift bounds that guarantee an expected runtime improvement over the baseline algorithm. At no point in the pipeline are the algorithms compared empirically. The agent generates a black-box optimisation algorithm with expected runtime $O(n^2)$ on a CycleUncover problem, where the classical (1+1) EA needs runtime $e^{\Omega(n)}$. The pipeline also designs and analyses a black-box optimisation algorithm for integer-valued submodular minimisation with expected runtime $O(n^{2+2c})$, and it matches the optimal order $O(n^2)$ on LeadingOnes. Across 8 problem classes, 12 of 15 runs with frontier models complete the pipeline with a machine-checked expected-runtime bound. An ablation study shows that removing the staging and asking the agent to zero-shot an algorithmic design with a runtime guarantee leads to a copy of the seeded baseline algorithm (random search) or to incomplete proofs. Our study suggests that machine-checked specifications in Lean can replace empirical evaluation in open-ended algorithm discovery. To the best of our knowledge, this is the first example of an automated pipeline that designs efficient black-box optimisation algorithms with machine-checked runtime bounds in Lean.
| Comments: | A github repository with source code will be published later |
| Subjects: | Artificial Intelligence (cs.AI); Neural and Evolutionary Computing (cs.NE) |
| Cite as: | arXiv:2610.35595 [cs.AI] |
| (or arXiv:2610.35595v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.35595 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Per Kristian Lehre [view email]
[v1]
Mon, 26 Oct 2026 15:22:04 UTC (557 KB)
来源：arXiv cs.AI · arxiv.org