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

Summary (Overview)

• Novel pipeline: The paper presents a staged pipeline that combines LLMs with the Lean theorem prover to automatically design black-box optimisation algorithms and prove their expected runtime bounds—with no empirical evaluation whatsoever.

• Key results: Across 8 problem classes, 12 of 15 runs with frontier models completed the pipeline with machine-checked runtime bounds. The agent designed an $O(n^2)$ algorithm for a novel CYCLEUNCOVER problem where the classical (1+1) EA requires $e^{\Omega(n)}$ runtime, and achieved the classical $O(n^2)$ runtime on LEADINGONES.

• Ablation findings: Removing the staging and asking for zero-shot algorithmic design leads to copies of the seeded baseline algorithm (random search) or incomplete proofs. Open-weight models (Goedel-Prover-V2-32B, Gemma 4) failed to complete the pipeline.

• Submodular minimisation: Over five generations of the pipeline, the agent rediscovered projected subgradient descent on the Lovász extension for integer-valued submodular minimisation, improving the runtime bound from $O(n^{3+2c})$ to $O(n^{2+2c})$.

• First of its kind: To the authors' knowledge, this is the first automated pipeline that designs efficient black-box optimisation algorithms with machine-checked runtime bounds in Lean.

Introduction and Theoretical Foundation

Background and Motivation

From a theoretical computer science perspective, algorithm design requires two artefacts: (1) the algorithm itself—a finite sequence of instructions, and (2) the analysis—a mathematical proof of correctness and complexity guarantees. Traditional algorithmic design is costly and requires deep expertise, motivating research into automated design of heuristics.

Recent LLM-based heuristic design approaches (e.g., AlphaEvolve, ShinkaEvolve, LLaMEA) evaluate candidate heuristics empirically on benchmark functions. While successful, these methods provide no guarantees on correctness or performance. The paper addresses the open problem of whether AI agents can carry out algorithmic design as understood in theoretical computer science—producing both algorithms and rigorous proofs of their efficiency.

Black-Box Optimisation Framework

The paper adopts the black-box optimisation scenario (also called the query model) from the theory of evolutionary algorithms:

• An adversary picks a fitness function $f \in F$, $f: \mathcal{X} \to \mathbb{R}$
• The algorithm queries search points $x_t$ and receives fitness values $f(x_t)$
• Runtime $T_{A,f}$ is the number of queries until the algorithm queries an optimal search point
• An algorithm is a tuple $A = (\mathcal{Y}, \text{init}, \text{query}, \text{step})$

The worst-case expected runtime over a function class is $T_{A,F} = \max_{f \in F} \mathbb{E}[T_{A,f}]$.

Drift Analysis

The pipeline builds on drift analysis (Hajek, 1982; He & Yao, 2001), which measures algorithm progress via a potential function $\Phi: \mathcal{Y} \to \mathbb{R}$. The drift is the change in potential per time step: $Z_{t+1} - Z_t$ where $Z_t = \Phi(y_t)$.

The paper introduces a simplified drift theorem (Corollary 3.1) that avoids measure-theoretic complications. For all $t \in \mathbb{N}$, with $X_t \in [0,1]$:

$$(1) \quad \mathbb{1}_{\{t < T\}} p \leq \mathbb{E}\left[\mathbb{1}_{\{t < T\}} \mathbb{1}_{\{X_{t+1} \leq X_t - \varepsilon\}} \mid \mathscr{G}_t\right]$$ $$\mathbb{E}\left[\mathbb{1}_{\{t < T\}} \mathbb{1}_{\{X_t < X_{t+1}\}} \mid \mathscr{G}_t\right] \leq \mathbb{1}_{\{t < T\}} p/2, \tag{2}$$ $$\mathbb{E}\left[\mathbb{1}_{\{t < T\}} \mathbb{1}_{\{X_t + \varepsilon < X_{t+1}\}} \mid \mathcal{G}_t\right] \leq \mathbb{1}_{\{t < T\}} \varepsilon p/4. \tag{3}$$

These conditions together yield the runtime bound $\mathbb{E}[T_A] \leq 4/(\varepsilon p)$.

Methodology

The Staged Pipeline

The pipeline (Figure 2 in the paper) is seeded with a problem card and an initial algorithm (uniform random search with expected runtime $O(2^n)$). It consists of informal stages (prose descriptions) and formal stages (Lean definitions/proofs verified by the prover). Stages are repeated upon Lean failure, with backtracking determined by a Luby sequence.

Algorithm Design Stages (0–8):

• Stage 0 (DesignLock): Agent proposes informal algorithm design with justification
• Stage 1 (ConstructAlgorithmComponents): Formalise the algorithm as tuple $A = (\mathcal{V}, \text{init}, \text{step}, \text{query})$
• Stage 2 (Completeness): Algorithm must be able to query any search point from any reachable state
• Stage 3 (NonAbsorbing): Algorithm must use randomness
• Stage 4 (NotRandomSearch): Algorithm must differ from uniform random search
• Stage 5 (Adaptiveness): State update must depend on fitness responses
• Stage 6 (QueryNonInjectivity): State must carry information beyond the current query

Potential Function Stages (9a–9f):

• Agent proposes candidate potential functions with a "drift story"
• Potential must be in $[0,1]$, measurable, and zero iff the state queries an optimum
• Guard against two-valued potentials (0 and 1 only)

Drift Certificates and Runtime Bound (10a–10j):

• Define sets Good(y), Worsen(y), BigWorsen(y) for each state y
• Prove drift conditions (1)–(3) of Corollary 3.1
• Prove jump probability lower bound $p_{\text{jump}}$
• Final stage applies the runtime bound $\mathbb{E}[T_A] \leq 4/(\varepsilon p)$

Models and Implementation

• Frontier models: Claude Opus 5, Opus 5.5, Fable 5.1 (CLI backend)
• Open-weight models: Goedel-Prover-V2-32B (formal stages, pass@256) + Gemma 4 26B-A4B (prose stages) via vLLM backend
• Two backends: CLI and vLLM, with the Kimina Lean server

Empirical Validation / Results

Benchmark Functions

CYCLEUNCOVER: A Novel Problem

The agent designed a fundamentally different algorithm from evolutionary approaches:

1. Build a two-colouring of the cycle graph by walking along it
2. Sample uniformly random vertices until finding an uncoloured neighbour of current vertex $u$
3. Colour it oppositely to $u$ and make it the new current vertex
4. After $O(n)$ steps, query the optimum (all vertices of one colour)

The algorithm needs $O(n)$ queries per step in expectation (probability $\Omega(1/n)$ of finding the single uncoloured neighbour), giving total runtime $O(n^2)$. This contrasts with the classical result:

Theorem 5.1: The expected runtime of the (1+1) EA on CYCLEUNCOVER is $e^{\Omega(n)}$.

Submodular Minimisation Over Generations

The pipeline was looped for 5 generations on integer-valued submodular minimisation:

The final bound $O(n^{2+2c})$ matches the asymptotic complexity of the classical Fujishige-Wolfe algorithm.

Ablation Studies

• Zero-shot ablation: Without staging, the agent reproduced the seeded random search algorithm for CYCLEUNCOVER, or failed to produce a runtime bound (BANDWIDTHVC)
• Weaker models: Claude Sonnet passed Stages 0–10g but failed at the mass bound (Stage 10h); open-weight models stopped much earlier (Stages 3–9d) and generated 25–124M output tokens per run

Theoretical and Practical Implications

On the Role of Formal Verification

The paper demonstrates that machine-checked specifications in Lean can replace empirical evaluation in open-ended algorithm discovery. This is significant because:

1. It provides rigorous guarantees that empirical benchmarking cannot
2. It eliminates the risk of overfitting to benchmark functions
3. It enables verification of stochastic algorithms (not just deterministic ones)

On Algorithm Discovery

The pipeline discovered algorithms that differ qualitatively from standard evolutionary approaches:

• CYCLEUNCOVER: A learn-then-solve strategy exploiting graph structure
• VERTEXCOVER (flat fitness): An edge-probing strategy that "cheats" by exploiting the black-box model's free offline computation
• Submodular minimisation: Rediscovery of Lovász subgradient descent, a classical convex optimisation technique

Limitations and Caveats

• Runtime bounds are often not tight (e.g., $O(n^3)$ vs true $O(n\log n)$ for ONEMAX)
• The simplified drift theorem (Corollary 3.1) prevents multiplicative drift analysis
• Only frontier models completed the pipeline; open-weight models failed
• The black-box model does not charge for offline computation, enabling "cheating" strategies

Conclusion

The paper presents the first automated pipeline that designs efficient black-box optimisation algorithms with machine-checked runtime bounds in Lean. Key takeaways:

1. Staging is essential: Breaking the design-and-analysis task into stages with formal guards is crucial for success; zero-shot attempts fail
2. Formal verification works: Lean guards effectively filter out flawed designs and enable rigorous runtime guarantees
3. LLMs can do theoretical computer science: The agent discovered novel algorithms for new problems (CYCLEUNCOVER) and rediscovered classical results (Lovász subgradient descent)

Future directions identified by the authors:

• Richer drift theorems for tighter bounds
• More iterations of the design loop
• Extension to continuous search spaces
• More comprehensive experimental design with statistical analysis

The authors acknowledge limitations: only frontier models completed the pipeline, the simplified drift theorem leads to non-tight bounds, and the search space is restricted to bitstrings. Nevertheless, this work establishes that automated formal algorithm design is feasible, potentially transforming how optimisation algorithms are discovered and verified.