Verifier-guided discovery of exact high-order mimetic operators with large language models

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

scope and result

The paper studies one-dimensional, uniform-grid mimetic finite-difference operators. Its central method is a strict division of labor: a language model chooses a typed construction architecture; deterministic compilation computes coefficients; an independent verifier tests the mathematical and numerical conditions; and exact rational reconstruction certifies selected candidates. The abstract states: “An LLM proposes only a typed construction program; a deterministic linear-program compiler generates coefficients; an independent verifier tests algebra, positivity, physical modes, conditioning, and manufactured PDEs; and coupled rational reconstruction provides exact certificates.” (Abstract, p. 1.)

The motivating fixed MOLE/Corbino–Castillo order-six and order-eight Dirichlet blocks have four non-real boundary-localized modes. The authors prove that, under their positive-definite norm and endpoint-support hypotheses, an endpoint-supported identity would force a real non-positive spectrum (Problem and fixed-closure obstruction, pp. 2–3). The search therefore changes the closure and norm architecture. The paper’s bounded claim is that models find promising structural regions while deterministic mathematics decides validity; it does not claim that models prove the operators (Verifier-guided search, p. 3).

technique: verifier-guided typed program search

What it is. A proposal is a typed record, rather than a coefficient vector. It specifies target interior order, left and right boundary orders, diagonal or positive local-block norm, reflected or independent closures, number of boundary rows, a support width for each row, norm bandwidth, coefficient bounds, positivity margin, and one of four objectives (Methods, “Program representation and deterministic compilation,” p. 9). Continuous objective weights make the program space non-enumerable. The model controls these representation-level choices, while the compiler and verifier are authoritative.

When to use it. Use this pattern when the design space has discrete architectural choices plus continuous coefficients, and when a cheap deterministic checker can reject invalid candidates. The paper warns that a model may propose a familiar stencil, invent a proof, or return approximately constraint-satisfying coefficients (Verifier-guided search, p. 3), so accepting model text as evidence is inappropriate.

How to apply it, following the paper.

1. Define the typed fields for order, closure, support, norm class, bounds, margin, and objective (Methods, p. 9).
2. Transform variables to A = QD and C = PG, then impose the linear endpoint-supported relation A + Cᵀ = B0, with B0 = −e1 e1ᵀ + e_{m+2} e_{m+1}ᵀ (Methods, Eq. 3–4, p. 9).
3. Add linear moment equations for polynomial exactness over shared boundary templates and encode diagonal norms or local block norms. The block cone is Qb = τI + Σ αo vo voᵀ, with τ > 0 and αo ≥ 0 (Methods, Eq. 5, p. 9).
4. Solve the resulting linear program and instantiate D = Q⁻¹A and G = P⁻¹C on design and holdout meshes (Methods, p. 9).
5. Have an external verifier check dimensions, finite coefficients, support, template transfer, derivative moments, conservation identities, the full endpoint identity, norm eigenvalue margins, physical eigenmodes, conditioning, and manufactured PDEs (Methods, “Independent verifier and exactification,” pp. 9–10).
6. Reject a candidate on any failed gate. The search’s fixed endpoint rejects non-real or extra low modes, imposes κ(LI)h² ≤ 2, error thresholds, and a mixed-frequency convergence-rate threshold (Methods, p. 10).

Verus form. Inference: VL can represent each proposal as a Rust/Verus data structure containing order and support fields, then use a deterministic executable compiler for coefficients and requires/ensures contracts for dimensions and affine identities. A proof fn can establish algebraic lemmas about exact matrices; executable code must not call proof functions at runtime. Verus can verify the supplied matrix contracts, but the paper’s LP, eigenvalue tests, and floating-point PDE measurements remain external trusted computations unless separately modeled. Verus has no paper-defined typed-program grammar, LP solver, or automatic spectral theorem, so those are an integration boundary rather than a direct translation.

Evidence and limits. Across 1,200 deterministic solver calls, full-metric feedback accepted 66/120 (55.0%), illumination archive 64/120 (53.3%), expert prior 120/240 (50.0%), and uniform random search 32/240 (13.3%) (Results, Table 1, p. 5). The denominator is calls under the common external verifier, not generated tokens. Both feedback comparisons had Holm-corrected p = 0.0117; the paper explicitly says this supports a yield advantage over random search, not dominance over expert search (Results, pp. 4–5). A diagnostic repair offer accepted 20/42 refined versus 25/55 fresh proposals (p = 0.840), and 637/638 (99.8%) LP-infeasible programs failed endpoint compatibility equations (Results, p. 5). These figures indicate global structural constraints, not a reliable one-step textual repair.

technique: coupled exactification and independent certification

What it is. Selected floating-point LP solutions are reconstructed in the complete coupled affine system, not coefficient by coefficient. An independent rational equation basis and reduced-row-echelon parameterization identify free coordinates; free coordinates are put on a common dyadic grid, pivot coordinates are solved exactly, and every original equation is rechecked (Methods, “Independent verifier and exactification,” p. 10).

How to apply it. Recompile the selected program; build the full affine equation system; compute an independent equation basis and reduced-row-echelon form; choose a common dyadic grid only for free coordinates; solve pivots exactly; recheck every original equation; certify norm positive-definiteness using leading principal minors; and rerun the numerical verifier on unseen meshes (Methods, p. 10). The paper reports that all four leading order-six-interior/order-four-boundary LLM constructions passed affine identities, direct positive-definiteness, physical-mode tests, and transfer through m = 640 (Results, p. 5).

Verus form. Inference: encode rational coefficients with exact integer numerator/denominator types and prove the affine identity using ensures on a proof function over sequences or matrices. Use a separate executable checker for Gaussian elimination and principal-minor calculations, and expose its result through a specification predicate only after independently validating its implementation. A Verus proof can certify the resulting exact identity; it does not by itself certify an unmodeled floating-point LP solution or a numerical eigenvalue computation.

Evidence. The strongest structure-only candidate used denominator 236 and changed the floating-point solution by at most 1.27 × 10⁻9 (Results, p. 5). At m = 160, it had ρ(L)h² = 6.165962, certified κQ = 1.830782, and mixed-frequency PDE RMS 8.91 × 10⁻8; relative to the prior positive-diagonal 6–3 candidate, the paper reports a 25.4% lower spectral-radius constant and a 62.7-fold lower PDE error (Results, p. 5). The reference was about 69 times more accurate on that manufactured problem but retained four non-real modes, so this is a structure–accuracy trade-off, not a uniform improvement.

technique: certificate-driven downstream guarantees

The exact identity yields a weighted energy certificate. For u̇ = LIu and EQ(u) = 1/2 uᵀQIu, the paper gives ĖQ = −uᵀ(GᵀPG)I,Iu ≤ 0 (Results, p. 6). At m = 200, the candidate’s normalized weighted-symmetry residual was 1.2 × 10⁻16; the order-six reference’s was 0.52. The candidate was contractive, while the reference reached 1.066 transient energy amplification at t/h² ≈ 0.333 (Results, pp. 6–7). Both nevertheless had the same RK4 limit, Δtmax/h² = 0.4517, so energy certification did not imply a larger explicit step.

The same certificate determines solver applicability. At m = 200, all seven exact constructions had weighted-symmetry residual at most 1.2 × 10⁻16, smallest eigenvalue +0.0493, and CG applicable; the four reference systems failed the weighted-symmetry and positivity conditions in their native quadrature (Results, Table 3, p. 7). Seven exact constructions required 114–120 CG iterations. Deliberately applying CG to the order-six reference’s symmetric part reached residual 5.0 × 10⁻11 but returned error 0.278; a dense direct solve and GMRES on the original system had errors about 1.00 × 10⁻9 and 1.01 × 10⁻9 (Results, pp. 7–8). The paper identifies symmetrization, rather than the reference discretization, as the source of that diagnostic failure.

Verus form. Inference: state the matrix identity and positive-definite quadratic-form obligations as spec fn predicates, then prove energy monotonicity with a proof fn using ensures. Use Verus’s supported arithmetic and sequence/matrix specifications for the finite-dimensional proof. CG iteration counts, RK stability bisection, and transient amplification are measurements requiring an executable numerical harness; they are evidence about an implementation and mesh, not universal Verus theorems.

what is proved, trusted, and left open

The formal mathematical result is the proposition that positive Q and P, the endpoint identity, norm-separation, and vanishing restricted boundary term imply a real non-positive Dirichlet spectrum (Problem and fixed-closure obstruction, p. 2). Exact candidates receive reconstructed affine identities and positive-definiteness checks. Numerical claims are bounded by the listed meshes, manufactured solutions, thresholds, and model schedules. The LP compiler, external verifier, rational-reconstruction implementation, eigenvalue and PDE libraries, floating-point arithmetic, model outputs, code repository, and the correctness of the written specification remain trusted or only experimentally checked. Inference: a Verus product should treat these as explicit trust-boundary components and separately verify the compiler/checker kernels where practical.

The paper says the primary feedback comparison is not fully causal because model-role schedules were generated separately; the expert prior is a strong control; the surrogate is lightweight; the grammar is constrained by a boundary-order preflight rule; and the novelty screen and operator library are incomplete (Discussion, p. 8). The study is one-dimensional and uniform-grid, and the block-positive cone is only a sufficient inner approximation of the full banded semidefinite cone (Discussion, p. 8). Inference: these restrictions make transfer to agent-written verified Rust an unmeasured product risk. The reusable product lesson is the propose–compile–verify–exactify boundary: agent suggestions can guide search, but only deterministic, independently checked artifacts should enter a trusted proof pipeline.

techniques for the catalog

• typed verifier-guided program search — let a model choose a constrained construction architecture while deterministic compilation and an external verifier decide validity
• coupled rational exactification — reconstruct selected numerical solutions in a coupled affine system and recheck every exact equation and positivity condition
• certificate-driven energy and solver checks — derive weighted energy and CG conditions from an exact matrix identity, then measure downstream dynamics separately

Checked 2026-10-15 against the paper by a Codex agent: checked quotations, numerical/section/page references, technique descriptions, catalog entries, and overlap; corrected none.

Last edited: 2026-10-15