Paper deep dive
Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits
Haifeng Li, Mo Hai
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 7/21/2026, 3:49:42 AM
Summary
This paper introduces a falsification-based verification framework for Large Language Model (LLM)-generated optimization models. It proposes a sound test battery that verifies model faithfulness by testing how the model responds to transformations of numeric 'slots' (typed quantities like costs, capacities, and requirements) without requiring a reference model or ground truth. The approach leverages optimization theory (duality, comparative statics, polyhedral limits) to derive six classes of tests (directional, curvature, crush, prohibitive, annihilation, exchange) that guarantee a zero false-positive rate. The authors characterize detection limits, proving that certain errors (like uniform objective rescaling) are invisible, while others are detectable with certainty. Experiments on 326 ground-truth models from NL4OPT and other benchmarks confirm the theory, showing the battery detects 70% of conditional-class mutants and 40.4% of mutants invisible to execution-accuracy scoring, significantly outperforming threshold-based testers.
Entities (10)
Relation Signals (15)
Mo Hai → affiliatedwith → Central University of Finance and Economics
confidence 98% · AUTHOR Mo Hai AFFSchool of Information, Central University of Finance and Economics
Haifeng Li → affiliatedwith → Central University of Finance and Economics
confidence 98% · AUTHOR Haifeng Li AFFSchool of Information, Central University of Finance and Economics
Falsification-Based Verification → achieves → Zero False-Positive Rate
confidence 96% · Every test is sound, so a violation certifies unfaithfulness and the false-positive rate is zero by design.
Falsification-Based Verification → uses → Test Battery
confidence 95% · This paper develops a theory of falsification-based verification... we derive a battery of test classes
Test Battery → outperforms → Threshold Tester
confidence 94% · The battery attains a 0.0% false-positive rate against 54.9% for a threshold tester
Test Battery → evaluatedon → NL4OPT
confidence 93% · Experiments on 326 ground-truth models from NL4OPT and four benchmark families confirm the theory.
Test Battery → includes → Exchange Tests
confidence 92% · battery of test classes covering directions, curvature, crush probes, prohibitive limits, annihilation, and exchange.
Test Battery → →
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Large language models now translate natural-language descriptions of decision problems into solver-ready optimization models, but they fail silently. A generated model often runs and still formulates the wrong problem. This paper develops a theory of falsification-based verification for this setting. Every numeric quantity in the description is a typed slot, and a candidate model is tested only through solver calls on slot-transformed instances; no reference model or label is consulted. From duality, comparative statics, and polyhedral limit arguments we derive a battery of test classes covering directions, curvature, crush probes, prohibitive limits, annihilation, and exchange. Every test is sound, so a violation certifies unfaithfulness and the false-positive rate is zero by design. We characterize what such verification can never see, give conditions under which the canonical error classes are detected with certainty, and prove that no fixed-threshold perturbation tester is simultaneously sound and nontrivial. Experiments on 326 ground-truth models from NL4OPT and four benchmark families confirm the theory. The battery attains a 0.0% false-positive rate against 54.9% for a threshold tester, detects 70.0% of certified conditional-class mutants, convicts 40.4% of the mutants invisible to execution-accuracy scoring, and reproduces the predicted detectability pattern including its zeros.
Tags
Links
- Source: https://arxiv.org/abs/2607.16646v1
- Canonical: https://arxiv.org/abs/2607.16646v1
Trouble viewing inline? Open PDF directly →
Full Text
100,231 characters extracted from source content.
Expand or collapse full text
Li and Hai -Based Verification of LLM-Generated Optimization Models Falsification-Based Verification of LLM-Generated Optimization Models: Sound Test Batteries and Their Detection Limits Haifeng Li of Information, Central University of Finance and Economics, @cufe.edu.cn Hai of Information, Central University of Finance and Economics, corresponding author, @cufe.edu.cn Large language models now translate natural-language descriptions of decision problems into solver-ready optimization models, but they fail silently. A generated model often runs, returns a solver-feasible solution, and still formulates the wrong problem. Existing safeguards either require a human reference model, ask a second language model to review the first, or apply perturbation checks with tuned thresholds and no guarantees. This paper develops a theory of falsification-based verification for this setting. Every numeric quantity in the description is treated as a typed slot, such as a capacity, a requirement, a rate, or a cost, and a candidate model is tested only through solver calls on slot-transformed instances. No reference model or label is consulted. From duality, comparative statics, and polyhedral limit arguments we derive a battery of test classes covering directions, curvature, crush probes, prohibitive limits, annihilation, and exchange. Every test is sound. Any candidate faithful to the asserted slot roles passes it, so a violation certifies unfaithfulness and the false-positive rate is zero by design. We then characterize what such verification can never see, including uniform objective rescaling, constraints that never bind on the probe orbit, and linear misuse of a single slot, which is invisible to every single-slot probe yet partially exposed by exchange tests. Conversely, we give sufficient conditions under which the canonical error classes are detected with certainty, and we prove that fixed-threshold perturbation testers cannot be simultaneously sound and nontrivial. Experiments on 326 ground-truth models from NL4OPT and on four benchmark families with a locally hosted 7B generator confirm the theory. The battery attains a 0.0% false-positive rate on faithful models while a reimplemented threshold tester attains 54.9%; it detects 56.1% of mutants in the five core error classes and 70.0% of conditional-class mutants whose preconditions are certified; among the mutants of the eight detectable classes that reproduce the correct optimal value at the benchmark instance, and are therefore invisible to execution-accuracy scoring even with perfect labels, it still convicts 40.4%; and it reproduces the predicted class-by-error detectability pattern, including its zeros and the exchange-only detection of single-slot misuse. On the generation pipeline it certifies role violations, relative to the extracted assertions, in 27.6% of label-matching NL4OPT candidates and 15.7% pooled over the four benchmark families. All code, data, and an open-source verifier accompany the paper. automated optimization modeling; large language models; verification; metamorphic testing; linear programming duality; comparative statics; trustworthy analytics 1 Introduction An operations researcher who receives a model from a junior colleague does not check it by re-deriving it from scratch. She interrogates it. If we double the budget, does the plan get better? If demand were zero, would we really spend nothing? Why does adding a truck make things worse? These questions require no knowledge of the correct model. They exploit the fact that the structure of the problem dictates how any correct formulation must respond to changes in its data. A model that spends money at zero demand, or deteriorates when given more capacity, convicts itself. This paper turns that interrogation into mathematics and software for a setting where it has become the bottleneck in practice, namely optimization models generated by large language models. A rapidly growing line of work fine-tunes or prompts LLMs to translate natural-language problem descriptions into solver-ready mathematical programs (Ramamonjison et al., 2023; Xiao et al., 2024; AhmadiTeshnizi et al., 2024; Huang et al., 2025; Jiang et al., 2025; Lu et al., 2025). The reported progress is real, but it is measured almost exclusively by execution accuracy, which generates a model, runs a solver, and compares the optimal value against a labeled reference. Deployment offers no such reference. Worse, execution accuracy is blind in both directions. A generated model can return the labeled value by accident while encoding the wrong feasible set, and a correct model can be scored wrong because the label itself is erroneous. Errors in the public test sets are documented, and Chen et al. (2025b) found it necessary to review and correct the NL4OPT and IndustryOR labels before evaluating on them. The gap between solver feasibility and semantic correctness reaches up to ninety percentage points on compositional problems (Lian et al., 2026). Silent failure rather than syntax error is the dominant failure mode, and it is precisely the failure mode that current evaluation cannot see. The community has responded with three families of safeguards. Reference-based evaluation compares generated models against human-written ground truth (Wang et al., 2025); it is rigorous but presupposes the artifact whose absence defines the problem. LLM-as-verifier schemes ask a second model to critique the first (Fang et al., 2026; Liu et al., 2026; Li et al., 2026); they inherit the reviewers’ blind spots and offer no guarantees, since self-critique is known to be unreliable exactly when the generator is unreliable (Huang et al., 2024a). Most recently, and closest to this paper, behavioral testing has emerged: Lian et al. (2026) perturb a parameter of the generated code toward an extreme, re-solve, and flag the model when the objective moves by less than a tuned threshold of five percent, interpreting insensitivity as a missing constraint. The instinct to route verification through the solver rather than through another language model is right, and Lian et al. (2026) demonstrate that it repairs real failures. As theory, however, it is incomplete in three ways. First, the thresholds are heuristic. A correct model whose capacity is slack at the probe fails the test, so the false-positive rate is structurally bounded away from zero, and false alarms trigger repairs that damage correct models. Second, the tests ask only whether the objective reacts at all, discarding the far sharper information that optimization theory supplies for free about the direction, the curvature, the limit, and the symmetry of the reaction. Third, and most fundamentally, nothing is known about what such testing can and cannot detect. There is no soundness statement, no characterization of invisible errors, and no separation from the naive alternatives. The empirical literature has, in effect, rediscovered sensitivity analysis as a testing device without the fifty years of theory that make it trustworthy. 1.1 This paper We supply that theory, and we show that it pays measurable dividends. Our starting point is a change of object. A word problem does not describe one optimization instance; it describes a parametric family. Every number in the text is a typed quantity that we call a slot, and its semantic role as a capacity, a requirement, a per-unit rate, a cost, a reward, or a share of a total is asserted by the text itself. A candidate model is faithful only if it responds to slot changes the way the asserted roles dictate. Faithfulness therefore becomes testable by relations alone. We transform slot values, re-solve the candidate, and compare the observed response against necessary conditions derived from optimization theory. No ground-truth model, label, or reference value is consulted at any point. Within this framework we make four contributions. (i) A sound battery. Section 4 derives six classes of structure tests. Directional tests check comparative statics in right-hand sides, objective coefficients, and technology rates, and rest on feasible-set inclusion and pointwise monotonicity. Curvature tests check midpoint convexity of the linear-programming value function and rest on duality. Certified crush probes drive a resource to zero or a requirement toward infinity and demand infeasibility, with no threshold anywhere. Prohibitive-limit probes price an activity out of the model and require exact agreement with the optimum under a hard zero, which a polyhedral finite-threshold argument justifies and a two-scale convergence criterion implements. Annihilation probes zero all requirements and demand exactly zero cost. Exchange probes swap the complete slot bundles of interchangeable entities and demand an unchanged value. Every test is proved sound for the asserted roles (Theorem 4.7). A faithful candidate passes all tests, under any degeneracy, so a violation is a certificate of unfaithfulness and the battery’s false-positive rate is zero by construction, a property that threshold-based testing cannot have (Proposition 5.7). A second, assertion-free layer of coherence tests (homogeneity, relaxation dominance, removal monotonicity, dual subgradient inequalities) is sound for any mixed-integer linear program and catches computational and reporting corruption in generated code. (i) Detection limits. Section 5 characterizes the blind set. Uniform positive rescaling of the objective is invisible to every oracle-free relational battery, and it is provably harmless because it preserves the optimal decisions (Proposition 5.1). Constraints that never bind on the probe orbit are invisible relative to that orbit (Proposition 5.2). Linear misuse of a single slot, the classic unit error in which one coefficient is off by a consistent factor, is invisible to all single-slot probes but is exposed by exchange probes whenever the slot lies in a certified interchangeable bundle (Proposition 5.3). We further prove an asymmetry. The prohibitive-limit equality holds on the cost side of minimization problems but degrades to a one-sided inequality for reward annihilation in maximization problems (Proposition 5.5). Conversely, Theorem 5.6 gives sufficient conditions under which each canonical error class is detected with certainty by a specific test class. The classes cover constraint direction flips, constraint omission, right-hand-side misassignment, dropped objective terms, wrong optimization sense, entity misbinding, and hard-coded data. Together the two results yield a falsifiable prediction in the form of a class-by-error detectability matrix, which our experiments reproduce, including its zeros. (i) A verifiable modeling interface. Section 6 operationalizes the theory for free-form generation. A first LLM pass extracts the typed slot table from the text; a second pass generates the model in a JSON intermediate representation that may reference quantities only through slot identifiers. Data binding, the map from text quantities to model coefficients that behavioral testing silently presupposes, thereby becomes explicit and checkable, and the battery applies to any model, from any generator, without touching solver code. (iv) Computational evidence. Section 7 evaluates the theory on 326 ground-truth models derived from the NL4OPT annotations, a controlled synthetic family, and four benchmark families (NL4OPT, MAMO EasyLP and ComplexLP, IndustryOR) with a locally hosted Qwen2.5-7B generator. The battery’s false-positive rate on faithful models is 0.0%, against 54.9% for the reimplemented threshold tester of Lian et al. (2026). Detection is 56.1% on the core classes M1–M5 (n=3361n=3361) and 70.0% on conditional-class mutants with certified preconditions (n=1515n=1515), against 23.5% where the preconditions fail to certify. The invisibility controls behave as predicted. Uniform objective scaling and orbit-redundant rows are flagged at exactly zero, and single-slot misuse is caught at 38.8%, essentially only through the exchange class, with a 0.8% certificate-transfer residue. Among the 1321 mutants of the eight detectable classes whose optimal value coincides with the correct one at the benchmark instance, which execution accuracy cannot catch even with perfect labels, the battery still convicts 40.4%. Used as a selector the battery does not dominate consensus, and we quantify why. 27.6% of label-matching NL4OPT candidates, and 15.7% pooled over all four families, carry certified role violations relative to the extracted assertions, so the metric and the verifier disagree where the metric rewards wrong structure. As an auditor, the battery isolates label and annotation defects in public benchmarks as a by-product. A solver-call budget analysis shows the battery needs a few dozen millisecond-scale LP solves per model. Throughout, we treat the closest prior work constructively. Lian et al. (2026) route verification through the solver, and we show that their presence heuristics are special cases of a family of tests that optimization theory extends with guarantees. 1.2 Why this matters for operations research The verification question is not an implementation detail of one NLP application. It is the adoption bottleneck for the entire program of automated modeling, and it is a question about optimization rather than about language. The necessary conditions we test are monotonicity of the value function in resources, convexity in right-hand sides, shadow-price consistency, symmetry under relabeling, and exactness of prohibitive limits. They are the accumulated capital of five decades of sensitivity analysis and duality theory. That capital is precisely what distinguishes optimization from generic program synthesis, where the oracle problem is notoriously unsolvable in general and metamorphic testing survives on ad hoc relations (Chen et al., 2018; Li et al., 2024). In optimization, the relations are theorems. The theory operations research already owns is thus an operational verification technology for the AI systems the field is beginning to deploy; using it in this role requires knowing its limits, which we map. 2 Related Work 2.1 LLMs for optimization modeling Translating natural language to mathematical programs began as a semantic parsing task with the NL4OPT competition (Ramamonjison et al., 2023) and has since split into prompting-based agents (Xiao et al., 2024; AhmadiTeshnizi et al., 2024; Mostajabdaveh et al., 2024), fine-tuned open models (Huang et al., 2025; Jiang et al., 2025; Lu et al., 2025; Yang et al., 2024), reinforcement learning with solver-execution rewards (Chen et al., 2025b; Guan et al., 2026; Luo et al., 2026), and inference pipelines with structured reasoning (Zhao et al., 2026b, a). Benchmarks have multiplied alongside, from NL4OPT, MAMO (Huang et al., 2024b), IndustryOR (Huang et al., 2025), OptMATH (Lu et al., 2025), and OptiBench (Yang et al., 2024) to compositional suites such as RetailOpt-190 (Lian et al., 2026) and ConstraintBench (Tso et al., 2026). Two facts from this literature motivate us. The same model that reaches roughly 85% on textbook-style problems drops to 38% on industrial ones (Huang et al., 2025), and the benchmark labels themselves are documented to be unreliable (Chen et al., 2025b). Both facts imply that the binding constraint is no longer generation quality but the ability to tell, for a specific generated model with no reference available, whether it is right. 2.2 Verification of generated models Approaches divide by what they trust. Reference-based evaluation compares against a human ground-truth model, as in the graph-isomorphism test of ORGEval (Wang et al., 2025) and the conversion audits of Klamkin et al. (2025), and therefore needs the human artifact we lack. LLM-trusting schemes organize generation around LLM validation of specification, formulation, and code as in TriVAL (Fang et al., 2026), cross-examine structure and solutions with LLMs as in Opt-Verifier (Liu et al., 2026), coordinate specialist LLM auditors under a fine-grained hallucination taxonomy as in OptArgus (Li et al., 2026), diagnose infeasible models conversationally as in OptiChat (Chen et al., 2025a), or let agent frameworks generate their own test code (Zadorojniy et al., 2025). All ultimately ask a language model to certify a language model. Solver-trusting methods began with ReLoop (Lian et al., 2026), which introduces constraint-presence and objective-presence testing by extreme perturbation with graduated thresholds; OptiLoop (Xu et al., 2026) extends the idea to coordination protocols, and VRPCoder (Luo et al., 2026) verifies vehicle-routing programs by injecting feasible and one-violation probe solutions and reuses the verifier as a training reward. Our work belongs to this third family and supplies the theory it lacks, with a formal framework, soundness guarantees in place of thresholds, a taxonomy of tests strictly generalizing presence checks, detection-limit theory, and a data-binding interface that makes the whole scheme well-defined for arbitrary generators. 2.3 Metamorphic testing and the oracle problem Software engineering addresses testing without expected outputs through metamorphic relations among inputs and outputs (Chen et al., 2018; Segura et al., 2016); LLM-generated code has been validated by cross-prompt consistency (Wang and Zhu, 2024), and surveys catalog relation-generation strategies (Li et al., 2024). The perennial weakness is the source of relations, which are guessed, mined, or crowd-sourced, so that their validity is itself uncertain. Our observation is that optimization is the rare domain where sensitivity analysis, duality, and symmetry supply an inexhaustible stock of provably valid metamorphic relations, and where a violation has a precise meaning as a certificate of unfaithfulness relative to typed assertions. Mutation analysis, which we use to measure detection power, follows the classical methodology (Jia and Harman, 2011) and the optimization-specific mutation study of Zadorojniy et al. (2025), whose binding-constraint counting bound we strengthen to a class-by-error characterization with matched impossibility results. 2.4 Sensitivity analysis and comparative statics The structural results we repurpose are classical, covering value-function convexity and shadow-price subgradients in linear programming (Bertsimas and Tsitsiklis, 1997; Vanderbei, 2020), monotone comparative statics (Topkis, 1998), and Le Chatelier-type principles (Milgrom and Roberts, 1996). Their traditional role is interpretation, that is, what-if analysis for a model assumed correct. Following the inversion first exploited heuristically by Lian et al. (2026), we use them as falsifiers for models assumed suspect; our contribution is to carry out the inversion with the theory’s own standards of rigor, including its impossibility half. The exchange tests connect to symmetry detection in integer programming (Margot, 2010), and the certified crush probes to irreducible infeasible subsystem analysis (Chinneck, 2008). 2.5 Trustworthy AI pipelines in operations Finally, this paper is an instance of a broader agenda of pairing learned components with optimization-theoretic guarantees at deployment time, as in constraint learning (Fajemisin et al., 2024) and decision-focused learning under verification (Sadana et al., 2025). We view sound verification of auto-formulated models as the entry gate through which LLM-based modeling must pass to be usable in regulated and high-stakes operations, in the spirit of model risk management for analytics pipelines. 3 The Verification Problem 3.1 Modeling tasks as parametric families A modeling task is a natural-language description T containing p numeric quantities θ0=(θ10,…,θp0)∈ℝpθ^0=(θ^0_1,…,θ^0_p) ^p. We call the positions j=1,…,pj=1,…,p slots. The text asserts, for each slot, a semantic type; we use the vocabulary qtype(j)∈capacity,requirement,rate,cost,reward,ratio, qtype(j)∈\ capacity,\ requirement,\ rate,\ cost,\ reward,\ ratio\, optionally an entity e(j)e(j) (the activity or product the quantity belongs to), and a global sense σ∗∈min,maxσ ∈\ , \. We write =(σ∗,qtype,e)A=(σ , qtype,e) for this assertion set. Assertions are cheap because they are surface reading rather than modeling. A phrase such as “at most 200” marks a capacity, and “$10 per trip” for vans marks a per-unit cost of the van activity. In our annotated experiments they come mechanically from the NL4OPT ground-truth declarations; in deployment they come from a dedicated extraction pass (Section 6). A candidate model is a parametric mixed-integer linear program Π^:θ↦[σx∈(θ)f(x;θ)=c(θ)⊤x+c0(θ)],(θ)=x∈ℝ≥0n:A(θ)x≶b(θ),xI∈ℤ, : θ\ \ [\ x (θ)σ\ \ f(x;θ)=c(θ) x+c_0(θ)\ ], (θ)=\x ^n_≥ 0:\ A(θ)x b(θ),\ x_I \, (1) where σ∈min,maxσ∈\ , \, ≶ denotes row-wise senses in ≤,≥,=\≤,≥,=\, and I indexes integer variables. The candidate is produced by an untrusted generator; we may execute it (solve at any θ) but not trust it. Define the value function v(θ)∈ℝ¯v(θ)∈ R of Π with the conventions v=+∞v=+∞ (min) or −∞-∞ (max) if (θ)=∅X(θ)= , and the opposite infinities for unboundedness. Definition 3.1 (Role-faithfulness) Candidate (1) is role-faithful to A if σ=σ∗σ=σ and there is a representation of (c,c0,A,b)(c,c_0,A,b) as functions of θ in which each slot j enters only at its asserted position, as the identity map: a capacity slot appears only as the right-hand side of one row of sense ≤ (a requirement slot: of sense ≥); a rate slot with entity e appears only as the coefficient of e’s variable in one constraint row; a cost/reward slot with entity e only as the objective coefficient of e’s variable; a ratio slot ρ with entity e only through a row expressing that e’s activity is at least/at most a ρ-share of the relevant total. All remaining data of Π are constants in θ. Definition 3.2 (Structure- and full faithfulness) When a complete declared formulation S∗S is available (annotated mode), Π is structure-faithful if Π^(θ)=S∗(θ)X_ (θ)=X_S (θ) for all θ in a neighborhood of the probe set, and faithful if in addition its objective agrees with S∗S ’s up to the gauge group of Proposition 5.1. 3.2 Oracle-free tests A probe is a finite collection of solver calls on transformed instances: slot substitutions θ0↦τ(θ0)θ^0 τ(θ^0) (change one or several slot values), model-level operations (relax integrality; fix an entity’s variables to zero), or both. A test t=(π,φ)t=(π, ) pairs a probe π with a predicate φ over the observed tuple of statuses and values (and, for Layer B, duals and incumbents). A battery ℬB is a finite set of tests; the verifier flags Π if some test fails. Definition 3.3 (Soundness and oracle-freeness) A test is sound for a class C of candidates if every Π^∈ passes it (in exact arithmetic). A battery is sound for C if all its tests are. A test is oracle-free if φ does not depend on any reference model, reference optimal value, or human label. Soundness separates certification from anomaly detection. When a sound battery fires, the candidate is provably not in C, and the failed test is a certificate of unfaithfulness. Silence is never claimed to certify correctness. Verification is thus falsification, in the precise Popperian sense, with the class C of faithful candidates playing the role of the theory under test. Two design rules keep the implemented battery sound in floating point. Predicates use one-sided tolerances, so that a violation must exceed ε in the forbidden direction, and every test carries a precondition that is certified before the test may fire, on the declared structure in annotated mode and on the candidate’s own structure in deployment mode. For a faithful candidate the two coincide, and a certification computed on an unfaithful candidate can only affect power, never soundness. 3.3 What the verifier reports For a candidate Π the verifier returns the list of failed tests with their probes. A typical report states that raising the budget slot from 200 to 401 worsened the objective from 3,540 to 3,890, which localizes the misbehavior to one slot and one structural property. We evaluate the detector and leave repair policies, whether to regenerate, patch, or escalate to a human, as orthogonal downstream choices; misdirected repair driven by unsound flags is precisely the failure mode our soundness guarantee eliminates. 4 A Sound Battery from Duality and Comparative Statics Table 4 summarizes the battery. Layer A tests structure against assertions. Layer B tests computational coherence and needs no assertions. We state all results in the main text and give complete proofs in E-Companion 9. The falsification battery. Each row is a family of tests instantiated per slot, row, or entity. The precondition column is certified before the test fires; v is the candidate’s value function. Class Probe Predicate (asserted sense) Precondition Basis A0 static none declared sense =σ∗=σ — assertion A1 rhs direction capacity/requirement slot ± v weakly improves/worsens — set inclusion A2 coef direction cost/reward/rate/ratio slot ++ v moves weakly as asserted x≥0x≥ 0 pointwise monotonicity A3 rhs curvature rhs slot at b−δ,b,b+δb\!-\!δ,b,b\!+\!δ (LP relax.) midpoint convexity (min) finiteness LP duality A4 crush capacity →0→ 0; requirement →R→ R infeasible declared infeasible certified transfer A5 prohibitive limit cost or rate of entity e→M1,M2e→ M_1,M_2 v→v(xe=0)v→ v(x_e=0), two-scale xe=0x_e=0 feasible polyhedral threshold A6 annihilation all requirements →0→ 0 v=0v=0 pure-cost min direct A7 exchange swap slot bundles of e1,e2e_1,e_2 v invariant congruence relabeling symmetry B1 homogeneity objective ×λ×λ v↦λv λ v — any MILP B2 relaxation LP relaxation vLPv_LP weakly better MILP weak duality B3 removal delete one row v weakly improves — set inclusion B4 dual gradient rhs ±δ±δ (LP relax.) subgradient inequality LP optimal convexity of v(b)v(b) 4.1 Directional and curvature tests Proposition 4.1 (Monotone comparative statics) Let Π be role-faithful to A. Then, for every slot j and in the asserted sense σ∗σ : (i) if qtype(j)=capacity qtype(j)= capacity, v is weakly improving in θj _j; if requirement, weakly worsening; (i) if qtype(j)=cost qtype(j)= cost (min) or reward (max), v is weakly worsening, respectively improving, in θj _j; (i) if qtype(j)=rate qtype(j)= rate in a row of sense ≤ (≥), v is weakly worsening (improving) in θj _j; (iv) if qtype(j)=ratio qtype(j)= ratio in a share row of sense ≥ (≤), v is weakly worsening (improving) in θj _j on [0,1][0,1]. All statements hold for mixed-integer candidates. Proposition 4.2 (Curvature) For any LP (in particular the LP relaxation of a role-faithful candidate), b↦vLP(b)b v_LP(b) is convex if σ∗=minσ = and concave if σ∗=maxσ = , on its effective domain; hence the midpoint predicate of test A3 holds along every slot segment on which the three probed values are finite. A3 is run on the relaxation by design. MILP value functions are not convex in b; the relaxation keeps the test sound while still probing the candidate’s constraint data. 4.2 Certified crush tests Presence testing in Lian et al. (2026) perturbs a capacity by ×0.001× 0.001 and flags the model if the objective moves by less than 5%. Soundness fails structurally, because a correct model whose capacity is not binding, or is protected by a tighter sibling constraint, moves by 0% and is flagged. Our crush test replaces the threshold with a certificate and fires only when the assertion structure itself guarantees the outcome. Proposition 4.3 (Certified crush) In annotated mode, suppose the declared structure S∗S is infeasible when capacity slot j is set to 0, or when requirement slot j is set to a large probe value R. Then every structure-faithful candidate is infeasible at the same probe. The certificate is computed by one solver call on S∗S and the test by one solver call on the candidate; no thresholds are involved. A candidate that omitted the row containing slot j, or bound the slot to the wrong row, remains feasible at the crush probe and is flagged with certainty (Theorem 5.6(i)). 4.3 Prohibitive-limit tests The subtlest tests exploit an exactness phenomenon. Pricing an activity out of the model is, beyond a finite threshold, identical to deleting it. Proposition 4.4 (Prohibitive limits, finite threshold) Let Π be role-faithful, let e be an entity whose variables are xex_e, and suppose xe=0x_e=0 is feasible at θ0θ^0 (precondition certified as in Section 3). Write ve0v_e0 for the optimal value of the candidate with xex_e fixed to 0. (i) (Cost side, σ∗=minσ = .) If slot set JeJ_e carries e’s objective costs, then there exists M¯<∞ M<∞ such that for all M≥M¯M≥ M, replacing θj↦M _j M for j∈Jej∈ J_e yields v=ve0v=v_e0 exactly. (i) (Rate side, either sense.) If slot j is a positive rate of e in a ≤-row with nonnegative data, then v(θj→M)→ve0v( _j→M)→ v_e0, with exact equality beyond a finite M¯ M; for integer xex_e the threshold is explicit, since every M>brM>b_r forces xe<1x_e<1 and hence xe=0x_e=0. Moreover, for minimization and every M, v(θj→M)v( _j→M) lies between v(θ0)v(θ^0) and ve0v_e0, a two-sided sandwich used as a runtime check. Because the residual ve0−v(M)v_e0-v(M) of a faithful candidate is nonnegative, nonincreasing, and convex in M and vanishes beyond M¯ M (E-Companion 9.14), the implementation solves at two scales M1≪M2M_1 M_2 and accepts iff |v(M2)−ve0|≤maxε, 4|v(M1)−v(M2)||v(M_2)-v_e0|≤ \ ,\,4|v(M_1)-v(M_2)|\, a convergence criterion that requires no data-dependent tuning. Test A6, which zeroes all requirements and demands the exact value 0 under a certified pure-cost precondition, is proved similarly and directly falsifies wrong-sense and spurious-constant errors. Remark 4.5 (Scale robustness of the two-scale criterion) The exact predicate of Proposition 4.4 refers to the limit and is threshold-free; the implemented acceptance rule fixes the probe scales (M1,M2)(M_1,M_2) and a contraction factor of 44. Concavity and piecewise linearity of v in the probe scale imply that the rule is sound for every faithful candidate whose polyhedral threshold satisfies M¯≤5M2−4M1 M≤ 5M_2-4M_1 (E-Companion 9.14); data whose cost ratios exceed the probe range can defeat it. The condition is verifiable, and the boundary sits exactly where the theory places it. On a constructed two-cost family the rule passes every faithful instance with M¯ M below the bound, rejects every one above it, and enlarging (M1,M2)(M_1,M_2) to cover the data range restores all passes (E-Companion Table 10). Soundness of A5 as implemented is therefore relative to a probe-scale assumption, exactly as Proposition 5.2 makes all guarantees orbit-relative. 4.4 Exchange tests Proposition 4.6 (Exchange invariance) Suppose the assertion structure certifies that entities e1,e2e_1,e_2 are congruent: their slot bundles carry identical multisets of (position, qtype) tags, they participate identically (up to the paired slots) in every row, and their entity-specific bound rows match in sense and unslotted data. Then for every faithful candidate, swapping the two entities’ complete slot-value bundles leaves v unchanged. Exchange tests are the battery’s only cross-slot relational probes, and Section 5 shows they see errors that every single-slot probe provably misses. 4.5 Layer B: coherence without assertions Layer B tests are theorems for arbitrary MILPs, covering positive homogeneity of the value in the objective vector (v(λc)=λv(c)v(λ c)=λ v(c)), relaxation dominance, removal monotonicity, and the dual subgradient inequality vLP(b′)≥vLP(b)+y⊤(b′−b)v_LP(b )≥ v_LP(b)+y (b -b) for minimization, valid for any optimal dual y even under degeneracy because optimal duals are subgradients of the convex function vLP(⋅)v_LP(·). Consequently Layer B has no power against faithful-looking formulation errors, whose corrupted models satisfy the same theorems (Proposition 5.3 formalizes the general phenomenon), but it convicts broken solver interfacing, such as mis-extracted objective values, inconsistent reported solutions, sign-flipped duals, and silent presolve failures. In our pipeline Layer B plays the role that execution-based checking plays in Lian et al. (2026), with inequalities replacing statuses. Theorem 4.7 (Battery soundness) In exact arithmetic: (i) every Layer-A test with a certified precondition passes on every structure-faithful candidate (annotated mode); (i) tests A0–A3, A5–A7 pass on every role-faithful candidate whose preconditions are certified on its own structure (deployment mode); (i) Layer-B tests pass on every MILP. Hence the battery’s false-positive rate against the corresponding class is zero, and every violation constitutes a machine-checkable certificate of unfaithfulness carrying the offending slot, probe, and property. 5 Detection Limits Soundness constrains what a battery may flag; this section characterizes what it can flag. Fix the probe orbit Θℬ=τ(θ0):τ∈ℬ _B=\τ(θ^0):τ _B\, the set of instances the battery may visit, and call two candidates battery-indistinguishable if they produce identical statuses and values on Θℬ _B (and identical reported duals/incumbents where Layer B reads them). Since every predicate is a function of these observations, indistinguishable candidates receive identical verdicts. Three invisibility results follow. 5.1 What no such verifier can see Proposition 5.1 (Gauge invisibility) Let Π^′ be obtained from a faithful Π by multiplying the entire objective (including any constant) by λ>0λ>0. Then Π^′ passes every oracle-free test whose predicate is invariant under positive rescaling of all observed values, a class that contains every test in this paper and every sign, ordering, ratio, or homogeneity predicate. Moreover the transformation is decision-irrelevant: Π^′ has the same optimal-solution correspondence as Π at every θ. The one Layer-A test that pins absolute scale, A6, requires the value 0, which is a fixed point of the gauge; a nonzero spurious constant is detected by A6 where certified. Gauge invisibility is thus benign, since what the verifier cannot see cannot change any decision. Proposition 5.2 (Orbit redundancy) Let Π^′ add to a faithful Π any constraints that are inactive at every θ∈Θℬθ∈ _B (e.g., dominated rows with slack bounded away from zero on the orbit). Then Π^′ is battery-indistinguishable from Π . Consequently, detection of superfluous-yet-inactive structure is possible only by enlarging the orbit, and any fixed battery’s guarantee is intrinsically relative to its orbit. This is the honest limit of behavioral verification, which certifies behavior only where it looks. The practical mitigation is orbit design. Our probes already visit the extremes used by the crush and prohibitive-limit tests, where mildly redundant rows typically activate, and rows engineered to remain dominated even there are semantically harmless on the entire probed region. Proposition 5.3 (Reparametrization invisibility and the reach of exchange) Let Π^′ misuse a single slot j linearly, so that every occurrence of θj _j is replaced by λθjλ _j for a fixed λ>0λ>0 with λ≠1λ≠ 1, the canonical unit error. Then: (i) in deployment mode (candidate-side certification), Π^′ passes every single-slot probe of the battery, covering direction, curvature, prohibitive limits, annihilation, and crush, where the requirement-side crush case requires λ≥1λ≥ 1 and the capacity crush probe value 0 is a fixed point. The reason is that each such predicate is invariant under an increasing linear reparametrization of the probed axis and every certificate is evaluated on the reparametrized model itself; (i) Π^′ is detected by an exchange test A7 whenever slot j belongs to a certified-congruent bundle and the swapped instance separates the values, which holds for generic data; (i) if the misuse applies uniformly to all objective slots (λcλ c), it is the gauge of Proposition 5.1 and is invisible to the entire battery. Remark 5.4 (Certificates buy power in annotated mode) In annotated mode the preconditions of the limit and crush tests are certified on the declared structure at θ0θ^0. A misused candidate behaves like the faithful family at the point whose jjth coordinate is rescaled by λ, where a certificate valid at θ0θ^0, say feasibility of xe=0x_e=0, may fail; the test then fires on a genuine unfaithfulness that deployment-mode certification would skip. Declared assertions thus strictly enlarge the detectable set. Section 7.2 quantifies the effect, where certificate transfer convicts an additional 0.8% of single-slot misuse mutants through the prohibitive-limit test. Proposition 5.3 yields the sharpest falsifiable prediction of the theory. Single-coefficient scale errors must be caught only by A7; uniform objective scaling and orbit-redundant additions, never. The experiments reproduce exactly this pattern (Table 7.1). Proposition 5.5 (Min/max asymmetry of annihilation) On the cost side of a minimization problem, the prohibitive limit of Proposition 4.4(i) is an equality. Its mirror on the reward side of a maximization problem, which sets entity e’s rewards to zero, satisfies only the one-sided bound v(rewardse→0)≥ve0v(rewards_e→0)\ ≥\ v_e0, which holds for arbitrary candidates and hence carries no detection power; equality can fail for faithful candidates because a zero-reward activity may still be used to satisfy joint requirements; the E-Companion gives an example. Rate-side limits, by Proposition 4.4(i), restore symmetric power for maximization problems. 5.2 What the battery provably catches We now fix the canonical error classes used throughout the empirical literature and our mutation study (cf. the taxonomy of Li et al. 2026); Π^′ denotes a faithful candidate corrupted by one operator. Theorem 5.6 (Class-by-error detectability) Let the assertion structure certify the stated precondition. Then the corrupted candidate is flagged with certainty (in exact arithmetic) as follows. (i) Sense flip (min↔max ): by A0; and by any A2 objective probe at which the faithful response is strict, and by A6 when certified with v>0v>0. (i) Constraint omission: by A4 whenever the omitted row’s crush certificate holds, because the corrupted model’s value is constant in the crushed slot and the model therefore remains feasible where infeasibility is certified. (i) Direction flip of a slotted row: by A1 at any probe where the row binds strictly on one side (the response reverses orientation); by A4 when the row carries a crush certificate (≤ made ≥ is feasible at zero capacity); by A6 when certified. (iv) RHS misassignment between two slotted rows: by A1 whenever the two slots’ asserted directions differ; by A4 whenever exactly one of them carries a crush certificate that the swap breaks. (v) Dropped objective term of entity e: by A5(i) whenever xe=0x_e=0 is certified feasible and using e is strictly profitable in the corrupted model at the prohibitive probe, i.e. vlim′<ve0′v _ <v _e0. (vi) Entity misbinding (rates of e1,e2e_1,e_2 swapped in one row): by A5(i) whenever the certified prohibitive-rate probe of e1e_1 leaves xe1x_e_1 strictly active in the corrupted model; by A7 under congruence with generic data. (vii) Broken data binding (a slot’s value hard-coded): by A4/A6 for rhs slots (the crushed model retains its hard-coded value, contradicting the certificate) and by A5(i) for rate slots; A1 and A2 are silent because weak monotonicity tolerates constancy, and presence detection is exactly the case where limits rather than directions are informative. The proofs in E-Companion 9 are short case analyses on top of Propositions 4.1–4.6; their value is the map they induce from error classes to test classes, which turns the battery’s verdict into a diagnosis, the mutation study into a controlled test of the theory, and each cell of Table 7.1 into a prediction. 5.3 Thresholds cannot be sound Proposition 5.7 (No sound nontrivial threshold tester) Fix any relative threshold τ>0τ>0 and consider the presence tester that flags a candidate when an extreme perturbation of a capacity slot changes the optimal value by a factor less than τ (the CPT rule of Lian et al. 2026). For every τ>0τ>0 there is a family of faithful two-variable candidates on which the tester’s false-positive rate is one (a capacity that remains slack under the extreme probe because a sibling bound is tighter); for τ=0τ=0 the tester never flags anything. Hence no threshold choice yields a sound and nontrivial presence tester, whereas the certified crush test A4 flags none of these faithful candidates and retains full power on the corresponding omissions by Theorem 5.6(i). The construction, given in the E-Companion, is not adversarial trickery but the ordinary situation in which one resource is abundant. Empirically, the reimplemented threshold tester flags 54.9% of faithful NL4OPT models for exactly this reason (Section 7). Lian et al. (2026) recognize the ambiguity of intermediate responses and route the band between their two thresholds to a non-blocking informational zone, but responses below the lower threshold still trigger repair. The theoretical point is that the ambiguity is not a tuning problem but an information problem, resolved only by certification. 5.4 Cost of verification Proposition 5.8 (Probe complexity) For a candidate with p slots, E entities, C certified congruent pairs, and R rows, the battery issues O(p+E+C+R)O(p+E+C+R) solver calls: 55 per rhs slot (22 for A1 and 33 for A3, whose probe points and relaxation modes differ), 11 per coefficient slot (A2), 11–22 per certified crush row (A4), 33 per entity and side (A5, two scales plus the fixed problem), 11 for A6, 22 per congruent pair (A7), and O(R)O(R) for Layer B. Because the implementation tests congruence for every entity pair, C≤(E2)C≤ E2 and the worst case is O(p+E2+R)O(p+E^2+R); on the benchmark corpora congruent pairs are rare and the observed cost sits in the linear regime. Each call is an LP/MILP of the candidate’s own size. On the benchmark corpus this is 25 solves and 0.01 seconds per model on one CPU core (Section 7), three orders of magnitude below the cost of generating the candidate with a 7B LLM on an A100 GPU. 6 A Verifiable Modeling Interface Behavioral testing of code silently presupposes a solved problem, because perturbing the capacity requires knowing which number in the program is the capacity. ReLoop extracts this map with an LLM at test time; we instead make data binding a first-class, checkable artifact of generation. Pass 1 (extraction). An LLM reads the description and emits the typed slot table (sk,θk0,qtypek,ek)\(s_k,θ^0_k, qtype_k,e_k)\ and the sense σ∗σ . This is assertion extraction, not modeling. The table is validated against the text (every slot value must appear; percentages are normalized) and is the sole carrier of semantic authority thereafter. Pass 2 (generation). The generator emits the model in a JSON intermediate representation whose coefficient and right-hand-side fields may reference quantities only as slot identifiers; numeric literals are reserved for structural constants (0,±10,± 1, ratio complements). Ratio slots are therefore encoded structurally rather than referenced by id; they are excluded from slot-coverage accounting and are untested by slot probes in deployment mode. The IR compiles deterministically to the solver; slot references resolve to the extractor’s values, so the binding is correct by construction, and models whose IR references unknown slots, omits declared quantities, or fails schema checks are rejected before any solve. The battery then runs in deployment mode (Theorem 4.7(i)): directional, curvature, limit, annihilation, and exchange tests with candidate-side certification; crush tests, whose certificates require a declared structure, are reserved for annotated corpora (the implementation skips A4 in deployment mode, where certificate and test would coincide in a single solve). Beyond enabling verification, the interface removes a documented failure source, indexing and data-access errors in free-form solver code (Lian et al., 2026), and makes candidate models diffable and auditable artifacts. The two-pass design also isolates responsibility. Extraction errors corrupt assertions, which are short structured outputs and hence votable; generation errors corrupt structure, which is what the battery tests. 7 Computational Study The experiments first test the theory’s predictions, then compare the battery against the natural alternatives, and finally measure end-to-end value in a realistic local-model pipeline. Generation and the LLM baselines run on one A100 GPU, and all solves run on CPU cores with HiGHS as the solver; code, seeds, and per-run JSON artifacts accompany the paper. Every number in this section is reproducible from a named artifact file, and the CPU stages, from the battery and the mutation study to the audits and post-processing, reproduce identically end to end on a second, independent machine. 7.1 Corpora and instrumentation Annotated corpus. The NL4OPT generation-track annotations provide, for each word problem, a declared ground-truth formulation with typed declarations. Our parser compiles 351 of 388 dev+test problems (90.5% coverage; failures are tabulated in the E-Companion) into the IR with slots and assertions derived mechanically from the declarations. Of these, 326 solve to a finite optimum; they form the faithful seeds. Whether the battery flags any of them is the clean false-positive measurement reported below, taken before any battery-based filtering. Synthetic families. Controlled production-planning (max) and covering (min) generators with fully certified preconditions isolate power from precondition coverage and support size scaling to 4040 variables and 2525 resource rows, integer and continuous. Benchmarks with a local generator. Questions are answered by the two-pass pipeline of Section 6 with Qwen2.5-7B-Instruct served locally with N=8N=8 candidates per problem, one greedy and seven sampled at temperature 0.80.8. The evaluated pools are NL4OPT test (239 of 289 problems, those with labels and parseable extractions), MAMO EasyLP (297 of 652), MAMO ComplexLP (128 of 211), and IndustryOR (88 of 100). For the MAMO and IndustryOR pools, generation covered a prefix subset of the official files, fixed by compute budget before any evaluation and never revisited; one pathological MILP instance is excluded by a solver time-limit rule declared in the replication scripts. Pipeline yields (problems with at least one valid candidate, candidate validity, and battery pass counts) are tabulated in E-Companion Table 10, and all selection results below score all problems in these pools, counting a problem with no valid candidate as a miss for every policy. Baselines. Threshold behavioral testing is our reimplementation of ReLoop’s CPT and OPT rules, with ×0.001× 0.001 and ×100× 100 extremes and τℓ=5% _ =5\%, applied to the same IR and slot table; the port is strictly charitable, since it inherits our exact binding instead of relying on code edits extracted by a language model. LLM-as-judge asks Qwen2.5-7B-Instruct and DeepSeek-R1-Distill-Qwen-7B to verdict each candidate, rendered as question plus canonical LP, as CORRECT or INCORRECT. Execution consensus is majority voting over candidate optimal values, the standard selection heuristic. Detectability matrix on NL4OPT faithful seeds: detection rates, ReLoop-style threshold tester, execution-blind shares, and per-class attribution of battery convictions. Predictions from Theorem 5.6 and Propositions 5.1–5.3. M7–M9 are invisibility controls: M8 (gauge) and M9 (orbit-redundant) are invisible to the entire battery; M7 (single-slot misuse) is invisible to every single-slot probe and detectable only through the exchange class A7, plus an 0.8% certificate-transfer residue via A5 (Remark 5.4). Op Error class n Battery Thresh. Blind Convicting classes M1 direction flip 849 73.5% 63.6% 5% A1:50%, A4:32%, A5:26% M2 omission 846 42.9% 86.8% 42% A4:33%, A5:12%, A7:2% M3 rhs swap 693 41.4% 62.9% 12% A4:34%, A6:23%, A1:16% M4 dropped obj. term 647 44.2% 89.8% 15% A7:31%, A5:13% M5 sense flip 326 100.0% 56.4% 1% A0:100%, A6:55%, A1:44% M6 entity misbinding 720 27.1% 78.5% 33% A5:26%, A7:2% M10 hard-coded rhs 709 60.8% 91.3% 34% A6:34%, A4:33%, A7:4% M11 hard-coded coef. 755 38.8% 94.8% 36% A7:32%, A5:14% M7 slot scale ×10× 10 750 38.8% 78.4% 30% A7:39%, A5:1% M8 objective ×2× 2 326 0.0% 54.9% 5% — M9 redundant row 326 0.0% 54.9% 100% — Threshold tester false-positive rate on the same faithful seeds: 54.9% (battery: 0.0%). Best-of-8 selection accuracy (execution accuracy of the selected candidate) of the Qwen2.5-7B two-pass pipeline under seven selection policies, with the oracle-any ceiling. For each benchmark, the first row scores all problems that entered the pipeline (a problem with no valid candidate counts as a miss for every policy, including the oracle); the second row conditions on ≥ 1 valid candidate. Benchmark n Greedy Random Majority Thresh. Battery Weighted Cascade Oracle NL4OPT 239 34.3 34.7 39.7 34.7 36.0 38.5 34.3 50.6 ≥ 1 valid 237 34.6 35.0 40.1 35.0 36.3 38.8 34.6 51.1 MAMO EasyLP 297 22.2 24.6 5.1 35.7 8.4 5.1 35.7 53.2 ≥ 1 valid 293 22.5 24.9 5.1 36.2 8.5 5.1 36.2 53.9 MAMO ComplexLP 128 10.9 13.3 4.7 19.5 6.2 4.7 19.5 25.0 ≥ 1 valid 82 17.1 20.7 7.3 30.5 9.8 7.3 30.5 39.0 IndustryOR 88 31.8 34.1 14.8 47.7 22.7 14.8 47.7 54.5 ≥ 1 valid 70 40.0 42.9 18.6 60.0 28.6 18.6 60.0 68.6 Accuracies in percent; labels are used only for scoring, never by any policy. Random selects uniformly among valid candidates; battery/threshold filters fall back to plain majority when no candidate survives the filter. The detectability matrix, visualized: per-class conviction shares for each mutation operator (left) and overall detection (right); dashed rows are the invisibility controls of Propositions 5.1–5.3 (M7: exchange-only). Soundness in practice. Left: false-positive rates on faithful models; the battery and threshold bars are measured on the 326 faithful seeds, the two judge bars on the 60 panel cleans (denominators differ; see Section 7.3). Right: detection, false-positive rate, and Youden J on the stratified panel. Execution-blind mutants (value-coincident at the nominal instance) and battery detection among them. Best-of-8 selection accuracy by policy and benchmark (Qwen2.5-7B two-pass pipeline; all-problems denominator of Table 7.1). Left: battery detection versus solver-call budget on the certified synthetic family, separately for the eight detectable/conditional operators and for all operators including the invisibility controls; dotted lines mark the full-battery rates, the marker the 95%-of-full-power budget. Right: battery cost versus model size. 7.2 E1: the detectability matrix For each faithful seed and each of eleven mutation operators (Table 7.1), up to three distinct single-error mutants are generated, 6947 in all, and passed to the battery in annotated mode. The operators map onto Theorem 5.6 and Propositions 5.1–5.3: five detectable classes (M1 direction flip, M2 omission, M3 rhs swap, M4 dropped objective term, M5 sense flip), two binding breaks (M10 hard-coded rhs, M11 hard-coded coefficient), one conditional class (M6 entity misbinding), and three theory-invisible controls (M7 single-slot scale misuse, exchange-only by Proposition 5.3; M8 uniform objective scaling; M9 orbit-redundant row). Throughout the empirical sections we fix three mutant populations. The core population comprises classes M1–M5 (n=3361n=3361); the conditional population comprises the mutants of M2, M4, M6, M10, and M11 whose stated preconditions certify on the specific mutant (n=1515n=1515, against n=2162n=2162 uncertified); the blind-analysis population comprises all eight detectable classes M1–M6, M10, and M11 (n=5545n=5545) and supports the execution-blindness statistics. Percentages refer to the named population. Three findings stand out (Table 7.1, Figure 7.1). First, soundness holds in practice. The battery flags 0.0% of the 326 faithful seeds, while the threshold tester flags 54.9% of the same models. Second, the detectability matrix matches the theory. M8 and M9 sit at exactly 0%0\% across all test classes; M7 is detected in 38.8% of mutants, all but a 0.8% residue through the exchange class A7 as Proposition 5.3 requires, the residue itself explained and predicted by the certificate-transfer mechanism of Remark 5.4; M5 is caught at 100%100\%. Certification governs the conditional classes asymmetrically. Certified omissions (M2) are caught at 100.0% (n=270n=270), matching the certainty clause of Theorem 5.6(i), and uncertified entity misbinding (M6) at exactly 0.0%, matching the necessity of its precondition; between these poles, certified detection is 87.4% for M10, 62.4% for M11, 60.5% for M4, and 48.4% for M6, short of certainty because Theorem 5.6 attaches additional strictness and genericity conditions to these classes that the certificates do not check. Pooled, certification raises detection from 23.5% to 70.0%. Third, execution accuracy is blind where the battery is not (Figure 7.1). 23.8% of the blind-analysis population, 1321 mutants, reproduce the correct optimal value at the nominal instance, so label comparison cannot separate them from correct models even with perfect ground truth, yet the battery convicts 40.4% of them. This population is the sharpest evidence that verification and evaluation are different problems. 7.3 E2: baselines on equal footing The panel comprises 132 mutants stratified over all eleven operators (twelve per operator, including the invisibility controls) and 60 faithful models drawn from the battery-passing seeds. Because the panel cleans are battery-passing seeds, their measured flag rate inherits E1’s clean false-positive result rather than estimating an independent one; Figure 7.1 therefore labels each bar with its own denominator. On the full panel the battery attains recall 47.7% at 0.0% false positives. The threshold tester and the Qwen judge flag more mutants (recall 78.8% and 87.1%) at false-positive rates that disqualify them as auditors (56.7% and 53.3%); the R1-distill judge is conservative (recall 43.2% at 1.7% false positives) but offers neither certificates nor slot-level localization. Because the panel is mutant-heavy, prevalence-dependent scores such as F1F_1 reward indiscriminate flagging (Qwen judge 0.82, threshold 0.77, battery 0.65, R1 judge 0.60); by the prevalence-free Youden index J=recall−FPRJ=recall-FPR the battery ranks first (0.48 versus 0.22, 0.34, 0.42). One design choice merits care. The panel labels every mutant as faulty, yet M8 is provably decision-irrelevant (Proposition 5.1) and M9 is orbit-invisible, so treating them as faults penalizes a sound verifier for correctly staying silent. Excluding the twenty-four M8/M9 control mutants (n=108n=108) raises the battery to recall 58.3% (J=0.58J=0.58) and the threshold tester to 81.5% (J=0.25J=0.25); the two LLM judges are shown on the full panel, their per-item verdicts accompanying the replication package. One difference frames the whole comparison. Only the battery’s flags carry certificates. A battery flag proves unfaithfulness relative to the assertions and names the offending slot and property, while judge flags are opinions and threshold flags are heuristics, and the distinction is operationally decisive when flags trigger costly repair or human escalation (Huang et al., 2024a). 7.4 E3: power, budget, and scale The synthetic family separates power from precondition coverage. None of the 20 solvable synthetic models is flagged, a measurement again taken before any filtering. On the eight detectable operators the full battery convicts 78.0% of mutants (n=313n=313); under a solver-call budget, detection reaches 95%95\% of that full-battery power by 88 solves and gains little thereafter, against a full-battery cost of roughly 105105 solves at this size (Figure 7.1, which also shows the all-operator curve including the invisibility controls). Battery cost grows near-linearly in model size with millisecond-scale LPs up to the largest sizes tested. The two-scale limit criterion is validated across four decades of M with one fixed misbinding mutant per seed reused at every scale pair. All 24 faithful models pass at every pairing, and the same 71.4% of the 21 mutants is flagged at every pairing, so the criterion’s verdict is scale-stable on this family (E-Companion Table 10); its scale limits are mapped by Remark 4.5 and E-Companion Table 10. 7.5 E4: verification as selection and as audit For each benchmark family, the deployment-mode battery scores the N=8N=8 candidates. We evaluate hard filtering, a majority vote among battery survivors; a weighted vote, with each candidate’s vote damped by 2−#violations2^-\#violations; the aggressive threshold prefilter; and a cascade that applies the threshold prefilter and then the violation-weighted vote. The comparators are greedy selection, uniform-random selection among valid candidates, and plain majority voting, with the oracle-any hit rate as headroom; filters fall back to plain majority when no candidate survives (Table 7.1, Figure 7.1). We report outcomes on the all-problems denominator, on which a problem with no valid candidate scores zero for every policy including the oracle; Table 7.1 also lists values conditioned on at least one valid candidate, and E-Companion Table 10 the pipeline yields. The results are instructive on both sides. Where consensus is reliable, on NL4OPT, sound verification does not pay as a raw selector; the weighted vote tracks plain majority within about one point and hard filtering costs about four points. The divergence quantified next explains why. On NL4OPT, 27.6% of label-matching candidates, 155 of 562 value-correct programs, carry a battery certificate of role violation relative to the extracted assertions. Curvature breaches certify that a declared limit was wired into coefficients, directional breaches certify inverted roles, and exchange breaches certify misbound entities. A selector that demotes such candidates loses measured accuracy exactly where the metric rewards wrong structure; pooled over the four families the share is 15.7%, 175 of 1113. Because deployment-mode certificates are relative to extracted assertions, extraction errors can contribute to these counts; the per-candidate certificates ship with the artifacts for audit. On the other three pools consensus itself collapses, with plain majority scoring below uniform random on MAMO EasyLP, MAMO ComplexLP, and IndustryOR because repeated degenerate formulations vote for the same wrong value, and there the ordering reverses. Hard battery filtering gains +8.0 points over majority on IndustryOR, and the aggressive presence prefilter, whose 54.9% false-positive rate disqualifies it as an auditor, is the strongest pure selector; the cascade matches the prefilter’s selection accuracy on the three collapsed pools (+33.0 points over majority on IndustryOR; paired McNemar tests in E-Companion Table 10) while attaching certificates to every flag it reports. Soundness and selection utility are different objectives. The first concerns what a flag proves, the second concerns ranking under a metric that cannot see structure, and both sides of the reversal follow from that distinction. Because the battery never consults labels, the same machinery doubles as an audit. Candidates that pass the full battery yet disagree with the published label localize suspicious labels, and cross-checking the NL4OPT annotations’ own optima against the labels isolates outright inconsistencies between the two official artifacts. Eighteen of 207 matched test problems fail a mechanical both-solve criterion, the annotation’s LP and all-integer optima both differing from the published label; the cases are catalogued with notes in E-Companion Tables 10 and 10, consistent with the label-noise reports of Chen et al. (2025b). 7.6 Scope and limitations Our theory is exact for the MILP families the benchmarks occupy and for the assertion vocabulary of Section 3; nonlinearities beyond positive homogeneity, uncertainty sets, and multi-objective structures need their own necessary-condition catalogs, which the framework accepts as new test classes. Deployment-mode guarantees are relative to extracted assertions; extraction is short, structured, and votable, but not infallible. The blind set of Section 5 is not empty, and provably cannot be; Proposition 5.2 makes all guarantees orbit-relative, and Remark 4.5 makes the implemented limit tests probe-scale-relative. The computational evidence has its own limits. It rests on a single 7B generator, a prefix subset of three of the four benchmark pools (E-Companion Table 10), LLM-judge baselines evaluated on the full panel only, and no ablation of the two-pass interface against free-form generation; the replication package includes scripts that extend generation to the complete benchmarks and to alternative generators, and all selection results are reported on the all-problems denominator so that later runs remain comparable. Finally, we evaluate detection, not repair; coupling certificates to repair policies is a natural sequel. 8 Conclusion Fifty years of sensitivity analysis were built to answer how an optimal plan changes when the data change, for models assumed correct. This paper reuses that theory, unchanged, to decide whether a model is right at all, for generators assumed fallible. The reuse yields sound tests with zero false alarms by construction, limits that are provable rather than anecdotal, and a detectability map that the experiments reproduce, including its zeros. The practical payoff is a verifier free of data-dependent tuning that outperforms heuristic perturbation and LLM judges as an auditor and exposes benchmark label defects as a by-product. The conceptual payoff is the one we would emphasize. Verification of AI-generated optimization models is an optimization problem, and the discipline already owns the tools to solve its tractable core. The authors thank the maintainers of the NL4OPT, MAMO, and IndustryOR benchmarks and of the HiGHS solver. All experiments used publicly available data and locally hosted open-weight models. E-Companion: Proofs, Constructions, and Additional Results 9 Proofs Throughout, Π is the candidate (1), v its value function with the infinity conventions of Section 3, and the words improves and worsens are read in the asserted sense σ∗σ , so that for minimization smaller is better and +∞+∞ is worst, with the mirrored reading for maximization. We use repeatedly that if ′⊆X then optimizing over ′X is weakly worse, for any objective, including over integer-restricted sets. 9.1 Proof of Proposition 4.1 (i) Let slot j be a capacity, entering (role-faithfulness) only as the RHS of one row a⊤x≤θja x≤ _j. For θj′≥θj _j ≥ _j the constraint set satisfies (θ)⊆(θ′)X(θ) (θ ) pointwise in all other coordinates, since a⊤x≤θj≤θj′a x≤ _j≤ _j ; hence v(θ′)≤v(θ)v(θ )≤ v(θ) for min (and ≥ for max ): v weakly improves. A requirement slot enters as a⊤x≥θja x≥ _j; raising θj _j shrinks X, so v weakly worsens. Infeasibility and unboundedness are covered by the conventions since inclusion of feasible sets preserves the extended-real ordering of optimal values. (i) Let slot j be a cost of entity e in a min problem, entering only as the objective coefficient of xe≥0x_e≥ 0: f(x;θ)=g(x)+θjxef(x;θ)=g(x)+ _jx_e. For each fixed feasible x, f(x;⋅)f(x;·) is nondecreasing in θj _j because xe≥0x_e≥ 0; the pointwise infimum of nondecreasing functions is nondecreasing, so v weakly worsens. reward in a max problem is the mirror statement with suprema. (i) Let slot j be a rate in row r of sense ≤: θjxe+(rest)r≤br _jx_e+(rest)_r≤ b_r. If θj′≥θj _j ≥ _j, any x≥0x≥ 0 feasible at θ′θ satisfies θjxe≤θj′xe≤br−(rest)r _jx_e≤ _j x_e≤ b_r-(rest)_r, hence is feasible at θ: (θ′)⊆(θ)X(θ ) (θ) and v weakly worsens. Sense ≥ is the mirror inclusion. (iv) A ratio slot ρ∈[0,1]ρ∈[0,1] of entity e in a ≥-share row reads, canonically, (1−ρ)xe−ρ∑w≠exw≥0(1-ρ)x_e-ρ _w≠ ex_w≥ 0, i.e. xe≥ρ 1⊤x_e≥ρ\,1 x. For ρ′≥ρ ≥ρ and x≥0x≥ 0, xe≥ρ′⊤x⇒xe≥ρ 1⊤x_e≥ρ 1 x\ \ x_e≥ρ\,1 x because ⊤x≥01 x≥ 0; the feasible set shrinks and v weakly worsens. Sense ≤ mirrors. Integrality never enters any argument above. 9.2 Proof of Proposition 4.2 Write the LP relaxation in the form vLP(b)=minc⊤x:Ax≤b,Bx=d,x≥0v_LP(b)= \c x:Ax≤ b,\ Bx=d,\ x≥ 0\ (rows of sense ≥ are negated into ≤; the probed slot moves one coordinate of b along a segment). LP duality gives, on the domain where the primal is feasible and bounded, vLP(b)=maxb⊤y+d⊤z:A⊤y+B⊤z≤c,y≤0v_LP(b)= \\,b y+d z:\ A y+B z≤ c,\ y≤ 0\,\, a pointwise supremum of affine functions of b; hence vLPv_LP is convex on its effective domain, and along any segment b(θj)b( _j) affine in θj _j the univariate restriction is convex, which is the midpoint predicate. If σ∗=maxσ = , the same argument on −v-v yields concavity. (The implemented test only fires when all three probed values are finite, staying inside the effective domain.) 9.3 Proof of Proposition 4.3 By structure-faithfulness, Π^(θ)=S∗(θ)X_ (θ)=X_S (θ) for all probe instances. The certificate is the solver’s proof that S∗(θ−j0,0)=∅X_S (θ^0_-j,0)= (capacity crush; requirement crush with value R analogous). Then Π^(θ−j0,0)=∅X_ (θ^0_-j,0)= : the candidate must report infeasible. The test never fires without the certificate, so on certified instances it cannot flag a structure-faithful candidate. 9.4 Proof of Proposition 4.6 Under the certified congruence, define the swap τ that exchanges the two entities’ slot-value bundles and the relabeling π that exchanges their variables. Congruence states that applying τ and π together maps the candidate’s data (c,c0,A,b)(c,c_0,A,b) at θ0θ^0 to itself: paired objective slots exchange coefficients of exchanged variables, paired rate slots exchange row entries of exchanged variables within each row, paired bound rows exchange as whole rows, and all unslotted entries touching the two entities agree by assumption. Hence the program at the swapped instance equals the original program up to the variable relabeling π. A relabeling is a bijection between the two feasible sets that preserves objective values and integrality, so the optimal values coincide, which is the predicate of test A7. 9.5 Proof of Proposition 4.4 We give the argument for (i), σ∗=minσ = ; (i) is analogous with the constraint squeezing xex_e in place of the objective penalty. Sandwich. Fix M≥0M≥ 0 and let v(M)v(M) denote the value at the probe θj↦M _j M for j∈Jej∈ J_e. Any x feasible with xe=0x_e=0 has probe objective equal to its original objective (role-faithfulness: the probed slots multiply only xex_e’s coordinates), so v(M)≤ve0v(M)≤ v_e0. Conversely the probe only increases objective coefficients of nonnegative variables (for M≥θj0M≥θ^0_j), so v(M)≥v(θ0)v(M)≥ v(θ^0) by Proposition 4.1(i): the claimed two-sided sandwich. Limit and finite threshold. Because xe=0x_e=0 is feasible, v(M)≤ve0<+∞v(M)≤ v_e0<+∞ for all M. Consider first the LP relaxation case (e continuous). The probe objective is c−e⊤x−e+Me⊤xec_-e x_-e+M\,c_e x_e with e>0c_e>0 on e’s coordinates (values θj _j replaced by the common scale M; taking all j∈Jej∈ J_e to a common M is what the implementation does). Parametric LP with a scalar parameter multiplying a fixed objective block admits finitely many optimal bases: there exist breakpoints 0=M0<M1<⋯<MK<∞0=M_0<M_1<…<M_K<∞ such that on (MK,∞)(M_K,∞) some fixed basis B∗B is optimal. If the corresponding optimal solution had xe≠0x_e≠ 0, its objective would grow without bound in M while v(M)≤ve0v(M)≤ v_e0 stays bounded, a contradiction. Hence for M>MK=:M¯M>M_K=: M an optimal solution has xe=0x_e=0, and its objective is then independent of M and equal to the best xe=0x_e=0 objective, i.e. v(M)=ve0v(M)=v_e0 exactly. For integer xex_e (case (i) with a ≤-row of nonnegative data), feasibility forces xe≤br/Mx_e≤ b_r/M once θj=M _j=M; M>brM>b_r forces xe<1x_e<1, hence xe=0x_e=0, and the probed program then coincides with the xe=0x_e=0 program, which gives the explicit threshold in the statement. For mixed problems: the sandwich keeps v(M)v(M) within [v(θ0),ve0][v(θ^0),v_e0]; on the branch xe≥1x_e≥ 1, every feasible point’s objective is at least M times a positive quantity plus a finite branch infimum (a negative-objective recession direction of the branch with xex_e fixed would be a recession direction of the nominal problem as well, contradicting finiteness of v(θ0)v(θ^0)), so beyond a finite threshold every optimum lies in the xe=0x_e=0 branch, where the parametric-LP argument applies for each of the finitely many relevant integer assignments; each is eventually constant, so the minimum is, with M¯ M the largest relevant breakpoint. Rate side for either sense. With slot j a positive rate of e in a ≤-row of nonnegative data, any feasible x satisfies xe≤br/M→0x_e≤ b_r/M→ 0; feasibility at xe=0x_e=0 is preserved, and by continuity of the (relaxed) value in the box constraint xe≤br/Mx_e≤ b_r/M together with the same finite-basis argument, v(M)=ve0v(M)=v_e0 beyond a finite threshold; the maximization case uses the identical squeeze (no objective sign enters). 9.6 Soundness of A6 and proof of Theorem 4.7 For A6, the certified preconditions are: σ∗=minσ = ; objective a nonnegative combination of x≥0x≥ 0 with zero constant; after zeroing all requirement slots, every ≥-row of the declared structure has RHS ≤0≤ 0, every ≤-row RHS ≥0≥ 0, every equality RHS =0=0, and all lower bounds are 0. Then x=0x=0 is feasible for any structure-faithful candidate at the probe and its objective is 0; nonnegativity of the objective gives v=0v=0 exactly. Theorem 4.7: (i) each Layer-A test was proved sound for structure-faithful (A4, A6, A7 with declared-side certificates) or already for role-faithful (A0–A3, A5) candidates; structure-faithfulness plus the declared origin of assertions implies role-faithfulness for the slotted positions, so all tests pass. (i) In deployment mode the certificates (entity-zero feasibility for A5; congruence for A7; the structural preconditions of A6) are computed on the candidate’s own structure; for a role-faithful candidate these coincide with the true properties, and each test’s proof applies verbatim. (i) Layer-B statements are classical theorems for arbitrary MILPs: positive homogeneity of optimal values; relaxation dominance; removal monotonicity (set inclusion); and the subgradient inequality, valid for every optimal dual y of the relaxation because vLPv_LP is convex and y supports it at b. Degeneracy affects uniqueness of y, not the support property. The one-sided implemented tolerances only widen the pass region. 9.7 Proof of Proposition 5.1 Observed statuses are invariant: scaling the objective by λ>0λ>0 changes neither feasibility nor boundedness. Every observed finite value scales by λ, and ±∞±∞ are fixed. Each predicate class is invariant: orderings and one-sided comparisons (u≤w+ε(u,w)u≤ w+ (u,w) with homogeneous tolerance), midpoint inequalities, equalities between observed values (A5, A7), the value 0 (A6), statuses (A4), homogeneity (B1, v(3λc)=3v(λc)v(3λ c)=3v(λ c)), dominance and removal comparisons, and the subgradient inequality (duals scale with the objective). Decision irrelevance: argmin sets of f and λfλ f coincide on any set. 9.8 Proof of Proposition 5.2 By assumption the added rows are inactive at every probe instance: removing them does not change the feasible set at any θ∈Θℬθ∈ _B, hence statuses, optimal values, optimal solutions, and (choosing the duals that assign them zero multipliers, as any vertex-optimal basis of the augmented system may) the observed duals coincide with the faithful model’s. All predicates are functions of these observations. 9.9 Proof of Proposition 5.3 Write the misused model as Π^′(θ)=Π^(λ∗jθ) (θ)= (λ _jθ) where λ∗jλ _j multiplies coordinate j by λ and Π is faithful. (i) Every single-slot test on slot j observes v′(θj=t)=v(λt)v ( _j=t)=v(λ t) along the j-axis (other slots at nominal), i.e. the faithful value function precomposed with an increasing linear map of the probed coordinate. Directional predicates compare t1<t2t_1<t_2: λt1<λt2λ t_1<λ t_2 preserves orientation, so the weak inequalities of Proposition 4.1 hold. The midpoint test uses equally spaced t-triples, which remain equally spaced (with spacing λδλδ) after the map, and convexity is preserved under affine precomposition. Crush maps 0↦00 0, so the certified status transfers. Prohibitive limits map M↦λM→∞M λ M→∞; both the limit value ve0v_e0 (unaffected: xe=0x_e=0 solutions do not see slot j when j∈Jej∈ J_e; when j is a rate of e, likewise) and the two-scale residual criterion (residuals r(M)=v(λM)−ve0r(M)=v(λ M)-v_e0 still vanish beyond M¯/λ M/λ and decay proportionally) are preserved. Annihilation (A6) probes requirement slots at 0, again a fixed point. Tests on slots k≠jk≠ j observe the faithful family with the jjth coordinate frozen at λθj0λθ^0_j, which is a faithful family with different nominal data, so they pass by Theorem 4.7. (i) is Proposition 5.1. (i) The exchange test swaps the bundles of the entity e1e_1 carrying slot j and its congruent partner e2e_2 carrying slot j′j . The misused model evaluates vswap,′=v(…,λθj′0 at j,θj0 at j′,…)v^swap, =v(…,λθ^0_j at j,\ θ^0_j at j ,…), whereas invariance (which the predicate asserts, and which holds for the faithful model by Proposition 4.6) requires vswap,′=v′(θ0)=v(…,λθj0,θj′0,…)v^swap, =v (θ^0)=v(…,λθ^0_j,\ θ^0_j ,…). The two right-hand sides are the faithful value at two different data points whenever λθj′0≠λθj0λθ^0_j ≠λθ^0_j i.e. θj0≠θj′0θ^0_j≠θ^0_j ; equality of the values is then a nontrivial equality of a piecewise-linear concave/convex function at two distinct arguments, which fails for data outside a finite union of lower-dimensional sets (where the two points share a linearity piece with gradient orthogonal to their difference). The word generic in the statement refers to this measure-zero exclusion, and empirically the separation occurred in every certified instance (Table 7.1). 9.10 Proof of Proposition 5.5 One-sidedness for arbitrary candidates: any x feasible with xe=0x_e=0 is unaffected by zeroing e’s rewards, so the zeroed problem’s supremum is at least ve0v_e0. For failure of equality on faithful models, the mechanism is that a zero-reward activity can still relieve a constraint on other activities. Take maxx2s.t.x2≤x1,x1≤1,x≥0 \ x_2\ s.t.\ x_2≤ x_1,\ x_1≤ 1,\ x≥ 0, with the rewards of e1=x1e_1=x_1 zeroed by the probe: the optimum is 11 at (1,1)(1,1), while ve0=0v_e0=0; the zero-reward activity x1x_1 is still used, so the would-be equality fails on a faithful model and no sound equality test exists on the reward side; the rate-side probe (ar1→Ma_r1→ M in x2≤x1≤bx_2≤ x_1≤ b-type structure) does force x1→0x_1→ 0 and retains power. 9.11 Proof of Theorem 5.6 Each case exhibits a specific test whose predicate the corrupted model violates, given the certified precondition; soundness of the test for faithful models makes the flag a correct conviction. (i) A0 compares declared senses: flip is caught syntactically. Behaviorally, let slot j be an objective slot at which the faithful response is strict at the probe pair; no certificate of this strictness is needed, because the test observes the corrupted model’s response directly. Under sense flip the corrupted value function is the faithful one with min/max / exchanged; raising a cost strictly improves the reported optimum whenever the faithful response was strict at the probe pair, violating A2’s weak inequality in the asserted sense. A6: the corrupted (max-sense) value at the annihilation probe is ≥ the largest objective of a feasible point and is strictly positive whenever any activity with positive cost coefficient is feasible at level >0>0; the predicate requires exactly 0. (i) The corrupted model contains no occurrence of the crushed slot, so its observations are constant along that slot’s axis; at the certified crush instance it reports the (finite) nominal status, while the predicate demands infeasibility. (i) At a probe pair around a strictly binding instance of the flipped row, the corrupted feasible set moves oppositely to the faithful one, producing a strict improvement where A1 requires weak worsening (or a strict worsening where A1 requires weak improvement); if the row carries a crush certificate, the flipped row (≥0≥ 0 capacity read as ≥) is satisfied by any nonnegative x at the crush instance, so the corrupted model is feasible there, violating A4; A6 similarly. (iv) If the two swapped slots’ qtypes assert opposite directions, A1 on either slot observes the other row’s response, whose orientation is reversed at any strictly responsive probe. If both are capacities but only row r has a crush certificate, the corrupted model at r’s crush instance has br=θr′0>0b_r=θ^0_r >0 (the swapped value), and remains feasible whenever the certificate was driven by row r alone; the theorem’s precondition that the swap breaks the certificate is exactly this configuration. (v) By Proposition 4.4 the predicate compares v′(M2)v (M_2) with ve0′v _e0 on the corrupted model. The corrupted model lacks e’s cost slots, so its observations are constant in them: v′(M)=v′(θ0)v (M)=v (θ^0) for all M. The certified precondition gives xe=0x_e=0 feasible; the stated strictness condition v′(θ0)<ve0′v (θ^0)<v _e0 (using e is strictly beneficial in the corrupted model when its cost is deleted, which is generic whenever e was used at all) is precisely the violation of the equality predicate. (vi) Rate misbinding sends e1e_1’s prohibitive-rate probe onto e2e_2’s column: the corrupted model at M squeezes xe2→0x_e_2→ 0 while leaving xe1x_e_1’s true consumption unpenalized, so v′(M)→ve20′≠ve10′v (M)→ v _e_20≠ v _e_10 generically, so the certified predicate compares against ve10′v _e_10 and fails; A7 detection under congruence is Proposition 5.3(i) applied to the swap misfit. (vii) A hard-coded rhs slot leaves observations constant along its axis, so the crush instance retains the nominal (feasible) status against a certified infeasibility (A4), and the A6 probe retains a strictly positive value; a hard-coded rate slot leaves xex_e unsqueezed at the prohibitive probe, reproducing case (v)’s violation. Weak directional tests are satisfied by constancy, which is the formal content of the observation that presence requires limit probes rather than directional probes. 9.12 Proof of Proposition 5.7 Consider the faithful family, indexed by s≥1s≥ 1: minx1+x2 \ x_1+x_2 s.t. x1+x2≥1x_1+x_2≥ 1 (demand), x1≤sx_1≤ s (capacity A), x1+x2≤2sx_1+x_2≤ 2s (capacity B, the audited row), x≥0x≥ 0. At the nominal instance the optimum is 11. The extreme probe multiplies bB=2sb_B=2s by 0.0010.001; for s≥500s≥ 500 the probed row still admits x1+x2≥1x_1+x_2≥ 1 (since 0.002s≥10.002s≥ 1), the optimum remains 11, the change ratio is 0<τ0<τ, and the tester flags the faithful model: false-positive rate one on this family. With τ=0τ=0 no finite observation can be flagged (any r≥0r≥ 0 passes), so the tester is trivial. The certified crush test raises no false alarm here: at bB=0b_B=0 the declared structure is infeasible, so the certificate holds and the test executes, and the faithful candidate is likewise infeasible at that probe, so A4 passes it, while a candidate that omitted row B remains feasible at bB=0b_B=0 and is convicted: soundness and power coexist exactly where the threshold rule cannot have both. 9.13 Proof of Proposition 5.8 Immediate from the per-class solve counts listed in the statement, which read off Table 4’s probe definitions and the implementation; A1 and A3 use different probe offsets and relaxation modes, so their solves do not pool. Certificates add one declared-side solve per crush row and one per entity (A5 precondition), also O(R+E)O(R+E); the all-pairs congruence scan contributes the O(E2)O(E^2) worst-case term. 9.14 Soundness bound for the two-scale criterion (Remark 4.5) Fix a faithful candidate with certified precondition and write g(M)=ve0−v(M)≥0g(M)=v_e0-v(M)≥ 0 along the probe scale (σ∗=minσ = ; the mirrored case is identical). By the proof of Proposition 4.4, v(M)v(M) is a pointwise minimum of functions affine in M, hence concave and, by Proposition 4.1(i), nondecreasing; so g is nonincreasing, convex, piecewise linear, and g(M)=0g(M)=0 for M≥M¯M≥ M. If M¯≤M2 M≤ M_2 the criterion accepts with gap 0. Otherwise g(M2)>0g(M_2)>0, and g cannot be flat on [M1,M2][M_1,M_2]: a flat piece of a convex nonincreasing function persists forever, contradicting g(M¯)=0g( M)=0. Convexity bounds the slope beyond M2M_2 by the average slope on [M1,M2][M_1,M_2]: g(M2)=g(M2)−g(M¯)≤(M¯−M2)|g′(M2+)|≤M¯−M2M2−M1(g(M1)−g(M2)).g(M_2)\;=\;g(M_2)-g( M)\;≤\;( M-M_2)\, g (M_2^+) \;≤\; M-M_2M_2-M_1\, (g(M_1)-g(M_2) ). The acceptance rule tolerates g(M2)≤4(g(M1)−g(M2))g(M_2)≤ 4\,(g(M_1)-g(M_2)), which the display guarantees whenever M¯−M2≤4(M2−M1) M-M_2≤ 4(M_2-M_1), i.e. M¯≤5M2−4M1 M≤ 5M_2-4M_1. 10 Parse coverage, benchmark audit, and additional tables Table 10 reports parser coverage on the NL4OPT annotations; Table 10 the finite-M validation and Table 10 the scale-robustness boundary of Remark 4.5; Table 10 summarizes the label audit and Table 10 lists the eighteen NL4OPT annotation-vs-label mismatches case by case with notes; Table 10 reports pipeline yields, Table 10 paired McNemar tests for the selection policies, and Table 10 Wilson confidence intervals for the headline rates. Implementation hyperparameters and pointers to the exact prompts follow in Section 11. NL4OPT annotation parser coverage. Parsed into IR 351 Unparseable annotations 37 ValueError:ratio needs var + percentage 5 ValueError:var ’premium one’ unknown 1 ValueError:var ’premium batch’ unknown 1 ValueError:var ’single-load machine’ unknown 1 ValueError:var ’electric-based stores’ unknown 1 Two-scale limit criterion across four decades of M on the certified synthetic family. One fixed M6 mutant per seed is reused at every pair, so columns are directly comparable. (M1,M2)(M_1,M_2) Faithful pass M6 detected (103,106)(10^3,10^6) 24/24 15/21 (104,107)(10^4,10^7) 24/24 15/21 (106,109)(10^6,10^9) 24/24 15/21 (107,1010)(10^7,10^10) 24/24 15/21 The flagged sets are identical across all four pairs (Figure 10): the criterion’s verdict is scale-stable on this family. Two-scale prohibitive-limit criterion across scale pairs: faithful pass rates and misbinding detection (fixed mutants across pairs). Scale-robustness boundary of the implemented two-scale criterion (Remark 4.5): faithful two-cost family minx1+Kx2 x_1+Kx_2, probe scales (M1,M2)=(106,109)(M_1,M_2)=(10^6,10^9), soundness bound M¯≤5M2−4M1 M≤ 5M_2-4M_1. K M¯=K/2 M=K/2 Predicted Observed Enlarged (1010,1013)(10^10,10^13) 106.010^6.0 105.710^5.7 pass pass pass 108.010^8.0 107.710^7.7 pass pass pass 109.010^9.0 108.710^8.7 pass pass pass 109.710^9.7 109.410^9.4 pass pass pass 1010.010^10.0 109.710^9.7 pass pass pass 1010.010^10.0 109.710^9.7 pass pass pass 1010.010^10.0 109.710^9.7 fail fail pass 1010.310^10.3 1010.010^10.0 fail fail pass 1011.010^11.0 1010.710^10.7 fail fail pass 1012.010^12.0 1011.710^11.7 fail fail pass Prediction matches observation in every row; enlarging the probe scales to cover the data range restores every pass. Benchmark label audit. Annotation-vs-label cases satisfy a mechanical criterion: the official annotation, solved both as an LP and as an all-integer program, differs from the official label in both solves. Consensus cases are flagged for inspection only. Benchmark Cases Both-solve mismatch Notes nl4opt annotation vs label 18 18 LP and integer IR both differ; 189 agree (71 integer-only) nl4opt consensus 19 0 battery-passing 6/8 consensus differs from label mamo_easy consensus 15 0 battery-passing 6/8 consensus differs from label mamo_complex consensus 3 0 battery-passing 6/8 consensus differs from label industryor consensus 1 0 battery-passing 6/8 consensus differs from label The 18 NL4OPT annotation-vs-label mismatches, with adjudication notes. ann LP/ann int: optimum of the official annotation solved as LP / all-integer. Problem ann LP ann int label note 2005236115 2333 2333 2400 label close to neither LP nor integer optimum 1703643437 47.78 50 -1e+05 label is a sentinel/placeholder value -642253022 6 6 8 label close to neither LP nor integer optimum -2027758451 16.67 17 18 label close to neither LP nor integer optimum 1165597365 7.5 – -1e+05 label is a sentinel/placeholder value -272035411 3 3 2.3 label close to neither LP nor integer optimum 1637604355 2.4 2.4 4 label differs by ¿50% from both solves 1402521519 1.125e+04 1.128e+04 2500 label differs by ¿50% from both solves -1765797791 55.56 54 50 label close to neither LP nor integer optimum 2041857060 5625 5625 7500 label close to neither LP nor integer optimum -1819716628 21.33 20.8 6.4 label differs by ¿50% from both solves 615752596 85.71 80 -1e+05 label is a sentinel/placeholder value -1062928915 0.72 0.5 6.5e+04 label differs by ¿50% from both solves -114149479 1200 1200 648 label differs by ¿50% from both solves 358766780 45.45 46 48 label close to neither LP nor integer optimum -169306566 56 56 32 label differs by ¿50% from both solves -1243268146 3200 3200 -1e+05 label is a sentinel/placeholder value -527722703 1.239e+04 1.26e+04 1.286e+04 label close to neither LP nor integer optimum Two-pass pipeline yield per benchmark: problems entering evaluation, problems with ≥ 1 valid candidate, and candidate-level validity and battery pass counts. Benchmark problems ≥ 1 valid candidates valid battery pass NL4OPT 239 237 1912 1500 1082 MAMO EasyLP 297 293 2376 1841 1632 MAMO ComplexLP 128 82 1024 377 282 IndustryOR 88 70 704 320 233 Generation covered a prefix subset of MAMO EasyLP (297 of 652), MAMO ComplexLP (128 of 211), and IndustryOR (88 of 100) fixed before any evaluation; see Section 7. Paired exact McNemar tests between selection policies (all-problems denominator): wins/losses of the row policy against plain majority voting, and the cascade against the threshold prefilter. cascade vs. majority cascade vs. threshold Benchmark win lose p win lose p NL4OPT 11 24 0.041 0 1 1 MAMO EasyLP 91 0 0 0 0 1 MAMO ComplexLP 19 0 0 0 0 1 IndustryOR 29 0 0 0 0 1 Wilson 95% confidence intervals for headline rates. Quantity k/nk/n Rate 95% CI Battery clean FPR (seeds) 0/326 0.0% [0.0%, 1.2%] Threshold clean FPR (seeds) 179/326 54.9% [49.5%, 60.2%] Core detection (M1–M5) 1886/3361 56.1% [54.4%, 57.8%] Certified-precondition detection 1060/1515 70.0% [67.6%, 72.2%] Execution-blind detection 534/1321 40.4% [37.8%, 43.1%] M7 detection (exchange) 291/750 38.8% [35.4%, 42.3%] Panel battery recall (all ops) 63/132 47.7% [39.4%, 56.2%] Panel battery recall (M8/M9 excl.) 63/108 58.3% [48.9%, 67.2%] 11 Prompts and implementation details The two-pass interface uses the fixed prompts shipped verbatim in the replication package in prompts.py; generation uses N=8N=8 candidates (one greedy, seven at temperature 0.80.8, top-p 0.950.95, maximum 900900 new tokens); extraction is greedy. The solver is HiGHS 1.x via highspy with feasibility and integrality tolerances 10−910^-9 and the battery’s one-sided violation slack ε=10−5 =10^-5 (relative). Experiments fix all random seeds (reported in each artifact) and run single-threaded per solve. References A. AhmadiTeshnizi, W. Gao, and M. Udell (2024) OptiMUS: scalable optimization modeling with (MI)LP solvers and large language models. In International Conference on Machine Learning (ICML), Cited by: §1, §2.1. D. Bertsimas and J. N. Tsitsiklis (1997) Introduction to linear optimization. Athena Scientific, Belmont, MA. Cited by: §2.4. H. Chen, G. E. Constante-Flores, and C. Li (2025a) OptiChat: bridging optimization models and practitioners with large language models. INFORMS Journal on Data Science. Cited by: §2.2. T. Y. Chen, F. Kuo, H. Liu, P. Poon, D. Towey, T. H. Tse, and Z. Q. Zhou (2018) Metamorphic testing: a review of challenges and opportunities. ACM Computing Surveys 51 (1), p. 1–27. Cited by: §1.2, §2.3. Y. Chen, J. Xia, S. Shao, D. Ge, and Y. Ye (2025b) Solver-informed RL: grounding large language models for authentic optimization modeling. arXiv preprint arXiv:2505.11792. Cited by: §1, §2.1, §7.5. J. W. Chinneck (2008) Feasibility and infeasibility in optimization: algorithms and computational methods. Springer. Cited by: §2.4. A. O. Fajemisin, D. Maragno, and D. den Hertog (2024) Optimization with constraint learning: a framework and survey. European Journal of Operational Research 314 (1), p. 1–14. Cited by: §2.5. Z. Fang, J. Wang, J. Zhong, and Y. Ong (2026) TriVAL: a tri-validation framework for faithful automatic optimization modeling. arXiv preprint arXiv:2605.23966. Cited by: §1, §2.2. R. Guan, X. Shen, J. Zhang, Y. Zhang, et al. (2026) Execution-verified reinforcement learning for optimization modeling. arXiv preprint arXiv:2604.00442. Cited by: §2.1. C. Huang, Z. Tang, S. Hu, R. Jiang, X. Zheng, D. Ge, B. Wang, and Z. Wang (2025) ORLM: a customizable framework in training large models for automated optimization modeling. Operations Research. Note: Articles in advance Cited by: §1, §2.1. J. Huang, X. Chen, S. Mishra, H. S. Zheng, A. W. Yu, X. Song, and D. Zhou (2024a) Large language models cannot self-correct reasoning yet. In International Conference on Learning Representations (ICLR), Cited by: §1, §7.3. X. Huang, Q. Shen, Y. Hu, A. Gao, and B. Wang (2024b) LLMs for mathematical modeling: towards bridging the gap between natural and mathematical languages (MAMO benchmark). arXiv preprint arXiv:2405.13144. Cited by: §2.1. Y. Jia and M. Harman (2011) An analysis and survey of the development of mutation testing. IEEE Transactions on Software Engineering 37 (5), p. 649–678. Cited by: §2.3. C. Jiang, X. Shu, H. Qian, X. Lu, J. Zhou, A. Zhou, and Y. Yu (2025) LLMOPT: learning to define and solve general optimization problems from scratch. In International Conference on Learning Representations (ICLR), Cited by: §1, §2.1. M. Klamkin, A. Deza, S. Cheng, H. Zhao, et al. (2025) DualSchool: how reliable are LLMs for optimization education?. arXiv preprint arXiv:2505.21775. Cited by: §2.2. R. Li, H. Liu, P. Poon, D. Towey, T. Y. Chen, and Z. Q. Zhou (2024) Metamorphic relation generation: state of the art and visions for future research. arXiv preprint arXiv:2406.05397. Cited by: §1.2, §2.3. Z. Li, Z. Guo, X. Lu, J. Wang, et al. (2026) OptArgus: a multi-agent system to detect hallucinations in LLM-based optimization modeling. arXiv preprint arXiv:2605.11738. Cited by: §1, §2.2, §5.2. J. J. Lian, Y. Sun, H. Chen, C. Zhang, H. Qin, and C. Teo (2026) ReLoop: structured modeling and behavioral verification for reliable LLM-based optimization. arXiv preprint arXiv:2602.15983. Cited by: §1.1, §1.1, §1, §1, §2.1, §2.2, §2.4, §4.2, §4.5, §5.3, Proposition 5.7, §6. H. Liu, J. Wang, B. Niu, X. Han, et al. (2026) Opt-Verifier: unleashing the power of LLMs for optimization modeling via dual-side verification. arXiv preprint arXiv:2605.29556. Cited by: §1, §2.2. H. Lu, Z. Xie, Y. Wu, C. Ren, Y. Chen, and Z. Wen (2025) OptMATH: a scalable bidirectional data synthesis framework for optimization modeling. arXiv preprint arXiv:2502.11102. Cited by: §1, §2.1. X. Luo, C. He, D. Geng, C. Shi, et al. (2026) Beyond objective equivalence: constraint injection for LLM-based optimization modeling on vehicle routing problems. arXiv preprint arXiv:2606.04816. Cited by: §2.1, §2.2. F. Margot (2010) Symmetry in integer linear programming. In 50 Years of Integer Programming 1958–2008, p. 647–686. Cited by: §2.4. P. Milgrom and J. Roberts (1996) The LeChatelier principle. American Economic Review 86 (1), p. 173–179. Cited by: §2.4. M. Mostajabdaveh, T. T. Yu, R. Ramamonjison, G. Carenini, Z. Zhou, and Y. Zhang (2024) Optimization modeling and verification from problem specifications using a multi-agent multi-stage LLM framework. INFOR: Information Systems and Operational Research 62 (4), p. 599–617. Cited by: §2.1. R. Ramamonjison, T. T. Yu, R. Li, H. Li, G. Carenini, B. Ghaddar, S. He, M. Mostajabdaveh, A. Banitalebi-Dehkordi, Z. Zhou, and Y. Zhang (2023) NL4Opt competition: formulating optimization problems based on their natural language descriptions. Proceedings of the NeurIPS 2022 Competition Track, PMLR 220. Cited by: §1, §2.1. U. Sadana, A. Chenreddy, E. Delage, A. Forel, E. Frejinger, and T. Vidal (2025) A survey of contextual optimization methods for decision-making under uncertainty. European Journal of Operational Research 320 (2), p. 271–289. Cited by: §2.5. S. Segura, G. Fraser, A. B. Sanchez, and A. Ruiz-Cortés (2016) A survey on metamorphic testing. IEEE Transactions on Software Engineering 42 (9), p. 805–824. Cited by: §2.3. D. M. Topkis (1998) Supermodularity and complementarity. Princeton University Press. Cited by: §2.4. J. Tso, P. Schmittou, Q. Huynh, and J. Hutchins (2026) ConstraintBench: benchmarking LLM constraint reasoning on direct optimization. arXiv preprint arXiv:2602.22465. Cited by: §2.1. R. J. Vanderbei (2020) Linear programming: foundations and extensions. 5th edition, Springer. Cited by: §2.4. X. Wang and D. Zhu (2024) Validating LLM-generated programs with metamorphic prompt testing. arXiv preprint arXiv:2406.06864. Cited by: §2.3. Z. Wang, Z. Zhu, Z. Li, C. Chen, et al. (2025) ORGEval: graph-theoretic evaluation of LLMs in optimization modeling. arXiv preprint arXiv:2510.27610. Cited by: §1, §2.2. Z. Xiao, D. Zhang, Y. Wu, L. Xu, Y. J. Wang, X. Han, X. Fu, T. Zhong, J. Zeng, M. Song, and G. Chen (2024) Chain-of-experts: when LLMs meet complex operations research problems. In International Conference on Learning Representations (ICLR), Cited by: §1, §2.1. Y. Xu, Z. Wang, and T. Dinh (2026) OptiLoop: coordination-in-the-loop verification and repair for LLM-generated optimization agents. arXiv preprint arXiv:2605.27630. Cited by: §2.2. Z. Yang, Y. Wang, Y. Huang, Z. Guo, W. Shi, X. Han, L. Feng, L. Song, X. Liang, and J. Tang (2024) OptiBench meets ReSocratic: measure and improve LLMs for optimization modeling. arXiv preprint arXiv:2407.09887. Cited by: §2.1. A. Zadorojniy, S. Wasserkrug, and E. Farchi (2025) An agent-based framework for the automatic validation of mathematical optimization models. arXiv preprint arXiv:2511.16383. Cited by: §2.2, §2.3. K. Zhao, Z. Di, H. Qian, X. Shu, et al. (2026a) MiniOpt: reasoning to model and solve general optimization problems with limited resources. arXiv preprint arXiv:2606.25832. Cited by: §2.1. R. Zhao, F. Li, Y. Zuo, R. Liu, Y. Liu, Y. Ma, F. Meng, and J. Feng (2026b) Strategy-aware optimization modeling with reasoning LLMs. arXiv preprint arXiv:2605.02545. Cited by: §2.1.