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

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

Penglin Zhu, Jungang Xu \corresponding

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 present ModelEquivBench , a certifying, multi-relational evaluation system that reports a per-pair semantic profile E ​ 0 E0 – E ​ 6 E6 : model construction and exact ingestion ( E ​ 0 E0 ), verified representation alignment ( E ​ 1 E1 ), same-space and projected feasible-set relations ( E ​ 2 E2 , E ​ 3 E3 ), objective-order equivalence ( E ​ 4 E4 ), optimal-value equality ( E ​ 5 E5 ), and optimizer-set equivalence ( E ​ 6 E6 ). Each decided entry carries relation-appropriate, independently re-checkable evidence: replayable traces or explicit maps for E ​ 0 E0 – E ​ 1 E1 , exact-rational certificates for positive E ​ 2 E2 – E ​ 6 E6 conclusions, and explicit witnesses for supported negatives. Incomplete mapping search, unsupported structure, and resource limits produce typed unknown or N/A outcomes rather than guesses, while unmet prerequisites are reported as absent . Using ModelEquivBench to 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: 49 49 , 35 35 , and 25 25 cells contain executable candidates that are nevertheless certified negative on at least one supported relation, and 25 25 , 8 8 , and 18 18 structural rejections occur on pairs for which E ​ 2 E2 certifies 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.

1 Introduction

Large language models (LLMs) are increasingly used to turn natural-language problem descriptions into runnable optimization models (Ramamonjison et al. 2022 ; AhmadiTeshnizi et al. 2024 ; Xiao et al. 2024 ; Huang et al. 2025 ) . 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 (Wang et al. 2025 ; Zhai et al. 2025 ) . 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 is ModelEquivBench , a certifying, multi-relational evaluation system that reports a per-pair semantic profile of seven dimensions, E ​ 0 E0 – E ​ 6 E6 , summarized in Table 1 . The dimensions range from model construction and exact ingestion ( E ​ 0 E0 ), through verified representation alignment ( E ​ 1 E1 ) and feasible-set relations in the aligned space ( E ​ 2 E2 ) and under an affine lift ( E ​ 3 E3 ), to objective order ( E ​ 4 E4 ), optimal value ( E ​ 5 E5 ), and optimizer sets ( E ​ 6 E6 ). Crucially, E ​ 0 E0 – E ​ 6 E6 form 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.

ModelEquivBench is certifying : each decided entry carries relation-appropriate evidence that an independent checker can re-verify. E ​ 0 E0 uses a replayable execution/ingestion trace, E ​ 1 E1 an explicit admissible map, and positive E ​ 2 E2 – E ​ 6 E6 conclusions 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 typed unknown or N/A outcomes; failed prerequisites make later dimensions absent . The bidirectional feasible-set containment engine we call Certifying Mapped-Containment (CMC) is the principal technical engine for E ​ 2 E2 and the supported part of E ​ 3 E3 ; it is a component inside ModelEquivBench , not a replacement for the E ​ 0 E0 – E ​ 6 E6 profile.

We instantiate ModelEquivBench on 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 of 173 173 base problems, each under paired Structured and Unstructured conditions ( 346 346 cells per model), with one generation per condition at temperature 0.0 0.0 and no repair or resampling . Their profiles differ sharply. GPT-5.4 produces ingestible candidates for 334 / 346 334/346 cells, compared with 156 / 346 156/346 for Claude Sonnet 4.6 and 196 / 346 196/346 for Qwen3.5-397B-A17B. Conditional E ​ 1 E1 coverage is nevertheless similar: 277 / 334 277/334 ( 82.9 % 82.9% ), 130 / 156 130/156 ( 83.3 % 83.3% ), and 164 / 196 164/196 ( 83.7 % 83.7% ). Qwen3.5-397B-A17B additionally records 17 17 provider/API errors before candidate creation; these are reported as E0 absent , not model-quality failures. Exact certification reveals 49 49 , 35 35 , and 25 25 execution-success overestimations and 25 25 , 8 8 , and 18 18 structural rejections despite E ​ 2 E2 -certified mapped feasible-set equality. Our contributions are: (1) ModelEquivBench , the E ​ 0 E0 – E ​ 6 E6 certifying 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.

Figure 1: The ModelEquivBench certifying E ​ 0 E0 – E ​ 6 E6 workflow. E ​ 0 E0 and E ​ 1 E1 establish prerequisites; E ​ 2 E2 – E ​ 6 E6 ask parallel, relation-specific questions. Decided facts carry replayable certificates or witnesses, while unresolved entries remain typed outcomes rather than a global verdict.

2 Related Work

2.1 LLM 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 (Ramamonjison et al. 2022 ) , agentic decomposition systems (AhmadiTeshnizi et al. 2024 ; Xiao et al. 2024 ) , and trained modelers (Huang et al. 2025 ; Lu et al. 2025 ) . 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 (Zhai et al. 2025 ) ; EquiBench studies LLMs’ program-equivalence reasoning (Wei et al. 2025 ) . These approaches target an overall equivalence judgment, whereas ModelEquivBench reports separately certified relations and typed abstentions.

2.2 Structural Comparison and Certifying Verification

Structural model comparison.

ORGEval compares optimization models by graph-theoretic canonicalization (Wang et al. 2025 ) . Structural matching is efficient but can reject pairs whose feasible sets coincide after a verified change of representation; our E ​ 2 E2 relation 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 ) to certified integer-programming reasoning (Cheung et al. 2017 ; Hoen et al. 2024 ; van Doornmalen et al. 2023 ; Bogaerts et al. 2022 ) . Feasible-set containment rests on Farkas’ lemma and polyhedral theory (Schrijver 1986 ) ; projected polyhedra and extended formulations are studied by Yannakakis ( 1991 ) , Conforti et al. ( 2013 ) , Kellner ( 2015 ) , and Liberti ( 2009 ) . Exact rational LP/MIP methods (Applegate et al. 2007 ; Cook et al. 2013 ) make the resulting evidence checkable without additional floating-point error during verification. We adapt these tools into ModelEquivBench , in which every decided fact is independently re-verified using exact arithmetic.

3 The ModelEquivBench Framework

3.1 Models, Evidence Policy, and Outcome States

Models.

Let M M have n M n{M} decision variables collected in x = ( x 1 , … , x n M ) ⊤ x=(x{1},\ldots,x{n{M}})^{\top} , with per-coordinate domains D M , i D{M,i} (continuous, integer, or binary) and D M = ∏ i D M , i ⊆ ℝ n M D{M}=\prod{i}D{M,i}\subseteq\mathbb{R}^{n{M}} . Its feasible set is F M = { x ∈ D M : A ub ​ x ≤ b ub , A eq ​ x = b eq } F{M}={x\in D{M}:A{\mathrm{ub}}x\leq b{\mathrm{ub}},,A{\mathrm{eq}}x=b{\mathrm{eq}}} ; it has linear objective f M ​ ( x ) = obj M ⊤ ​ x f{M}(x)=\mathrm{obj}{M}^{\top}x , sense in { min , max } {\min,\max} , optimal value opt ​ ( M ) \mathrm{opt}(M) in the extended reals, and optimizer set argopt ​ ( M ) \mathrm{argopt}(M) . Empty-set conventions apply, and all coefficients are stored as exact rationals. We write R , C R,C for reference and candidate, with ingested feasible sets F R , F C F{R},F_{C} (bounds folded into inequalities). ModelEquivBench derives 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 from E ​ 2 E2 onward 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 guessed false outcomes. Unmet prerequisites are recorded separately as absent .

Dim.

Relation compared

Positive evidence / negative witness

Typed abstention

E0

Candidate code builds a structurally valid exact-rational model that ingests

Re-runnable parse/build trace; FALSE carries the failing trace

unknownresource (exec. cap); unknownunsupported (e.g. quadratic)

E1

A verified admissible alignment φ ∈ Φ adm \varphi\in\Phi_{\mathrm{adm}} exists (type/domain-compatible)

Explicit φ \varphi (permutation, complement, sign, or affine lift), re-checked exactly

unknown : no map found in the searched family (coverage-limited, never false )

E2

Same-space feasible-set relation φ ​ ( F C ) \varphi(F{C}) vs. F R F{R} (equal / strict rel. / strict restr. / incomparable)

Two-way Farkas containment multipliers (equal); separating witness ( false_within )

unknown if no certified-equal and universe not exhaustive; unknown_resource

E3

Projected relation of a lifted candidate: π ​ ( F C ) \pi(F{C}) vs. F R F{R} under section σ \sigma

Farkas obligations for π ​ ( F C ) ⊆ F R \pi(F{C})!\subseteq!F{R} , σ ​ ( F R ) ⊆ F C \sigma(F{R})!\subseteq!F{C} , π ∘ σ = id \pi!\circ!\sigma!=!\mathrm{id}

unknown outside the affine-lift schema; n/a if no auxiliary vars

E4

Objective-order equivalence under φ \varphi

Identity/lift/complement objective identity; FALSE: two oppositely ranked points

unknown ; n/a

E5

Optimal-value equality opt ​ ( R ) = opt ​ ( C ) \mathrm{opt}(R)=\mathrm{opt}(C)

Two LP weak-duality sandwiches (LPs only; not used for integer models); implications from E2/E3

unknown ; unknown_resource ; n/a

E6

Optimizer-set bijection argopt ​ ( R ) ↔ argopt ​ ( C ) \mathrm{argopt}(R)!\leftrightarrow!\mathrm{argopt}(C)

Identity or 0–1 complement involution certificate (positive-only)

unknown (no certified-negative type); n/a

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, whereas absent means that an upstream prerequisite was not met. ur = unknownresource ; falsewithin = falsewithindeclared_universe .

Outcome states and definedness.

A profile entry is not merely true or false . A dimension may also be unknown because the supported procedure established neither a positive conclusion nor a supported negative conclusion, unknownresource because its resource budget was exhausted, unknownunsupported because the model lies outside the implemented envelope, or N/A because the relation is mathematically inapplicable. We reserve absent for a different situation: an upstream prerequisite was not established, so the later dimension was never evaluated. For example, if no candidate model ingests, E ​ 4 E4 is absent , not N/A; if a same-space candidate has no auxiliary variables, E ​ 3 E3 is N/A. This distinction matters both logically and statistically. A rate such as “ E ​ 2 E2 decided given E ​ 1 E1 ” conditions on the dimensions that were actually entered, whereas a cohort-wide count retains absent cells 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.2 Construction and Representation Alignment

E ​ 0 E0 : construction and exact ingestion.

E ​ 0 E0 asks whether the candidate code executes and yields a structurally valid exact-rational model that ingests. It is true with a re-runnable build trace, false with the failing parse/build/execution trace, unknownresource when the execution cap is exceeded, and unknownunsupported for a valid but out-of-envelope construct (e.g. a quadratic objective). E ​ 0 E0 does not require a solver result: infeasible and unbounded models may still be E ​ 0 E0 true . E ​ 0 E0 is established from ingestion and checkpointed before any later work, so a downstream timeout cannot corrupt it.

E ​ 1 E1 : verified representation alignment.

Because a candidate may name and order variables differently, E ​ 1 E1 searches 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 complement x ↦ 1 − x x\mapsto 1-x (0–1 only), and sign negation x ↦ − x x\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 ​ 1 E1 is true if at least one admissible φ \varphi is verified and unknown if none is found in the searched family. Critically, E ​ 1 E1 is never false : absence of a found map is not proof that no map exists, so the outcome is coverage-limited, not a refutation.

3.3 Feasible-Set Relations

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

Fixing a verified same-space φ \varphi , E ​ 2 E2 compares the mapped candidate feasible set φ ​ ( F C ) \varphi(F{C}) with F R F{R} as subsets of the same semantic variable space and classifies the pair as equal ( F R = φ ​ ( F C ) F{R}=\varphi(F{C}) ), strict relaxation ( F R ⊊ φ ​ ( F C ) F{R}\subsetneq\varphi(F{C}) ), strict restriction ( φ ​ ( F C ) ⊊ F R \varphi(F{C})\subsetneq F{R} ), incomparable , or unknown . Each containment direction P ⊆ Q P\subseteq Q is certified by exact nonnegative Farkas multipliers ( μ , λ ) (\mu,\lambda) with a ⊤ = μ ⊤ ​ G + λ ⊤ ​ H a^{\top}=\mu^{\top}G+\lambda^{\top}H and β ≥ μ ⊤ ​ h + λ ⊤ ​ h eq \beta\geq\mu^{\top}h+\lambda^{\top}h{\mathrm{eq}} for every row ( a , β ) (a,\beta) of Q Q ; a failure to contain is witnessed by a feasible point of P P violating a specific row of Q Q . 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 ​ 2 E2 is true if some admissible φ \varphi is certified equal (and re-verified); it is falsewithindeclareduniverse only if that universe is exhaustive and every map in it separates with a re-verified witness (no equal, no unknown); otherwise it is unknown . The universe is declared exhaustive only when the type-compatible permutation family is fully enumerable ( n ≤ 7 n\leq 7 ) and no binary coordinate is present, since binary complements are not exhaustively enumerated. Thus falsewithindeclared_universe is 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 aggregate E ​ 2 E2 outcome is essential. A certified strict restriction under a particular φ \varphi does 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 still unknown . 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 ​ 3 E3 : projected feasible-set relation.

When the candidate carries auxiliary variables, E ​ 3 E3 compares F R F{R} with the projection of the higher-dimensional F C F{C} . With an affine projection π : ℝ n C → ℝ n R \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— π ​ ( F C ) ⊆ F R \pi(F{C})\subseteq F{R} , σ ​ ( F R ) ⊆ F C \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 π ​ ( F C ) = F R \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) yield unknown , and same-space cases with no auxiliary variables are N/A. If a prerequisite such as E ​ 0 E0 or E ​ 1 E1 is missing, E ​ 3 E3 is absent rather than N/A. We stress that E ​ 3 E3 is not a level above E ​ 2 E2 : E ​ 2 E2 compares aligned sets in one space, while E ​ 3 E3 bridges spaces of different dimension; they are different relations, reported independently.

3.4 Objective and Solution Relations

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

Under a verified candidate-to-reference map φ \varphi ( φ = π \varphi=\pi for lifts), E ​ 4 E4 checks whether f C f{C} and f R ∘ φ f{R}\circ\varphi induce 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 ​ 5 E5 certifies 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 from E ​ 2 E2 / E ​ 3 E3 equality with a preserved objective; duality certificates are refused for integer variables , since a relaxation bound does not certify the integer optimum. E ​ 6 E6 certifies 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 under E ​ 2 E2 -equality with identical objective, or a 0–1 complement involution). E ​ 6 E6 is positive-only in the current envelope: no certified-negative type exists yet, so absence of a correspondence is unknown , never false ; and E ​ 3 E3 -equality does not yield E ​ 6 E6 because the affine section is only a right inverse. These non-implications ( E ​ 2 ⇏ E ​ 4 E2\not\Rightarrow E4 , E ​ 4 ⇏ E ​ 5 E4\not\Rightarrow E5 , E ​ 5 ⇏ E ​ 6 E5\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, making E ​ 2 E2 true and E ​ 4 E4 false. Distinct feasible sets can share one optimum value, so E ​ 5 E5 does not imply E ​ 2 E2 . 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.

4 Certifying Implementation

4.1 Exact Ingestion and Certificate Generation

ModelEquivBench orchestrates 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 a 30 30 s 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 ​ 1 E1 map 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 for E ​ 2 E2 equality, witness verification for separations, the affine-lift obligations for E ​ 3 E3 , and the weak-duality re-check for E ​ 5 E5 —and only re-verified facts are reported; all emitted certificate and witness artifacts were independently re-verified in all three runs (Table 3 ); the reported denominator counts artifacts rather than unique cells. Evaluation is dimension-level checkpointed , so a per-dimension timeout yields a typed unknown_resource for exactly that dimension while preserving earlier results. The protocol enforces no repair and no resampling : a malformed or code-less response is a genuine E ​ 0 E0 outcome, 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 any E ​ 1 E1 – E ​ 6 E6 conclusion; 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.2 Independent 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.

ModelEquivBench takes a reference model and one generated candidate as its unit of evaluation and emits three linked products: the typed E ​ 0 E0 – E ​ 6 E6 profile, 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 in E ​ 5 E5 , for example, does not erase a previously verified E ​ 2 E2 certificate. 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.

5 Experiments

5.1 Experimental Setup

Cohort.

Bench4Opt contains 394 394 source records (Wang et al. 2025 ) ; in our paired representation these form 197 197 base 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 ( 20 20 ), a formal primary cohort ( 173 173 ), an unsupported audit set ( 4 4 , e.g. nonlinear structure outside the envelope), and a malformed-or-missing set ( 0 ). We report results only on the frozen 173 173 -problem formal cohort (SHA-256 prefix e9ad2018 ). This reference-only partition was frozen before formal generation, so no LLM output or evaluator result influenced inclusion. The 20 20 -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 identifier full ) and Unstructured ( concise )—giving 173 × 2 = 346 173\times 2=346 cells 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 , and Qwen3.5-397B-A17B . For each cell we take one generation at temperature 0.0 0.0 with no repair and no resampling ; the candidate is executed under a 30 30 s cap and the E ​ 1 E1 – E ​ 6 E6 evaluator under a uniform 120 120 s 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 exports candidate.lp . Provider/API errors before candidate creation are kept separate from genuine E0 failure.

Baselines and reporting.

Alongside the ModelEquivBench profile, 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, and unknown , unknownresource , unknownunsupported , N/A, absent , provider/API failure, and certified negatives are kept distinct throughout; unknown never means “incorrect,” N/A means the relation is mathematically inapplicable, and absent means 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 all 346 346 cells 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 ​ 1 E1 coverage is conditioned on E ​ 0 E0 - true , and the main E ​ 2 E2 decided rate on E ​ 1 E1 - true . The paired analysis instead uses all 173 173 base 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 certified false .

Table 3 reports the formal profiles, while Table 2 summarizes relation-specific baseline discrepancies.

Diagnostic GPT-5.4 Sonnet 4.6 Qwen3.5

Execution-success overestimation 49 35 25

ORGEval rejection despite E2 equality 25 8 18

Strict value-match false acceptance 0 0 0

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

Dimension / metric (denominator)

GPT-5.4 Sonnet 4.6 Qwen3.5

173 base problems × \times { Structured, Unstructured } = 346 =346 cells per model; identical SHA-256 cohort-hash prefix e9ad2018

E0 true (/346)

334 (96.5%) 156 (45.1%) 196 (56.6%)

genuine E0 false / unsupported / provider error

12 / 0 / 0 190 / 0 / 0 131 / 2 / 17

E1 map found (/E0- true )

277/334 (82.9%) 130/156 (83.3%) 164/196 (83.7%)

E1 unknown

57 26 32

E2 decided (/E1- true )

114/277 (41.2%) 45/130 (34.6%) 87/164 (53.0%)

E2 true / false_within

108 / 6 41 / 4 84 / 3

E2 unknown / unknown_resource

118 / 45 61 / 24 50 / 27

E3 decided

0 0 0

E4 decided

139 40 91

E5 true / false

107 / 42 36 / 31 79 / 22

E6 true (positive-only)

70 16 58

Certificate/witness artifacts re-verified

358/358 123/123 250/250

120 s cap-hit cells (union over dimensions)

70 35 39

Table 3: Formal ModelEquivBench profiles under the same single-generation, temperature- 0.0 0.0 , no-repair protocol. Qwen3.5-397B-A17B’s 17 17 provider/API errors occurred before candidate creation and are reported separately from genuine E0 failure. falsewithin abbreviates falsewithindeclareduniverse . Re-verification denominators count emitted dimension-verdict artifacts, not unique cells.

5.2 Stage-Wise Model Profiles

Execution does not settle semantics.

GPT, Sonnet, and Qwen produce ingestible candidates for 334 / 346 334/346 , 156 / 346 156/346 , and 196 / 346 196/346 cells. Yet their E2 decided counts are only 114 / 277 114/277 , 45 / 130 45/130 , and 87 / 164 87/164 among E1- true cells. Across the three runs, 49 49 , 35 35 , and 25 25 E0- true cells 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: 196 196 cells are E0- true , while among 329 329 successful API responses 131 131 are genuine E0 failures and 2 2 are unsupported; another 17 17 cells 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% , and 83.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 on 87 / 164 87/164 ( 53.0 % 53.0% ), compared with 114 / 277 114/277 ( 41.2 % 41.2% ) for GPT and 45 / 130 45/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.3 Baseline Discrepancies and Certified Case

Exact certification exposes baseline blind spots.

ORGEval returns not_equivalent on 25 25 , 8 8 , and 18 18 cells 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, whereas E ​ 2 E2 certifies 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.

Figure 2: A replayable ModelEquivBench all-applicable-positive case ( B4OBASE0031 , 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 shows a Sonnet case, B4OBASE0031 (Unstructured). An identity map aligns two models, each with five binary variables and 18 inequalities; exact enumeration certifies both E ​ 2 E2 directions, and E ​ 4 E4 – E ​ 6 E6 independently re-verify true ( E ​ 3 E3 is N/A). ORGEval returns notequivalent , while the LP-relaxation value baseline returns notequal ; the latter does not contradict E ​ 5 E5 , which concerns the original binary optima. The paired Structured cell has the same applicable profile, but ORGEval returns equivalent , illustrating representation sensitivity. Persisted paths and SHA-256 hashes make the case replayable.

5.4 Coverage, Abstention, and Reporting

Coverage and abstention are results, not errors.

The three runs contain 57 57 , 26 26 , and 32 32 E1- unknown cells; their E2 resource-timeout counts are 45 45 , 24 24 , and 27 27 . At least one evaluator dimension hits the 120 120 s cap in 70 70 , 35 35 , and 39 39 cells. No formal cell receives a decided E ​ 3 E3 outcome, 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 and 3 .

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.

ModelEquivBench suggests 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 for E ​ 5 E5 but silent about E ​ 2 E2 , 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 govern unknown and falsewithindeclared_universe .

Scope of claims.

Results are limited to gpt-5.4 , claude-sonnet-4-6 , and Qwen3.5-397B-A17B on the frozen 173 173 -base cohort, one generation per condition at temperature 0.0 0.0 , no repair or resampling, and the 120 120 s evaluator policy. We claim neither universal superiority, state-of-the-art generation, nor completeness over all mathematical programs.

6 Limitations 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 yield unknownunsupported . The finite E ​ 1 E1 grammar is incomplete, E ​ 3 E3 supports only the declared affine-lift schema, and E ​ 6 E6 has no certified-negative type. Exact rational verification also incurs resource limits: under the 120 120 s policy, at least one dimension returns unknownresource in 70 70 , 35 35 , and 39 39 GPT, 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 decided E ​ 3 E3 outcome, so empirical coverage of projected equivalence remains unestablished.

Conclusion.

ModelEquivBench reports each candidate–reference pair as a certified E ​ 0 E0 – E ​ 6 E6 semantic 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.