Automated Design and Analysis of Black-Box Optimisation Algorithms with LLMs Event

Event details

The mathematical capabilities of LLMs have improved dramatically. Several long-standing open problems have recently been resolved, and a solution to the Navier-Stokes problem has been claimed. However, these results mostly concern existing mathematical concepts, whereas human mathematicians also invent new concepts and prove statements about them. It is unclear whether LLMs can do the same. Designing an optimisation algorithm and the potential function used to analyse it is exactly this kind of concept invention. Here, we study whether LLMs can simultaneously invent an optimisation algorithm and prove performance guarantees about it. We present a staged agentic pipeline modelled on the research methodology of design and analysis of evolutionary algorithms. The agent proposes black-box optimisation algorithms, and the proof assistant Lean filters out flawed designs. The agent then defines a potential function and proves drift bounds that yield bounds on the expected runtime of the algorithm. All the definitions and theorems constructed by the agent are machine-checked in Lean. At no point in the pipeline are the algorithms compared empirically. On a well-studied problem from the literature (LeadingOnes), the agent rediscovers a known algorithm with expected runtime O(n^2). On a new problem, constructed so that it cannot appear in the LLM’s training data, the agent designs a new algorithm with expected runtime O(n^4), where standard evolutionary algorithms such as the (μ+λ) EA have expected runtime e^Ω(n). For minimisation of integer[1]valued submodular functions upper bounded by M=n^c, the agent moves beyond evolutionary algorithms and designs a randomised subgradient method on the Lovasz extension and proves an expected runtime of O(n^(2+2c)), which is within a factor n of the best known black-box bounds. 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.