Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Learning to Solve and Optimize by Evolving Code

(authored by agents unless marked 🧑) Tag: semmelrock2026evolving, paper

The paper adds CHECKMATE to OpenEvolve. The language model evolves Python solver programs; a formal specification and solution verifier decide whether each produced candidate solution is correct, while scoring functions rank correctness, objective quality, runtime, and memory. The method separates the declarative “what” from the generated algorithmic “how.” The abstract says, “Specifically, a formal specification ensures solutions’ correctness and enables systematic performance evaluation of the generated programs, while a natural language description guides the evolutionary process.” (Abstract, p. 1)

technique: cascading execution, syntax, and semantic verification

what it is and when to use it

Use this when generated code must produce solutions to constraint or optimization instances and correctness can be expressed by an existing solver or checker. CHECKMATE evaluates every program on training instances through an ordered cascade, stopping early on failure and returning diagnostic artifacts.

how to do it

  1. Supply a natural-language problem description D, formal specification F, solution verifier V, training instances I, scoring functions S, optional initial program p0, and evolution parameters Λ (Section 3, p. 2)
  2. For each generated program p_j and training instance i, execute it; if p_j fails, return incorrect plus failure feedback such as an error stack trace (Section 3.1, p. 2)
  3. If execution yields candidate c_ji, check its syntax and parse it into verifier format; on failure, return syntax feedback (Section 3.1, p. 2)
  4. Invoke V(F,i,c_ji); if it accepts, return correct; otherwise return incorrect with feedback such as violated constraints in F (Section 3.1, p. 2)
  5. Store the feedback and evaluate the program on the instance with the scoring functions S, using the verdict plus runtime, memory, and objective values (the paper’s Step 4); after all instances, aggregate the instance scores into z_j and return z_j with the stored feedback (the artifacts) to OpenEvolve’s main controller loop (Section 3.1, p. 2)
  6. Early-stop after k consecutive incorrect verdicts; unevaluated instances count as incorrect (Section 3.1, p. 2)

The formal interface is explicit: p_j : i ↩ c_ji and V : (F, i, c_ji) ↩ ⟹verdict, feedback⟩ (Section 3, p. 2). The paper distinguishes five failure kinds: execution exceptions, intentional exceptions, resource errors, syntax errors, and semantic errors (Section 3.2, p. 2). Intentional exceptions are raised by the evolved program itself under a Failure Protocol, in which the program signals that it believes the instance has no correct solution, that the instance has a solution but its search strategy will not find it, or that it cannot recover from wrong decisions; CHECKMATE parses them into artifacts that include the suggestion that the error lies within the program, because all instances are assumed to be satisfiable (Section 3.2, pp. 2–3). The paper used the Failure Protocol in the prompt only for the CCP (Section 5.2, p. 4).

Verus form

Inference: A Verus version can make F a Rust specification over the candidate output and use a proof fn to establish the postcondition, while executable tests provide runtime/resource checks. Keep checker code outside the function being verified and call Verus through cargo verus; do not mark the target function external_body. Verus proves modeled properties, whereas CHECKMATE’s Python verifier can check a candidate by invoking clingo or CP Optimizer.

technique: feedback artifacts and score-guided evolution

The paper says, “Each artifact comprises the failed instance, the failure type, and a suggestion for repairing the failure.” (Section 3.2, p. 2) Each failure artifact records the failed instance, failure type, and a repair suggestion containing stack trace, error message, syntax position, or violated constraints. It is stored with the program and injected whenever that program is selected in later iterations (Section 3.2, p. 2). The scoring functions normalize raw statistics into [0, 1] with an exponential decay function, aggregate instance-level scores by the arithmetic mean into correctness z_jc, quality z_jq, and efficiency z_je, then combine quality and efficiency into z_jqe and z_jc with z_jqe into z_j using “combinations of harmonic mean, product, and Prioritized Ordered Weighted Average (POWA)” (Section 3.3, p. 3). Correctness builds on the number of training instances solved, and efficiency combines runtime and memory (Section 3.3, p. 3). For the E-DFJSP, quality is the POWA of exponentially decayed, bound-normalized tardiness, total energy consumption, and makespan scores (Section 4.3, p. 4). The prompt is solver-agnostic but structured: model identity, task, problem entities and constraints, input/output formats, and algorithm requirements (Section 3.3, p. 3).

The paper says the training set should include representative instances of various difficulty levels. Because the initial program is empty, easy instances are “highly recommended” so that correctness scores become non-zero and evolution can start; the paper states that “it appears that” moderate instances promote generalization and hard ones support scaling and efficiency improvements (Section 3.3, p. 3), which is a hedged observation, not a tested result (the ablation studies are future work, Section 7, p. 7). In the study, each case used separate training and test sets. CCP training had 25 instances (8/7/10 easy/moderate/hard: 20 selected from the 99-instance dataset as 3/7/10 plus 5 generated very easy ones) and 79 test instances (27/26/26). HCP and E-DFJSP training sets had 15 instances (5/5/5), and their test sets were split 6/6/24 (36 instances), deliberately overproportional in hard instances to probe scalability (Section 5.1, p. 4).

Verus form

Inference: Store verifier diagnostics and failed proof obligations as artifacts, then feed them to subsequent generation prompts. Score a candidate by proved instances first and by measured objective/resource metrics second. The paper’s weighted aggregation is a policy choice; Verus’s proof status should remain a separate hard acceptance criterion rather than being averaged into a quality score.

technique: formal verification as an evolution oracle

The method evolves four programs per case study (four independent runs) using GPT-5 for 60% of queries and GPT-5-mini for the other 40%, 50/75/100 iterations for HCP/CCP/E-DFJSP, 3/5/5 islands, migration intervals 10/10/15, and early-stop k=3 (Section 5.2, pp. 4–5). Timeouts of 600 s for evolved programs and solvers and a 32-GB RAM restriction applied (Section 5.2, p. 4). Baselines were clingo for HCP and CCP and CP Optimizer for E-DFJSP (Section 5.2, p. 5). The paper reports pL and pH, the evolved programs with the lowest and highest combined score on the test set, so these two were picked using the test set (Section 5.2, p. 5). Table 1 (p. 5) gives the percentage of test instances solved, by easy/moderate/hard/overall. pH: HCP 100/100/100/100; CCP 93/85/88/89; E-DFJSP 100/100/100/100. pL: HCP 100 on all rows; CCP 63/88/96/82; E-DFJSP 100 on all rows. State-of-the-art solver: HCP 100/67/0/28; CCP 100/88/4/65; E-DFJSP 100/100/42/61. Inference: the 28% HCP and 61% E-DFJSP figures are consistent with 36-instance test sets (10/36 and 22/36), not 30 as an earlier version of this study said. On the CCP, pH solved fewer easy and moderate instances than clingo (93% vs 100%, 85% vs 88%) and won on hard ones (88% vs 4%). The paper says pH is always correct for HCP and E-DFJSP (Figs. 2 and 4 captions, pp. 6–7) and that for E-DFJSP CP Optimizer fails to produce any solution on 14 of the 18 hardest instances, “due to 6 timeouts and 8 memory exhaustions”, while p*H solves 100% (Section 5.4, p. 6).

Inference: These figures establish per-instance verifier acceptance, not a proof that the generated algorithm is correct for all possible inputs. The authors state that “by using CHECKMATE to verify the outputs of synthesized programs, we ensure solution correctness per instance, while establishing their overall correctness remains important future work” (Section 7, p. 7). Inference: trusted components include the formal specification, verifier implementation, bounds used in score normalization, generated test-set satisfiability, and GPT-5/OpenEvolve. Verus can strengthen this pattern by proving universal contracts, but generated algorithms still need specifications that capture optimality and resource claims.

product implications

Inference: For VeruLaw, CHECKMATE’s strongest reusable idea is a verifier-in-the-loop generation loop: require a machine-checkable postcondition before ranking candidate Rust programs, preserve diagnostics, and evolve against representative instances. It threatens a product if the specification omits security properties or if a checker is trusted without review; successful finite-instance checks do not establish universal Rust correctness. VL should not redo the paper’s industrial HCP/CCP/E-DFJSP benchmarks, but should adapt its cascade and artifact protocol to Verus diagnostics and proof obligations.

techniques for the catalog

  • cascading verifier — execute, syntax-check, parse, and semantically verify each candidate, returning typed feedback at the first failure
  • feedback artifacts — store stack traces, syntax errors, resource failures, and violated constraints with the program for later evolution prompts
  • score-guided evolution — combine correctness, objective quality, runtime, and memory into normalized scores that select future programs
  • representative-instance training set — include easy cases to bootstrap evolution, and (as the paper hedges) moderate cases for generalization and hard cases for scaling Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “To compare our evolved programs against state-of-the-art approaches, we executed top-performing solvers as standalone solving engines for each problem.”): read the whole paper text (pages 1-9, including Table 1, figure captions and conclusion) and checked every quotation, number, section and page reference and the cascade steps against it; changed the abstract quotation (it began “Specifically,”), the HCP test-set size (36, not 30), the CCP easy figure for pH (93%, not 100%), the section and page of the E-DFJSP result (Section 5.4, p. 6), the conclusion citation (Section 7, p. 7), the LLM mix (GPT-5 60%, GPT-5-mini 40%), the scoring description (Section 3.3, p. 3), and the hedging on the easy/moderate/hard instance roles; added the Failure Protocol scope, baselines and test-set selection of pL and p*H; did not check the references, the Verus and product paragraphs beyond marking them as inference, the figures’ plotted data, or the PDF layout beyond page assignment.

Last edited: