PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Per Kristian Lehre

arXiv:2610.35595v2cs.AIcs.NE

TL;DR

LLM-driven heuristic design is largely empirical, while automated theorem proving generally addresses supplied statements, leaving limited evidence that AI can both design algorithms and prove their efficiency. This paper uses a staged pipeline that combines algorithm proposals with Lean-checked drift analysis. Across eight problem classes, frontier-model runs produced machine-checked expected-runtime bounds, including an O(n^2) CYCLEUNCOVER algorithm where the classical (1+1) EA needs e^Omega(n).

  • Problem

    LLM heuristic-design approaches evaluate candidates empirically without guarantees, while theorem provers prove given statements; evidence that AI can design algorithms and guarantee their efficiency is limited.

    Source: §1 · p. 2

  • Method

    A staged pipeline has an agent propose black-box optimisation algorithms and potentials, while Lean guards and drift proofs formalise designs and certify runtime bounds.

    Source: §1 · p. 2, §4.1 · p. 7, §4.2 · p. 8

  • Results

    Across 8 problem classes, 12 of 15 frontier-model runs completed; the agent found O(n^2) on CYCLEUNCOVER versus e^Omega(n) for the (1+1) EA and matched O(n^2) on LEADINGONES.

    Source: §6 · p. 14

  • Takeaways & Limitations

    The study demonstrates automated black-box algorithm design with machine-checked expected-runtime bounds, without empirical evaluation or comparison of algorithms.

    Source: §1 · p. 2

    Only frontier models completed the pipeline; the search space is restricted to bitstrings, and the simplified drift theorem makes precise variable-drift analyses difficult.

    Source: §6 · p. 14

Abstract

from arXiv · show

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 classical runtime $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.

1 INTRODUCTION

LLM-guided heuristic design is largely empirical, while theorem provers generally prove supplied statements; whether AI can design algorithms and formally guarantee their performance remains open. This paper combines algorithm proposals with Lean-checked analysis in a staged pipeline, demonstrating runtime bounds on several problems.

1 INTRODUCTION

  • Theoretical algorithm design requires both a finite procedure and a proof of correctness and resource guarantees, with design and analysis informing one another.The paper contrasts this with LLM heuristic-design approaches that evaluate candidates empirically but provide no correctness or performance guarantees.Source: §1 · pp. 1–2
  • The pipeline combines LLM proposals with Lean formalisation and proof guards, using drift analysis to derive runtime bounds for black-box optimisation algorithms.It is seeded with a problem card and an algorithm with a stated runtime bound, and uses uniform random search with expected runtime O(2^n) in the reported experiments.Source: §1 · p. 2
  • On CYCLEUNCOVER, the pipeline produced a polynomial-runtime algorithm while the classical (1+1) EA has exponential runtime; without staging, ablations failed to construct efficient algorithms.The work reports no empirical algorithm comparisons; Table 1 places it at the intersection of LLM-proposed designs, LLM-produced analyses, and machine-checked expected-runtime properties.Source: §1 · p. 2, Table 1 · p. 3

2 RELATED WORK

Related work spans formal analysis of human-designed algorithms, theorem proving for supplied statements, and LLM-driven algorithm discovery evaluated empirically. This paper combines automated design and analysis with machine-checked runtime guarantees.

2 RELATED WORK

  • Formalisation efforts machine-check analyses of existing, human-designed algorithms, while their proofs remain human-designed.Examples include Lean, Coq, and Isabelle/HOL work on optimisation, probabilistic programs, and machine learning.Source: §2 · p. 3
  • LLM-assisted theorem proving produces proofs for given theorems or specifications, whereas LLM-based algorithm search proposes variants and evaluates them on benchmarks without machine-checked guarantees.The passage names AlphaEvolve, ShinkaEvolve, LLaMEA, and EoH among empirical algorithm-search systems.Source: §2 · pp. 3–4
  • Other adjacent work certifies optimisation-problem reformulations or synthesises software with proofs of specification compliance, rather than automating this paper’s algorithm-design-and-runtime-analysis task.The passage discusses FLARE and automated software verification and vericoding.Source: §2 · p. 4

3 RUNTIME ANALYSIS OF BLACK-BOX OPTIMISATION ALGORITHMS

The paper models black-box optimisation as an algorithm interacting with a fitness oracle, with runtime measured by the number of queries until an optimum is queried. It uses drift analysis to translate potential changes and their probabilities into expected-runtime bounds.

3.1 BLACK-BOX OPTIMISATION ALGORITHMS

  • A black-box algorithm queries an oracle for fitness values and updates its state using the query history; its runtime is the number of queries until an optimal point is first queried.The framework’s tuple specifies the state space, initialisation, query, and state-transition functions, and the algorithm is defined independently of the objective function.Source: §3.1 · pp. 4–5

3.2 DRIFT ANALYSIS

  • Drift analysis tracks a potential function of the algorithm’s state; expected potential decrease can yield a bound on the time to reach zero.The pipeline simplifies the drift theorem by bounding probabilities of improving and worsening steps, bounding the potential in [0, 1], and requiring a positive probability of jumping to the target; together the conditions yield E[TA] ≤ 4/(εp).Source: §3.2 · p. 5, Figure 1 · p. 6

4 THE STAGED PIPELINE

The pipeline breaks algorithm design and runtime analysis into informal proposals and Lean-checked formal stages. Formal guards filter candidate algorithms and potentials before drift certificates yield a runtime bound.

4 THE STAGED PIPELINE

  • The staged pipeline breaks the difficult task of jointly designing an algorithm and analysing its runtime into informal design proposals, formalisation, potential design, and drift analysis.Candidate designs are filtered through formal proof obligations intended to reject flawed designs.Source: §4 · p. 6

4.1 ALGORITHM DESIGN (STAGES 0–8)

  • Stages 0–8 formalise algorithm proposals and apply guards for measurability, reachability of search points, use of randomness, non-random-search behaviour, adaptiveness, and non-injective queries.The completeness guard supports proving eventual querying of an optimum and finite expected hitting time; the other guards filter specified degenerate or restricted designs.Source: §4.1 · pp. 6–7

4.2 POTENTIAL FUNCTION (STAGES 9A–9F)

  • Stages 9a–9f select and formalise a potential that is bounded in [0, 1], zero exactly at optimal-query states, and takes an intermediate value.The intermediate-value guard excludes the seeded two-valued potential, which the paper says is insufficient to capture gradual progress of an efficient algorithm.Source: §4.2 · pp. 7–8

4.3 DRIFT CERTIFICATES AND RUNTIME BOUND (STAGES 10A–10J)

  • Stages 10a–10j prove drift and jump-probability conditions, then apply the resulting certificates to obtain E[TA] ≤ 4/(εp).Positive drift, bounds on worsening steps, and a lower bound on direct jumps to the target are among the required conditions.Source: §4.3 · p. 8

5 RESULTS

The pipeline produced machine-checked runtime bounds across benchmark, graph, and submodular problems, including polynomial-time CYCLEUNCOVER search where the classical (1+1) EA has exponential expected runtime. Results also expose limits: some bounds are weaker than known runtimes, and zero-shot runs sometimes fail to establish a runtime guarantee.

5 RESULTS

  • Incomplete frontier-model runs stopped at drift stages, most often at the Stage 10h mass bound; drift and runtime stages took about half the completed runs’ wall-clock time.Open-weight runs on ONEMAX also failed to complete the pipeline; they stopped earlier and generated about two orders of magnitude more output tokens than frontier-model runs.Source: §5 · p. 8, §5.5 · pp. 13–14

5.1 THEORETICAL BENCHMARK FUNCTIONS

  • 4e(n + 1)(n + 2) = O(n^2) on LEADINGONES followed a supplied inequality that enabled a sharper drift bound.An earlier analysis of the same fitness-adaptive mutation approach gave O(n^3).Source: §5.1 · p. 10
  • O(n^(k+1)) on JUMPk was machine-checked after adding an inequality, but remained a factor n weaker than the algorithm’s O(n^k) runtime.The initial bound was O(n^(k+2)).Source: §5.1 · p. 10

5.2 CYCLEUNCOVER

  • O(n^2) expected runtime on CYCLEUNCOVER contrasts with e^Ω(n) for the classical (1+1) EA.The algorithm builds a two-colouring by fitness queries, then selects one colour class as an optimum.Source: §5.2 · pp. 10–11

5.3 VERTEXCOVER

  • O(n^4) runtime was obtained on WELLCOVEREDVC with regime-changing asymmetric mutation rates, including from an anonymised problem card.The anonymised-card run used mutation-rate asymmetry of Θ(n); the run with full structural information used a factor of two.Source: §5.3 · p. 12
  • O(kn) queries on BANDWIDTHVC came from probing only vertex pairs within distance k + 1, then computing the optimum offline.For general VERTEXCOVER, the analogous probing strategy gave O(n^3); the offline computation is not bounded.Source: §5.3 · p. 12

5.4 SUB-MODULAR MINIMISATION

  • O(n^2B^2) runtime for submodular minimisation matches the asymptotic runtime of the Fujishige-Wolfe algorithm.The third generation achieved this bound; later generations brought constant-factor improvements to about 8.13 · B^2(n + 1)^2.Source: §5.4 · p. 13

5.5 ABLATION EXPERIMENTS

  • The zero-shot CYCLEUNCOVER run copied random search, while the BANDWIDTHVC run constructed a (1+1) EA but did not prove a runtime bound.The CYCLEUNCOVER run used a tail-sum argument; the BANDWIDTHVC attempt tried a fitness-level argument.Source: §5.5 · p. 13

6 CONCLUSION

Across 8 problem classes, 12 of 15 frontier-model runs completed the staged pipeline with machine-checked expected-runtime bounds. The results include polynomial-time CYCLEUNCOVER, while the authors note scope and drift-analysis limitations.

6 CONCLUSION

  • 12 of 15 runs across 8 problem classes completed the pipeline; nine produced polynomial bounds with explicit computation between queries.Of the other three, two learn a VERTEXCOVER instance with polynomially many queries and solve it offline, while one improves on random search only by a constant factor.Source: §6 · p. 14
  • O(n^2) on CYCLEUNCOVER improves on the (1+1) EA's e^Ω(n) runtime; the pipeline also matched O(n^2) on LEADINGONES.For integer-valued submodular minimisation, the agent rediscovered projected subgradient descent on the Lovász extension and improved its bound to O(n^(2+2c)) over five generations.Source: §6 · p. 14
  • Only frontier models completed the pipeline, and the search space is restricted to bitstrings.The high run cost also prevented a more complete experimental design with statistical analysis.Source: §6 · p. 14
  • With standard potential functions, the simplified drift theorem made more precise variable-drift analyses difficult, leading to non-tight runtime bounds such as O(n3) on ONEMAX for (1+1) EA variants.Source: §6 · p. 14

AI USE STATEMENT

The paper reports extensive LLM use in generating algorithms, potentials, drift certificates, and Lean proofs, with every proof checked by Lean. Its formal pipeline distinguishes stages that introduce definitions from stages that prove properties of earlier definitions.

AI USE STATEMENT

  • All reported algorithms, potentials, drift certificates, and Lean proofs were generated by the named models, and every proof was checked by Lean.LLMs also helped derive the Lean library's combinatorial drift results, translate definitions into pseudocode, and polish the writing; the author takes responsibility for the paper.Source: AI USE STATEMENT · p. 15

A FORMAL STATEMENT OF THE PIPELINE STAGES

  • Table 3 states the pipeline stages formally; [F*] stages introduce Lean definitions, while [F-] stages prove properties of earlier definitions.Declarations produced in either formal stage are checked by Lean and carried forward.Source: A FORMAL STATEMENT OF THE PIPELINE… · p. 19, Table 3 · p. 19
  • Stage 9f packages the potential Φ and the Stage 9b–9e witnesses into a single potential record.Source: A FORMAL STATEMENT OF THE PIPELINE… · p. 20
  • Drift design fixes closed forms for ε, p, and pjump and defines four draw sets; later stages check positivity and a speed-up certificate against the previous algorithm-potential pair.The formal conditions also constrain drift-set properties and probability mass, with a jump-mass bound applying at every state to support hitting-time integrability.Source: A FORMAL STATEMENT OF THE PIPELINE… · p. 20

B PROOFS OF THE DRIFT CONDITION

The appendix states the additive drift theorem used for runtime bounds and says the Lean formalization follows its presented proof almost exactly. It also describes the pipeline's retry controls and the information supplied to the agent at each stage.

B PROOFS OF THE DRIFT CONDITION

  • Under its stated drift and integrability assumptions, the additive drift theorem bounds E[Ta | G0] by Z0/ε.The Lean formalization developed for the staged pipeline follows almost exactly the proof presented in the appendix.Source: B PROOFS OF THE DRIFT CONDITION · p. 20

C IMPLEMENTATION AND PROMPT

  • Each stage uses a Luby-sequence attempt allowance; failures trigger backtracking, while the pipeline restarts after its run budget or 100 consecutive attempts without progress.The first failure at an exhausted stage backtracks one stage, with subsequent failures backtracking farther; the stated parameters apply to all Table 2 runs.Source: C IMPLEMENTATION AND PROMPT · p. 21
  • Both CLI and vLLM backends use the same stages, Lean statements, and checks, while differing in how they serve model responses.The CLI backend is used with Claude models; the vLLM backend serves open-weight models and samples multiple candidates per attempt.Source: C IMPLEMENTATION AND PROMPT · p. 21
  • Stage prompts combine accepted declarations, a shared framework and Lean API, a problem-specific card, and a proof cookbook.After a failed attempt, the agent receives the failing declaration, Lean error, previous attempts, and facts verified in earlier stages.Source: C IMPLEMENTATION AND PROMPT · p. 21

D THEORETICAL BENCHMARK FUNCTIONS

The benchmark functions cover counting ones, leading ones, and a deceptive gap near the optimum. Their instance classes hide the optimum, and the JUMPk analysis must hold uniformly for an unknown gap width.

D THEORETICAL BENCHMARK FUNCTIONS

  • ONEMAX counts ones, LEADINGONES counts ones before the first zero, and JUMPk behaves like ONEMAX except for a width-k gap below the optimum.Source: D THEORETICAL BENCHMARK FUNCTIONS · p. 22
  • For the (1+1) EA with mutation rate 1/n, expected optimisation times are Θ(n log n) on ONEMAX, Θ(n^2) on LEADINGONES, and Θ(n^k) on JUMPk for constant k ≥ 2.Source: D THEORETICAL BENCHMARK FUNCTIONS · p. 22
  • Each instance class hides its optimum, and every JUMPk proof must be uniform in the unknown constant gap width k ≥ 2.Each instance has the unique optimum complement of z; algorithms treating all bits alike have the same expected time on every class instance as on the underlying function.Source: D THEORETICAL BENCHMARK FUNCTIONS · p. 22

E CYCLEUNCOVER: DEFINITION AND RUNTIME OF THE (1+1) EA

The section analyzes the classical (1+1) EA on CYCLEUNCOVER and establishes an exponential expected-runtime lower bound. It also gives runtime-analysis conventions and definitions for the staged algorithms and problem classes.

E CYCLEUNCOVER: DEFINITION AND RUNTIME OF THE (1+1) EA

  • The (1+1) EA uses uniform random initialization, bitwise mutation, and elitist selection that accepts offspring with fitness at least that of the parent.The mutation probability is p; the analysis considers an initial search point with many 1-bits and both endpoints of the first edge set to 1.Source: E CYCLEUNCOVER: DEFINITION AND RUNTIME… · p. 22
  • The (1+1) EA has expected runtime e^Ω(n) on CYCLEUNCOVER.The proof conditions on a starting event of probability at least 1/5 and bounds failure probabilities over two phases.Source: E CYCLEUNCOVER: DEFINITION AND RUNTIME… · pp. 22–23

F ALGORITHMS, POTENTIALS AND RUNTIME BOUNDS OF ALL RUNS

  • The staged-run runtime theorem bounds expected runtime by 4/(ε1p1) for n ≥ 3, with drift ε1 and Good-set mass p1 supplied for each run.Here, “machine-checked” means the Lean file compiles with no sorry.Source: F ALGORITHMS, POTENTIALS AND RUNTIME… · p. 23
  • The problem cards specify ONEMAX, LEADINGONES, JUMPk, integer-valued SUBMODULARMIN, and CYCLEUNCOVER, including hidden-instance or class parameters.For SUBMODULARMIN, the function range is {0, 1, . . . , B}, with B = n^c and opaque c ≥ 1; CYCLEUNCOVER uses h = ⌊n/2⌋ and optimum value 3h.Source: F ALGORITHMS, POTENTIALS AND RUNTIME… · pp. 23–24
  • The bandwidth vertex-cover cards assume every edge uv satisfies |u − v| ≤ k; well-covered cards further restrict graphs so all minimal covers are minimum.The wcvc card is an anonymised copy with names and derived facts removed.Source: F ALGORITHMS, POTENTIALS AND RUNTIME… · p. 24

F.1 ONEMAX, OPEN-WEIGHT MODELS (STAGED; INCOMPLETE)

The open-weight ONEMAX runs did not complete, while the staged pipeline produced machine-checked runtime bounds for several other problem settings. The section reports the runs’ proof bottlenecks and the algorithms and bounds obtained for ONEMAX, LEADINGONES, JUMPk, and CYCLEUNCOVER.

F.1 ONEMAX, OPEN-WEIGHT MODELS (STAGED; INCOMPLETE)

  • Across 14 runs using the three most recent pipeline versions (September 2026), no run completed: ten got stuck at Stage 4 (NotRandomSearch), three at Stage 1c or 2, and one reached Stage 9d (PotentialFineGrained).Each ended after 21–46 hours of wall-clock time.Source: §F.1 · p. 24
  • All Stage 4 proof samples failed for the reported PBIL-like designs, while the uniform-random-search run later failed Stage 9d despite a true statement.The latter run passed Stage 9c three times; its Stage 4 pass used an unreachable witness, which a later pipeline version requires to be reachable.Source: §F.1 · pp. 24–25

F.2 ONEMAX, CLAUDE OPUS 5 (STAGED; COMPLETE)

  • The staged ONEMAX hill-climber has expected runtime O(n^3).Its mutation rate is 1/(n + 1).Source: §F.2 · p. 25

F.3 LEADINGONES, CLAUDE OPUS 5.5 (STAGED; COMPLETE)

  • The LEADINGONES algorithm has expected runtime O(n^3), using a mutation rate read from the learned fitness.The version with the supplied e−1 lemma uses the same algorithm and potential as the preceding version.Source: §F.3 · p. 25, §F.4 · p. 26

F.4 LEADINGONES WITH THE e−1 LEMMA, CLAUDE OPUS 5.5 (STAGED; COMPLETE)

  • With the e−1 lemma, the LEADINGONES version keeps the same algorithm and potential as the preceding version.The supplied passages do not give a separate runtime bound for this version.Source: §F.4 · p. 26

F.5 JUMPk, CLAUDE OPUS 5.5 (STAGED; COMPLETE)

  • The JUMPk hill-climber has expected runtime O(n^(k+2)).The bound is given as 4(n + k + 1)(n + 1)^(k+1).Source: §F.5 · p. 26

F.6 JUMPk WITH THE e−1 LEMMA, CLAUDE OPUS 5.5 (STAGED, 3 GENERATIONS; COMPLETE)

  • With the e−1 lemma, all three JUMPk generations have runtime O(n^(k+1) and share a potential, differing only in mask rate.The generations retain a strictly elitist search point; the stated bound is 4e^2(n + k + 1)(n + 2)^k.Source: §F.6 · p. 26

F.7 CYCLEUNCOVER, CLAUDE FABLE 5.1 (STAGED; COMPLETE)

  • The CYCLEUNCOVER cycle-walk algorithm has expected runtime O(n^2).Its stated bound is 12(n + 1)(2⌊n/2⌋ + 2).Source: §F.7 · p. 28

F.8 CYCLEUNCOVER, CLAUDE FABLE 5.1 (ZERO-SHOT ABLATION; COMPLETE)

The CYCLEUNCOVER zero-shot ablation reproduces random search, while staged runs produce both completed and incomplete designs across CYCLEUNCOVER, VERTEXCOVER, and BANDWIDTHVC. The completed VERTEXCOVER and flat-fitness BANDWIDTHVC analyses bound fitness evaluations, but leave offline computation unbounded.

F.8 CYCLEUNCOVER, CLAUDE FABLE 5.1 (ZERO-SHOT ABLATION; COMPLETE)

  • The CYCLEUNCOVER zero-shot run samples uniformly at random each iteration, making it essentially identical to the provided baseline.No potential is constructed because this run omits the staged pipeline.Source: §F.8 · p. 28

F.9 CYCLEUNCOVER, CLAUDE SONNET (STAGED; INCOMPLETE)

  • The staged CYCLEUNCOVER design accepts only strictly better mutants, but its runtime bound was not proved before the run stopped at Stage 10h.The design uses a potential based essentially on normalised Hamming distance to the optimum.Source: §F.9 · pp. 28–29

F.10 VERTEXCOVER, CLAUDE FABLE 5.1 (STAGED; COMPLETE)

  • O(n^3) fitness evaluations are bounded for VERTEXCOVER, but the non-constructive offline optimum computation between queries is not bounded.The algorithm probes Θ(n^2) potential edges, then computes an optimum for the learned graph and queries it.Source: §F.10 · p. 29

F.11 BANDWIDTHVC, CLAUDE FABLE 5.1 (STAGED, FLAT FITNESS; COMPLETE)

  • O(kn) fitness evaluations are bounded for flat-fitness BANDWIDTHVC, but computation between queries is not bounded.The algorithm interleaves window probing with solving the graph learned from those probes.Source: §F.11 · pp. 29–30

F.12 BANDWIDTHVC, CLAUDE FABLE 5.1 (STAGED, GRADED FITNESS; INCOMPLETE)

  • The graded-fitness BANDWIDTHVC asymmetric-mutation design has no proved runtime bound because the run stopped at Stage 10h.The reported mass bound at that stage is false for this design.Source: §F.12 · p. 30

F.13 BANDWIDTHVC, CLAUDE FABLE 5.1 (ZERO-SHOT ABLATION; INCOMPLETE)

The BANDWIDTHVC zero-shot attempt and several staged designs do not yield proved runtime bounds, while other staged runs complete analyses for BANDWIDTHVC, SUBMODULARMIN, and WELLCOVEREDVC. The completed results include a submodular-minimisation bound and a WELLCOVEREDVC bound of O(n^4).

F.13 BANDWIDTHVC, CLAUDE FABLE 5.1 (ZERO-SHOT ABLATION; INCOMPLETE)

  • The zero-shot BANDWIDTHVC run uses a (1+1) EA with mutation rate 1/n, but its runtime bound was left as sorry.No potential was supplied for this attempt.Source: §F.13 · p. 31

F.14 BANDWIDTHVC, CLAUDE FABLE 5.1, SECOND SESSION (STAGED; INCOMPLETE)

  • The staged fill-then-prune BANDWIDTHVC design has no proved runtime bound; the run stopped at Stage 10c.It fills when the incumbent is not a cover and prunes once it is a cover.Source: §F.14 · p. 31

F.15 BANDWIDTHVC, CLAUDE OPUS 5.5 (STAGED; COMPLETE)

  • The completed BANDWIDTHVC window-repair design stays close to random search, redrawing the first ℓ bits near the incumbent under a stated condition.When all first ℓ sampled bits are 1, it copies those bits from the incumbent and mutates them with probability 1/3.Source: §F.15 · p. 32

F.16 SUBMODULARMIN, INTEGER-VALUED, CLAUDE OPUS 5.5 (STAGED; COMPLETE)

  • Generations 2–5 of SUBMODULARMIN yield the stated expected-runtime bound O(n^(2+2c)) for integer-valued submodular minimisation.The algorithm is projected subgradient descent on the Lovász extension, using a subgradient update after a chain of queries.Source: §F.16 · p. 33

F.17 WELLCOVEREDVC, ANONYMISED CARD, CLAUDE FABLE 5.1 (STAGED; INCOMPLETE)

  • The anonymised-card WELLCOVEREDVC design has no proved runtime bound because the run stopped at Stage 10h.The proposed mutation adapts its direction to whether the incumbent is a cover.Source: §F.17 · pp. 33–34

F.18 WELLCOVEREDVC, ANONYMISED CARD, CLAUDE OPUS 5.5 (STAGED; COMPLETE)

  • The completed anonymised-card WELLCOVEREDVC design switches between shrinking and growing mutation according to whether the incumbent is a cover.The runtime passage gives a bound, though its numeric expression is not legible in the supplied text.Source: §F.18 · p. 34

F.19 WELLCOVEREDVC, NAMED CARD, CLAUDE FABLE 5.1 (STAGED; COMPLETE)

  • The named-card WELLCOVEREDVC design proves an expected runtime bound of O(n^4).Its mutation direction changes according to whether the incumbent is a cover.Source: §F.19 · p. 34

G PIPELINE PROGRESS AND PER-STAGE STATISTICS

The pipeline statistics show that drift and runtime analysis take the largest share of wall-clock time across completed frontier-model runs. They also locate common technical failures and the stages where incomplete runs stop.

G PIPELINE PROGRESS AND PER-STAGE STATISTICS

  • Figure 4 plots stages passed by round for completed runs, including backtracking, and highest stage reached on a logarithmic round axis for incomplete runs.Zero-shot runs are omitted; the figure caption notes that rows 12 and 17 continue for thousands of rounds after reaching their best level.Source: Figure 4 · p. 35
  • 53% of wall-clock time goes to drift and runtime stages, compared with 34% for algorithm construction and 13% for potential construction.Pointwise drift and mass proofs are among the most expensive stages.Source: Figure 5 · p. 35, G PIPELINE PROGRESS AND PER-STAGE… · p. 36
  • DriftConstantProperties failed on the first attempt in all 12 completed runs, mostly over baseline-constant normal forms; StepMeasurability did so in 11.Incomplete frontier-model runs stopped at drift stages, while the open-weight runs stopped at earlier stages.Source: G PIPELINE PROGRESS AND PER-STAGE… · p. 36

Related papers

Loading 2610.35595v2…