ThRaSH Seminar Autumn 2026

LLMs now prove hard theorems in Lean. In this talk, we ask whether they can also design evolutionary algorithms and prove their efficiency. We present two contributions.

First, we describe a Lean formalisation of runtime analysis of black-box optimisation algorithms. Built from measure-theoretic and martingale foundations, it includes additive and multiplicative drift theorems and general conditions for finite expected hitting times. As an application, we prove the asymptotically tight upper bound \((1+o(1))\;en\ln n\) on the expected runtime of the (1+1) EA on OneMax.

Second, building on this library, we present a staged agentic pipeline modelled on the research methodology of our field. Starting from random search, the agent proposes algorithms, with Lean guards checking admissibility conditions. It then defines a potential function and proves drift bounds that guarantee a runtime improvement. All definitions and theorems are machine-checked, and at no point are algorithms compared empirically.

Across eight problem classes, 12 of 15 runs with frontier models complete the pipeline with a machine-checked runtime bound. On CycleUncover, a new problem on which the (1+1) EA needs \(e^{\Omega(n)}\) expected runtime, the agent designs an \(O(n^2)\) algorithm that first learns the hidden structure. On well-covered vertex cover, given an anonymised fitness definition, it designs an \(O(n^4)\) EA with regime-switching mutation rates. For integer-valued submodular minimisation, it moves beyond evolutionary algorithms and rediscovers subgradient descent on the Lovász extension. Without the staging, the agent copies random search or leaves proofs incomplete. Experiments with open-weight models were unsuccessful.

To the best of our knowledge, this is the first Lean formalisation of runtime analysis of black-box optimisation algorithms, and the first automated pipeline that designs efficient black-box optimisation algorithms with machine-checked runtime bounds.

We seek to understand the optimization behavior for Vertex Coloring in two ways: By analyzing what types of local optima are present and by finding run time bounds. For a variety of graph classes each, we determine whether the induced landscapes are unimodal, plateau-unimodal (all optima are just one plateau), equimodal (all local optima are global) or truly multimodal. We do this for two different neighborhood operators, one based on making only a single change and one also allowing swaps (interchanging two parts of the solution). Further, we show that even on unimodal instances, the run time is still exponential on two simple graph classes. We introduce an improved fitness function that produces a more favourable landscape and therefore allows for a polynomial run time.

Abstract (TBA)

Multi-objective evolutionary algorithms (MOEAs) are popular tools for multi-objective optimization (MOO), and have been successfully applied to many real-world MOO problems. However, the theoretical study has lagged behind their practical success and remains largely confined to synthetic pseudo-Boolean functions. To close this gap, this paper–drawing inspiration from a class of popular continuous problems with real-world relevance– introduces a multi-objective benchmark defined on an integer space, featuring an analyzable landscape and the presence of local optima. We conduct a running time analysis on the proposed benchmark and derive several theoretical results. Specifically, we prove that a widely-studied MOEA, GSEMO, using unit-step mutation can be trapped in local optimal regions and fail to identify the Pareto front. Fortunately, we find that this difficulty can be overcome either by incorporating an ageing mechanism or using heavy-tailed mutations that allow multivalued changes along each dimension of an individual. In addition, we demonstrate the extendability of the proposed benchmark to more complex landscapes with numerous local optima, resembling well-established problems in the field (e.g., those from the ZDT and DTLZ suites). We hope this work is a step forward for the theoretical study of MOEAs on problems that are closely related to those commonly investigated in empirical research.

Abstract (TBA)

Abstract (TBA)

Genetic Programming (GP) is a search paradigm inspired from natural evolution for the automated discovery of expressions, functions, and computer programs. Cartesian GP (CGP) is a flavor of GP that uses a graph-based model to encode candidate programs, as contrasted to the conventional Tree-based GP (TGP). Since its inception two decades ago, CGP has predominantly been analyzed empirically, thus little is known regarding its theoretical performance guarantees.

This work analyzes CGP for the MAX problem, which has been only rigorously studied for TGP with a proven expected runtime superlinear in the optimal program length \(n\). We prove that the expected time for the (\(1\)+\(1\)) CGP employing common mutation operators to evolve an equivalent optimal of the same output is polylogarithmic in \(n\), specifically at most \(O(\log^9{n})\). This is remarkable, as it shows an exponential speedup by switching to CGP. Our results shed light on the benefit and the compactness of the graph-based representation for programs, and on how CGP can navigate its search and fitness spaces efficiently. This is a first proven performance guarantee for CGP on an established benchmark problem. Experiments complement our theoretical findings.

Abstract (TBA)

Abstract (TBA)