ModelEquivBench: Certifying Multi-Relational Evalua... | AI Research

ModelEquivBench is a certifying evaluation system designed to assess the correctness of optimization models generated by large language models (LLMs). Instead of relying on a single "correct/incorrect" label or simple execution success, the system provides a multi-dimensional semantic profile that breaks down how a generated model compares to a ground-truth reference across seven distinct criteria.

The Semantic Profile (E0–E6)

The framework evaluates models using a seven-dimension profile, E0 through E6, which covers different aspects of mathematical and structural equivalence:

• E0 (Construction and Ingestion): Verifies that the candidate code builds a valid, exact-rational model.

• E1 (Representation Alignment): Searches for a map that aligns the candidate’s variables with the reference model.

• E2 (Same-Space Feasible-Set): Compares the feasible sets of the two models within the same variable space.

• E3 (Projected Feasible-Set): Compares the models when the candidate uses auxiliary variables that must be projected to match the reference.

• E4 (Objective-Order): Checks if both models rank feasible points in the same order.

• E5 (Optimal-Value): Verifies if both models result in the same optimal value.

• E6 (Optimizer-Set): Confirms if the sets of optimal solutions are in bijection.
  These dimensions are not a hierarchy; they are independent, meaning a model might pass one check while failing another.

Certifying Evidence

A core feature of ModelEquivBench is its "certifying" nature. For every positive conclusion, the system provides independently re-checkable evidence, such as replayable execution traces, explicit variable maps, or exact-rational certificates (e.g., Farkas multipliers). For negative conclusions, the system provides explicit witnesses, such as a failing trace or a point that violates a constraint.
If the system cannot reach a definitive conclusion due to resource limits, unsupported structures, or incomplete mapping, it reports a typed "unknown" or "N/A" outcome rather than guessing. This ensures that the evaluation results are based on verifiable facts rather than probabilistic outputs.

Experimental Findings

Researchers Penglin Zhu and Jungang Xu applied ModelEquivBench to 173 base problems using three LLM snapshots: GPT-5.4, Claude Sonnet 4.6, and Qwen3.5-397B-A17B. The results showed that these models often produce "executable" code that is nonetheless semantically incorrect.
For instance, the study found that 49, 35, and 25 cells (for the respective models) contained candidates that ran successfully but were certified negative on at least one semantic relation. Additionally, the researchers observed structural rejections in cases where the feasible sets were actually equivalent under a verified map. These findings suggest that traditional metrics, such as execution-success rates, are insufficient for determining the true quality of LLM-generated optimization models.

Limitations and Design

ModelEquivBench is designed to be "fail-closed," meaning it reports missing prerequisites as "absent" rather than attempting to evaluate downstream dimensions. The framework is not intended to be a new dataset, but rather a tool for evaluating existing ones. Because the system relies on exact-rational arithmetic and specific mapping grammars, it is limited to the supported envelope of linear and bounded-discrete models. The authors emphasize that because the dimensions of the profile are logically independent, the results cannot be reduced to a single accuracy score, as different models fail at different stages of the evaluation process.