ModelEquivBench: Certifying Multi-Relational Evaluation of LLM-Generated Optimization Models

# Certifying Multi-Relational Evaluation of LLM-Generated Optimization Models
Source: [https://arxiv.org/html/2607.29431](https://arxiv.org/html/2607.29431)
###### Abstract

Large language models increasingly generate optimization models from natural language, but existing evaluation often reduces a generated model and its ground truth to a single*equivalent*/*not\-equivalent*verdict or an execution\-success rate—labels that are neither independently checkable nor faithful to the multiple distinct senses in which two formulations can agree\. We presentModelEquivBench, a certifying, multi\-relational evaluation system that reports a per\-pair*semantic profile*E​0E0–E​6E6: model construction and exact ingestion \(E​0E0\), verified representation alignment \(E​1E1\), same\-space and projected feasible\-set relations \(E​2E2,E​3E3\), objective\-order equivalence \(E​4E4\), optimal\-value equality \(E​5E5\), and optimizer\-set equivalence \(E​6E6\)\. Each decided entry carries relation\-appropriate, independently re\-checkable evidence: replayable traces or explicit maps forE​0E0–E​1E1, exact\-rational certificates for positiveE​2E2–E​6E6conclusions, and explicit witnesses for supported negatives\. Incomplete mapping search, unsupported structure, and resource limits produce typedunknownor N/A outcomes rather than guesses, while unmet prerequisites are reported asabsent\. UsingModelEquivBenchto evaluate three model snapshots—GPT\-5\.4, Claude Sonnet 4\.6, and Qwen3\.5\-397B\-A17B—on the same frozen cohort of 173 base problems \(346 cells per model\) under a no\-repair protocol, the resulting profiles expose distinctions that coarse baselines do not represent:4949,3535, and2525cells contain executable candidates that are nevertheless certified negative on at least one supported relation, and2525,88, and1818structural rejections occur on pairs for whichE​2E2certifies mapped feasible\-set equality under a verified map\. The three model snapshots fail at different stages of the profile and therefore cannot be meaningfully reduced to a single accuracy score\.

## 1Introduction

Large language models \(LLMs\) are increasingly used to turn natural\-language problem descriptions into runnable optimization models\(Ramamonjisonet al\.[2022](https://arxiv.org/html/2607.29431#bib.bib26); AhmadiTeshniziet al\.[2024](https://arxiv.org/html/2607.29431#bib.bib27); Xiaoet al\.[2024](https://arxiv.org/html/2607.29431#bib.bib28); Huanget al\.[2025](https://arxiv.org/html/2607.29431#bib.bib29)\)\. Assessing whether a generated model is*correct*, however, remains unsettled\. Common signals include \(i\)*execution success*—the code runs and a solver returns a number—and \(ii\) a single*equivalent*/*not\-equivalent*verdict against a ground\-truth model, produced by value comparison or structural graph matching\(Wanget al\.[2025](https://arxiv.org/html/2607.29431#bib.bib1); Zhaiet al\.[2025](https://arxiv.org/html/2607.29431#bib.bib2)\)\. Neither by itself answers all of the semantic questions relevant to formulation correctness\. Execution success says nothing about whether the model*means*the right thing: a program can build, export, and solve a model that encodes the wrong feasible region or objective\. A single global equivalence label, in turn, conflates several genuinely different questions—do the feasible sets coincide, do the objectives induce the same ordering, are the optimal values equal, are the optimizer sets in bijection?—and is typically returned without a proof that a third party could independently re\-check\.

We take a different stance\. Given an LLM\-generated \(*candidate*\) model and a*reference*model, we ask:*in which distinct semantic senses do they agree or disagree, and which of those conclusions can be independently certified?*Our answer isModelEquivBench, a certifying, multi\-relational evaluation system that reports a per\-pair*semantic profile*of seven dimensions,E​0E0–E​6E6, summarized in Table[1](https://arxiv.org/html/2607.29431#S3.T1)\. The dimensions range from model construction and exact ingestion \(E​0E0\), through verified representation alignment \(E​1E1\) and feasible\-set relations in the aligned space \(E​2E2\) and under an affine lift \(E​3E3\), to objective order \(E​4E4\), optimal value \(E​5E5\), and optimizer sets \(E​6E6\)\. Crucially,E​0E0–E​6E6form a*profile*, not a ladder: the indices order the dimensions’*definedness*prerequisites, not their logical strength, and equal feasible sets do not imply equal objective order, value, or optimizers\. There is no “deepest passing level” and no scalar collapse\.

ModelEquivBenchis*certifying*: each decided entry carries relation\-appropriate evidence that an independent checker can re\-verify\.E​0E0uses a replayable execution/ingestion trace,E​1E1an explicit admissible map, and positiveE​2E2–E​6E6conclusions exact\-rational certificates \(Farkas, affine\-lift, objective\-identity, or primal–dual evidence\)\. Supported negatives carry a failing trace or explicit witness\. Incomplete search, unsupported structure, and resource limits yield typedunknownor N/A outcomes; failed prerequisites make later dimensionsabsent\. The bidirectional feasible\-set containment engine we call*Certifying Mapped\-Containment*\(CMC\) is the principal technical engine forE​2E2and the supported part ofE​3E3; it is a component insideModelEquivBench, not a replacement for theE​0E0–E​6E6profile\.

We instantiateModelEquivBenchon the supported envelope of linear and bounded\-discrete models and evaluate three model snapshots—GPT\-5\.4, Claude Sonnet 4\.6, and Qwen3\.5\-397B\-A17B—on a frozen cohort of173173base problems, each under paired Structured and Unstructured conditions \(346346cells per model\), with one generation per condition at temperature0\.00\.0and*no repair or resampling*\. Their profiles differ sharply\. GPT\-5\.4 produces ingestible candidates for334/346334/346cells, compared with156/346156/346for Claude Sonnet 4\.6 and196/346196/346for Qwen3\.5\-397B\-A17B\. ConditionalE​1E1coverage is nevertheless similar:277/334277/334\(82\.9%82\.9\\%\),130/156130/156\(83\.3%83\.3\\%\), and164/196164/196\(83\.7%83\.7\\%\)\. Qwen3\.5\-397B\-A17B additionally records1717provider/API errors before candidate creation; these are reported as E0absent, not model\-quality failures\. Exact certification reveals4949,3535, and2525execution\-success overestimations and2525,88, and1818structural rejections despiteE​2E2\-certified mapped feasible\-set equality\. Our contributions are: \(1\)ModelEquivBench, theE​0E0–E​6E6certifying multi\-relational evaluator and its typed\-abstention discipline; \(2\) a certifying implementation with independent re\-verification of every decided fact; and \(3\) a three\-model formal study showing distinctions that execution\-only, value\-only, and structural baselines do not represent\. The contribution is an evaluator and certification system, not a new benchmark dataset: Bench4Opt supplies the experimental instances\. Supplement Sections A–E give the full definitions, certificate soundness proofs, boundary cases, and explicit non\-implication examples\.

![Refer to caption](https://arxiv.org/html/2607.29431v1/x1.png)Figure 1:TheModelEquivBenchcertifyingE​0E0–E​6E6workflow\.E​0E0andE​1E1establish prerequisites;E​2E2–E​6E6ask parallel, relation\-specific questions\. Decided facts carry replayable certificates or witnesses, while unresolved entries remain typed outcomes rather than a global verdict\.
## 2Related Work

### 2\.1LLM Optimization Modeling and Evaluation

#### LLM optimization modeling\.

A growing line of work prompts or fine\-tunes LLMs to formulate optimization models from text, including the NL4Opt competition\(Ramamonjisonet al\.[2022](https://arxiv.org/html/2607.29431#bib.bib26)\), agentic decomposition systems\(AhmadiTeshniziet al\.[2024](https://arxiv.org/html/2607.29431#bib.bib27); Xiaoet al\.[2024](https://arxiv.org/html/2607.29431#bib.bib28)\), and trained modelers\(Huanget al\.[2025](https://arxiv.org/html/2607.29431#bib.bib29); Luet al\.[2025](https://arxiv.org/html/2607.29431#bib.bib9)\)\. These works focus on*generation*; we focus on*certifying evaluation*of generated models against a reference\.

#### Evaluating generated mathematical programs\.

Evaluation has largely relied on execution success and optimal\-value matching, or on a single equivalence verdict\. EquivaMap uses an LLM to propose mappings between decision\-variable spaces and then verifies feasibility and optimality preservation\(Zhaiet al\.[2025](https://arxiv.org/html/2607.29431#bib.bib2)\); EquiBench studies LLMs’ program\-equivalence reasoning\(Weiet al\.[2025](https://arxiv.org/html/2607.29431#bib.bib3)\)\. These approaches target an overall equivalence judgment, whereasModelEquivBenchreports separately certified relations and typed abstentions\.

### 2\.2Structural Comparison and Certifying Verification

#### Structural model comparison\.

ORGEval compares optimization models by graph\-theoretic canonicalization\(Wanget al\.[2025](https://arxiv.org/html/2607.29431#bib.bib1)\)\. Structural matching is efficient but can reject pairs whose feasible sets coincide after a verified change of representation; ourE​2E2relation certifies exactly this same\-space, mapped feasible\-set equality without claiming full\-profile equivalence\.

#### Proof certificates and exact verification\.

Certifying algorithms attach independently checkable evidence to their answers, from proof\-carrying code\(Necula[1997](https://arxiv.org/html/2607.29431#bib.bib23)\)to certified integer\-programming reasoning\(Cheunget al\.[2017](https://arxiv.org/html/2607.29431#bib.bib4); Hoenet al\.[2024](https://arxiv.org/html/2607.29431#bib.bib5); van Doornmalenet al\.[2023](https://arxiv.org/html/2607.29431#bib.bib6); Bogaertset al\.[2022](https://arxiv.org/html/2607.29431#bib.bib22)\)\. Feasible\-set containment rests on Farkas’ lemma and polyhedral theory\(Schrijver[1986](https://arxiv.org/html/2607.29431#bib.bib19)\); projected polyhedra and extended formulations are studied byYannakakis \([1991](https://arxiv.org/html/2607.29431#bib.bib10)\),Confortiet al\.\([2013](https://arxiv.org/html/2607.29431#bib.bib11)\),Kellner \([2015](https://arxiv.org/html/2607.29431#bib.bib7)\), andLiberti \([2009](https://arxiv.org/html/2607.29431#bib.bib12)\)\. Exact rational LP/MIP methods\(Applegateet al\.[2007](https://arxiv.org/html/2607.29431#bib.bib20); Cooket al\.[2013](https://arxiv.org/html/2607.29431#bib.bib21)\)make the resulting evidence checkable without additional floating\-point error during verification\. We adapt these tools intoModelEquivBench, in which every decided fact is independently re\-verified using exact arithmetic\.

## 3The ModelEquivBench Framework

### 3\.1Models, Evidence Policy, and Outcome States

#### Models\.

LetMMhavenMn\_\{M\}decision variables collected inx=\(x1,…,xnM\)⊤x=\(x\_\{1\},\\ldots,x\_\{n\_\{M\}\}\)^\{\\top\}, with per\-coordinate domainsDM,iD\_\{M,i\}\(continuous, integer, or binary\) andDM=∏iDM,i⊆ℝnMD\_\{M\}=\\prod\_\{i\}D\_\{M,i\}\\subseteq\\mathbb\{R\}^\{n\_\{M\}\}\. Its feasible set isFM=\{x∈DM:Aub​x≤bub,Aeq​x=beq\}F\_\{M\}=\\\{x\\in D\_\{M\}:A\_\{\\mathrm\{ub\}\}x\\leq b\_\{\\mathrm\{ub\}\},\\,A\_\{\\mathrm\{eq\}\}x=b\_\{\\mathrm\{eq\}\}\\\}; it has linear objectivefM​\(x\)=objM⊤​xf\_\{M\}\(x\)=\\mathrm\{obj\}\_\{M\}^\{\\top\}x, sense in\{min,max\}\\\{\\min,\\max\\\}, optimal valueopt​\(M\)\\mathrm\{opt\}\(M\)in the extended reals, and optimizer setargopt​\(M\)\\mathrm\{argopt\}\(M\)\. Empty\-set conventions apply, and all coefficients are stored as exact rationals\. We writeR,CR,Cfor reference and candidate, with ingested feasible setsFR,FCF\_\{R\},F\_\{C\}\(bounds folded into inequalities\)\.ModelEquivBenchderives all claims from the models, never from declared labels\.

#### Global disciplines\.

Four rules govern every dimension: \(i\) positive facts carry replayable traces, verified maps, or exact\-rational certificates as appropriate; \(ii\) supported negatives carry failing traces or re\-checkable witnesses; \(iii\) every fact fromE​2E2onward is tied to a named, verified mapφ\\varphi; and \(iv\) the evaluator is fail\-closed—missing prerequisites, unsupported classes, extraction failures, and resource limits produce typed abstentions, never guessedfalseoutcomes\. Unmet prerequisites are recorded separately asabsent\.

Table 1:The E0–E6 semantic profile\. Each dimension is a distinct relation with its own certificate/witness type and typed abstention vocabulary\. The dimensions are prerequisites for one another’s*definedness*, not rungs of a monotone equivalence ladder; a pair receives a profile, not a single label\. N/A means a relation is mathematically inapplicable, whereasabsentmeans that an upstream prerequisite was not met\.ur=unknown\_resource;false\_within=false\_within\_declared\_universe\.
#### Outcome states and definedness\.

A profile entry is not merelytrueorfalse\. A dimension may also beunknownbecause the supported procedure established neither a positive conclusion nor a supported negative conclusion,unknown\_resourcebecause its resource budget was exhausted,unknown\_unsupportedbecause the model lies outside the implemented envelope, or N/A because the relation is mathematically inapplicable\. We reserveabsentfor a different situation: an upstream prerequisite was not established, so the later dimension was never evaluated\. For example, if no candidate model ingests,E​4E4isabsent, not N/A; if a same\-space candidate has no auxiliary variables,E​3E3is N/A\. This distinction matters both logically and statistically\. A rate such as “E​2E2decided givenE​1E1” conditions on the dimensions that were actually entered, whereas a cohort\-wide count retainsabsentcells in the accounting without treating them as failures of the relation\. The resulting profile is therefore a partial, typed set of claims rather than a seven\-bit vector\.

### 3\.2Construction and Representation Alignment

#### E​0E0: construction and exact ingestion\.

E​0E0asks whether the candidate code executes and yields a structurally valid exact\-rational model that ingests\. It istruewith a re\-runnable build trace,falsewith the failing parse/build/execution trace,unknown\_resourcewhen the execution cap is exceeded, andunknown\_unsupportedfor a valid but out\-of\-envelope construct \(e\.g\. a quadratic objective\)\.E​0E0does not require a solver result: infeasible and unbounded models may still beE​0E0true\.E​0E0is established from ingestion and*checkpointed before*any later work, so a downstream timeout cannot corrupt it\.

#### E​1E1: verified representation alignment\.

Because a candidate may name and order variables differently,E​1E1searches for an admissible map from candidate to reference variables\. The admissible family isΦadm=Φsame∪Φlift\\Phi\_\{\\mathrm\{adm\}\}=\\Phi\_\{\\mathrm\{same\}\}\\cup\\Phi\_\{\\mathrm\{lift\}\}, whereΦsame\\Phi\_\{\\mathrm\{same\}\}contains type\-compatible coordinate permutations composed with per\-coordinate transforms—identity, binary complementx↦1−xx\\mapsto 1\-x\(0–1 only\), and sign negationx↦−xx\\mapsto\-x\(free continuous only\)—andΦlift\\Phi\_\{\\mathrm\{lift\}\}contains affine projection/section pairs with injective sections, relating a lower\-dimensional reference to a higher\-dimensional candidate\. Candidate maps are proposed by a deterministic grammar \(exact and original name matching, type\-compatible permutation, signature matching, sign, complement, and affine lift\) and each is checked for admissibility \(dimension match, permutation bijectivity, per\-transform legality by variable type, section injectivity, and the exact right\-inverse identityπ∘σ=id\\pi\\circ\\sigma=\\mathrm\{id\}for affine lifts\)\.E​1E1istrueif at least one admissibleφ\\varphiis verified andunknownif none is found in the searched family\. Critically,E​1E1is*never*false: absence of a found map is not proof that no map exists, so the outcome is coverage\-limited, not a refutation\.

### 3\.3Feasible\-Set Relations

#### E​2E2: same\-space feasible\-set relation\.

Fixing a verified same\-spaceφ\\varphi,E​2E2compares the mapped candidate feasible setφ​\(FC\)\\varphi\(F\_\{C\}\)withFRF\_\{R\}*as subsets of the same semantic variable space*and classifies the pair as*equal*\(FR=φ​\(FC\)F\_\{R\}=\\varphi\(F\_\{C\}\)\),*strict relaxation*\(FR⊊φ​\(FC\)F\_\{R\}\\subsetneq\\varphi\(F\_\{C\}\)\),*strict restriction*\(φ​\(FC\)⊊FR\\varphi\(F\_\{C\}\)\\subsetneq F\_\{R\}\),*incomparable*, or*unknown*\. Each containment directionP⊆QP\\subseteq Qis certified by exact nonnegative Farkas multipliers\(μ,λ\)\(\\mu,\\lambda\)witha⊤=μ⊤​G\+λ⊤​Ha^\{\\top\}=\\mu^\{\\top\}G\+\\lambda^\{\\top\}Handβ≥μ⊤​h\+λ⊤​heq\\beta\\geq\\mu^\{\\top\}h\+\\lambda^\{\\top\}h\_\{\\mathrm\{eq\}\}for every row\(a,β\)\(a,\\beta\)ofQQ; a failure to contain is witnessed by a feasible point ofPPviolating a specific row ofQQ\. This bidirectional, certificate\-or\-witness containment is the CMC engine; multipliers and witnesses are round\-tripped through an independent verifier\. Per\-map relations are aggregated across the declared map universe:E​2E2istrueif*some*admissibleφ\\varphiis certified equal \(and re\-verified\); it isfalse\_within\_declared\_universeonly if that universe is*exhaustive*and*every*map in it separates with a re\-verified witness \(no equal, no unknown\); otherwise it isunknown\. The universe is declared exhaustive only when the type\-compatible permutation family is fully enumerable \(n≤7n\\leq 7\) and no binary coordinate is present, since binary complements are not exhaustively enumerated\. Thusfalse\_within\_declared\_universeis a completeness\-relative negative—“no admissible representation in the complete declared universe makes the feasible sets equal”—not a failed search\.

#### Per\-map and aggregated claims\.

The distinction between a relation under one named map and the aggregateE​2E2outcome is essential\. A certified strict restriction under a particularφ\\varphidoes not rule out a second map that makes the sets equal\. Hence a positive aggregate equality is existential, whereas a negative aggregate statement requires a complete finite universe and a re\-verified separation for every member\. When the universe is incomplete, the strongest sound conclusion after testing many non\-equal maps is stillunknown\. This asymmetric policy deliberately sacrifices recall to prevent a failed representation search from being mislabeled as semantic inequality\. Certificates and witnesses retain the map identifier, the exact transformed constraints, and the verified obligation, so every aggregate claim can be decomposed into independently checkable per\-map facts\.

#### E​3E3: projected feasible\-set relation\.

When the candidate carries auxiliary variables,E​3E3comparesFRF\_\{R\}with the*projection*of the higher\-dimensionalFCF\_\{C\}\. With an affine projectionπ:ℝnC→ℝnR\\pi:\\mathbb\{R\}^\{n\_\{C\}\}\\to\\mathbb\{R\}^\{n\_\{R\}\}and an affine sectionσ​\(x\)=C​x\+d\\sigma\(x\)=Cx\+d, the checker certifies three obligations—π​\(FC\)⊆FR\\pi\(F\_\{C\}\)\\subseteq F\_\{R\},σ​\(FR\)⊆FC\\sigma\(F\_\{R\}\)\\subseteq F\_\{C\}, andπ∘σ=id\\pi\\circ\\sigma=\\mathrm\{id\}—each via verifier\-accepted Farkas multipliers or exact affine identities\. Together these certifyπ​\(FC\)=FR\\pi\(F\_\{C\}\)=F\_\{R\}: the reference set is exactly the affine projection of the candidate’s feasible set\. Projections outside the supported affine\-lift schema \(integer\-auxiliary elimination, non\-affine projection, reference equalities\) yieldunknown, and same\-space cases with no auxiliary variables are N/A\. If a prerequisite such asE​0E0orE​1E1is missing,E​3E3isabsentrather than N/A\. We stress thatE​3E3is*not*a level aboveE​2E2:E​2E2compares aligned sets in one space, whileE​3E3bridges spaces of different dimension; they are different relations, reported independently\.

### 3\.4Objective and Solution Relations

#### E​4E4–E​6E6: objective and optimizer relations\.

Under a verified candidate\-to\-reference mapφ\\varphi\(φ=π\\varphi=\\pifor lifts\),E​4E4checks whetherfCf\_\{C\}andfR∘φf\_\{R\}\\circ\\varphiinduce the same ordering on candidate feasible points with consistent optimization sense\. Positives use an exact identity in the identity/lift/complement schema \(additive constants cancel in comparisons\); negatives use two oppositely ranked feasible points\.E​5E5certifies*optimal\-value equality*opt​\(R\)=opt​\(C\)\\mathrm\{opt\}\(R\)=\\mathrm\{opt\}\(C\)by two LP weak\-duality sandwiches of equal value or by implications fromE​2E2/E​3E3equality with a preserved objective; duality certificates are*refused for integer variables*, since a relaxation bound does not certify the integer optimum\.E​6E6certifies an*optimizer\-set bijection*argopt​\(R\)↔argopt​\(C\)\\mathrm\{argopt\}\(R\)\\leftrightarrow\\mathrm\{argopt\}\(C\)for a map with a certified inverse on optimizers \(identity underE​2E2\-equality with identical objective, or a 0–1 complement involution\)\.E​6E6is*positive\-only*in the current envelope: no certified\-negative type exists yet, so absence of a correspondence isunknown, neverfalse; andE​3E3\-equality does not yieldE​6E6because the affine section is only a right inverse\. These non\-implications \(E​2⇏E​4E2\\not\\Rightarrow E4,E​4⇏E​5E4\\not\\Rightarrow E5,E​5⇏E​6E5\\not\\Rightarrow E6, and their converses\) are exactly why the framework reports a profile rather than a level\.

#### Why the relations cannot be collapsed\.

The profile separates logically independent phenomena\. Two formulations can have the same feasible set but opposite objective senses, makingE​2E2true andE​4E4false\. Distinct feasible sets can share one optimum value, soE​5E5does not implyE​2E2\. Likewise, equal optimal values do not identify the same optimizers, and an optimizer correspondence says nothing about non\-optimal feasible points\. Even when one relation entails another under additional premises, the evaluator records the premises and the resulting certificate rather than silently propagating an unqualified global label\. This is also why a baseline that checks only execution, value, or structure cannot be treated as an oracle for the whole profile\.

## 4Certifying Implementation

### 4\.1Exact Ingestion and Certificate Generation

ModelEquivBenchorchestrates a verification core; synthesis is never trusted, and every artifact is re\-verified before a decided fact is reported\. Candidate code is extracted deterministically and executed in isolation under a3030s cap; it must export an LP or MPS file, which is ingested into an exact\-rational internal model\. Every serialized decimal token is converted directly to a rational, so certification is exact with respect to the LP/MPS coefficients and introduces no additional floating\-point error\.E​1E1map proposals come from the deterministic grammar above\. Feasible\-set containment uses an exact\-rational LP oracle to search for Farkas multipliers \(positive direction\) or a separating feasible point \(negative direction\); bounded 0–1 systems are handled by exact enumeration\. Affine\-lift and primal–dual optimality certificates are synthesized similarly\. Every synthesized object is then re\-checked by an independent verifier—two\-way containment forE​2E2equality, witness verification for separations, the affine\-lift obligations forE​3E3, and the weak\-duality re\-check forE​5E5—and only re\-verified facts are reported; all emitted certificate and witness artifacts were independently re\-verified in all three runs \(Table[3](https://arxiv.org/html/2607.29431#S5.T3)\); the reported denominator counts artifacts rather than unique cells\. Evaluation is*dimension\-level checkpointed*, so a per\-dimension timeout yields a typedunknown\_resourcefor exactly that dimension while preserving earlier results\. The protocol enforces*no repair and no resampling*: a malformed or code\-less response is a genuineE​0E0outcome, not an occasion to re\-prompt\.

Gurobi plays a strictly bounded role: it builds and exports the generated models and reads LP/MPS artifacts, and it backs the value\-matching and structural \(ORGEval\-style\) baselines used only for comparison\. It does*not*certify anyE​1E1–E​6E6conclusion; all framework certificates use the exact\-rational oracle and the independent verifier\. Handling of transport timeouts and character\-decoding failures in the harness provides engineering robustness and is not part of the evaluation semantics\.

### 4\.2Independent Verification and Replay

#### Independent checking boundary\.

Certificate construction and certificate acceptance are separate code paths\. The constructor may use an exact LP oracle to search for multipliers or witnesses, but the verifier only receives the serialized model, map, and proposed evidence and recomputes the required rational identities and inequalities\. It does not trust solver status, LLM text, cached verdicts, or floating\-point tolerances\. A failed check prevents the proposed fact from being reported as decided rather than downgrading it to an uncertified Boolean\. This separation is the operational basis for our use of “certified”: a third party can replay the compact evidence without replaying the generation process or accepting the constructor’s control flow\.

#### System interface and replay artifacts\.

ModelEquivBenchtakes a reference model and one generated candidate as its unit of evaluation and emits three linked products: the typedE​0E0–E​6E6profile, the evidence objects supporting each decided entry, and a provenance manifest recording the map identifier, resource outcome, and source artifact hashes\. This interface separates model generation from semantic assessment: a new generator can be evaluated without changing the certifier, while an updated certifier can replay persisted candidates without another paid model call\. Dimension\-level checkpoints also make partial profiles stable under interruption—a timeout inE​5E5, for example, does not erase a previously verifiedE​2E2certificate\. The resulting artifact is therefore more informative than a final boolean: it states what was proved, under which representation, what remained unresolved, and which compact objects a third party must check to reproduce the claim\. Supplement Section F provides construction/replay pseudocode and the evidence schema\.

## 5Experiments

### 5\.1Experimental Setup

#### Cohort\.

Bench4Opt contains394394source records\(Wanget al\.[2025](https://arxiv.org/html/2607.29431#bib.bib1)\); in our paired representation these form197197base problems\. A ground\-truth–only support audit—depending solely on properties of the reference artifacts, never on any LLM output—partitions them into a development pilot set \(2020\), a formal primary cohort \(173173\), an unsupported audit set \(44, e\.g\. nonlinear structure outside the envelope\), and a malformed\-or\-missing set \(0\)\. We report results*only*on the frozen173173\-problem formal cohort \(SHA\-256 prefixe9ad2018\)\. This reference\-only partition was frozen before formal generation, so no LLM output or evaluator result influenced inclusion\. The2020\-problem pilot was used only for development and is excluded from formal results\. Each base problem is presented under two paired natural\-language conditions—*Structured*\(legacy internal identifierfull\) and*Unstructured*\(concise\)—giving173×2=346173\\times 2=346cells per model\. The two conditions are paired by base problem\. Besides condition\-specific rates, we derive base\-level discordant counts, exact McNemar tests, and paired bootstrap intervals as descriptive analyses of this frozen cohort; they are not population\-level claims\.

#### Models and protocol\.

We evaluate three snapshots served through the AutoDL OpenAI\-compatible endpoint:gpt\-5\.4,claude\-sonnet\-4\-6, andQwen3\.5\-397B\-A17B\. For each cell we take*one*generation at temperature0\.00\.0with*no repair*and*no resampling*; the candidate is executed under a3030s cap and theE​1E1–E​6E6evaluator under a uniform120120s cap\. Prompts, cohort, mapping family, certificate rules, and baseline semantics are identical across all three models\. Every run uses the same frozen prompt contract requesting one self\-contained program that exportscandidate\.lp\. Provider/API errors before candidate creation are kept separate from genuine E0 failure\.

#### Baselines and reporting\.

Alongside theModelEquivBenchprofile, we run two comparison baselines: a solver\-based*value\-matching*implementation and the ORGEval\-style structural implementation used in our harness\. We do not claim that the latter is the unmodified official ORGEval implementation\. Every rate names its denominator, andunknown,unknown\_resource,unknown\_unsupported, N/A,absent, provider/API failure, and certified negatives are kept distinct throughout;unknownnever means “incorrect,” N/A means the relation is mathematically inapplicable, andabsentmeans a prerequisite was not met\. Supplement Sections G–J provide the complete cohort/protocol record, full outcome tables, paired statistics, failure taxonomy, and replay instructions\.

#### Outcome accounting\.

We report both cohort\-wide counts and conditional coverage\. Cohort\-wide rows retain all346346cells and expose where upstream generation or ingestion prevents later evaluation\. Conditional rows ask, among cells for which a dimension is defined, how often the evaluator decides it:E​1E1coverage is conditioned onE​0E0\-true, and the mainE​2E2decided rate onE​1E1\-true\. The paired analysis instead uses all173173base problems per model and defines binary end\-to\-end indicators for E0 success, E1 map\-found, and E2/E5/E6 decided\. Typed unknowns, N/A, and absence remain visible in the source matrix and are never relabeled as certifiedfalse\.

Table[3](https://arxiv.org/html/2607.29431#S5.T3)reports the formal profiles, while Table[2](https://arxiv.org/html/2607.29431#S5.T2)summarizes relation\-specific baseline discrepancies\.

Table 2:Relation\-specific baseline diagnostics\. An execution\-success overestimation is an E0\-truecell with a certified negative on at least one supported relation\. The second row counts structural rejections on pairs for whichE​2E2certifies mapped feasible\-set equality; it is anE​2E2\-specific disagreement, not necessarily a full\-profile false rejection\. The ORGEval implementation is the one used in our harness\.

Table 3:FormalModelEquivBenchprofiles under the same single\-generation, temperature\-0\.00\.0, no\-repair protocol\. Qwen3\.5\-397B\-A17B’s1717provider/API errors occurred before candidate creation and are reported separately from genuine E0 failure\.false\_withinabbreviatesfalse\_within\_declared\_universe\. Re\-verification denominators count emitted dimension\-verdict artifacts, not unique cells\.

### 5\.2Stage\-Wise Model Profiles

#### Execution does not settle semantics\.

GPT, Sonnet, and Qwen produce ingestible candidates for334/346334/346,156/346156/346, and196/346196/346cells\. Yet their E2 decided counts are only114/277114/277,45/13045/130, and87/16487/164among E1\-truecells\. Across the three runs,4949,3535, and2525E0\-truecells carry a certified negative on at least one supported relation\. An execution\-only evaluator would count every one of these as successful\.

#### The evaluated snapshots fail at different stages\.

GPT has high E0 coverage \(96\.5%96\.5\\%\), so most losses occur downstream\. Sonnet has the lowest E0 coverage \(45\.1%45\.1\\%\) under the frozen output contract\. Qwen lies between them:196196cells are E0\-true, while among329329successful API responses131131are genuine E0 failures and22are unsupported; another1717cells end in a provider/API error before E0 is defined\. Conditional E1 coverage is almost identical across the three models \(82\.9%82\.9\\%,83\.3%83\.3\\%, and83\.7%83\.7\\%\), showing why generation, ingestion, and semantic coverage must be reported separately\.

#### Conditional coverage changes the comparison\.

Among cells with a verified map, Qwen reaches an E2 decision on87/16487/164\(53\.0%53\.0\\%\), compared with114/277114/277\(41\.2%41\.2\\%\) for GPT and45/13045/130\(34\.6%34\.6\\%\) for Sonnet\. This does not define a global winner: the denominators exclude different upstream losses\. Rather, it shows how a model with lower end\-to\-end ingestion can have higher conditional certifier coverage, a distinction hidden by one aggregate score\.

### 5\.3Baseline Discrepancies and Certified Case

#### Exact certification exposes baseline blind spots\.

ORGEval returnsnot\_equivalenton2525,88, and1818cells for which E2 certifies mapped feasible\-set equality for GPT, Sonnet, and Qwen, respectively\. These are relation\-specific discrepancies: the structural baseline rejects the pair globally, whereasE​2E2certifies equality of the mapped feasible sets\. This comparison does not by itself assert objective\-order, optimal\-value, or optimizer\-set equivalence\. No batch exhibits a strict value\-match false acceptance, but value matching addresses only one scalar relation and supplies no evidence for feasible\-set, objective\-order, or optimizer\-set claims\.

![Refer to caption](https://arxiv.org/html/2607.29431v1/x2.png)Figure 2:A replayableModelEquivBenchall\-applicable\-positive case \(B4O\_BASE\_0031, Unstructured, Claude Sonnet 4\.6\)\. A verified identity map and exact enumeration certify E2; E4–E6 independently re\-verify as true and E3 is N/A\. Both coarse baselines nevertheless reject the pair\.
#### A replayable all\-applicable\-positive case\.

Figure[2](https://arxiv.org/html/2607.29431#S5.F2)shows a Sonnet case,B4O\_BASE\_0031\(Unstructured\)\. An identity map aligns two models, each with five binary variables and 18 inequalities; exact enumeration certifies bothE​2E2directions, andE​4E4–E​6E6independently re\-verifytrue\(E​3E3is N/A\)\. ORGEval returnsnot\_equivalent, while the LP\-relaxation value baseline returnsnot\_equal; the latter does not contradictE​5E5, which concerns the original binary optima\. The paired Structured cell has the same applicable profile, but ORGEval returnsequivalent, illustrating representation sensitivity\. Persisted paths and SHA\-256 hashes make the case replayable\.

### 5\.4Coverage, Abstention, and Reporting

#### Coverage and abstention are results, not errors\.

The three runs contain5757,2626, and3232E1\-unknowncells; their E2 resource\-timeout counts are4545,2424, and2727\. At least one evaluator dimension hits the120120s cap in7070,3535, and3939cells\. No formal cell receives a decidedE​3E3outcome, so the study empirically exercises E0–E2 and E4–E6 while E3 records a zero\-coverage boundary of the current affine\-lift schema\. The complement of a decided rate therefore mixes search incompleteness, unsupported structure, and resource abstention rather than forming a model error rate\.

#### Auxiliary paired analysis\.

For GPT and Sonnet, base\-level Structured–Unstructured comparisons show descriptive positive differences for downstream E1/E2 coverage, but no exact McNemar test survives Holm correction\. We retain this as an auxiliary observation rather than a three\-model ranking; all primary comparisons use the common aggregate denominators in Tables[2](https://arxiv.org/html/2607.29431#S5.T2)and[3](https://arxiv.org/html/2607.29431#S5.T3)\.

#### Soundness and coverage are separate axes\.

Every decided relation is backed by evidence that can be replayed independently, while coverage reports how often the current map family, supported schema, and resource budget reach a decision\. High coverage without evidence risks confident but ungrounded labels; sound certification with limited coverage is transparent but incomplete\. The profile reports both, preserving certified negatives, unresolved searches, resource limits, N/A, and upstream absence rather than forcing them into one score\.

#### Implications for evaluator design\.

ModelEquivBenchsuggests that evaluation reports should separate at least three quantities that are often conflated: end\-to\-end generation success, conditional semantic coverage after ingestion, and the distribution of certified positive, certified negative, and abstaining outcomes within each relation\. The same generator can look strong on the first quantity and weak on the second, or vice versa, as the three snapshots illustrate\. A scalar “equivalence accuracy” cannot reveal whether errors arise from output contract violations, representation search, semantic disagreement, unsupported structure, or exhausted resources\. Profile\-level reporting also makes baseline comparisons relation\-specific: value matching may be informative forE​5E5but silent aboutE​2E2, while structural matching can disagree with a certified same\-space feasible\-set relation\. In practical benchmark use, the profile can therefore serve both as a scorecard and as a debugging record, directing model or prompt improvements to the stage where evidence actually fails rather than to an undifferentiated final label\.

A minimum auditable report should therefore pair the eligible cohort with end\-to\-end counts, per\-relation conditional coverage, outcome distributions, re\-verification rates, and the resource and map\-completeness assumptions that governunknownandfalse\_within\_declared\_universe\.

#### Scope of claims\.

Results are limited togpt\-5\.4,claude\-sonnet\-4\-6, andQwen3\.5\-397B\-A17Bon the frozen173173\-base cohort, one generation per condition at temperature0\.00\.0, no repair or resampling, and the120120s evaluator policy\. We claim neither universal superiority, state\-of\-the\-art generation, nor completeness over all mathematical programs\.

## 6Limitations and Conclusion

#### Limitations\.

We evaluate three model snapshots with one generation per condition; broader claims require more models and repeated sampling\. The supported envelope covers linear and bounded\-discrete structure, while quadratic and general nonlinear models yieldunknown\_unsupported\. The finiteE​1E1grammar is incomplete,E​3E3supports only the declared affine\-lift schema, andE​6E6has no certified\-negative type\. Exact rational verification also incurs resource limits: under the120120s policy, at least one dimension returnsunknown\_resourcein7070,3535, and3939GPT, Sonnet, and Qwen cells\. Results may depend on provider\-specific serving, and one sample per cell cannot quantify generation variance\. The paired prompt analysis is descriptive—no McNemar comparison survives Holm correction—and the frozen cohort is not a random population sample\. Finally, no formal cell has a decidedE​3E3outcome, so empirical coverage of projected equivalence remains unestablished\.

#### Conclusion\.

ModelEquivBenchreports each candidate–reference pair as a certifiedE​0E0–E​6E6semantic profile rather than one opaque label\. The frozen three\-model study shows that execution is weak evidence of semantic correctness, different snapshots fail at different stages, and exact evidence with typed abstention makes both decisions and current coverage limits auditable\.

## References

- A\. AhmadiTeshnizi, W\. Gao, and M\. Udell \(2024\)OptiMUS: scalable optimization modeling with \(MI\)LP solvers and large language models\.InProceedings of the 41st International Conference on Machine Learning \(ICML\),Proceedings of Machine Learning Research, Vol\.235,pp\. 577–596\.Cited by:[§1](https://arxiv.org/html/2607.29431#S1.p1.1),[§2\.1](https://arxiv.org/html/2607.29431#S2.SS1.SSS0.Px1.p1.1)\.
- D\. L\. Applegate, W\. Cook, S\. Dash, and D\. G\. Espinoza \(2007\)Exact solutions to linear programming problems\.Operations Research Letters35\(6\),pp\. 693–699\.Cited by:[§F\.4](https://arxiv.org/html/2607.29431#A6.SS4.p1.1),[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- B\. Bogaerts, S\. Gocht, C\. McCreesh, and J\. Nordström \(2022\)Certified symmetry and dominance breaking for combinatorial optimisation\.InProceedings of the 36th AAAI Conference on Artificial Intelligence,pp\. 3698–3707\.Cited by:[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- K\. K\. H\. Cheung, A\. Gleixner, and D\. E\. Steffy \(2017\)Verifying integer programming results\.InInteger Programming and Combinatorial Optimization: 19th International Conference \(IPCO 2017\),pp\. 148–160\.Cited by:[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- M\. Conforti, G\. Cornuéjols, and G\. Zambelli \(2013\)Extended formulations in combinatorial optimization\.Annals of Operations Research204\(1\),pp\. 97–143\.Cited by:[Appendix D](https://arxiv.org/html/2607.29431#A4.p2.3),[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- W\. Cook, T\. Koch, D\. E\. Steffy, and K\. Wolter \(2013\)A hybrid branch\-and\-bound approach for exact rational mixed\-integer programming\.Mathematical Programming Computation5\(3\),pp\. 305–344\.Cited by:[§F\.4](https://arxiv.org/html/2607.29431#A6.SS4.p1.1),[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- A\. Hoen, A\. Oertel, A\. Gleixner, and J\. Nordström \(2024\)Certifying MIP\-based presolve reductions for 0\-1 integer linear programs\.InIntegration of Constraint Programming, Artificial Intelligence, and Operations Research \(CPAIOR 2024\),Lecture Notes in Computer Science, Vol\.14742,pp\. 310–328\.Cited by:[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.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 Research73\(6\),pp\. 2986–3009\.Cited by:[§1](https://arxiv.org/html/2607.29431#S1.p1.1),[§2\.1](https://arxiv.org/html/2607.29431#S2.SS1.SSS0.Px1.p1.1)\.
- K\. Kellner \(2015\)Containment problems for projections of polyhedra and spectrahedra\.External Links:1509\.02735Cited by:[Appendix D](https://arxiv.org/html/2607.29431#A4.p2.3),[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- L\. Liberti \(2009\)Reformulations in mathematical programming: definitions and systematics\.RAIRO – Operations Research43\(1\),pp\. 55–85\.Cited by:[Appendix D](https://arxiv.org/html/2607.29431#A4.p2.3),[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- H\. Lu, Z\. Xie, Y\. Wu, C\. Ren, Y\. Chen, and Z\. Wen \(2025\)OptMATH: a scalable bidirectional data synthesis framework for optimization modeling\.InProceedings of the 42nd International Conference on Machine Learning \(ICML\),Proceedings of Machine Learning Research, Vol\.267,pp\. 40769–40802\.Cited by:[§2\.1](https://arxiv.org/html/2607.29431#S2.SS1.SSS0.Px1.p1.1)\.
- G\. C\. Necula \(1997\)Proof\-carrying code\.InProceedings of the 24th ACM SIGPLAN\-SIGACT Symposium on Principles of Programming Languages \(POPL\),pp\. 106–119\.Cited by:[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.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 \(2022\)NL4Opt competition: formulating optimization problems based on their natural language descriptions\.InProceedings of the NeurIPS 2022 Competitions Track, PMLR,Vol\.220,pp\. 189–203\.Cited by:[§1](https://arxiv.org/html/2607.29431#S1.p1.1),[§2\.1](https://arxiv.org/html/2607.29431#S2.SS1.SSS0.Px1.p1.1)\.
- A\. Schrijver \(1986\)Theory of linear and integer programming\.John Wiley & Sons\.Cited by:[§C\.1](https://arxiv.org/html/2607.29431#A3.SS1.p1.2),[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- J\. van Doornmalen, L\. Eifler, A\. Gleixner, and C\. Hojny \(2023\)A proof system for certifying symmetry and optimality reasoning in integer programming\.External Links:2311\.03877Cited by:[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- Z\. Wang, Z\. Zhu, Z\. Li, C\. Chen, Y\. Han, Y\. Lin, Z\. Lin, A\. Gu, X\. Hu, R\. Sun, and T\. Ding \(2025\)ORGEval: graph\-theoretic evaluation of LLMs in optimization modeling\.External Links:2510\.27610Cited by:[§G\.1](https://arxiv.org/html/2607.29431#A7.SS1.p1.1),[§1](https://arxiv.org/html/2607.29431#S1.p1.1),[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px1.p1.1),[§5\.1](https://arxiv.org/html/2607.29431#S5.SS1.SSS0.Px1.p1.9)\.
- A\. Wei, J\. Cao, R\. Li, H\. Chen, Y\. Zhang, Z\. Wang, Y\. Liu, T\. S\. F\. X\. Teixeira, D\. Yang, K\. Wang, and A\. Aiken \(2025\)EquiBench: benchmarking large language models’ reasoning about program semantics via equivalence checking\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing \(EMNLP\),pp\. 33868–33881\.Cited by:[§2\.1](https://arxiv.org/html/2607.29431#S2.SS1.SSS0.Px2.p1.1)\.
- 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\.InThe Twelfth International Conference on Learning Representations \(ICLR\),Cited by:[§1](https://arxiv.org/html/2607.29431#S1.p1.1),[§2\.1](https://arxiv.org/html/2607.29431#S2.SS1.SSS0.Px1.p1.1)\.
- M\. Yannakakis \(1991\)Expressing combinatorial optimization problems by linear programs\.Journal of Computer and System Sciences43\(3\),pp\. 441–466\.Cited by:[Appendix D](https://arxiv.org/html/2607.29431#A4.p2.3),[§2\.2](https://arxiv.org/html/2607.29431#S2.SS2.SSS0.Px2.p1.1)\.
- H\. Zhai, C\. Lawless, E\. Vitercik, and L\. Leqi \(2025\)EquivaMap: leveraging LLMs for automatic equivalence checking of optimization formulations\.InProceedings of the 42nd International Conference on Machine Learning \(ICML\),Proceedings of Machine Learning Research, Vol\.267,pp\. 74288–74305\.Cited by:[§1](https://arxiv.org/html/2607.29431#S1.p1.1),[§2\.1](https://arxiv.org/html/2607.29431#S2.SS1.SSS0.Px2.p1.1)\.

Supplementary Material

ModelEquivBench: Certifying Multi\-Relational Evaluation of

LLM\-Generated Optimization Models

This technical appendix provides formal statements and proofs for the E0–E6 relations, certificate and witness schemas, algorithms for profile construction and independent verification, detailed cohort and protocol information, complete three\-model outcome accounting, paired analyses, failure taxonomies, and reproduction instructions\.

## Appendix AFormal Setup, Scope, and Typed Outcomes

### A\.1Optimization models and exact semantics

###### Definition A\.1\(Optimization model\)\.

A modelMMis a tuple

M=\(n,D,Aub,bub,Aeq,beq,c,s\),M=\(n,D,A\_\{\\rm ub\},b\_\{\\rm ub\},A\_\{\\rm eq\},b\_\{\\rm eq\},c,s\),wherennis the number of variables;D=D1×⋯×DnD=D\_\{1\}\\times\\cdots\\times D\_\{n\}withDi∈\{ℝ,ℤ,\{0,1\}\}D\_\{i\}\\in\\\{\\mathbb\{R\},\\mathbb\{Z\},\\\{0,1\\\}\\\}\(possibly intersected with exact rational bounds\);Aub​x≤bubA\_\{\\rm ub\}x\\leq b\_\{\\rm ub\}andAeq​x=beqA\_\{\\rm eq\}x=b\_\{\\rm eq\}are exact\-rational constraints;c∈ℚnc\\in\\mathbb\{Q\}^\{n\}is a linear objective; ands∈\{min,max\}s\\in\\\{\\min,\\max\\\}is the objective sense\. Its feasible set and optimizer set are

FM=\{x∈D:\\displaystyle F\_\{M\}=\\\{x\\in D:\\;Aub​x≤bub,\\displaystyle A\_\{\\rm ub\}x\\leq b\_\{\\rm ub\},Aeqx=beq\},\\displaystyle A\_\{\\rm eq\}x=b\_\{\\rm eq\}\\\},XM∗\\displaystyle X\_\{M\}^\{\*\}=argoptx∈FMc⊤​x\.\\displaystyle=\\operatorname\*\{argopt\}\_\{x\\in F\_\{M\}\}c^\{\\top\}x\.The optimal valuevM∗v\_\{M\}^\{\*\}is interpreted in the extended reals\. For minimization,vM∗=\+∞v\_\{M\}^\{\*\}=\+\\inftywhenFM=∅F\_\{M\}=\\varnothingandvM∗=−∞v\_\{M\}^\{\*\}=\-\\inftywhen the objective is unbounded below; the signs are reversed for maximization\.

The reference model is denotedRRand the generated candidateCC\. Every numeric token serialized in LP/MPS is converted directly to a rational\. Thus, all certificate checks are exact with respect to the serialized model; the claim does not reconstruct real\-valued quantities that may have been rounded before serialization\.

### A\.2Profiles are partial typed claim sets

The output for one candidate/reference pair is

𝒫​\(C,R\)=\(E​0,E​1,E​2,E​3,E​4,E​5,E​6\),\\mathcal\{P\}\(C,R\)=\\bigl\(E0,E1,E2,E3,E4,E5,E6\\bigr\),but this tuple is not a seven\-bit vector and the indices are not a strength ranking\. Each component records a relation, its applicability, its evidence, and a typed reason if no decision is returned\.

Table 4:Typed outcome vocabulary\. N/A andabsentare deliberately distinct\.
### A\.3Evidence discipline and prerequisite DAG

The framework obeys four global rules\.

1. 1\.Every positive semantic fact is accepted only after exact independent re\-verification of a certificate\.
2. 2\.Every supported negative fact carries a concrete witness\.
3. 3\.E2–E6 are conditioned on a named verified representation map produced by E1\.
4. 4\.Missing prerequisites, unsupported structure, failed evidence construction, and resource exhaustion never become guessed negatives\.

E0 gates ingestion\. E1 gates map\-conditioned relations\. E2 and E3 ask different feasible\-set questions and do not form consecutive rungs\. E4–E6 may be considered once an admissible map exists, but none is silently inferred from a lower index without recording the additional premises and evidence\.

## Appendix BE0 and E1: Ingestion and Representation Alignment

### B\.1E0: candidate construction and exact ingestion

###### Definition B\.1\(E0\)\.

E0 asks whether a model response yields a deterministic candidate program that executes within the declared cap, exports an LP/MPS model, and is ingested into a structurally valid exact\-rational model\. E0 istruewith an independently replayable trace; it is a genuinefalsewhen a successful model response contains no usable program, fails deterministically, or exports an invalid model\. A provider/API failure before a candidate exists leaves E0absent\. A valid but unsupported model isunknown\_unsupported, and an execution\-cap event isunknown\_resource\.

This definition separates three questions that are frequently conflated: provider delivery, candidate validity, and semantic correctness\. E0trueasserts only the second\. It makes no claim about E1–E6\.

###### Proposition B\.2\(E0 trace replay\)\.

If the independent replay harness re\-executes the recorded candidate program under the specified environment and obtains the same normalized LP/MPS\-derived exact model, then the E0 positive claim is independently reproducible\.

###### Proof\.

The trace specifies the candidate program, execution command, resource cap, exported model, and deterministic exact\-ingestion procedure\. Replaying these objects reconstructs the same normalized tuple in Definition[A\.1](https://arxiv.org/html/2607.29431#A1.Thmdefinition1); the replay decision does not rely on a solver’s semantic judgment\. ∎

### B\.2E1: admissible mappings

A mapping aligns semantic decision variables before any relation is tested\. The general admissible schema contains:

1. 1\.type\-compatible coordinate permutations, including identity;
2. 2\.binary complementxi↦1−xix\_\{i\}\\mapsto 1\-x\_\{i\}for 0–1 variables;
3. 3\.sign negationxi↦−xix\_\{i\}\\mapsto\-x\_\{i\}for free continuous variables;
4. 4\.a declared affine lift/section pair for the supported E3 schema\.

The general mapping schema admits sign negation for free continuous variables\. In the reported formal run, however, the instantiated proposer manifest is the finite family listed in Supplement Section[F\.2](https://arxiv.org/html/2607.29431#A6.SS2): stable\-name match, original\-name match, identity, signature permutation, binary complement, and affine lift\. No standalone sign\-negation proposal is instantiated, so E1 and aggregate E2 coverage do not quantify over such maps\.

###### Definition B\.3\(Same\-space admissible map\)\.

A same\-space map is an affine bijection

φ​\(x\)=P​x\+q,\\varphi\(x\)=Px\+q,wherePPis a signed permutation matrix andqqis an exact offset\. A negative entry denotes either sign negation on a free continuous coordinate with zero offset, or binary complement on a 0–1 coordinate with unit offset\. It is admissible only if dimensions, variable types, bounds, and every coordinate transform are legal and the inverse is exact\. In the reported finite proposal family, negative entries are instantiated only by binary complements\.

###### Definition B\.4\(Lift admissibility\)\.

FornC\>nRn\_\{C\}\>n\_\{R\}, a supported lift consists of a projectionπ:ℝnC→ℝnR\\pi:\\mathbb\{R\}^\{n\_\{C\}\}\\to\\mathbb\{R\}^\{n\_\{R\}\}and an affine sectionσ​\(x\)=C​x\+d\\sigma\(x\)=Cx\+dsatisfyingπ∘σ=id\\pi\\circ\\sigma=\\mathrm\{id\}exactly, together with compatible domains for all mapped variables\.

###### Proposition B\.5\(Why E1 has no aggregate false\)\.

Failure to find an admissible map in a finite searched family does not prove that no semantics\-preserving map exists outside that family\. Therefore the sound aggregate outcome isunknown, notfalse\.

###### Proof\.

The deterministic mapping search evaluates a declared subset of all possible bijections and affine encodings\. A negative conclusion over that subset cannot quantify over unsearched maps\. Since E2–E6 may become positive under an unsearched map, the only sound result is a coverage\-limited abstention\. ∎

Each accepted E1 artifact records the mapping type, exact parameters, domain compatibility checks, and a stable identifier used by every downstream certificate and witness\.

## Appendix CE2: Same\-Space Mapped Feasible\-Set Relations

### C\.1Directional containment certificates

Let

P\\displaystyle P=\{x:G​x≤h,H​x=heq\},\\displaystyle=\\\{x:Gx\\leq h,\\ Hx=h\_\{\\rm eq\}\\\},Q\\displaystyle Q=\{x:A​x≤b\}\.\\displaystyle=\\\{x:Ax\\leq b\\\}\.with exact rational data after domain handling\. The certificate form follows Farkas’ lemma and standard polyhedral containment arguments\(Schrijver[1986](https://arxiv.org/html/2607.29431#bib.bib19)\)\. Equalities may be carried explicitly or converted to paired inequalities where supported\.

###### Proposition C\.1\(Farkas row certificate\)\.

For a rowai⊤​x≤bia\_\{i\}^\{\\top\}x\\leq b\_\{i\}ofQQ, suppose there existμi≥0\\mu\_\{i\}\\geq 0and unrestrictedλi\\lambda\_\{i\}such that

ai=G⊤​μi\+H⊤​λi,bi≥h⊤​μi\+heq⊤​λi\.a\_\{i\}=G^\{\\top\}\\mu\_\{i\}\+H^\{\\top\}\\lambda\_\{i\},\\qquad b\_\{i\}\\geq h^\{\\top\}\\mu\_\{i\}\+h\_\{\\rm eq\}^\{\\top\}\\lambda\_\{i\}\.Then everyx∈Px\\in Psatisfiesai⊤​x≤bia\_\{i\}^\{\\top\}x\\leq b\_\{i\}\.

###### Proof\.

Forx∈Px\\in P,

ai⊤​x=μi⊤​G​x\+λi⊤​H​x≤μi⊤​h\+λi⊤​heq≤bi,a\_\{i\}^\{\\top\}x=\\mu\_\{i\}^\{\\top\}Gx\+\\lambda\_\{i\}^\{\\top\}Hx\\leq\\mu\_\{i\}^\{\\top\}h\+\\lambda\_\{i\}^\{\\top\}h\_\{\\rm eq\}\\leq b\_\{i\},where the first inequality usesμi≥0\\mu\_\{i\}\\geq 0andG​x≤hGx\\leq h\. ∎

###### Corollary C\.2\(Containment\)\.

If Proposition[C\.1](https://arxiv.org/html/2607.29431#A3.Thmdefinition1)has a verified multiplier pair for every row ofQQ, thenP⊆QP\\subseteq Q\.

###### Proposition C\.3\(Separating witness\)\.

If a rational pointzzis independently verified to satisfy all constraints and domains ofPPand violates at least one row ofQQ, thenP⊈QP\\nsubseteq Q\.

###### Proof\.

The pointzzbelongs toPPbut notQQ, which directly refutes containment\. ∎

For bounded 0–1 systems, exhaustive enumeration of all declared assignments is an exact finite certificate\. The replay verifier re\-checks every assignment or a compact deterministic enumeration trace\.

### C\.2Per\-map relation classification

Fix one verified same\-space mapφ\\varphiand writeP=φ​\(FC\)P=\\varphi\(F\_\{C\}\)andQ=FRQ=F\_\{R\}\. Two directional checks yield:

- •*equal*:P⊆QP\\subseteq QandQ⊆PQ\\subseteq P;
- •*strict relaxation*:Q⊆PQ\\subseteq Pand a witness provesP⊈QP\\nsubseteq Q;
- •*strict restriction*:P⊆QP\\subseteq Qand a witness provesQ⊈PQ\\nsubseteq P;
- •*incomparable*: witnesses refute both directions;
- •*unknown*: at least one required direction is unresolved\.

###### Proposition C\.4\(Soundness of the five\-way per\-map diagnostic\)\.

Whenever all evidence required by one of the first four labels above passes the independent verifier, the corresponding set relation holds under the recorded mapφ\\varphi\.

###### Proof\.

Equality follows from antisymmetry of set inclusion\. Each strict label combines one certified inclusion with a verified point in the set difference\. Two verified set\-difference points establish incomparability\. ∎

### C\.3Aggregation across maps

Letℳ⊆Φadm\\mathcal\{M\}\\subseteq\\Phi\_\{\\mathrm\{adm\}\}be the declared verified map universe\.

###### Definition C\.5\(Aggregate E2\)\.

The aggregate E2 result is:

- •trueif someφ∈ℳ\\varphi\\in\\mathcal\{M\}has certified equality;
- •false\_within\_declared\_universeonly whenℳ\\mathcal\{M\}is declared complete and every member has a verified non\-equality witness;
- •unknownotherwise\.

###### Proposition C\.6\(Soundness of aggregate E2\)\.

Atrueaggregate means that a named admissible representation makes the feasible sets equal\. Afalse\_within\_declared\_universeaggregate means no map in the complete declared universe makes them equal\. Neither statement quantifies over maps outside the declared grammar\.

###### Proof\.

The positive case is existential and inherits the per\-map equality proof\. In the negative case, completeness of the finite declared universe plus a verified non\-equality witness for every member proves the universal claim restricted to that universe\. Without completeness, such a universal conclusion is invalid, so the framework returnsunknown\. ∎

The implementation declares the simple type\-compatible permutation universe complete only when it is exhaustively enumerable \(currentlyn≤7n\\leq 7\) and no binary coordinate is present\. Binary\-complement subsets are not exhaustively enumerated, so any binary coordinate makes the declared universe incomplete\. This conservative boundary prevents failed map search from being mislabeled as semantic inequality\.

### C\.4Degenerate feasible sets

The empty set obeys ordinary containment conventions:∅⊆Q\\varnothing\\subseteq Qfor everyQQ, andP⊆∅P\\subseteq\\varnothingonly whenP=∅P=\\varnothing\. A positive empty\-set equality therefore requires evidence that both sides are empty\. A solver status alone is insufficient; the accepted artifact must be replayable under the exact supported procedure\. Unboundedness is not an E2 special case because E2 concerns sets, not objective values\.

## Appendix DE3: Projected Feasible\-Set Equality Under an Affine Lift

E3 applies when the candidate has auxiliary variables and a supported affine projection/section pair has passed E1\.

###### Proposition D\.1\(Affine\-lift equality\)\.

Letπ:ℝnC→ℝnR\\pi:\\mathbb\{R\}^\{n\_\{C\}\}\\to\\mathbb\{R\}^\{n\_\{R\}\}andσ:ℝnR→ℝnC\\sigma:\\mathbb\{R\}^\{n\_\{R\}\}\\to\\mathbb\{R\}^\{n\_\{C\}\}satisfy:

π​\(FC\)\\displaystyle\\pi\(F\_\{C\}\)⊆FR,\\displaystyle\\subseteq F\_\{R\},\(1\)σ​\(FR\)\\displaystyle\\sigma\(F\_\{R\}\)⊆FC,\\displaystyle\\subseteq F\_\{C\},\(2\)π∘σ\\displaystyle\\pi\\circ\\sigma=idℝnR\.\\displaystyle=\\mathrm\{id\}\_\{\\mathbb\{R\}^\{n\_\{R\}\}\}\.\(3\)Thenπ​\(FC\)=FR\\pi\(F\_\{C\}\)=F\_\{R\}\.

###### Proof\.

Equation \([1](https://arxiv.org/html/2607.29431#A4.E1)\) gives one containment\. For anyx∈FRx\\in F\_\{R\}, Equation \([2](https://arxiv.org/html/2607.29431#A4.E2)\) givesσ​\(x\)∈FC\\sigma\(x\)\\in F\_\{C\}, and Equation \([3](https://arxiv.org/html/2607.29431#A4.E3)\) yieldsx=π​\(σ​\(x\)\)∈π​\(FC\)x=\\pi\(\\sigma\(x\)\)\\in\\pi\(F\_\{C\}\)\. HenceFR⊆π​\(FC\)F\_\{R\}\\subseteq\\pi\(F\_\{C\}\), proving equality\. ∎

The two set\-containment obligations are discharged using exact Farkas evidence or bounded enumeration, while the right\-inverse identity is checked by exact matrix arithmetic\. This is a deliberately restricted, certifying instance of projected\-polyhedron and extended\-formulation reasoning\(Yannakakis[1991](https://arxiv.org/html/2607.29431#bib.bib10); Confortiet al\.[2013](https://arxiv.org/html/2607.29431#bib.bib11); Kellner[2015](https://arxiv.org/html/2607.29431#bib.bib7); Liberti[2009](https://arxiv.org/html/2607.29431#bib.bib12)\)\. Notice thatπ\\pineed not be injective; the sectionσ\\sigmais injective as a consequence ofπ∘σ=id\\pi\\circ\\sigma=\\mathrm\{id\}\.

E3 returns N/A for same\-space candidates with no auxiliary variables\. It returnsunknownoutside the declared affine\-lift schema, including unsupported integer\-auxiliary elimination, non\-affine projection, and reference\-equality cases outside the implemented schema\. If E0 or E1 is missing, E3 isabsent, not N/A\. No formal\-cohort cell satisfies the implemented E3 certificate schema; this is a zero\-coverage boundary, not evidence against Proposition[D\.1](https://arxiv.org/html/2607.29431#A4.Thmdefinition1)\.

## Appendix EE4–E6: Objective Order, Optimal Value, and Optimizers

### E\.1E4: objective\-order equivalence

For a verified map pairing candidate pointyywith reference pointx=φ​\(y\)x=\\varphi\(y\), define the strict and weak preference relations induced by the recorded objective sense\.

###### Definition E\.1\(E4\)\.

E4 is positive when, for every paired feasibley1,y2y\_\{1\},y\_\{2\},

fR​\(φ​\(y1\)\)⪯RfR​\(φ​\(y2\)\)⇔fC​\(y1\)⪯CfC​\(y2\),f\_\{R\}\(\\varphi\(y\_\{1\}\)\)\\preceq\_\{R\}f\_\{R\}\(\\varphi\(y\_\{2\}\)\)\\iff f\_\{C\}\(y\_\{1\}\)\\preceq\_\{C\}f\_\{C\}\(y\_\{2\}\),where⪯M\\preceq\_\{M\}uses the sense of modelMM\.

###### Proposition E\.2\(Positive\-affine objective certificate\)\.

If the senses agree and, on paired feasible points,

fC​\(y\)=α​fR​\(φ​\(y\)\)\+βfor exact​α\>0,β∈ℚ,f\_\{C\}\(y\)=\\alpha f\_\{R\}\(\\varphi\(y\)\)\+\\beta\\qquad\\text\{for exact \}\\alpha\>0,\\ \\beta\\in\\mathbb\{Q\},then E4 holds\.

###### Proof\.

A strictly positive affine transform preserves all weak, strict, and equality comparisons\. The additive constant cancels in pairwise differences\. ∎

The implemented positive forms include identity, supported lifts, and binary complements that induce an exact positive\-affine identity\. A supported negative is a pair of feasible points whose rankings disagree, re\-checked against both models and the named map\.

### E\.2E5: optimal\-value equality

###### Definition E\.3\(E5\)\.

E5 asks whethervR∗=vC∗v\_\{R\}^\{\*\}=v\_\{C\}^\{\*\}as extended\-real values under the original variable domains and recorded senses\.

###### Proposition E\.4\(Primal–dual optimum certificate\)\.

For a continuous rational LP, a primal\-feasible point and a dual\-feasible point with equal objective values certify the exact optimum by weak duality\. If such certificates forRRandCCyield the same rational value, E5 is positive\.

###### Proof\.

Weak duality places every primal objective on one side of every dual objective\. Equality of a feasible primal and dual pair closes the bound and proves optimality\. Repeating this for both models and comparing the exact values proves E5\. ∎

For integer or binary variables, an LP\-relaxation dual certificate does not certify the integer optimum and is refused\. Bounded 0–1 cases may instead use exact enumeration\. E5 can also be implied by a certified feasible\-set equality and objective identity, but the report records those premises rather than silently transferring a global equivalence label\.

### E\.3E6: optimizer\-set equivalence

###### Definition E\.5\(E6\)\.

E6 is positive when the recorded admissible map restricts to a bijection betweenXC∗X\_\{C\}^\{\*\}andXR∗X\_\{R\}^\{\*\}\.

###### Proposition E\.6\(Optimizer transport\)\.

Supposeφ\\varphiis a bijection betweenFCF\_\{C\}andFRF\_\{R\}and E4 holds\. Theny∈XC∗y\\in X\_\{C\}^\{\*\}if and only ifφ​\(y\)∈XR∗\\varphi\(y\)\\in X\_\{R\}^\{\*\}, soφ\\varphirestricts to an optimizer\-set bijection\.

###### Proof\.

Ifyyis candidate\-optimal, no feasibley′y^\{\\prime\}is strictly preferred\. E4 transports this ordering to the reference set, and feasible\-set bijectivity ensures every reference competitor has a candidate preimage\. Thereforeφ​\(y\)\\varphi\(y\)is reference\-optimal\. The reverse direction follows fromφ−1\\varphi^\{\-1\}\. ∎

E6 accepts positive certificates only for forms with an exact certified inverse on optimizers \(identity and the supported 0–1 complement involution\)\. The implemented schema has no certified\-negative E6 type\. Consequently, unsupported or unproved cases areunknown, neverfalse\. E3 equality alone does not imply E6 because its section is only a right inverse and need not represent every candidate optimizer uniquely\.

### E\.4Explicit non\-implications

Table 5:Why the profile cannot be collapsed into a deepest passing level\.

## Appendix FCertificate Construction, Independent Replay, and Algorithms

### F\.1End\-to\-end evaluator

Algorithm 1Prerequisite\-aware construction of one E0–E6 profile0:cell

zz, fixed provider configuration

θ\\theta, cohort hash

hh
1:Load the response identified by fingerprint

\(z,θ\)\(z,\\theta\), or record providerabsent\.

2:ifno successful response existsthen

3:Set E0–E6 toabsent; record provider status;

4:return\.

5:endif

6:Extract at most one program; execute under the 30\-s cap; ingest the exported LP/MPS exactly\.

7:Set E0 from construction and ingestion\.

8:ifE0 is nottruethen

9:Set E1–E6 toabsent; record the profile;

10:return\.

11:endif

12:Exhaustively propose and exactly check every map in the declared E1 family\.

13:ifno admissible map is foundthen

14:Set E1 tounknownand E2–E6 toabsent; record the profile;

15:return\.

16:endif

17:Set E1 totrueand run E2–E6 in order under one 120\-s pair\-level wall cap\.

18:Serialize each proposed certificate or witness and independently replay it\.

19:Emit a decided fact only if replay succeeds; otherwise emit the appropriate typed abstention\.

20:Store checkpoints, hashes, evidence, baseline records, and the profile\.

Prerequisite normalization follows one rule for every profile: an unmet prerequisite isabsent, whereas N/A is reserved for a relation that is mathematically inapplicable after all prerequisites hold\. This distinction is used in Tables[9](https://arxiv.org/html/2607.29431#A8.T9)and[10](https://arxiv.org/html/2607.29431#A8.T10)\.

### F\.2Deterministic E1 search and applicability

The evaluation uses no LLM map proposer\. The implementation exhaustively runs its deterministic proposer list, de\-duplicates identical maps, and checks each proposal structurally before it can support any downstream claim\. The declared family evaluated for every E1 profile is

> stable\-name\-match; original\-name\-match; identity; signature\-permutation; binary\-complement; affine\-lift\.

Name matching yields either a same\-space coordinate map or, when the candidate contains additional variables, a projection map\. Identity and signature permutation require equal dimension\. Binary complement is proposed only for pure binary same\-space pairs and is then rechecked exactly\. The affine\-lift proposal records projected reference coordinates; E3 separately verifies the projection/section obligations\.

E1 istrueif at least one proposal is admissible andunknownif the complete declared family yields none\. It is never a certified negative\. Once E1 istrue, E2 is applicable only to admissible same\-space maps\. Seven formal cells \(two GPT\-5\.4 and five Claude Sonnet 4\.6\) contain an admissible affine\-lift map but no admissible same\-space map; their E2 state is therefore N/A rather thanunknown\. E3 then records whether the supported affine\-lift schema can be certified\.

Algorithm 2E2 relation under the complete declared same\-space map universe0:exact models

\(MC,MR\)\(M\_\{C\},M\_\{R\}\)and admissible E1 maps

Φadm\\Phi\_\{\\mathrm\{adm\}\}
1:

Φs←\{φ∈Φadm:φ​is same\-space\}\\Phi\_\{s\}\\leftarrow\\\{\\varphi\\in\\Phi\_\{\\mathrm\{adm\}\}:\\varphi\\text\{ is same\-space\}\\\}
2:if

Φs=∅\\Phi\_\{s\}=\\varnothingthen

3:

4:returnN/A\.

5:endif

6:foreach

φ∈Φs\\varphi\\in\\Phi\_\{s\}do

7:Normalize

φ​\(FC\)\\varphi\(F\_\{C\}\)and

FRF\_\{R\}in a common exact coordinate system\.

8:Certify

φ​\(FC\)⊆FR\\varphi\(F\_\{C\}\)\\subseteq F\_\{R\}, or verify a separating point\.

9:Certify

FR⊆φ​\(FC\)F\_\{R\}\\subseteq\\varphi\(F\_\{C\}\), or verify a separating point\.

10:Store the per\-map relation implied by the two verified directions\.

11:endfor

12:ifsome map is certified equalthen

13:

14:returntruewith that map and both directional certificates\.

15:elseifevery map has a verified non\-equality witnessthen

16:

17:returnfalse\_within\_declared\_universewith the complete map manifest and witnesses\.

18:elseifthe pair\-level cap was reachedthen

19:

20:returnunknown\_resource\.

21:else

22:

23:returnunknown\.

24:endif

### F\.3Independent replay and evidence schema

Algorithm 3Independent replay of a proposed relation fact0:normalized model hashes, named map, relation claim, serialized evidence

1:Re\-load the exact models and verify all source hashes\.

2:Re\-check map admissibility without consulting constructor booleans\.

3:Dispatch on evidence type: Farkas multipliers, separating point, affine projection/section, objective identity or ranking witness, primal/dual optimum certificate, or optimizer bijection\.

4:Recompute rational identities, domain membership, feasibility, strict violations, and right\-inverse identities as applicable\.

5:ifevery obligation holds exactlythen

6:

7:returnverified\.

8:else

9:

10:returnrejected; the proposed decided fact is removed\.

11:endif

The replay verifier reads neither natural\-language prompts nor solver status strings\. Each evidence record contains the cell and cohort identifiers, exact model hashes, map identifier, relation and directional obligation, rational multipliers/points/matrices/vectors, constructor status, verifier status, checkpoint timing, and source hashes\. Reported re\-verification denominators count dimension\-verdict artifacts rather than unique cells; one cell can contribute multiple E4–E6 artifacts\.

### F\.4Exactness, support envelope, and timeout semantics

Gurobi is used for candidate construction/export, LP/MPS parsing support, and the external value and structural baselines\. It is not the E1–E6 certifier\. Exact acceptance uses rational arithmetic in the certifying tradition ofApplegateet al\.\([2007](https://arxiv.org/html/2607.29431#bib.bib20)\); Cooket al\.\([2013](https://arxiv.org/html/2607.29431#bib.bib21)\)\. Continuous linear containment uses Farkas certificates or exact separating witnesses; bounded pure\-binary cases use complete enumeration where declared\. Unsupported general\-integer containment, unimplemented lift schemas, and unavailable optimizer\-set negatives produce typed abstentions rather than guessed booleans\.

The 120\-s limit is one hard wall\-clock cap for the complete E1–E6 pair evaluator, not a fresh 120 s for every dimension\. The evaluator records a checkpoint before each dimension\. If the cap is reached, E0 and all completed dimensions keep their recorded outcomes; the in\-progress dimension and every unreached successor are set tounknown\_resource\. Consequently, the cap\-hit statistic is a union over cells, whereas the per\-dimension resource counts are cumulative\. Provider responses are identified by request fingerprints\.

## Appendix GCohort, Models, Prompt Contract, and Statistical Protocol

### G\.1Cohort construction and eligibility

Table 6:Disjoint and exhaustive Bench4Opt paired\-base accounting\. Only the 173\-base formal cohort contributes to primary results\.Bench4Opt contains 394 Structured/Unstructured records, grouped into 197 paired base problems\(Wanget al\.[2025](https://arxiv.org/html/2607.29431#bib.bib1)\)\. Eligibility is determined from reference artifacts only\. The 20\-base pilot subset is defined by sorting canonical base indices and taking the first 20 reference pairs inside the declared linear envelope, skipping unsupported base 0016; this gives bases 0000–0015 and 0017–0020\. For the remaining 177 bases, inclusion requires \(i\) both paired records, \(ii\) exact E0\-successful ingestion of the reference LP, and \(iii\) membership in \{continuous LP, bounded pure binary, general\-integer MILP\}\. Candidate outputs play no role in selection\. The formal stratum counts are 112, 29, and 32, respectively\.

Table 7:Unsupported reference instances\. No paired record is malformed or missing\.The formal cohort hash is

e9ad20181d447143a3b53b377426af88d 395753cfd6f733eac0872373376b31c

The accompanying reproducibility archive includes the 197\-base eligibility record, the pilot list, the 173\-base manifest, and the four exclusion reasons\.

### G\.2Model aliases and generation protocol

Table 8:Generation and evaluation protocol\. No model\-specific prompt adaptation is used\.The exact template, model configuration files, request fingerprints, and credential\-free provider\-status records are included in the reproducibility archive\. Provider aliases are reported exactly as used by the evaluation client\. The provider did not expose immutable served checkpoint hashes, so model aliases and request fingerprints are the strongest available identifiers\.

### G\.3Software environment

The local evaluator and the ORGEval\-style baseline implementation used in our harness run under Python 3\.9\.7 on Windows 11, build 26100, with Gurobi 10\.0\.2, NetworkX 2\.6\.3, and NumPy 1\.26\.4\. Exact verification additionally uses Python’sfractions\.Fraction\. Provider\-side hardware is not observable\. CPU and RAM identifiers were not recorded in the profile metadata; the archive provides a replay environment specification and a system\-information collector\.

### G\.4Provider\-aware and prerequisite\-aware accounting

Provider delivery status is reported separately from model semantics\. A terminal provider/API failure before a response yields E0–E6absent\. All 346 GPT\-5\.4 cells have successful responses\. Claude Sonnet 4\.6 has 337 successful responses and nine terminal read\-timeout errors; among successful responses, 156 are E0trueand 181 are E0false\. Qwen has 329 successful responses and 17 terminal provider errors; among successful responses, 196 are E0true, 131 are E0false, and two areunknown\_unsupported\.

Among the 190 Claude Sonnet 4\.6 cells without an E0\-truecandidate, 181 are candidate\-level E0falseoutcomes and nine are provider absences\. All E1–E6 denominators condition on the 156 E0\-truecells\.

### G\.5Statistical unit

Profile counts use the cell as unit; Structured–Unstructured comparisons use the 173 paired base problems\. The paired analysis uses five binary end\-to\-end indicators: E0 success, E1 map found, E2 decided, E5 decided, and E6 decided\. Table[12](https://arxiv.org/html/2607.29431#A9.T12)reports exact two\-sided McNemar tests and 10,000 base\-level paired bootstrap resamples with seed 13\. Holm correction covers all 15 model\-by\-indicator tests\. These analyses describe the evaluated cohort and do not establish universal prompt effects\.

## Appendix HComplete Formal Results and Baseline Outputs

### H\.1Stage\-wise outcome accounting

MetricGPT\-5\.4SonnetQwenCells346346346Successful API responses346337329Provider/API error; E0absent0917E0true334156196Candidate\-level E0false12181131E0unknown\_unsupported002E1 map found / E0true277/334130/156164/196E1unknown572632E2 decided / E1true114/27745/13087/164E2true/false\_within\_declared\_universe108/641/484/3E2unknown/ N/A116/256/550/0E2unknown\_resource452427E3 decided000E4 decided1394091E5true/false107/4236/3179/22E6true701658Evidence artifacts independently verified358/358123/123250/250Cells hitting at least one 120\-s cap703539Worker termination/corrupt profiles000Table 9:Stage\-wise summary after provider and prerequisite normalization\. The model columns are GPT\-5\.4, Claude Sonnet 4\.6, and Qwen3\.5\-397B\-A17B\. Conditional denominators are explicit; complements are not automatically semantic errors\.Table 10:Complete prerequisite\-normalized typed outcome matrix over all 346 cells per model\.F𝒰F\_\{\\cal U\}denotesfalse\_within\_declared\_universe;UrU\_\{r\},UuU\_\{u\}, and A denoteunknown\_resource,unknown\_unsupported, andabsent\. Every row sums to 346\.
### H\.2Complete typed outcome matrix

Table[10](https://arxiv.org/html/2607.29431#A8.T10)is exhaustive: every dimension row totals 346\. For Qwen, E4–E6 areabsentin 182 cells because E0 or E1 is not established\. The corresponding E4/E5/E6unknowncounts are 40, 25, and 67, and theunknown\_resourcecounts are 33, 38, and 39\.

### H\.3External baseline outputs

Baseline outcomeGPT\-5\.4Sonnet 4\.6Qwen3\.5Value match: equal16954108Value match: not equal766251Value match: abstain894037Value match: absent \(no E0\-true candidate\)12190150ORGEval: equivalent16884110ORGEval: not equivalent1637184ORGEval: unknown312ORGEval: absent \(no E0\-true candidate\)12190150Execution\-success overestimation493525ORGEval rejection despite E2 equality25818Strict value\-match false acceptance000Table 11:Baseline outputs and relation\-specific certified discrepancies\. Baseline “absent” combines every cell without an E0\-true candidate, including provider absence, because no baseline pair exists\.An ORGEval rejection despite E2 equality means that the harnessed ORGEval implementation returnsnot\_equivalentwhile E2 certifies mapped feasible\-set equality under a verified map\. This is an E2\-specific discrepancy, not a claim of complete profile equality\. A strict value\-match false acceptance requires value equality together with an E2\-certified strict/incomparable feasible\-set relation; none is observed\.

## Appendix IPaired Conditions, Case Study, and Failure Taxonomy

### I\.1Structured versus Unstructured paired statistics

Table 12:Base\-paired Structured \(S\) versus Unstructured \(U\) descriptive analysis for all three models\. Exact two\-sided McNemar tests use discordant pairs; confidence intervals use 10,000 paired base\-level bootstrap resamples with seed 13; Holm correction covers the 15 model\-by\-indicator tests\.No row remains significant after the 15\-test Holm correction\. The smallest raw values are Claude Sonnet 4\.6 E2 \(p=0\.0241p=0\.0241\), GPT\-5\.4 E1 \(p=0\.0294p=0\.0294\), and Qwen E1 \(p=0\.0488p=0\.0488\); their adjusted values are 0\.362, 0\.412, and 0\.634\. The table therefore supports only descriptive coverage patterns\.

### I\.2Replayable certified case

ForB4O\_BASE\_0031under the Unstructured condition, the Claude Sonnet 4\.6 candidate and reference each contain five binary variables and 18 inequalities\. E1 verifies the identity map\. Complete enumeration over all25=322^\{5\}=32assignments independently verifies both E2 containments\. The profile stores E1/E2 replay status in the map\-level containment evidence, where both directional checks are independently verified\. E4, E5, and E6 also verify positive; E3 is N/A because no auxiliary variables exist\. ORGEval nevertheless returnsnot\_equivalent, and the value baseline returnsnot\_equal, illustrating why baseline labels must be tied to their precise relation\. This is the case visualized in Main Figure 2\.

### I\.3Failure taxonomy

Analysis keeps the following categories disjoint: terminal provider/API error; successful response without an extractable program; execution/export failure; unsupported serialized model; no admissible E1 map in the complete declared family; certified semantic negative; unresolved semantic search; resource cap; mathematically inapplicable relation; and downstream absence after a failed prerequisite\. This is why E0 failure, E1 coverage, semantic disagreement, and resource abstention are not collapsed into one error rate\.

## Appendix JReproduction Procedure and Artifact Contract

### J\.1Reproducibility archive contents

The reproducibility code/data archive is organized as follows:

- •code/certequivbench/: ingestion, mapping, relation construction, independent verification, baselines, cohort eligibility, and reporting code;
- •artifacts/cohort/: the 197\-base eligibility record, 20 pilot IDs, 173\-base manifest, and four unsupported records;
- •artifacts/profiles/: all 1,038 per\-cell profiles;
- •artifacts/candidates/: candidate programs where available; normalized candidate models and their hashes are retained in the per\-cell profiles; exported LP/MPS files were not retained;
- •artifacts/baselines/: per\-cell value and ORGEval records;
- •artifacts/provider\_status/: credential\-free call status, model alias, fingerprint, retry, error category, and usage metadata;
- •analysis/: normalization, table\-generation, paired\-analysis, and selected\-case scripts plus their deterministic outputs;
- •environment/: replay requirements, the recorded provenance, and a system\-information collector\.

Raw API keys, author identities, absolute personal paths, and provider response text are excluded\. The third\-party Bench4Opt corpus is not duplicated; the manifest supplies stable IDs and hashes, and the README explains how to place an authorized local copy for full re\-ingestion\.

### J\.2Replay sequence and invariants

A reproducer first verifies the archive manifest and cohort hash, installs the specified environment, and places Bench4Opt at the documented local path\. The replay then \(i\) executes the reference\-support eligibility check, \(ii\) ingests the recorded candidate models without provider access, \(iii\) independently verifies all certificates and witnesses, \(iv\) rebuilds normalized profile and baseline summaries, \(v\) recomputes the 10,000\-resample paired analysis with seed 13, and \(vi\) compiles the appendix and checklist\. The process fails closed on a cohort hash, cell identity, model hash, evidence verdict, conditional denominator, provider\-category partition, or cap\-accounting mismatch\.

### J\.3Claim\-to\-evidence index

- •Profile is not a hierarchy\.Main Secs\. 1, 3\.1, and 3\.4; Supp\. A and E\. Replay the non\-implication examples and prerequisite DAG\.
- •E2 equality is sound\.Main Sec\. 3\.3; Supp\. C\. Check two directional Farkas certificates or complete finite enumeration\.
- •E2 aggregate negatives are scoped\.Main Sec\. 3\.3; Supp\. C\.3\. Check the complete declared map manifest and a verified witness for every map\.
- •E3 affine\-lift equality is sound\.Main Sec\. 3\.3; Supp\. D\. Check projection/section matrices, two containments, and the exact right\-inverse identity\.
- •E4–E6 are distinct\.Main Sec\. 3\.4; Supp\. E\. Check objective identities or ranking witnesses, optimum certificates, and optimizer bijections\.
- •Decided facts are independently checked\.Main Secs\. 4\.1–4\.2; Supp\. F\. Replay serialized evidence with the independent verifier\.
- •Three\-model counts share one cohort\.Main Secs\. 5\.1–5\.2; Supp\. G–H\. Check the cohort manifest/hash and per\-cell profile matrix\.
- •Baseline discrepancies are relation\-specific\.Main Sec\. 5\.3; Supp\. H–I\. Join each baseline record to its E2/E4–E6 profile by cell ID\.
- •Provider failures are not E0 failures\.Main Secs\. 5\.1–5\.2; Supp\. G\.4 and H\. Check provider\-status records and the normalized typed\-outcome matrix\.
- •Paired prompt results are descriptive\.Main Sec\. 5\.4; Supp\. G\.5 and I\.1\. Recompute the paired matrix, seed\-13 bootstrap, McNemar tests, and Holm correction\.

## Appendix KInterpretive Clarifications

#### IsModelEquivBencha new dataset?

No\. It is an evaluator and certifying artifact system; Bench4Opt supplies the experimental instances\.

#### Do E0–E6 define an equivalence ladder?

No\. E0 and E1 are prerequisites/alignments; E2 and E3 compare different spaces; E4–E6 ask distinct objective and solution questions\.

#### Does E1unknownmean non\-equivalence?

No\. It means the complete finite declared family yielded no admissible map\.

#### When is a state N/A rather thanabsent?

N/A requires satisfied prerequisites and mathematical inapplicability\. For example, E2 is N/A when E1 found only an affine\-lift map, and E3 is N/A when a same\-space map leaves no auxiliary variables\. If E0 or E1 fails, downstream relations areabsent\.

#### Why is E3 decided on zero formal cells?

No formal cell both required and satisfied the one implemented affine\-lift certificate schema\. This is a coverage result, not a counterexample to the E3 theorem\.

#### Why can E5 be positive while a value baseline says not equal?

The baseline may compare a solver\-derived or relaxed scalar, whereas E5 is accepted only from exact relation\-specific evidence for the declared domains\.

#### Why can ORGEval reject an E2\-equal pair?

A structural graph comparison can distinguish alternative encodings even when exact mapped feasible sets coincide\. The discrepancy is relation\-specific\.

#### Why only one generation per cell?

The protocol evaluates one output per cell and excludes repair or best\-of\-kkselection\. It therefore does not estimate within\-model sampling variance\.

## Appendix LLimitations, Machine\-Readable Contract, and Responsible Use

The guarantees are conditional on exact ingestion, the named admissible map, the supported certificate envelope, and the correctness of the independent verifier\. They do not prove that the reference model captures the source natural\-language intent\. The mapping family is finite, E3 implements one lift schema, general\-integer containment remains incomplete, and E6 has no certified negative type\. Exact procedures may exhaust the pair\-level resource cap\. The empirical study uses three provider aliases, one fixed prompt, and one sample per condition; it is diagnostic rather than a universal ranking\.

### L\.1Machine\-readable profile contract

A portable profile record exposes at least

> cell\_id, base\_id, model\_alias, condition, cohort\_hash; provider\_status, request\_fingerprint, candidate\_status, e0\_status; e1\_status, declared\_map\_family, searched\_maps\[\], admissible\_maps\[\]; e2\.\.e6: status, relation, map\_id, reason, evidence\_id, verifier\_status; elapsed\_seconds, pair\_cap, checkpoint, baselines, source\_hashes, environment\_fingerprint\.

Provider status is separate from E0\. Each downstream entry carries its map and prerequisite context\. Replay status is recorded either at the relation level or in the referenced map\-level evidence object; the verifier resolves the referenced evidence before assigning the relation outcome\.

### L\.2Threats to validity

#### Construct validity\.

The reference is treated as ground truth\.ModelEquivBenchmeasures candidate\-to\-reference semantics, not whether either model faithfully captures the source problem\.

#### Internal validity\.

Separate construction and replay paths, exact arithmetic, hashes, and fail\-closed routing reduce but cannot eliminate implementation defects\. The provider\-aware normalization is deterministic and preserves the source records\.

#### External validity\.

Conclusions are limited to the supported Bench4Opt cohort, the three served aliases, the fixed prompt/output contract, and the recorded software envelope\.

#### Statistical conclusion validity\.

Primary tables are exact finite\-cohort counts\. Paired tests characterize the 173 bases and are not estimates of an open\-ended model population\.

### L\.3Responsible use

The evaluator may expose generated code and optimization artifacts\. Any shared archive must remove credentials, identities, absolute personal paths, and non\-redistributable provider content\. Certification against a reference model must not be presented as validation of a real\-world deployment without separate checks of reference correctness, data provenance, operational constraints, and domain consequences\.