Working Theory · Certificates, Error Dynamics & Verification

The Theory Behind AlgoGens

Our thesis: pairing a general generative prior G with a non-neural algorithmic authority V and a search topology S changes what can be certified, how errors correlate, and how much search is needed. This page is a framing. Each result below is labelled as a known result, a proposition, a claim or a prediction, and full statements and proofs will appear with the papers.

1. What an Evaluator Can Certify

A natural question is whether scaling a foundation model will remove the need for external solvers and verifiers. This page does not claim an unconditional complexity separation, which would settle open problems. It makes a narrower point about which kind of statement a score can back up.

Primal claim: value(x) ≥ v vs. Optimality claim: value(x') ≤ v for every x' in X

Proposition (certificate type; stated here without proof): An evaluator can certify primal claims of the form “this object has value at least v”. Checking one means running the evaluator on one object, so such claims are NP-type: short to verify once the object is in hand. Optimality claims, “no object in X has value above v”, need a dual certificate: a bound, a proof or an exhaustive argument that covers all of X. A score from running the evaluator is not such a certificate.

Prediction (testable, not yet tested): Discoveries driven by an evaluator alone, of the AlphaEvolve type, are primal-only. They produce new constructions with a higher value, not proofs that the value is the best possible. We plan to check this against the cards in the library.

This is why an AlgoGen A = (G, X, V, S, F) pairs the generator with an authority that can do more than score. G proposes candidates, and V certifies primal claims. Where the problem allows it, S supplies the bound or the exhaustive search that turns a score into an optimality claim, as when a branch-and-bound solver reports an optimality gap. We do not claim that a neural network can never produce such a certificate.

2. Why a Prior Helps: Valid Solutions Are a Tiny Fraction

In scientific and algorithmic discovery (such as de novo protein design, crystal lattice generation, or matrix multiplication tensor decomposition), the candidate space X can be astronomically large, while the subset of valid, high-performing solutions X* = {x ∈ X : V(x) = 1 and S(x) ≥ τ} can occupy a very small share of it under the uniform measure. The orders of magnitude below are illustrative, not measurements:

μ_uniform(X*) = |X*| / |X| (illustrative scale: 10⁻⁵⁰ or smaller)

Idealized target distribution: Rather than enumerating grammar rules blindly (classical CEGIS) or sampling unconstrained neural outputs (standalone LLMs), an AlgoGen aims at the following target. Real systems approximate it by filtering, repair and search:

P_A(x) = (1 / Z) · P_G(x | F) · I[V_hard(x) = 1] · exp(β · S_score(x))

Why Classical Search (S + V without G) Stalls: Uniform or local syntactic enumeration has expected hitting time E[τ] = 1 / μ_uniform(X*), which becomes impractical when the share of valid solutions is tiny.
Why Standalone Generation (G without V + S) Fails: Because X* is bounded by sharp formal constraints (a single flipped sign invalidates a Lean proof; a single steric clash breaks a protein), unchecked sampling from P_G(x) can place substantial probability mass outside X*.
Where the Gain Comes From: If P_G puts far more mass on X* than the uniform measure does, then sampling from P_G, filtering with V and climbing S(x) reaches X* in far fewer trials than uniform enumeration. The size of the gain depends on how well P_G concentrates on X*, and no general bound is claimed here.

3. Independent Errors & Diagnostic Feedback

Why can neural self-correction (Self-Refine), multi-agent debate, and LLM-as-a-judge stagnate or degrade as test-time compute increases? Let e_G(x | c) denote the error indicator of generator G given prompt context c, and let e_critic(x | c) denote the error indicator of a neural critic.

Self-Refine: Cov(e_G(x | c), e_critic(x | c)) > 0 (shared weights and context) • Idealized AlgoGen: Cov(e_G(x | c), e_V(x)) = 0

Claim 1 (diagnostic condition, one repair round; stated without proof): Partition candidate errors into validator-legible errors D (detectable by deterministic check V with targeted repair gain Δ_d > 0) and non-legible errors U (with residual drift Δ_u). Validator-guided repair is expected to beat ungrounded self-refinement when:

Pr(D) · Δ_d > Pr(U) · |Δ_u|

This is a sufficient condition, not an exact criterion. An exact multi-round statement and its proof will accompany the paper's preprint.

Because a non-neural verifier V (compiler, SMT/MIP solver, PDDL planner, or proof kernel) evaluates the formal candidate x directly without reading the noisy prompt c, its errors are expected to be largely independent of the generator's. This is an idealization. A sound but incomplete validator still passes some wrong answers, and a wrong specification passes it entirely. Table 1 reports one measured comparison on Planetarium PDDL compilation:

Table 1 · Cross-model semantic equivalence on Gripper PDDL compilation (n = 109). Counts come from the raw run logs and are being re-verified for the paper's preprint. The GPT-5.4 row is one exploratory run through an unpinned model alias.
Model Family	One-Shot (%)	Self-Refine (%)	AlgoGen Repair (%)	Δ (Repair vs. OS)	Cohen's h ( vs. SR)	Regressions
Claude Sonnet 4.6	32.1%	78.0%	76.1%	+44.0 pp	−0.04	2 (50 fixed : 2 lost)
GPT-5.4	2.8%	0.9%	69.7%	+66.9 pp	+1.78 (p < 10⁻²²)	0 (73 fixed : 0 lost)

Table 2 · Robustness under prompt perturbations: under re-verification. Earlier drafts of this table disagreed with each other, so it has been withdrawn. Canonical numbers will appear with the paper's preprint.

4. Ordering Multi-Fidelity Verification Cascades

In complex scientific and engineering domains, exact verification can be computationally expensive (for example, quantum Density Functional Theory takes hours per crystal; full solver reachability takes seconds). An AlgoGen structures V = (V₀, V₁, ..., V_m) as a sequential short-circuit cascade where stage V_i has execution cost c_i and conditional rejection probability p_i.

c₀ / p₀ ≤ c₁ / p₁ ≤ ... ≤ c_m / p_m ⇒ min E[C_V] = Σ_i=0..m c_i Π_{j < i} (1 − p_j)

Known result (cost ordering for independent stages): When stage outcomes are independent, running the checks in non-decreasing order of the ratio c_i / p_i minimizes expected verification cost per candidate. This is a classical result from the literature on sequential testing and scheduling (Mitten, 1960; Garey, 1973; Simon and Kadane, 1975), not a contribution of this framework. It does not carry over to dependent stages. If a cheap check rejects mostly the same candidates as an expensive one, the best order can be different.

V₀ (Implicit Constrained Decoding / Tool Schema, < 1 ms): Enforces valid JSON/AST grammar at token sampling time, eliminating raw parse failures before explicit checks run.
V₁..V₃ (Syntactic, Type, Grounding & Consistency Checks, < 10 ms): Catches undeclared symbols, arity mismatches, and contradictory literals in milliseconds.
V₄ (Exact Solver, Proof Kernel, or Surrogate Potential, 0.3 s to 10 s): Executes reachability, SMT/MIP solving, or neural interatomic relaxation only on structurally sound candidates, guarded by a timeout guard so inconclusive timeouts never overwrite verified states.
V₅ (High-Fidelity Quantum DFT or Wet-Lab Assay, hours to days): Reserved for the top-ranked survivors of the computational funnel (as in GNoME, MatterGen, and RFdiffusion).

5. Diagnostic Feedback (F) as a Directional Signal

Classical discrete optimization is difficult because combinatorial spaces (program ASTs, formal proofs, PDDL specifications, molecular graphs) lack continuous analytical gradients: ∇_x f(x) does not exist. Random mutation in evolutionary search or unguided resampling therefore explores blindly.

In an AlgoGen, the composition of the verifier and feedback channel (F ˆ V)(x_t) extracts a localized counterexample trace, unsat core, compiler traceback, or failed proof obligation and projects it into natural/symbolic language that G can condition on:

x_t+1 ~ P_G(x | x_t, F(V(x_t)))

Because G encodes the joint distribution between syntactic structures and their semantic behaviors, conditioning on the diagnostic F(V(x_t)) can act as a directional signal in discrete space, loosely analogous to a gradient step in continuous optimization. How much a corrective round gains, and how that changes over rounds, is being re-measured. Per-round figures from earlier drafts are withdrawn, and canonical numbers will appear with the paper's preprint.

6. Three-Phase Intra-Algorithmic Blueprints

Rather than treating algorithms merely as external black-box tools, the AlgoGen methodology places generative intelligence inside the three internal execution phases of classical algorithms. Where the model only makes a choice the algorithm allows to be arbitrary (a tie-break, a branching variable, a pivot rule, a mutation proposal), the algorithm's correctness is kept. Where the model replaces a component the guarantee depends on (an A* heuristic, a preconditioner), the guarantee holds only if that component passes a checkable contract, such as admissibility or positive definiteness. The table lists where interventions can go. It does not say that every one preserves a guarantee.

Table 3 · Illustrative intra-algorithmic interventions across classical algorithm families.
Algorithm Family	Phase 1: Semantic Preprocessing	Phase 2: Inner `while` Loop Steering	Phase 3: Postprocessing & Authority
A* & Heuristic Graph Search	Topology conditioning & anomaly pruning on raw graph inputs.	Dynamic context-aware adjustment of heuristic `h(n)` inside `while OpenSet`.	Exact path cost verification & admissibility bound check.
Branch-and-Bound & MIP	Natural-language-to-MILP compilation & warm-start primal proposal.	Prior-guided branching variable selection & primal heuristic diving.	Exact dual bound proof & explicit optimality gap certificate.
Genetic & Quality-Diversity (MAP-Elites)	Semantic population seeding across behavioral niches.	Code-level semantic crossover, AST mutation & adaptive selection pressure.	Sandbox execution scoring & elitist archive retention.
MCTS & Proof-State Tree Search	Autoformalization of theorem statement into formal kernel types.	Policy prior over tactic branching & value estimation inside tree expansion.	Formal kernel typecheck (Lean 4, Coq, Isabelle, DD+AR).
Simulated Annealing	Initial feasible configuration synthesis.	Context-guided move generation & adaptive cooling schedule control.	Energy objective evaluation & Metropolis acceptance criterion.
Finite Element & PDE Solvers	Semantic geometry analysis for adaptive mesh coarsening/refinement.	Dynamic time-step control & local solver scheme switching.	Residual norm verification & conservation law auditing.
Sparse Matrix & Linear Solvers	Sparsity pattern classification & storage format selection (CSR/COO/CSC).	Predictive preconditioner synthesis & Krylov subspace steering.	Exact backward error & residual convergence check.
Bayesian Inference & BO	Prior distribution synthesis from unstructured scientific literature.	Generative acquisition function proposal in high-dimensional discrete space.	Likelihood evaluation & posterior consistency validation.

Read the paper

The survey behind this page is public as a preprint (v1, CC BY 4.0): doi.org/10.5281/zenodo.24091751.

Shachar, A. (2026). AlgoGens: A Survey and Theory of Generator-Authority Systems (v1). Zenodo. https://doi.org/10.5281/zenodo.24091751

Browse the 99-system library Read About & Inclusion Criteria