EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations

We sincerely thank the reviewer for the detailed feedback and for acknowledging the importance of our work:

"This work tries to address an important challenge in modeling equivalence checking, where previous works have not provided sufficiently satisfying solutions."

and for recognizing the soundness of our definition:

"The definition of quasi-Karp equivalence is sound and reasonable."

We appreciate the opportunity to clarify aspects that may have been misunderstood. While we recognize the importance of evaluating generalization and scalability, we note that some of the concerns—particularly regarding the MAMO and IndustryOR datasets—go beyond what these datasets can currently support. They do not offer the mathematical formulations and/or solver-compatible code needed for EquivaMap to systematically compare different instantiations of the same optimization problem. Below, we address these points and provide additional context.

C1: Generalizability to More Complex Datasets (e.g., MAMO (ComplexLP), IndustryOR)

A1: We appreciate the reviewer’s interest in evaluating EquivaMap on more datasets. However, datasets like MAMO (ComplexLP) and IndustryOR are not compatible with our evaluation method. While these datasets provide natural language problem descriptions and the respective optimal objective values, they do not include the corresponding mathematical formulations or solver code for obtaining such values. Our framework evaluates equivalence in formulations, thus any viable dataset for assessing it requires the existence of the formulations.

Specifically, EquivaMap tests quasi-Karp equivalence by identifying and verifying mappings between different mathematical formulations of the same optimization problem. This process requires access to mathematical formulations (or their equivalent solver-accessible code). Since MAMO (ComplexLP) and IndustryOR provide neither, they cannot be used to assess our method.

Though the original datasets cannot be used to assess EquivaMap, as an initial step to assess our method’s performance on MAMO and IndustryOR, we manually constructed the mathematical formulations and solver-compatible code of five instances from each dataset (we made sure to choose instances with different underlying formulations). We then applied the equivalent and non-equivalent transformations (described in Section 4) and evaluated EquivaMap accordingly. In all cases, EquivaMap achieved 100% accuracy. We will add this discussion to our paper.

We also respectfully disagree that the NLP4LP dataset, which contains over 300 instances, is too simplistic for evaluating equivalence mapping. The average description length of NLP4LP (hard) exceeds 900 characters, indicating rich semantic content. It also includes multi-dimensional parameters, like MAMO (ComplexLP) and IndustryOR. This information is shown in Table 1 of [1].

[1] AhmadiTeshnizi, A., et al. (2024). Optimus-0.3: Using LLMs to model and solve optimization problems at scale.

C2: Scalability with the increase of the dimensionality of the problem and corresponding input prompt length

A2: A key feature of EquivaMap is that it operates over sets of variables, rather than individual variables in a large-scale instance.

For example, in a graph coloring problem, although there is one decision variable per node, the formulation defines a set of variables (e.g., x[i] for each node i). EquivaMap only needs to reason about how one such variable set maps to another, rather than processing all individual variables (e.g., x[1], x[2], …) one-by-one. This is reflected in our input JSON format, where each set of variables and constraints is represented once, along with its index set.

This enables scalability because the number of sets of variables is typically much smaller than the total number of variables. In contrast, approaches that rely on analyzing variable-constraint graphs (e.g., in the WL-test) must operate over formulations that account for the total number of variables, leading to significant overhead as the problem size increases.

C3: Reliability on LLMs introduces a risk of hallucinations, where the model might generate plausible but incorrect equivalence mappings

A3: EquivaMap is designed to be robust to LLM hallucinations. In EquivaMap, for a given LLM-found mapping, we run it through a verification step (L239 - L245 right column) that checks whether the mapped solution preserves optimality. Mappings that fail are discarded. This sampling + verification pipeline ensures correctness even when the LLM is imperfect.

This distinguishes EquivaMap from naive prompting-based approaches that treat LLM output as inherently reliable. Our method instead treats the LLM as a heuristic mapping generator, embedded within a strict verification loop that ensures only correct mappings are accepted.

We sincerely thank the reviewer for the detailed feedback and for acknowledging the contribution of our work:

"The introduction of Quasi-Karp Equivalence is an important conceptual contribution."

” The EquivaFormulation dataset is a valuable resource for future research.”

” The work is timely, given the increasing interest in AI-assisted optimization modeling.”

Below, we address the questions raised:

Q1: "... Could you provide a more challenging example that better demonstrates the depth of reasoning needed to discover a valid mapping?"

A1: Below we present a more challenging transformation as an illustration: a digit-based reformulation where a single bounded integer variable is replaced by its base-10 representation. In this case, a bounded integer variable $x \leq 10^6$ is represented by 7 new variables $d_0, d_1, ..., d_6$, each representing one decimal digit of x, along with corresponding bounds and integrality constraints. Thus, the mapping $f$ will map $d_0, d_1, …, d_6$ to $x$, i.e., $x = \sum_{i = 0}^6 10^i d_i$. To successfully identify this mapping, EquivaMap must understand that a single variable $x$ can be decomposed into multiple variables representing digits, and recognize the weighted sum structure linking $x$ to its digits. In this case, EquivaMap also achieved 100% accuracy as demonstrated in our experiments.

Q2: "..., users would have to run the framework for every single problem instance. In addition, handling stochastic LLM outputs requires multiple runs. Do you see this as a serious limitation for real-world usage, especially in time-sensitive scenarios or in modeling copilots?"

A2: First, we note that per-instance evaluation is standard across all existing metrics, including canonical accuracy, execution accuracy, and the WL-test. This is inherent to the nature of automatic equivalence evaluation of optimization formulations, where ground-truth mappings are known and correctness is assessed instance by instance. Importantly, this is an offline task—it’s not meant to be executed in real-time during modeling. In modeling copilot settings, EquivaMap is meant to be used as an evaluator for a proposed copilot as it can evaluate its performance against correct formulations (instead of being the copilot itself).

We would also like to clarify that compared to execution accuracy, EquivaMap does not require additional MILP solving beyond the original problem instances. In particular, during the final verification step, we only evaluate whether the solution induced by the mapped variables satisfies the constraints in the target formulation and matches the known optimal objective value. This check is computationally lightweight and avoids any further calls to optimization solvers. In other words, once the MILPs are solved initially, no further solving is needed to verify a candidate mapping.

Q3: "... Have you explored or considered approaches that could ensure (or at least give stronger guarantees of) equivalence across all instances rather than one?"

A3: We agree that automatically checking equivalence across an entire family of instances is a powerful and exciting direction! Achieving this would likely require extending our verification process to work on symbolically parameterized formulations, and leveraging formal methods or symbolic solvers to validate that the discovered mapping preserves equivalence under all admissible inputs. We see this as a promising direction for future work.

Q4: "... Have you investigated whether more general classes of transformations (e.g., piecewise-linear or polynomial mappings) are feasible, or do you view the linear assumption as a fundamental design choice? If it is fundamental, what types of practically important reformulations do you expect it might fail to handle?"

A4: Thank you for this thoughtful question! To clarify: EquivaMap does not require $f$ to be linear by design—the only theoretical requirement is that the mapping function $f$ needs to be polynomial-time computable (L254 - L264, left column), in line with the notion of quasi-Karp equivalence. In practice, we choose $f$ to be linear because it suffices to cover all the equivalence-preserving transformations we included in our dataset. We will clarify this in our paper.

C1: “The methods… partial equivalence … formulations align.”

A5: We appreciate the reviewer raising this point and believe that this could be an interesting future line of work. In many cases, partial equivalence between optimization formulations is not a well-defined or semantically meaningful concept. That is, in these settings, a formulation either preserves the objective and feasible set, or it does not, and thus does not have a direct connection to partial equivalence. Precisely identifying when partial equivalence makes sense and how it should be defined is of future interest.

We sincerely thank the reviewer for their positive and thoughtful comments, and for recognizing the novelty of our work:

“The paper gives a novel connection between computational complexity and LLMs.”

Below, we address the specific questions and suggestions:

Q1: "Since you are mentioning cutting planes, do you see any connections of your work to proof complexity, etc.?"

A1: We indeed view our work as a first step toward automated reasoning about proof complexity. If Quasi-Karp Equivalence can be applied to two instances of two different families of optimization problems, it might be viewed as a potential heuristic for checking if two optimization problems are of the same complexity. That said, we recognize that these connections to proof complexity remain speculative and require further investigation. We thank the reviewer for highlighting this promising line of inquiry.

Q2: "Algorithm 1: I think you should elaborate on the LLM prompt. This step is a bit hand-wavy"

A2: Thank you for this suggestion! Currently, in Appendix A, we provide the exact prompt template generator used in all of our current experiments. We will include more details on this in our paper.

Q3: "Why is it a reasonable assumption that LLM inference is in poly-time?"

A3: Thank you for raising this question. As noted in The Expressive Power of Transformers with Chain of Thought (ICLR 2024) as well as comments by Reviewer FhjQ, it is shown that “a polynomial number of steps [in terms of the input] turns transformers into strong reasoners.”

Moreover, in EquivaMap, we typically call the LLM once per set of variables, not per individual variable. Since the number of sets of variables is often orders of magnitude smaller than the total number of variables in an instance, this further supports the practicality and tractability of our approach. We will add these discussions in the paper.

Q4: "I think that in the Discussion, you should elaborate more on future work directions."

A4: We agree that the future directions are rich in this space and worth expanding. In the final version, we will include more concrete directions, such as the potential usage of quasi-Karp equivalence to work as a heuristic for checking if two optimization problems are of the same complexity.

We are grateful for the reviewer's recognition of both the conceptual novelty of quasi-Karp equivalence and the empirical strength of EquivaMap on the benchmarked transformations. Below, we address the reviewer’s questions individually.

C1: “It's not clear whether EquivaMap will also work equally well in natural and real settings, … or in scenarios where multiple transformations are stacked together.”

A1: We appreciate the reviewer’s concern about the performance of EquivaMap on compositional or stacked transformations. To assess this, we designed a new set of experiments where we combined three transformation types—Add Slack Variables, Add Valid Inequalities, and Replace by Linear Combinations. In this case, we have 59 LPs + 115 MILPs. We found that EquivaMap achieved 100% accuracy on these new experiments with compositional transformations. We will add these experimental results along with other stacked transformation experiments to our paper.

C2: "... I am unclear why the authors didn't define problem formulations alpha and alpha' to be equivalent if alpha quasi-Karp reduces to alpha' AND alpha' quasi-Karp reduces to alpha."

A2: We appreciate the reviewer’s thoughtful observation! In classical complexity theory, equivalence is defined via a two-way reducibility. However, in our setting, we intentionally use a quasi-Karp (one-way) definition to better reflect the practical considerations of optimization modeling. As discussed in Section 3.2 (page 5), we relax the condition that a no-instance (which, in our setting, corresponds to an infeasible or suboptimal solution) under one formulation needs to be mapped to a no-instance of the other. This distinction is important in settings where a MILP formulation may exclude some, but not all, optimal solutions to improve efficiency. A common example is the addition of symmetry-breaking constraints, which preserve the objective and feasible set semantics, but eliminate functionally equivalent solutions. Because such transformations are often introduced in practice, we believe that a one-way reduction is sufficient and more appropriate for capturing formulation equivalence in applied contexts. Hence the use of the “quasi-” prefix.

C3: "I don't quite see how the 2nd and 3rd bullet are different. Isn't it the case that f is found to be polynomial if and only if A computing f runs in polynomial time?"

A3: Thank you for this careful observation! While it’s true that in many cases these two conditions collapse, we intentionally separate them to illustrate the difference: it is theoretically possible for $A$ to output a description of $f$ in polynomial time (e.g., a program that implements $f$), but for $f$ itself to take super-polynomial time to evaluate. For example, $A$ could construct a branch-and-bound solver as $f$—in which case $A$ runs in polynomial time, but $f$ may not.

C4: "In several places, the paper highlights the new notion being instance-specific… What is instance-specific about it? Wouldn't the transformation function be identical to two different instances of, say, a traveling salesman problem?"

A4: As the reviewer has mentioned, the mapping $f$ discovered by EquivaMap is not instance-specific. We feed the LLM a LaTeX-style formulation, where parameters such as TotalPeople or CapacityLargeUnit are left symbolic. The LLM then infers a symbolic mapping between the two formulations.

However, the verification step in our algorithm is instance-specific: to check whether a proposed mapping preserves optimality, we instantiate the symbolic formulation with concrete parameter values and verify that the mapped solution is valid and optimal.

To conclude, the mapping is over formulations, while the verification check is over instances.

C5: “In several places, the paper highlights the new notion is a mapping from solutions to solutions, … But the mapping is still from variables of one to variables of the other.”

A5: We agree with the reviewer's comment and will make it clear in our paper that we are not “suggesting that a Karp reduction is not.”

We would also sincerely thank the reviewer for the other comments or suggestions session. We will update our citations to address these comments in the future version of the paper. We greatly appreciate your close reading and thoughtful suggestions, which help us improve both the precision and presentation of our work.

We sincerely thank the reviewer for the positive and thoughtful review, and for appreciating the design of our experiments. We also appreciate your suggestion to include a runtime discussion of the EquivaMap algorithm.

Compared to execution accuracy, EquivaMap does not require additional MILP solving beyond the original problem instances. In particular, during the final verification step, we only evaluate whether the solution induced by the mapped variables satisfies the constraints in the target formulation and matches the known optimal objective value. This check is computationally lightweight and avoids any further calls to optimization solvers. In other words, once the MILPs are solved initially, no further solving is needed to verify a candidate mapping.

In practice, EquivaMap typically completes in a few seconds per instance, including both the LLM inference step and the verification step (typically very fast). We will add a more detailed runtime analysis in the future version of the paper.