Proof-Carrying Evolution: Black-Box Search, White-Box Flight

Amit Jain; Sergio Sanchez-Hurtado; Victor Rodriguez-Fernandez; Richard Linares

cs.ROOct 30, 2026

Proof-Carrying Evolution: Black-Box Search, White-Box Flight

Authors: Amit Jain, Sergio Sanchez-Hurtado, Victor Rodriguez-Fernandez, Richard Linares

Organizations: Massachusetts Institute of Technology. · Universidad Politécnica de Madrid.

Abstract

We study whether a language model can help design controllers whose behavior can be formally checked. In proof-carrying evolution (PCE), a search proposes controllers together with their certificates. Their mathematical forms are fixed; a proposer chooses their numerical parameters together. Certificate checks guide selection, and only a certified candidate can be returned. The deployed artifact is a control law and its certificate; the language model is used only during design. We compare four language models with classical search and synthesis on docking under a speed limit, pursuit of a maneuvering target, and attitude control on SO(3), using paired runs and shared proposal allowances. Certificates are checked in exact rational arithmetic during search on the linear problems. On SO(3), the search uses floating-point checks, followed by exact re-verification of every reported champion. The best run of each method also receives Lean 4 proofs of its stated control properties. On the linear problems, the strongest models beat the standard classical baselines on every run, but a classical optimizer that chooses certificates for the same objective closes most of that lead. Among the cited pursuit champions, the ranking does not survive a change from Euler to zero-order-hold dynamics. On SO(3), no model detectably outperforms CMA-ES when mixed with classical mutation. When models write every proposal, one tested model improves on CMA-ES and the other performs worse than its mixed variant. All search medians remain below the hand-tuned law. In a docking control with the objective and mutation operator held fixed, retaining certified candidates yields new certified designs in every run; removing this rule yields none.

Figures & tables

Figure 1: Proof-carrying evolution. A proposer chooses the parameters of a controller and its certificate, selection favors candidates whose certificate passes the check, and each run’s best certified design has an exact check; the best run of every arm also receives a Lean proof (Table gives the checks on each problem).

Problem	Parameters searched	Check during the search	Check afterwards
Docking	gain $K$ and certificate factor $L$	exact: stability, the speed-limit envelope and the docking bound $N$	Lean proof for the best run of each arm
Pursuit	gain $K$ and certificate factor $L$	exact: robust decrease and the capture radius	exact re-certification of each champion; Lean proof for the best run of each arm
SO(3)	fifteen diagonal gains of the controller and the certificate	floating point: regional decrease, by a linear program	exact re-check of each champion and of the positivity of $V$ ; Lean proof for the best run of each arm and for the hand-tuned law

Table 1: What is searched and checked on each problem.

Figure 2: The hand-tuned SO(3) law’s regional certificate: (a) the certified contraction against the size of the region, (b) the closed loop from the edge of the region under the certified envelope, and (c) the commanded torque against its certified bound.

	Docking	Pursuit	SO(3) attitude
Objective	bound $N$ (min.)	radius $r_{\mathrm{cap}}$ (min.)	angle $\theta_{\max}$ (max.)
Paired seeds	20	20	20
Population $\times$ generations	$28\times 24$	$28\times 24$	$12\times 10$
Proposal allowance per run	534	534	120
Model proposals	a batch of eight every third generation
Share written by the model	about 1 in 8	about 1 in 8	about 1 in 5

Table 2: Campaign settings for the three problems.

Figure 3: Design of the optimizer studies: optimizers by models, with models in release order. We ran the framed cells using two seeds, with a cost run and a bound run per seed. The optimizer axis (a column) and the model axis (a row) meet at the Sol baseline; the references use no model.

Figure 4: The docking campaign, with BIPOP and the certificate optimizer at the right: (a) the certified bound per seed and arm, (b) the same bounds against the proposals each run spent, and (c) the paired difference from synthesis at the full allowance, with the median and its bootstrap 95% CI.

Figure 5: Best certified docking bound so far against generation: median and interquartile range over the twenty seeds, with the classical baselines’ final medians as horizontal lines.

Panel of Figure 6 — Figure 6: The certificate of a typical Astra run ( $N=38$ steps, $\rho=0.7720$ ): (a) the theorem’s envelope bounding the simulated state norm from the three mission starts, and (b) the certified set, projected onto position and speed, inside the safe set.

Control	A	B	$n$	A	B	A / B / T	$p$ (Holm $p$ )
				median
interface	Astra (coding agent)	Astra	20	38	38.5	11 / 6 / 3	$0.18$
interface	Astra (text-only)	Astra	20	38.5	38.5	6 / 5 / 9	$0.72$
interface	Opus (CLI)	Opus	20	66.5	68.5	11 / 8 / 1	$0.31$ ( $0.94$ )
reasoning effort	Fable (effort low)	Fable (effort high)	20	49.5	39	2 / 17 / 1	$2.5\times 10^{-4}$
reasoning effort	gpt-oss	gpt-oss (effort high)	20	95	95.5	10 / 9 / 1	$0.70$

Table 5: Control experiments: each row compares two runs of one model that differ in one setting (in the first two reasoning-effort rows, also the output-token ceiling), paired by seed, on docking unless marked (A / B / T: seeds on which A is better, B is better, or they tie).

	unequal thrusters		tighter speed limit		wider initial set
Arm	cert.	median $N$	cert.	median $N$	cert.	median $N$
Gaussian mutation	10/10	370.5	8/10	430.0	10/10	454.0
CMA-ES	10/10	675.5	8/10	1005.5	10/10	610.0
alternating SDP synthesis (full allowance)	8/10 †	51.0	10/10	64.0	10/10	62.0
Astra	4/4	38.0	–	–	–	–
Fable (effort high)	8/8	38.0	–	–	–	–

Table 6: Docking on the three modified problems: runs that certified out of runs completed, and the median certified bound (“–”: no seed completed before the provider’s spending cap stopped the runs).

Figure 7: The pursuit task on one certified controller against an evader that thrusts on its bound and keeps turning: (a) the local orbital frame, (b) the target’s frame with the certified capture ball, and (c) the relative state norm under the theorem’s envelope.

		$r_{\mathrm{cap}}$			vs. PD grid
Arm	Cert.	Median	Best	First batch	med. $\Delta r$	W / L / T	Holm
Gaussian mutation	20/20	0.04140	0.03671	–	$+0.0075$	0 / 20 / 0	$4.0\times 10^{-5}$
CMA-ES	20/20	0.04446	0.03696	–	$+0.0106$	0 / 20 / 0	$4.0\times 10^{-5}$
PD grid search †	20/20	0.03388	0.03388	–	reference
Astra	20/20	0.02857	0.02857	0.02857	$-0.0053$	20 / 0 / 0	$9.3\times 10^{-5}$
Sol	20/20	0.02960	0.02857	0.04444	$-0.0043$	20 / 0 / 0	$9.0\times 10^{-4}$

Table 8: Pursuit: the certified capture radius (smaller is better) of each arm, paired within seed against the PD grid.

Figure 8: The pursuit campaign, with the certificate optimizer at the right: (a) the certified capture radius per seed and arm, and (b) each arm’s paired difference from the PD grid, with the median’s bootstrap 95% CI.

Arm	$\times 1$ (24 gen.)	$\times 2$ (48 gen.)	$\times 4$ (96 gen.)
Gaussian mutation	0.04039	0.03861	0.03850
CMA-ES	0.04577	0.03418	0.02943
PD grid search	0.03388	0.03879	0.03563
gpt-oss	0.03946	0.03739	0.03703

Table 9: The budget sweep: median certified capture radius on seeds 0–9 at one, two and four times the generations.

Figure 9: Median certified capture radius against proposals spent, seeds 0–9, at one, two and four times the generations; the grey labels give Gaussian mutation’s step size in its last generation.

Figure 10: The SO(3) campaign: (a) the certified angle per seed and arm, (b) each arm’s paired difference from CMA-ES, and (c) the median best angle so far against proposals spent.

Figure 11: Certified cost

J

(a) and bound

N

(b). Markers distinguish seeds, bars show geometric means, dotted lines the Sol baseline, and faded markers cross-objective scores; grey marks the time-limited Opus run.

Figure 12: Best certified cost

J

over evaluations for the optimizer (a) and model (b) axes; the dashed line marks 491 evaluations.

Figure 13: Cost (a) and bound (b) relative to the Sol baseline for each seed; leftward bars indicate better results.

Figure 14: Best certified cost

J

across four prime-agent runs with Opus; bands show final Opus and Astra costs.

Figure 15: Final cost-run designs against position gain

k_{p}=-(K_{11}+K_{22})/2

; dashed line shows the log-log fit.

Appendix figures & tables8 assets

Supplementary material from the paper’s appendix.

Appendix

Statement class	Checked by
Per-candidate control theorems: stability, safety envelope, safe_forever , docking within $N$ ; the strategy-quantified pursuit bound and trajectory-level capture; the nine-cell saturated decrease and its trajectory chain; the SO(3) step and regional decrease; template- or LLM-authored alike	Lean 4 kernel ; footprint by an independent Lean.collectAxioms driver, a subset of [propext, Classical.choice, Quot.sound]
In-loop admissibility on the linear problems; step counts $N$ ; certificate completions; the stage rescoring of Table ; the re-verification of every SO(3) champion and the positive definiteness of its $V$	Exact rational arithmetic (Python Fraction )
Campaign medians, paired differences, bootstrap intervals, Wilcoxon and Holm $p$	Float statistics , recomputed from the run summaries before every release
Fitness, the SO(3) in-loop scoring, trajectories, attack results, session-log audits	Float simulation and forensics (unverified)

Appendix

Table 11: Which part of the pipeline checks each kind of statement.

Figure 16: Padded proxy versus certified bound (a) and contraction factors (b) for optimizer-study designs.

Population or statistic	Value
Seeded population: cross-term ratio	2.5
Gaussian champions: cross-term ratio	2.9
Synthesis champions: cross-term ratio	4.5
gpt-oss champions: cross-term ratio	3.5
Opus champions: cross-term ratio	3.6
Astra champions: cross-term ratio	6.3

Appendix

Table 14: Ratio of the cross terms of

L

to its position weights.

optimizer	implementation	per model call	stops at
GOA GEPA	GEPA 0.1.4 (PyPI), gepa engine	one reflection: reads a candidate and its feedback, writes one revision	250 reflections or 560 evaluations
GOA Meta-Harness	GEPA GitHub commit 48f1f65d , meta_harness engine	one agent session: reads all earlier candidates, may run code, writes up to 10	60 sessions or 560 evaluations
GOA Omni	same commit, optimize_best_of then optimize_sequential	as the engine running (GEPA, Meta-Harness, AutoResearch)	$3\times 62$ , then $2\times 187$ evaluations; unused allowances are not passed on
prime-agent	prime-agent 0.9.7, autonomous mode	one agent turn in a persistent Python kernel, often submitting tens of genomes by script	560 evaluations, or a time or spending limit

Appendix

Table 17: Optimizer versions, model interactions and stopping limits; all use the same evaluator and 560-evaluation cap.

Figure 17: Optimizer runtime (a), model calls (b), designs per call (c) and estimated price (d), on logarithmic axes.

Figure 18: First failing checker stage for rejected designs, comparing the first 100 evaluations with the remainder.

		simulated peak			certified-set peak
Problem	Arm	median	max	$>u_{m}$	median	max	$>u_{m}$
docking	Gaussian mutation	0.021	0.028	0/20	0.030	0.040	0/20
docking	CMA-ES	0.014	0.023	0/20	0.025	0.035	0/20
docking	alternating SDP synthesis (full allowance)	0.137	0.158	0/20	0.213	0.219	20/20
docking	Astra	0.026	0.048	0/20	0.061	0.094	0/20
docking	Sol	0.027	0.170	0/20	0.063	0.223	2/20

Appendix

Table S3: Peak commanded acceleration per axis (m/s 2 ), in simulation and over the docking certified sets.

docking: Clohessy–Wiltshire, Euler step at $\Delta t=1$ s
Design	Exact check	Lean theorems	Trajectory	Model step	Noise, rounding	Thrust limit	Zero-order hold
Gaussian mutation	in loop	19	Lean	Lean	Lean	Lean	exact
CMA-ES	in loop	19	Lean	Lean	Lean	Lean	exact
alternating SDP synthesis	in loop	19	Lean	Lean	Lean	Lean	exact
Astra	in loop	19	Lean	Lean	Lean	Lean	exact
Sol	in loop	19	Lean	Lean	Lean	Lean	exact

Appendix

Table S4: Guarantees established for the cited designs, grouped by problem.

Formal Verification

Formal verification uses mathematical models and machine-checked proofs to establish whether software and systems satisfy precise specifications.

See all 354 papers

Feb 25, 2026

Code World Models for Parameter Control in Evolutionary Algorithms

Can an LLM learn how an optimizer behaves -- and use that knowledge to control it? We extend Code World Models (CWMs), LLM-synthesized Python programs that predict environment dynamics, from deterministic games to stochastic combinatorial optimization. Given suboptimal trajectories of

(1{+}1)

\text{RLS}_k

, the LLM synthesizes a simulator of the optimizer's dynamics; greedy planning over this simulator then selects the mutation strength

k

at each step. On \lo{} and \onemax{}, CWM-greedy performs within 6% of the theoretically optimal policy -- without ever seeing optimal-policy trajectories. On \jump{

_k

}, where a deceptive valley causes all adaptive baselines to fail (0% success rate), CWM-greedy achieves 100% success rate -- without any collection policy using oracle knowledge of the gap parameter. On the NK-Landscape, where no closed-form model exists, CWM-greedy outperforms all baselines across fifteen independently generated instances (

36.94

vs.\

36.32

;

p<0.001

) when the prompt includes empirical transition statistics. The CWM also outperforms DQN in sample efficiency (200 offline trajectories vs.\ 500 online episodes), success rate (100% vs.\ 58%), and generalization (

k{=}3

: 78% vs.\ 0%). Robustness experiments confirm stable synthesis across 5 independent runs.

Camilo Chacón Sartori, Guillem Rodríguez Corominas

ICN2 – Catalan Institute of Nanoscience and Nanotechnology, Barcelona, Spain · Artificial Intelligence Research Institute (IIIA-CSIC), Barcelona, Spain · Universitat Politècnica de Catalunya (UPC), Barcelona, Spain

Code World Models Large Language Model-Guided Optimization LLMs for Evolutionary Optimization World Models Evolutionary Optimization Combinatorial Optimization

Ask PDF

Jun 23, 2026

Bayesian control for coding agents

Modern coding agents pair LLM generators with various tools, including cheap diagnostics and expensive verifiers. The tool-use decisions are typically governed by orchestrators that often use fixed rules and ignore uncertainty. We formulate orchestration as cost-sensitive sequential hypothesis testing: a Bayesian controller maintains a belief over candidate correctness and dynamically decides whether to gather more evidence, refine the candidate, verify it, or stop. Across six generators and nine coding benchmarks, Bayesian control proves to be most valuable when verification is costly and critics are informative but imperfect. Beyond control, the belief state yields an interpretable correctness score that outperforms token-probability and raw tool-success baselines for uncertainty quantification.

Theodore Papamarkou, Vladislav Smirnov, Viktor Mazanov +4

1PolyShape · 3MBZUAI

Language Model-Based Control Coding Agents Bayesian Decision Theory LLM Uncertainty Estimation Sequential Hypothesis Testing

Ask PDF

Sep 28, 2026

Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization

The upgrade and rewriting of large scientific codebases has traditionally been a major challenge. While evolutionary search with large language models (LLMs) can port and accelerate legacy code, repair feedback in prompts alone does not prevent subsequent candidates from repeating the same errors. We introduce Certificate-Driven Evolutionary Search (CDES), which extends evolutionary search with enforceable restrictions derived from failed candidates, recorded as certificates of assumptions, checker evidence, and justified restrictions. Its control logic enforces these restrictions through rejection, backtracking, and targeted repair while preserving compatible edits. We apply CDES to CPU-to-GPU translation of two particle-simulation functions from the Geant4 toolkit, evaluated with a harness that goes beyond unit tests to combine formal checks, numerical comparisons, physics checks, and GPU safety tests. Generated implementations achieve 13.78x and 23.54x function-level speedups over CPU code, including data conversion and transfers; for one function, GPU throughput exceeds an expert implementation by 14.9%, reaching 16.1% when complementary components are combined. In an ablation over execution settings, certificate feedback increases the fraction of candidates passing required correctness checks from 55% to 90%.

Piyush Jha, Aishik Ghosh, Vijay Ganesh

School of Computer Science, Georgia Institute of Technology, USA · School of Physics, Georgia Institute of Technology, USA · Lawrence Berkeley National Laboratory, USA

Code Translation GPU Kernel Optimization Evolutionary Optimization Large Language Model-Guided Optimization Scientific Code Generation

Ask PDF

Abstract

Formal Verification

Explore similar work

Code World Models for Parameter Control in Evolutionary Algorithms

Bayesian control for coding agents

Towards Certificate-Driven Software Porting: A Self-Improving Agentic Harness for Scientific Program Optimization