Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean

Per Kristian Lehre

cs.AIOct 26, 2026

Agentic Algorithm Design: LLMs that Propose, Formalise, and Prove Runtime Bounds for Evolutionary Algorithms in Lean

Authors: Per Kristian Lehre

Organizations: School of Computer Science, University of Birmingham, UK

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^{Ω(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.

Figures & tables

Work	Algorithmic artefact	Process	Designed by	Analysed by	Machine-checked property
Li et al. (2024)	first-order convex methods	deterministic	human	human	convergence rate
Vajjha et al. (2021)	value / policy iteration	stochastic (MDP)	human	human	convergence
Schäffeler & Abdulaziz (2025)	approximate policy iteration	stochastic (MDP)	human	human	convergence
Ospanov et al. (2025) ; Varambally et al. (2025) ; Li et al. (2026)	(proof / code search)	n/a	n/a	LLM	given theorem or code specification
Romera-Paredes et al. (2024) ; Novikov et al. (2025) ; Lange et al. (2025)	heuristics, constructions	—	LLM	—	none (empirical validation)
van Stein & Bäck (2025)	black-box optimisation algorithms (metaheuristics)	stochastic	LLM	—	none (empirical benchmarking)

Table 1: Overview of some related work in automating the design and formal analysis of algorithms. The first group machine-checks analyses of human-designed algorithms. The second group produces machine-checked proofs, but of a theorem or specification given to it. The third group discovers algorithms, but validates them only empirically. This work lies at the intersection: the algorithm is proposed by an LLM, its analysis is produced by an LLM, and the property machine-checked is the expected runtime of a stochastic process.

Panel of Figure 2 — Algorithm 1 Black-Box Optimisation Algorithm

Figure 1: Drift conditions checked by the pipeline (Corollary 3.1 , Stages 10f–10i) at a reachable, non-optimal state

y

. The sets of random draws

\mathrm{Good}(y)

\mathrm{Worsen}(y)

\mathrm{BigWorsen}(y)

and

\mathrm{Jump}(y)

are shown by where they send the next potential

\Phi^{\prime}

; the arrows give the required probability bounds, which together yield

\mathds{E}\left[T_{A}\right]\leq 4/(\varepsilon p)

Figure 2: A simplified overview of the staged pipeline. The pipeline is seeded with a problem card, an algorithm $A^{i}$ , and a proof of its running time. The pipeline produces a new algorithm $A^{i+1}$ with improved runtime bound relative to algorithm $A^{i}$ . Table 3 provides detailed descriptions of the pipeline stages shown in red.

#	Problem	Model	Pipeline	#gen	Algorithm	Complete	Order	Tokens	Lean	App.
1	OneMax	Opus 5	staged	1	$(1{+}1)$ EA, rate $\frac{1}{n+1}$	yes	$O(n^{3})$	n/r	2,036	F.2
2	LeadingOnes	Opus 5.5	staged	1	fitness-dependent rate $\frac{1}{\mathrm{LO}+2}$	yes	$O(n^{3})$	160k	1,262	F.3
3	LeadingOnes , $e^{-1}$ lemma	Opus 5.5 §	staged	1	fitness-dependent rate $\frac{1}{\mathrm{LO}+2}$	yes	$O(n^{2})$	191k	1,553	F.4
4	Jump k	Opus 5.5	staged	1	$(1{+}1)$ EA, rate $\frac{1}{n+1}$	yes	$O(n^{k+2})$	144k	1,086	F.5
5	Jump k , $e^{-1}$ lemma	Opus 5.5	staged	3	rate cycling with a learned phase bit	yes	$O(n^{k+1})$	396k	1,335	F.6
6	CycleUncover	Fable 5.1	staged	1	cycle walk (learn-then-solve)	yes	$O(n^{2})$	538k	2,373	F.7

Table 2: All runs. Each row is one pipeline session driven by the named model. Rows 1–18 use the CLI backend, through which the model exchanges prompts and responses with the pipeline over stdin/stdout; rows 19–21 use the vLLM backend ( Appendix C ). “Staged” is the full pipeline of Table 3 ; “zero-shot” is the one-stage ablation of Section 5.5 . Rows 16–21 are ablations: the zero-shot pipeline, or a weaker model; rows 19–21 use open-weight models run on HPC clusters ( Section F.1 ). Complete means that every stage was machine-checked with no sorry ; otherwise the last stage passed is given in parentheses (the run stopped at the following stage). Order is the order of the machine-checked bound on

\mathds{E}\left[T_{A}\right]

, which holds for all

n\geq 3

and every instance (for staged runs it is

4/(\varepsilon_{1}p_{1})

). Tokens is the number of output tokens (including reasoning) generated by the model that drove the run, from launch to the last accepted stage; n/r means not recorded. Lean is the number of lines of Lean code the model contributed to the accepted proof, excluding blank lines, comments, the prompt, the API and the problem card. LO is the fitness of the elitist reference point; the LeadingOnes card marked “

e^{-1}

lemma” additionally supplies the inequality

e^{-m/(r-1)}\leq(1-1/r)^{m}

k

is the bandwidth for BandwidthVC and the gap width for Jump k , and

n^{c}

bounds the values of a SubmodularMin instance. #gen is the number of generations of the pipeline used to obtain the result; for a run with several generations, the row reports the last generation only (Tokens and Lean are those of that generation). Pseudocode, potentials and constants of every run are given in Appendix F .

Figure 3: CycleUncover . Right: problem definition in human-readable form. Left: visualisation of an instance for even

n

(not shown to the agent). The vertices

\sigma(1),\dots,\sigma(2h)

form a cycle of even length

2h

; for odd

n

, bit

\sigma(n)

does not affect the fitness. The problem is to find a maximum independent set of the cycle; an optimal selection, of value

3h

, is shown in red.

Appendix figures & tables24 assets

Supplementary material from the paper’s appendix.

Appendix

Stage	Name	Formalisation
Algorithm construction (Stages 0–8)
0	DesignLock [I]	Commit to $\mathcal{Y},\mathtt{init},\mathtt{step},\mathtt{query}$ and a qualitative account of which component of $y\in\mathcal{Y}$ tracks $f$ ; no numeric constants yet.
1	Construct- AlgorithmCom- ponents [F*]	Define $\mathcal{Y}$ , $\mathtt{init}:\mathcal{Z}\to\mathcal{Y}$ , $\mathtt{step}:\mathcal{Z}\times\mathcal{Y}\times\mathbb{R}\to\mathcal{Y}$ , $\mathtt{query}:\mathcal{Y}\to\mathcal{X}$ .
1c	StepMeasur- ability [F-]	$\mathtt{step}$ is measurable.
2	Completeness1 [F-]	$\forall x\in\mathcal{X},\forall y\in\mathcal{Y},\ \mathtt{reachable}(y)\rightarrow\exists z\in\mathcal{Z},\exists f\in\mathbb{R},\ \mathtt{query}(\mathtt{step}(z,y,f))=x$ .
3	NonAbsorbing [F-]	$\forall y\in\mathcal{Y},\ \mathtt{reachable}(y)\rightarrow\forall f\in\mathbb{R},\ \exists z_{1},z_{2}\in\mathcal{Z},\ \mathtt{query}(\mathtt{step}(z_{1},y,f))\neq\mathtt{query}(\mathtt{step}(z_{2},y,f))$ .

Appendix

Table 3: The stages of the pipeline that generates one algorithm

A^{i+1}=(\mathcal{Y},\mathtt{init},\mathtt{step},\mathtt{query})

and proves it faster than its predecessor, restated in the

(\mathcal{X},\mathcal{Y},\mathcal{Z},\mathbb{R})

formalism of Algorithm 1 . [I] is an informal stage producing prose (no Lean code) with candidate selection (see Section 4.1 and Section 4.2 ), [F*] is a formal stage that introduces new Lean definitions used by later stages, and [F-] a formal stage that only proves properties of definitions introduced earlier; in both, the Lean declarations produced are checked by Lean and carried forward.

f\in\mathcal{F}

denotes a fixed fitness function (an element of the problem class, e.g. OneMax composed with an unknown target bitstring), so that

\mathtt{reachableWith}(f,y)

(as opposed to

\mathtt{reachable}(y)

) restricts to states reachable when the true fitness fed to

\mathtt{step}

is always

f

z,z_{1},z_{2}\in\mathcal{Z}

denote random draws;

\mathrm{unif}(z)\in\mathcal{X}

is the bitstring obtained by sampling each coordinate of

z

against threshold

1/2

n

is the bitstring length, and a ‘prev’ subscript refers to the previous algorithm/potential pair in the outer self-improvement loop.

Panel of Figure 8 — Algorithm 2 (1+1) EA

Run	Cluster	Started	Pipeline version	Hours	Last passed
generous-dragon-779	Sulis	2026-09-21	optimisation	23.8	3
driven-blaze-773	Sulis	2026-09-18	optimisation	23.8	1
denim-paper-771	Sulis	2026-09-17	split_v9	21.6	3
super-moon-761	Sulis	2026-09-15	split_v9	23.3	3
bumbling-plant-742	Sulis	2026-09-13	split_v9	23.2	3
avid-waterfall-734	Isambard-AI	2026-09-12	split_v9	23.6	3

Appendix

Table 4: Open-weight runs on OneMax with the most recent pipeline versions. “Last passed” is the last stage that was machine-checked.

Panel of Figure 10 — Algorithm 3 $(1{+}1)$ -style hill-climber with rate $1/(n+1)$ ( OneMax , Claude Opus 5).

Panel of Figure 11 — Algorithm 4 Fitness-dependent mutation around an elitist reference point ( LeadingOnes , Claude Opus 5.5).

Panel of Figure 12 — Algorithm 5 $(1{+}1)$ -style hill-climber with rate $1/(n+1)$ ( Jump k , Claude Opus 5.5).

Panel of Figure 13 — Algorithm 6 Self-adjusting mask rate ( Jump k with the $e^{-1}$ lemma, generation 1).

Panel of Figure 14 — Algorithm 7 Failure-doubled mask rate ( Jump k with the $e^{-1}$ lemma, generation 2).

Panel of Figure 15 — Algorithm 8 Rate cycling with a learned phase bit ( Jump k with the $e^{-1}$ lemma, generation 3).

Panel of Figure 16 — Algorithm 9 Cycle walk ( CycleUncover , Claude Fable 5.1).

Panel of Figure 17 — Algorithm 10 Random search with a recorded incumbent ( CycleUncover , zero-shot, Claude Fable 5.1).

Panel of Figure 18 — Algorithm 11 Design 4 ( CycleUncover , Claude Sonnet).

Panel of Figure 19 — Algorithm 12 Edge probing, then solve ( VertexCover , Claude Fable 5.1).

Panel of Figure 20 — Algorithm 13 Interleaved window probing and solving ( BandwidthVC , Claude Fable 5.1).

Panel of Figure 21 — Algorithm 14 Direction-adaptive asymmetric mutation ( BandwidthVC , Claude Fable 5.1).

Panel of Figure 22 — Algorithm 15 $(1{+}1)$ EA with rate $1/n$ ( BandwidthVC , zero-shot, Claude Fable 5.1).

Panel of Figure 23 — Algorithm 16 Fill-then-prune mutation ( BandwidthVC , Claude Fable 5.1).

Panel of Figure 24 — Algorithm 17 Window-repair random search ( BandwidthVC , Claude Opus 5.5, attempt 2).

Panel of Figure 25 — Algorithm 18 Projected subgradient descent on the Lovász extension ( SubmodularMin , Claude Opus 5.5).

Panel of Figure 26 — Algorithm 19 Polarity-adaptive asymmetric mutation ( wcvc , Claude Fable 5.1).

Panel of Figure 27 — Algorithm 20 Regime-switching asymmetric mutation ( wcvc , Claude Opus 5.5).

Panel of Figure 28 — Algorithm 21 Fitness-directed asymmetric mutation ( WellCoveredVC , Claude Fable 5.1).

Figure 4: Progress through the 28 pipeline stages for the runs of Table 2 , numbered as in the table, one point per round. (a) Runs that completed the pipeline: the number of stages passed, including the drops caused by backtracking; the final point at 28 marks completion. Row 14 includes a first attempt that stalled at Stage 10c before the pipeline restarted.x1 (b) Runs that did not complete: the highest stage reached so far, on a logarithmic round axis (rows 12 and 17 continue for thousands of automatic rounds after their best level). The zero-shot runs (rows 16 and 18) have a single stage and are omitted.

Figure 5: Per-stage statistics of the runs of Table 2 , numbered as in the table. Top: number of attempts per stage (colour on a logarithmic scale; the number is shown when a stage needed more than one attempt); a red frame marks the stage at which an incomplete run stopped. For rows 19–21 (vLLM backend) one attempt is a batch of 256 samples. Bottom: share of wall-clock time spent in each stage, averaged over the 12 completed frontier-model runs. Each run is counted up to its first completion or, if it did not complete, up to its last round at its highest stage. The zero-shot runs (rows 16 and 18) have a single stage and are omitted.

Automated Algorithm Discovery

Automated algorithm discovery develops methods that generate and test executable algorithms for optimization, science, software, and machine learning.

See all 169 papers

Mar 9, 2026

Advancing Automated Algorithm Design via Evolutionary Stagewise Design with LLMs

With the rapid advancement of human science and technology, problems in industrial scenarios are becoming increasingly challenging, bringing significant challenges to traditional algorithm design. Automated algorithm design with LLMs emerges as a promising solution, but the currently adopted black-box modeling deprives LLMs of any awareness of the intrinsic mechanism of the target problem, leading to hallucinated designs. In this paper, we introduce Evolutionary Stagewise Algorithm Design (EvoStage), a novel evolutionary paradigm that bridges the gap between the rigorous demands of industrial-scale algorithm design and the LLM-based algorithm design methods. Drawing inspiration from CoT, EvoStage decomposes the algorithm design process into sequential, manageable stages and integrates real-time intermediate feedback to iteratively refine algorithm design directions. To further reduce the algorithm design space and avoid falling into local optima, we introduce a multi-agent system and a "global-local perspective" mechanism. We apply EvoStage to the design of two types of common optimizers: designing parameter configuration schedules of the Adam optimizer for chip placement, and designing acquisition functions of Bayesian optimization for black-box optimization. Experimental results across open-source benchmarks demonstrate that EvoStage outperforms human-expert designs and existing LLM-based methods within only a couple of evolution steps, even achieving the historically state-of-the-art half-perimeter wire-length results on every tested chip case. Furthermore, when deployed on a commercial-grade 3D chip placement tool, EvoStage significantly surpasses the original performance metrics, achieving record-breaking efficiency. We hope EvoStage can significantly advance automated algorithm design in the real world, helping elevate human productivity.

Chen Lu, Ke Xue, Chengrui Gao +5

National Key Laboratory for Novel Software Technology, Nanjing University, China · School of Artificial Intelligence, Nanjing University, China · Huawei Noah’s Ark Lab, China

Automated Algorithm Discovery Automated Heuristic Design Evolutionary Optimization Electronic Design Automation Bayesian Optimization

Ask PDF

Mar 3, 2026

From Heuristic Selection to Automated Algorithm Design: LLMs Benefit from Strong Priors

Large Language Models (LLMs) have already been widely adopted for automated algorithm design, demonstrating strong abilities in generating and evolving algorithms across various fields. Existing work has largely focused on examining their effectiveness in solving specific problems, with search strategies primarily guided by adaptive prompt designs. In this paper, through investigating the token-wise attribution of the prompts to LLM-generated algorithmic codes, we show that providing high-quality algorithmic code examples can substantially improve the performance of the LLM-driven optimization. Building upon this insight, we propose leveraging prior benchmark algorithms to guide LLM-driven optimization and demonstrate superior performance on two black-box optimization benchmarks: the pseudo-Boolean optimization suite (pbo) and the black-box optimization suite (bbob). Our findings highlight the value of integrating benchmarking studies to enhance both efficiency and robustness of the LLM-driven black-box optimization methods.

Qi Huang, Furong Ye, Ananta Shahane +2

Leiden Institute of Advanced Computer Science (LIACS), Leiden University, 2333 CC Leiden, The Netherlands

Large Language Model-Guided Optimization Automated Algorithm Discovery Automated Heuristic Design Black-Box Optimization

Ask PDF

Oct 2, 2026

AdaEva: Accelerating LLM-Driven Algorithm Design with Adaptive Partial Evaluation

Large Language Models (LLMs) are increasingly used for automated algorithm design. However the computational cost of evaluating the generated algorithms can be excessive. We consider the common LLM-driven automated algorithm design (LLM4AD) setting in which a candidate algorithm is evaluated by aggregating its performance over a shared set of training instances. This instance-wise structure raises a natural question: must every candidate be evaluated on the entire instance set before deciding whether it remains competitive? Taking inspiration from algorithm configuration, we introduce AdaEva, a drop-in adaptive partial-evaluation framework that progressively evaluates candidates on larger subsets of the same instance pool and eliminates unpromising candidates as evidence accumulates. Importantly, AdaEva leaves the underlying LLM4AD procedure and per-instance evaluator unchanged and requires no prior knowledge about instance difficulty. We instantiate this idea using successive halving (AdaEva-S) and statistical racing (AdaEva-R), and evaluate both mechanisms across three representative LLM4AD frameworks, multiple LLM backbones, and optimization domains spanning combinatorial and continuous black-box optimization. Under matched evaluation budgets, AdaEva more reliably balances evaluation effort across candidates than fixed partial-evaluation strategies, yielding strong search efficiency and anytime performance together with improved held-out generalization across the evaluated settings.

Tai Nguyen, Fei Liu, Phong Le +2

University of St Andrews, United Kingdom · Sorbonne Universit´e, CNRS, LIP6, France · University of Zurich and ETH Zurich, Switzerland

Large Language Model-Guided Optimization Automated Algorithm Discovery

Ask PDF

Abstract

Automated Algorithm Discovery

Explore similar work

Advancing Automated Algorithm Design via Evolutionary Stagewise Design with LLMs

From Heuristic Selection to Automated Algorithm Design: LLMs Benefit from Strong Priors

AdaEva: Accelerating LLM-Driven Algorithm Design with Adaptive Partial Evaluation