EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
Authors: Haotian Zhai
Connor Lawless
Ellen Vitercik
Liu Leqi
Venue: ICML 2025 poster (2025)
Keywords: Combinatorial Optimization
Large Language Models
Mixed Integer Linear Programming
AI for OR
Primary area: optimization->discrete_and_combinatorial_optimization

Abstract: A fundamental problem in combinatorial optimization is 
identifying equivalent formulations. Despite the growing need for automated equivalence checks---driven, for example, by *optimization copilots*, which generate problem formulations from natural language descriptions---current approaches rely on simple heuristics that fail to reliably check formulation equivalence.
Inspired by Karp reductions, in this work
we introduce *Quasi-Karp equivalence*, a formal criterion for determining when two optimization formulations are equivalent
based on the existence of a mapping 
between their decision variables. We propose *EquivaMap*, a framework that leverages large language models to automatically discover such mappings for scalable, reliable equivalence checking, with a verification stage that ensures mapped solutions preserve feasibility and optimality without additional solver calls. To evaluate our approach, 
we construct *EquivaFormulation*, the first open-source dataset of 
equivalent optimization formulations, generated
by applying transformations 
such as adding slack variables or valid inequalities
to existing formulations.
Empirically, *EquivaMap*
significantly outperforms existing methods, achieving substantial 
improvements in correctly identifying formulation equivalence.

and EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
Haotian Zhail Connor Lawless
Ellen Vitercik 2
Liu Leqi
Abstract
theoretical computer science, and machine learning. Its ap- plications range from classic problems such as shortest path (Korte & Vygen, 2012) and maximum flow (Schrijver, 1983) to modern challenges neural architecture search (Elsken et al., 2019) and hyperparameter optimization (Khadka et al., 2024).
A fundamennal problem in combinatorial opti- mization is identifying equivalent formulations. Despite the growing need for automated equiva- for example, by optimiza- tion copilots, which generate problem formula- tions from natural language descriptions- current approaches rely on simple heuristics that fail to liably check formulation equivalence. Inspired by Karp reductions, in this work we introduce Quasi- Karp equivalence, formal criterion for determin- ing when two optimization formulations are equiv- alent based on the existence a mapping between their decision variables. We propose EquivaMap. framework that leverages large language mod- els to automatically discover such mappings for scalable, reliable equivalence checking, with ver- ification stage that ensures mapped solutions pre- serve feasibility and optimality without additional solver calls. To evaluate our approach, we con- struct FquuivaFormulation, the first open-source dataset of equivalent optimization formulations, generated by applying transformations such adding slack variables or valid inequalities to ex- isting formulations. Empirically, EquivaMap sig- nificantly outperforms existing methods, achiev- ing substantial improvements in correctly identi- fying formulation equivalence.!
lence
current
A fundamental problem in combinatorial optimization is identifying equivalent formulations. Historically, estab- lishing equivalence has played pivotal role in unifying problem-solving techniques and advancing theoretical char- acterizations of problem's computational complexity. In theoretical computer science, equivalence between prob- lems underpins the concept of NP-completeness (Cook, 1971; Karp, 1972), which unifies many seemingly distinct problems-such SAT, Vertex Cover, and Subset Sum- into the same equivalence class. This unification enables researchers to prioritize the development of algorithms for canonical problems while ensuring their applicability across equivalent problems. Similarly, applied fields such as network design (Kan, 1978) and semiconductor scheduling (Fang al., 2023), recognizing equivalence between opti- mization problems has historically facilitated the transfer of algorithms, reducing duplication of effort.
The advent of large language models (LLMs) has exposed a new frontier in combinatorial optimization, introducing opportunities to automate problem formulation, while also presenting new challenges among them, the need for reliable equivalence checking. Recent research has focused developing optimization copilots, systems that automate the translation of natural language descriptions into formal optimization formulations, particularly for mixed-integer linear programming (MILP) problems (Ramamonjison et al., 2023; Xiao et al., 2023; AhmadiTeshniz et al., 2024; As- torga et al., 2024). These advancements hold significant po- tential for democratizing access optimization techniques, broadening the reach of powerful tools for better decision- making (Wasserkrug et al., 2024). However, the widespread adoption of optimization copilots hinges on reliable evalua- tion mechanisms capable of verifying whether the generated formulations are equivalent to their ground-truth counter- parts. Moreover, automatic formulation equivalence check- ing is critical improving optimization copilots by serving
1. Introduction
Combinatorial optimization lies at the heart of many of today's most pressing challenges in operations research,
'The University of Texas at Austin, TX, USA SStanford University, CA, USA. Correspondence Haotian Zhai <hao- Man.zhai@utexas.
Proceedings of the nd International Conference on Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).
'The code and datasets are available at https: //github. com/ https: hetps://hugor /ugggi ngface. iqui Pquuvaaormulae in

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
as intermediate step, facilitating more efficient formula- tion search and refinement (Astorga al., 2024).
2.1. Combinatorial Optimization and MILPs
Combinatorial optimization (CO) broadly deals with find- ing optimal object from finite (or countably infinite) set of feasible candidates. Such problems arise in diverse fields, including operations research, computer science, and engineering, where discrete variables model decisions in practical scenarios such as routing, scheduling, or allocation of limited resources (Papadimitriou & Steiglitz, 1998).
Despite the importance of equivalence checking in combi- natorial optimization, existing automatic approaches rely heavily on heuristics (e.g., comparing optimal objective val- ues) and lack a precise, universally accepted definition of what constitutes formulation equivalence. Formal methods such as Karp reductions (Karp, 1972) offer valuable theoret- ical insights into problem equivalence but were not designed for modern automated settings, often requiring considerable human time and expertise to construct.
A foundational tool for combinatorial optimization is mixed- inleger linear programming (MILP), formulated
min c CTT =ERPXEN-P
Towards precise and reliable equivalence checking, we pro- pose a formal definition of formulation qquivalenee-Quan Karp Segnivalence-gruunee ductions. Quasi-Karp Equivalence determines whether two formulations are equivalent by checking for the existence of a mapping between their decision variables. We pro- pose EquivaMap, an approach that automates equivalence checking by using LLMs to identify mappings between for- mulations, followed by a lightweight verification step to ensure these mappings preserve optimality and feasibility without additional MILP solver calls. Grounded in precise definition of formulation equivalence, EquivaMap allows for automatic equivalence verification for optimization for- mulations.
subject to orob, 8
in the principles of Karp re-
where x is the vector of decision variables, e is the cost vector, A is the constraint coefficient matrix, and b is the
vector of constraint bounds. The notation Ax o b represents a system of linear constraints, where denotes relational operators from the set {s, =.). The variables x are parti- tioned into p continuous variables and n-p integer variables. Let x² denote an optimal solution (1), and let =" be the corresponding optimal objective value. If all decision variables are continuous (p = n), the problem is a linear program (LP). MILPs capture many prominent combinato- rial problems such as the traveling salesman problem (TSP) (Cook et al., 201 1), knapsack problem (Pisinger & Toth, 1998), and network design problems (Kan, 1978).
xt
Our contributions can be summarized as follows:
We identify pitfalls of existing equivalence checking meth- ods (Section 3.1).
Many fundamental CO problems -nniemmi-iccudinng TSP and Knapsack-are known to be NP-hard. A key contribution to the theory of NP-completeness was provided by Karp (1972), who demonstrated that a number of widely stud- ied problems are mutually reducible in polynomial time (often referred to as "Karp reductions").. These reductions establish deep structural connections among CO problems, showing that if polynomial-time algorithm exists for one, it can be systematically adapted to solve many others.
We propose Quasi-Karp equivalence as a formalism for defining when two optimization formulations are equiv- alent through the existence of a mapping between their decision variables (Section 3.2) and present EquivaMap, a scalable method that uses LLMs to discover candidate mappings, paired with a separate verification step to en- sure correctness (Section 3.3).
2.2. Language Models for MILP Modeling
To evaluate the performance of equivalence-checking methods, we introduce, to the best of our knowledge, the first dataset- Eegisst--Egqiaaooollaatoooo that documents both equivalent formulations and the transformation between them (Section 4.1). Empirically, we show that EquivaMap outperforms existing methods across various equivalent transformations (Section 4.2).
The of language models for MILP modeling has sparked considerable interest in the Al-for-OR community. The NL40pt competition (Ramamonjison et al., 2023) focused on using natural language processing (NLP) methods to formulate optimization problems based on their text descrip- tions. More recently, with the advent of LLMs, a number of LLMdbased optimization copilots aim automate MILP modeling (Mostajabdaveh al., 2024; Ahmed & Choud- hury, 2024; Li et al., 2023b; Yu & Liu, 2024; Huang et al., 2024a; Kadıoglu et al., 2024; Yang et al., 2024). Both the Chain-of-Experts (Xiao et al., 2023) and OpúMUS (Ahma- di diTeshnizi et al., 2024) frameworks designed LLM- b-baeed multi-agent systems to automate the modeling of complex optimization problems by leveraging the reasoning capabili-
2. Background and Related Work
Our work connects important lines of research on combi- natorial optimization (especially MILPs), LLMs for MILP modeling, and automatic equivalence-cheese checking methods for optimization formulations.
2

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
ties of the LLMs. Tang et al. (2024) further demonstrated the potential of LLMs by fine-tuning open-source models with synthetic data tailored for modeling optimization prob- lems, achieving significant performance improvements over baseline methods. Building on these capabilities, LLM- powered chatbots have been used to allow users to interact with optimization models in a number of contexts includ- ing supply chain management (Li al., 2023a), meeting scheduling (Lawless et al., 2024b), debugging infeasible models (Chen et al., 2023), and improving solver configura- tions (Lawless et al., 2024a). These advancements highlight why LLMs are particularly suitable for MILP modeling: their ability to process and generate structured information from natural language aligns well with the requirements of optimization problem formulation. The rapid development of optimization copilots underscores the need for reliable, scalable evaluation techniques.
cally check such equivalence. In the general setup, we have two formulations a and a' corresponding to the same (feasi- ble) optimization problem P. with optimal objective values x* and z" respectively. For example, Figure 1 presents two formulations a and a' of an optimization problem P - the stable set problem. Our method aims to evaluate the equiva- Ience of a and a' for a given instantiation of the problem. In Figure 1, an instantiation of P would be defined by a specific input graph.
3.1. Pitfalls of Existing Equivalence Checking Methods
We discuss existing methods for evaluating formulation equivalence, including canonical accuracy, execution ac- curacy, and the WL-test, and exhibit settings where these methods fail.
Canonical accuracy is based on matching declarations be- tween predicted and reference programs, where a declara- tion represents either an optimization objective or a con- straint (Ramamonjison et al., 2023).
2.3. Existing Automatic Equivalence Checking Methods
The central task of evaluating optimization copilots is tomatically checking whether the generated formulation is equivalent to a ground-truth correct one. The earliest method used in the NL4OPT benchmark (Ramamonjison et al., 2023) for evaluating formulation equivalence is canon- ical uccuracy, which looks at direct equivalence between declarations (e.g., objective, constraints) between a refer- ence correct formulation and a generated formulation. This method is sensitive to permutations of the order of the dec- larations in formulation and fails when multiple valid for- mulations exist for the same problem. The method used in benchmarks such as NLP4LP (AhmadiTeshnizzi et al., 2024), MAMO (Huang et al., 2024b), and IndustryOR (Tang et al., 2024) is execution accuracy, which evaluates whether two MILP formulations are equivalent by solving them (using MILP solver such as Gurobi) and checking if they have the same optimal objective value. Execution accuracy is sensitive to variable re-scaling, which can create inconsisten- cies even when the formulations are functionally equivalent. To address these issues, recent approaches utilize Graph Edit Distance (Xing et al., 2024) and a modified Weisfeiler- Lehman (WL) test (Wang et al., 2024) to measure structural similarity between the generated and reference formulations. These methods offer insights into equivalence beyond the optimal objective value but have limitations. They are par- ticularly sensitive to structural modifications, such as adding cutting planes, which keep the formulation equivalent but change its structural information. Beyond these methods, Steever et al. (2022) proposed an image-based based approach to detect structural similarity among large-scale MILPs.
Definition 3.1 (Canonical Accuracy). Given reference declaration d (objective or constraint) and generated dec- laration d, they are said to be matched if d = d. Let DD and D denote the sets of reference and generated declarations, respectively. A False Positive (FP) is a generated declara- tion d that is unmatched, while a False Negative (FN) is a reference declaration that is unmatched. The canonical accuracy is defined as:
min (FP + [NN, (D)
[D]
where any score under 100% indicates that the formulations are not equivalent.
Canonical accuracy imposes a strong assumption that gen- erated MILPs must adhere to the same variable order as the ground-truth MILP. As illustrated in Figure 1, if the constraints in are permuted differently from those in a', they are erroneously treated as nonequivalent, despite being functionally identical. More broadly, canonical accuracy fails in cases where the two formulations differ based on variable or constraint permutations.
Execution accuracy captures whether two optimization problems have the same optimal objective value (Ahma- diTeshnizi et al., 2024).
Definition 3.2 (Execution Accuracy). a and a' are consid- ered equivalent if = = =²"
Execution accuracy has clear limitation: it is not robust to rescaling, common transformation in MILPs that may simply reflect change in units. For example, in Figure 1, the objective function in a' is rescaled, which would lead execution accuracy to incorrectly classify a and a' as non- equivalent.
3. Methodology
This section introduces Quasi-Karp Equivalance and EquivaMap, our method for leveraging LLMSs to automati-
3

---

EquivaMap:
Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
Example:
Given a graph G = (V, E), where V represents the set of vertices and E represents the set of edges, find the largest stable set, where stable set is subset S C V such that two vertices in S adjacent (i.., there edge (u, v) E with u, S).
Y/.
max
[
max
Z1
EEV
Formulation Base
Formulation a' Strengthened & Rescaled
3/
13 S
V(i,)) E
2; + 3j 1 v(t,)) E 10 ViEV
> 5 tkEK
PER
Vi E {0,1}
ViE
LLM Generated Mappingf
2, f(v) ViEV
Figure 1: A classic stable set problem, where the two formulations correspond to the same problem description. Formulation uses the standard formulation, while formulation a' rescales the objective function and adds cutting planes based on cliques (where K. denotes the set of cliques in G). LLMs are used to find the mapping function f that maps the variables of a' into the variable space of a. An example mapping would be the identity function f((: yí-
Previous studies have shown that MILPs can be represented as bipartite graphs (Chen et al., 2023a;b; Khalil al., 2017: Gasse al., 2019), providing foundation for defining equivalence using graph-isomorphism based approaches such as the WL-test. To construct this bipartite graph, node is added for each variable and each constraint of the graph. An edge connects a variable node to a constraint node if that variable has a non-zero coefficient in the cor- responding constraint. The nodes and edges are endowed with various real-valued attributes describing the MILP (for example, variable node's attributes will include its coeffi cient in the objective function). The WL-test tests whether two graphs are isomorphic.
(2024) also introduced a related method based on graph- edit distance, which softer version of the WL-test. Since graph-based methods evaluate equivalence after transform- ing formulations and a' into bipartite graphs, they will treat the two formulations as non-equivalent if structural modifications change the number of variables or constraints. Such modifications are extremely common (and desired) in MILPs, as techniques like adding cutting planes, refor- mulating constraints, or introducing auxiliary variables are frequently used to improve solver efficiency and tighten linear relaxations. For example, the second formulation in Figure I includes clique cutting planes:
Σ 5 E
Definition 3.3 (WL-test (Douglas, 2011)). Let G = EV and H = (V', V E') be two graphs. The Weisfeiler-Lemman test is an iterative label refinement procedure used to deter- mine whether and are distinguishable. Initially, each vertex u E assigned label (o()). each iteration the label of each vertex v is updated as follows:
for cliques & E K. in the graph. These cutting planes well-known to strengthen the linear relaxation of the stable set MILP formulation (Conforti et al., 2014).
3.2. MILP Equivalence Based on Karp Reduction
(4+((0) hash (c), (u( u (()))))))
Towards a more formal notion of MILP formulation equiva- lence, we introduce new definition inspired by a classical tool from complexity theory called a Karp Reduction: Definition 3.4 (Karp Reduction). Two decision problems P. Q are said to be equivalent if there exists function that maps arbitrary instances of P to Q such that:
where (w) denotes the set of neighbors of v, and the func- tion hash(-) provides unique encoding neighboring nodes' labels. The process continues iteratively until convergence. To compare graphs, the WL-test computes the multisets of final labels for G' and И. If these multisets differ at any iteration, the graphs are determined to be non-isomorphic, which indicates that they are not equivalent.
If is yes-instance of P. then f (p) is yes-instance of Q
Modifications the WL-test were proposed by Wang et al. (2024) to evaluate formulation equivalence. Xing et al.
If is no-instance of P, then f(p) is a no-instance Q, and

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
ʃ can be computed in polynomial time.
Algorithm 1 EquivaMap
1: Input: Two optimization formulations a, a' with objec- tive min e xr min x' respectively. A solver S that finds an optimal solution x" for and x'* for a'.
A Karp reduction can be used to show that two decision problems are equivalent (i.e., solution to one can be used to find a solution to the other). These reductions hold for arbitrary instances of the two decision problems, but we leverage a similar approach to establish the equivalence between two specific formulations of an MILP problem in- stance. Consider two optimization problem formulations o, a' that correspond to the same optimization problem P. Our goal is to formally check that an optimal solution to one for- mulation can be used to generate an optimal solution to the other formulation for a specific instantiation of the problem. Unlike traditional Karp reductions, which define mappings for arbitrary instances, we focus on instance-specife map- pings. Moreover, our approach maps between solutions of the optimization problem rather than the instance itself.
2: Output: A Boolean value indicating whether a and a' are Quasi- Karp equivalent.
3: # {Call an LLM with mnstanceddependen prompt to find a mapping]
4: < A(aa, a')
5: # {Ohtain optimal solution of a' using solver S}
6: x' + S(a')
7: # (Map the solution x²* to a candidate solution in a}
8: ā + f(x"))
9: # {Check if is optimal and feasible for a}
10: if c T = c x" and e feasible for a then
11: return True
12: else
We also relax the condition that a no- no-instance (which cor- responds 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, opti- mal solutions improve efficiency. For example, adding commetr--breakeeee constraints to an optimization model is a common modeling practice that removes functionally equivalent solutions. With these distinctions in mind, we for- malize a new notion of equivalence for MILP formulations which we call Quasi-Karp Equivalence:
13: return False
14: end if
optimal values. If both formulations are infcasible, then nei- ther has valid solution, making any comparison between them trivial and uninformative. Declaring two infeasible problems equivalent does not provide any insight into their structural or computational properties. Likewise, if one for- mulation is infeasible while the other feasible, then no valid mapping f can transform an optimal solution of one into the other. Finally, if a formulation is unbounded, then it lacks a finite optimal solution, so no single "optimal" point can be mapped from one formulation to another. Thus, we use Quasi-Karp Equivalence to check equivalence between feasible, bounded formulations.
Definition 3.5 (Quasi-Karp Equivalence). Suppose and a' are two optimization problems over Rd and RR",, re- spectively. We say a' is Quasi-Karp equivalent to if there exists an algorithm A(a, a') that produces mapping f: RRd Rd such that:
x is an optimal solution to a', then f(**) is an optimal solution to a,
3.3. EquivaMap: LLM-Based Mapping Discovery with Lightweight Verification
f can be computed in polynomial time, and
To determine the mapping between a and a', we propose EquivaMap, a framework that leverages LLMs as the map- finding algorithm AA from Definition 3.5. Specifically, given two formulations a and a' corresponding to a given in- stance of the problem P, the algorithm A returns a mapping function f that aligns their solutions:
A(aa, a') runs in polynomial time for all a, a'.
Note that the defintion of Quasi-Karp equivalence is direc- tional, meaning that a' being Quasi-Karp equivalent to a does not necessarily imply that a is Quasi-Karp equivalent to a'. Also note there is a distinction between the second and third point in definition 3.5: is possible for A to run in polynomial time (e.g., a program implementing f), but for I itself to require super-polynonial time to evaluate. For example, A could construct a branch-and-bous solver as f-in which case A runs in polynomial time, but may not.
A(a,a')
In EquivaMap (Algorithm 1), we first use the LLM A to find the mapping f for the pair of formulations (a,a') using an instance-specific prompt ( (Appendix A). Using a solver S, we compute an optimal solution x'* a'. With f. we obtain candidate solution # f(x") for a. We verify whether å is an optimal solution of a by substituting å into and verifying that á is feasible and optimal (i.e., c i = c x*).
In Figure 1, an example of one such mapping / would be I; = ys, Vi E V. which is a linear function. Intuitively, the notion of Quasi-Karp Equivalence is meaningful only when the optimization problem is NP-hard and both opti- mization formulations admit feasible solutions with finite
A key component of EquivaMap is the mnstaccesspecife prompt, which guides the LLM in finding the mapping func- tion f. The prompt includes a structured description of
5

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
Probiemm P
Formulation a
Formulation
LLM
Massing Function
Optinal Feasbbee
Equivalent
Text pilon
Dheer intion
Outle
Coulo
Masssed
Candidane
Verifer
Soution
Salver
Solution of
Optimal
Not equivalent
Figure 2: Workflow of EquivaMap. The method evaluates equivalence between two formulations (a and a') of the same optimization problem instance P. LLM generates mapping function (f) to map between the variable spaces of a and a'. The mappings are applied to transform the optimal solution of a' into a candidate solution in a. verifier assesses whether the candidate solution is feasible and optimal for a. If the verification succeeds, and a' are deemed equivalent; otherwise, they are classified as not equivalent.
each variable in the formulation (a), including its textual description, the constraints in which it appears, and whether appears in the objective function. Note that a variable defined over a set (e.g., Z2 Vi E V in Figure 1), the defi- nition of the variable is only included once in the prompt. This allows the prompt scale with the number of sets of variables, which can be far less than the number of indi- vidual variables for large-scale problems (see Appendix C for an example). We provide an analogous description of the formulation (a'). The prompt then instructs the LLM to generate a linear mapping for each variable in a, expressed as list of coefficients and corresponding variable names in o.. For more details, defer to Appendix A.
is valid. Thus, while the mapping is over formulations, the verification check is over instances.
Comparing EquivaMap to Definition 3.5 of Quasi-Karr Equivalence, we note that, under the reasonable assumption that the LLM's inference time is polynomial in the length of its input prompt, EquivaMap runs in polynomial time. Moreover, by restricting the mapping function f to be linear, we ensure that it can be computed in polynomial time.
Stochasticity in LLMs and Aggregation. Since LLMs have stochastic outputs, we run Algorithm K times and then aggregate the outputs by declaring (a, a') equivalent if at least one of the K attempts produces valid mapping.
Below we illustrate this procedure using the example in Figure 1. Suppose the optimal solution of a' is of for all E V. Applying the identity mapping function f, we compute é;- = f(y() = y for all E V. We confirm & is feasible, and substitute à; into the objective function
4. Experiments
We conduct a comprehensive evaluation of EquivaMap by introducing EquivaFormuulation to the best of our knowl- edge, the first dataset that contains equivalent formulations of MILP instances. Moreover, the dataset includes details about the transformations used to create these equivalent formulations (Section 4.1).
Σ g iEV
to verify whether
Next, we evaluate EquivaMap on this dataset and com- pare its performance against established baselines including canonical accuracy, execution accuracy, and the WL-test (Section 4.2).
Σ VEV
34
Σ x iEV
Note that the mapping f discovered by EquivaMap is not speccfc but operates at the formulation level. We feed the LLM symbolic formulations where parameters and sets, such as the graph G (V, E), remain abstract instead of being replaced by real values. The LLM then infers symbolic mapping between the two formulations that is applicable across all instances. A more explicit prompt example can be found in Appendix B. However, the veri- fication step (1.9-14) in our algorithm is aestance-specifii we instantiate the symbolic formulation with concrete pa- rameter values and sets and verify that the mapped solution
4.1. EquivaFormulation: dataset of equivalent MILP formulations
We construct EquivaFormulation based on the NLP4LP dataset (AhmadiTeshnizzi et al., 2024). NLP4LP comprises diverse set of optimization problems with distinct problem sizes, objective functions, and constraints. Each instance in NLP4LP is composed of three components: (1) de- scription file with a high-level description of the problem in natural language. (2) An information file which con-
6

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
Table 1: Overview of the equivalent and nonequivalent transformations between formulations considered in EquivaFormula- tion. Transformation Name describes the type of transformation; How It Is Transformed explains the modification applied to the problem; Example (Before/After) provides short snippet demonstrating the difference; Equivalent? indicates whether the transformation preserves the original problem's optimal solutions; and Size shows the number of affected instances, reported the count of LP and MILP problems.
Transformation Name
How It Is Transformed
Example (Before/After)
Equivalent?
Size
Substitute Objective Functions
Replace objective function
Before: minc'
Yes
92LP + 140MILP
min x with auxiliury vari- able adding new constraint c²x
After: min 2, s.t. 2 ==== c
Add Slack Variables
Trunsform constraint g(x) into g(x) + = 2
1 After: x + 2g + 5,
Before:
Yes
59LP 134MILP
Replace by Buse-10 Representation
Express an integer variable N in its decimal expansion
Before: x s 100
Yes
44LP + 123MILP
After: x Ei d: 10f, 0 59, cz
Add Valid Inequalities
Include cutting plunes or valid linear combinations that do not exclude any integer feasible so- lution
Before: {z + 2y S 3, a 155)
Yes
92LP + 142MILP
After: 2 + 2y 3, x 1.5, 2x By 4.5)
Rescaling
Change units/scales for variables or objectives (e.g.. hours to min- utes)
Before: at (hours)
Yes
60LPP 133MILP
After: 60z' (minutes)
Replace by Linear Combinations
Decompose a variable æ into z a+ x with x+,x" 2
Before: æ
Yes
77LP + 115MILP
After: x x0"
Random Order
Substitute the original instance with completely unrelated, ran- domly chosen instance
c Before: min
No
87LP 142MILP
After: max y, s.t. y 3
Loose Constraints
Delete certain constraints that are tight the optimum, alter- ing the feasible set
Before: + 2y < (binding)
No
53LP 120MILP
After: remove x + 2y S 3 c
Feasibility
Turn both the original and ran- domly chosen instunce into fea- sibility problems (replace objec- tives with 0)
Before: min O,
No 87LP 142MILP
After: maxU, S.t. y = 3
tains the corresponding mathematical formulation of the optimization instance, written in LaTeX. (3) A file that con- tains the GurobiPy code corresponding to the mathematical formulation.
iary variables - are commonly employed to enhance solver efficiency and tighten relaxations while preserving the for- mulation's 's optimal solution. Finally, we incorporate non- equivalent transformations to evaluate the susceptibility of equivalence-checking methods to false positives. These se- lected transformations in EquivaMap are designed to test the robustness of different equivalence-checkinn methods in handling diverse MILP formulations.
As discussed in Section 3.2, we carefully select optimization problems in the NLP4LP dataset by removing the infeasi- ble and unbounded instances. In EquivaFormulation, we introduce seven (Quasi-Karp) equivalent transformations and three non-equivalent transformations to transform the formulations in NLP4LP to corresponding (aasi-KKar)) equivalent and nonequivalent counterparts, respectively (Ta- ble 1). Our proposed equivalent transformations capture widely used and important modeling techniques in MILPs. Standard practices such as substituting the objective func- tion, adding slack variables, and decomposing variables into positive and negative components help simplify con- straints and enforce non-negativity. Additionally, robustness to rescaling is crucial, as quantities can be represented in different units (e.g.. 1 kg rather than 1000 g). Similarly, certain structural transformations such adding valid inequalities, reformulating constraints, or introducing auxil-
Since the selected transformations in EquivaFormula- tion are deterministic, to prevent the mapping finder or other equivalence- cuts-such as mapping decision variables based their or- der (e.g.. if variable names are assigned alphabetically)--e apply several transformations to the formulation before pro- cessing. Specifically, we randomly permute the order of problem parameters, decision variables, and constraints in the information file. Additionally, we assign distinct names to all decision variables and use GPT-4o to generate var- ied natural language descriptions for them. These transfor- mations are implemented to reduce the similarity between formulation and a', ensuring that LLMSs cannot exploit
methods from exploiting short-

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
Table Accuracy equivalence--cheeking methods on formulations obtained from equivalent non-equivalent transformations.
Canonical Acc.
Execution Acc.
WL-test
naive-LLM
EquivaMap
Equivalent Transformations
Worst Case
0%
0%
0%
3.3%
100 %
Substitute Objective Functions
0%
100 %
0%
91.2%
100 %
Add Slack Variables
0%
100 %
0%
36.1%
100% %
Replace by Base-10 Representation
0%
100 %
0%
53.1%
100% %
Add Valid Inequalities
100 %
0%
3.3%
100 %
Rescaling
0%
0%
0%
69.9%
100 %
Replace by Linear Combinations
0%
100 %
0%
24.4%
100%
Non-Equivalent Transformations
Worst Case
100 %
0%
100
93.6%
100
Random Order
100 %
100% %
100 %
98.7%
100 %
Loose Constraints Feasibility
100 %
100 %
100% %
93.6%
100% %
100 %
0%
100% %
100 %
100%
recognizable transformation patterns to deduce the mapping directly.
accuracy.
The results for non-equivalent variations further highlight the reliability of our method. For the Feasibility transfor- mation, execution accuracy fails with 0% accuracy, yet our method achieves perfect accuracy for all instances. Under other non-equivalent settings, our method also works well, achieving 100% accuracy.
4.2. Performance
We use GPT-4 (Achiam et al., 2023) the mapping finder in EquivaMap, and evaluate our method against existing baselines, plus a naive I.IM baseline (naive-LL.M). The naive-LLM baseline uses a prompt that includes two formu- lations a and a' and directly checks they are equivalent. The prompt can be found in Appendix A. We K 3, and report the accuracy the percentage of paired formula- tions and a' that are correctly identified as equivalent or nonequivalent, and summarize the results in Table 2.
We additionally perform runtime analysis comparing EquivaMap with baseline methods such as Execution Ac- curacy and the WL-test. The results, which show that EquivaMap operates within seconds, are presented in Ap- pendix D.
The results demonstrate that our method consistently out- performs all baseline approaches, achieving perfect or near-perfect accuracy in almost every scenario. Notably, EquivaMap performs perfectly even in cases where all base- line approaches completely fail.
Key observations. EquivaMap outperforms all existing equivalence-checking methods, including the naive-ILLM baseline. This highlights the necessity of our algorithm without the explicit map finding and optimality verification steps, naively using LLMs with strong reasoning capabilitics will not ensure reliability in checking formulation equiva- lence. Moreover, these results demonstrate that our method is reliable across diverse transformations. It consistently outperforms all baselines, especially in scenarios where execution accuracy and other methods fail.
For the equivalent transformations (Table 3), our method per- forms exceptionally well under challenging transformations, such as Add Valid Inequalities, Rescaling, and Replace by Linear Combinations. Execution accuracy and the WL-test fail universally in these settings, achieving 0% accuracy across all variations. In contrast, EquivaMap achieves 100% accuracy. These transformations are critical test cases be- cause they highlight the fundamental weaknesses of existing approaches: they struggle with capturing key modeling tech- niques such as cutting planes and variable rescaling. For example, exccution accuracy fails at Rescaling, since a naive solver run does not recognize scaled problem instances as equivalent, while WL-test fails at Add Valid Inequalities Replace by Linear Combinations since these transfor- mations break isomorphisms in the graph representation. Our method reliably handles them, achieving near perfect
5. Discussion
How can we define the equivalence of two formulations of the same optimization problem instance? In this paper, address this conceptual gap by proposing Quasi-Kant equivalence and framework, EquivaMap, to systematically check such equivalence. Through extensive experiments on MILP problems, we demonstrate that EquivaMap out- performs existing approaches by large. Additionally, by introducing the first well-documented pool of equivalent
8

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
optimization formulations, encompassing diverse transfor- mations such as the addition of cutting planes, we provide valuable dataset for advancing research in this domain.
optimization problems. INFOR: Information Systems and
Operational Research, 62(4):559-572, 2024.
Astorga, N., Liu, T., Xiao, Y., and van der Schaar, M. Auto-
Beyond examining whether two formulations represent the same problem instance, a promising direction for future research is to leverage EquivaMap to check equivalences across diverse optimization problems, such as the equiva- Ience between max-flow and min-cut problems. It is also worth noting that our current work focuses on relatively straightforward transformations, thereby omitting more in- tricate reformulations such as those emerging from decom- position algorithms. As more complex optimization copilots are developed, we may need certivalenn-cchekkng tools that can tackle these more complex transformations.
formulation of mathematical optimization models using llms. arXiv preprint arXiv:2411.01679, 2024.
Chen, H., Constante-Flores,, G. E., and Li, C. Diagnosing infeasible optimization problems using large language models. arXiv preprini urXiv:2308. /2923, 2023.
Chen, Z., Liu, J., Wang, X., and Yin, W. On representing lin- ear programs by graph neural networks. In The Eleventh International Conference on Learning Representations, 2023a.
Chen, Z., Liu, J., Wang, X., and Yin, W. On representing mixed-integer linear programs by graph neural networks. In The Eleventh International Conference on Learning Represemaatins, 2023b.
Impact Statement
Our framework for checking the formulation equivalence of combinatorial optimization problems offers the potential to streamline the development and deployment of optimization models across diverse fields, including operations research, logistics, and engineering. By systematically identifying equivalences among different formulations, our approach can reduce redundant effort, promote reproducibility, and accelerate innovation. In particular, the ability to recognize and compare formulations at finer granularity could serve as a critical building block for "optimization copilots" that assist researchers and practitioners in designing, debugging, and refining complex models. At the same time, these ad- vantages come with important considerations. When compu- tational tools can automatically detect formulation similari- ties, there is a possibility of overlooking nuanced domain- specific constraints or ethical requirements if they are not explicitly accounted for. Over-reliance on such tools could inadvertently propagate modeling oversights or marginalize expert judgment. Furthermore, democratizing advanced op- timization capabilities may amplify existing disparities if access to these methods remains unevenly distributed.
Conforti, M., Cornuejols, G., and Zambelli, G. Integer programming. Springer, 2014.
Cook, A. The complexity of theorem- provinn procedures. In Proceedings of the third annual ACM symposium Theory of computing, pp. 151-158. 1971.
Cook, J.J., Applegate, D. L.., Bixby, R. E., and Chvatal, V. The traveling salesman problem: a computational study. Princeton university press, 2011.
Douglas, B. L. The weisfeiler-lehman method and graph isomorphism testing. arXiv preprint arXiv:1101.5211 2011.
Elsken, T., Metzen, J. H., and Hutter, F. Neural architecture search: A survey. Journal of Machine Learning Research, 20(55):1-21, 2019.
Fang. J., Cheang, B., and Lim, A. Problems and solution methods of machine scheduling in semiconductor man- ufacturing operations: A survey. Sustainability, 15(17): 13012, 2023.
References
Achiam, J., Adler, S., Agarwal, S., Ahmad, L.,, Akkaya, I, Aleman, F. L., Almeida, D., Altenschmidt, J., Altman, S.,
Gasse, M., Chételat, D.,, Ferroni, N., Charlin, L., and Lodi, A. Exact combinatorial optimization with graph convolu- tional neural networks. Advances in neural information processing systems, 32, 2019.
Anadkat, S., et al. GPT-4 technical report. arXiv preprint arX1v:2303.08874, 2023.
AhmadiTeshnizi, A., Gao, W., and Udell, M. Optimus: Scal- able optimization modeling with (mi) lp solvers and large language models. In Forty-first International Conference on Machine Learning, 2024.
Huang, S., Yang, K., Qi, S., and Wang, R. When large language model meets optimization. arXiv preprint arXi::2405 2024a.
Huang, X., Shen, Q., Hu, Y., Gao, A., and Wang, B. Mamo: a mathematical modeling benchmark with solvers. arXiv preprint arXiv:2405. 13/.///4444 2024b.
Ahmed, T. and Choudhury, S. Lm4opt: Unveiling the poten- tial of large language models in formulating mathematical

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
Kadıoğlu, S., Pravin Dakle, P., Uppuluri, K., Politi, R., Raghavan, P., Rallabandi, S., and Srinivasamurthy, R. Ner4opt: named entity recognition for optimization mod- elling from natural language. Constraints, 29(3):261-299, 2024.
Ramamonjison, R., Yu, T., Li, R.,, Li, H., Carenini, G., Ghad- dar, B., He, S., Mostajabdaveh, M., Banitalebi-Dehkordi,, A., Zhou, Z., et al. Nl4opt competition: Formulating optimization problems based on their natural language descriptions. In NeurlPS 2022 Competition Track, pp.
189-203. AMLR,2023.
Kan, A. R. The complexity of the network design problem. Networks, 8(4):279-288) 1978.
Schrijver, A. Min-Max Results in Combinatorial Optimiza- tion, pp. 439-500. Springer Berlin Heidelberg, Berlin, Heidelberg, 1983.
Karp, R. M. Reducibility among combinatorial problems. In Complexity of Computer Computations, pp. 85-103. Plenum Press, 1972.
Steever, Z., Murray, C., Yuan, J., Karwan, M., and Lübbecke, M. An image-based based approach to detecting structural similarity among mixed integer programs. INFORMS Journal on Computing, 3444):1849-1870, 2022.
Khadka, K., Chandrasekaran, J., Lei, Y., Kacker, R. N., and Kuhn, D. R. A combinatorial approach to hyperparame- ter optimization. In Proceedings of the IEEE/ACM 3rd International Conference on Al Engineering- e Engineering for AI, pp. 140-149, 2024.
Tang, Z., Huang, C., Zheng, X., Hu, S., Wang, Z., Ge, D., and Wang, B. Orlm: Training large language models for optimization modeling, arXiv preprint arXiv:2405. 2024.
Khalil, E., Dai, H., Zhang, Y., Dilkina, B., and Song, L. Learning combinatorial optimization algorithms over graphs. Advances in neural information processing sys- tems, 30, 2017.
Wang. Z., Zhu, Z., Han, Y., Lin, Y., Lin, Z., Sun, R., and Ding, T. Optibench: Benchmarking large language mod- els in optimization modeling with equivalence-detection evaluation. 2024.
Korte, B. and Vygen, J. Shortest paths. Combinatorial Op- fimization: Theory and Algorithms, pp. 157-171, 2012.
Wasserkrug, S., Boussioux, L.,, Hertog, D. d., Mirzazadeh, F., Birbil, I., Kurtz, J., and Maragno, D. From large language models and optimization to decision optimiza- tion copilot: A research manifesto. arXiv preprint arXiv:2402. 16269, 2024.
Lawless, C., Li, Y., Wikum, A., Udell, M., and Vitereik, E. Lims for cold-start cutting plane separator configuration. arXiv preprint arXiv:24122 / 2024a.
Lawless, C., Schoeffer, J., Le, L., Rowan, K., Sen, S., St. Hill, C., Suh, J., and Sarrafzadeh, B. "i want that way": Enabling interactive decision support using large language models and constraint programming. ACM Transactions on Interactive Intelligent Systems, 14(3): 1-33, 2024h.
Xiao, Z., Zhang, D., Wu, Y., Xu, I.., Wang, J.J., Han, X., Fu, X., Zhong, T., Zeng, J., Song, M., et al. Chain-of- experts: When Ilms meet complex operations research problems. In The Twelfth International Conference on Learning Representations, 2023.
Li, B., Mellou, K., Zhang, B., Pathuri, J., and Menache, Large language models for supply chain optimization. arXiv preprint arXiv:2307.03875 2023a.
Xing, L., Wang, X., Feng, Y., Fan, Z., Xiong, J., Guo, Z., Fu, X., Ramamonjison, R., Mostajabdaveh, M.. Han, X., et al. Towards human-aligned evaluation for linear program- ming word problems. In Proceedings of the 2024 Joint International Conference on Computational Linguistics, Language Resources and Evaluation CLREC-COLING 2024), pp. 16550-16556, 2024.
Li, Q.. Zhang, L., and Mak-Hau, V. Synthesizing mixed- integer linear programming models from natural language descriptions. arXiv preprint arXiv:2311.152 15271, 2023b.
Mostajabdaveh, M., Yu, T. T., Ramamonjison, R., Carenini, G., Zhou, Z., and Zhang, Y. Optimization modeling and verification from problem specifications using multi- agent multi-stage Ilm framework. INFOR: Information Systems and Operational Research, 62(4))599-617, 2024.
Yang, 7.,, Wang. Y., Huang, Y., Guo, 7., Shi, W., Han, X., Feng, L., Song, L., Liang, X., and Tang. J. Optibench meets resocratic: Measure and improve llms for opti- mization modeling. arXiv preprint arXiv:2407.09887 2024.
Papadimitriou, C. H. and Steiglitz, K. Combinatorial opti- mization: algorithms and complexity. Courier Corpora- tion, 1998.
Yu, H. and Liu, Deep insights into automated optimization with large language models and evolutionary algorithms. arXiv preprint arXiv:2410.2088 2024.
Pisinger, D. and Toth, P. Knapsack problems. 1998.
Springer,
10

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
A. Additional Experimental Details and Results
In this section, we segment our main results by problem class (i.e., LP vs. MILP), and equivalence (i.e., equivalent vs. nonequivalent). We also include the fraction of each instance solved correctly for each problem type. Our results are consistent across both LP and MILP instances, highlighting that EquivaMap outperforms all baseline methods all settings.
Table 3: Accuracy of equivalence-checle methods formulations obtained from equivalent transformations. Rows partitioned by whether the problems are linear programming problems (LP) or mixed-integer linear programming problems (MILP). Numbers in parentheses correspond to the raw fraction of instances solved correctly.
Transformation
Canonical Acc.
Execution Acc.
WL-test
naive-LLMM
EquivaMap
I.P
Substitute Objective Functions
0%(0/92)
100%(92/92)
0%:(0/92)
94.6%(87/92)
(009(92//
Add Slack Variables
(%(0/59)
(005())9)5))
0%(0/59)
49.1%(29/59)
1009k(59/59)
Replace by Base-10 Representation
0%(0/44)
100%(44444))
0%(0/44)
50%(22/44)
100%/(44/44)
Add Valid Inequalities
(%/()/))
(92992)
0%:(0/92)
(.5%))/92)
(00%(92/92)
Rescaling
(0/6)))
(%((1/))
0%6(0/))
766766))
(6066)))))
Replace by Linear Combinations
(%707/
(777777777)
0%6(7/7)
13.0%
1007(77777)
MILP
Substitute Objective Functions
0%6(0/14))
(10%(140/144 140)
0%(0//40)
(7.9%((233114))
100%((40//440)
Add Slack Variables
0%%(0/)3)
100%(1344/34) 334
0%(0/134)
23.14(31//34)
100%(134/134)
Replace by Base-10 Representation
016(O//23)
0%((1/13)
56.19(69//13)
100%(123/123)
Add Valid Inequalities
(%/(4/)))
(142(14//)42)
0%(0//12)
(%(0//42)
100%(142/142)
Rescaling
(%113))
(%%(1/)))
(%(0//33)
(3.29((84/133))
100%(133/133)
Replace by Linear Combinations
0%(0//15)
100%(115/115)
0%(0/115)
35.7%(441/115)
100%((15/115)
Table 4: Accuracy of equivalence-ccecking methods on formulations obtained from nonequivalent transformations. Rows are partitioned
by whether the problems are linear programming problems (LP) mixed-integer linear programming problems (MILP). Numbers in parentheses correspond the raw fraction instances solved correctly.
Transformation
Canonical Ace.
Execution Acc.
WL-test
naive-LLM
EquivaMap
LP
Random Order
1008()7/87)
(80887)7)7))
1009(87787)
98.97)))
100%((7787)
Loose Constraints
1005(53/53)
100%(53/53)
100%(53/53)
88.7%(47/53)
100%(53/53)
Feasibility
1808(87/87)
0%(0//7)
1009(877/7))
100%(87/87)
100%((7787))
MILP
Random Order Loose Constraints
(00%(142//42)
(002(142/142)
(002(142/142)
98. (140/(14))142)
100%(142/142)
(020(12)/)
100%(120/120)
100((120/120)
96. 96.7%(116//20)
(000(120/120)
Feasibility
100%(142/142)
(0114/)))
(00((1442/42))
(042(1422442)
100% (142/14))
B. Prompts
B.1. naive-LLM Prompt
Listing 1: naive-LLM Prompt
You are given two optimization problem formulations (both declared as MIP). Decide if they are equivalent formulations.
First problem formulation (Problem
"A laundromat can buy two types of washing machines, a top- loading model and front-loading model. The top-loading model can wash MashiatteTooLoodding itens per day while the front-loading model can wash MashRateeFrotLLoddii items per day. The top-loading model consumes therggcoonammptioroooloaaaddii kwh per day while the front Front-loading model consumes

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
amergyoonsnmpiiorrootttooodddia kwh per day. The laundromat must able wash
least MinItemaPerDay items per day and has available MaxtnergyPerDay kwh per day. Since the top-loading machines are harder to use, at most MaxFraction wtt.rraacticntoooaadingg of the machines can be top-Loading. Further, at least MinNumPronticacinn machines should be front-loading. How many of each machine should the laundromat buy minimize the total nunber of washing machines?", "keywords"; "N.A."
"parameters";
"washiateeloplladdinn""
"description "Number of items washed per day by top-loading machine", "shape": []
"ashiatterrnnnoddinn""
description": "Number of items washed per day by a front-loade machine", "shape": []
"dscripttion. "Energy consumed per day by top-loading machine (kWh)
"shape": []
"escription" "Energy consumed per day by tront-loading machine (kNa)
"shape" []
Mi "MinitemsPerbaa":
"éeccription; "Minimum number items to wash per day", "shape": []
"MaxnneggyPeraa"::
"dscrrpptinn"; "Maximum available energy per day (kWh)", "shape": []
"MaxPractticnnoooooednnn"" {
"éescriptinn" "Maximum fraction of machines that can be top-loading", "shape": []
description"; "Minimum number of front-loading machines", sshae": []
"variables":
"NunTopLoading":
"description"; "The number of top-loading machines", "type": "continuous",
"shape": []
"NunFrontlicading::
"descriptien"; "The number of front-loadin ng machines", "type": "continuous",
"shape": []
"constraints": [
"description:; "A top-loading machine washes WashRateTopIoadiing itema per day and front-loading machine washes rashatoFrootioading items per day, The total number of items washed per day must least MinItemsPerDay."" formulation"; "WashRateeTopLoadingg Veddot NunTopLoading + WistRatteFrottLoddinn W cdot NumFrontLoadinng Vige MinItemsPerDay",
cooe":
"gurcbipy"; "model addConstt (MashRateTogLoaddLng MunTopLoading WashRater enneRateFroteee Frott NumFrontLoadiin MinIt minI=emsPerDDy)
12

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
"description": "A top-loading machine consumes EneeggyOonsuumiiio////ooooooa küh per day and front-loading machine consumes wrrryyCoosuumtiioFrooooloaae küh per day. The total energy consumption per day cannot exceed MaxEnergyPerDay küh," "ormulation"; "NumTopLoading \\times mmerggyoneumpiionToplooo. Witimes EnoreyConssumiiooorrooo... code":
NunFrontLoading
Vileq MaxEnergyPexDay""
"gurobipy"; "model. addConstr wat.ooatttccttoooooooooooooooooo NunZopLoading
RnergyConsumpt
onFrontloading omorryyoossmppppooooooooooooooo NumProntlooading <- MaxinnegyPPertay)
"description": "At most MaxfrrcttionTopIodddin fraction of the total machines can be top-loading.",
formulation"; "NunTopicadiin \ \lleq MaxPractlontopLoadung Wtines (NunTopLoading NumFrontLoading))
code":
"gurcbipy": "model. addeonssdcCtsttt (Nomoooooaong <= MaxFractionnoolloddinn
NumTopLoading + NumFrontLoading))
"description"; "At least MaNWunFrontIoadinn machines must be front-Loading.";
formulation"; "Num'ronti Vggeq Mi Minhum/rontiooddnng".
"coee: {
"gurobipy"; "model.addCom (NumfrontiLoadiing Minlumtrronttioddinnn)
1,
"objective";
"dcscriptica"; "Minimize the tctal number of washing machines purchased.", "formulatica"; "Min V\ NumTopLoading NunFrontioading",
"code": {
"gurobipy"; "model "model. setobjecttt (NurTTolooadnn NumFrontloading,
Second problem formulation (Problem :):
bearametrieedddescriptttt
"A laundromat can buy two types of washing machines, top- loading model and front-loading model. The top-loading model can wash V items per day while the front-loading model can wash T items F küh per day while the front-loading model consumes A kWh per day. The Laundromat must be able to wash at least items per day and has available kWth per day. Since the top-loading machines are harder to use, at most of the machines can be top-loading. Further, at least W machines should be front-loading. How many of each machine should the laundromat buy to minimize the total number of washing nachines?",
day. The top-loading model
"keywords": "N.A."
"parameters";
"W":
description"; "The smallest quantity of front-loading machines. ",
shape": []
"A": (
ddscription": "Daily electricity usage of front-loading washer (kWh)
sshap"" []
"R":
13

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
description"; "The highest amount energy that can obtained in single day kwh) ,, "shape": []
"S": { "description"; "The highest percentage of machines that can have top-loading feature.",
"shape": []
"F": ( description"; "Daily energy usage of a lod-laading washing machine in kilowatt- hours",
shape" []
"J": (
"dscription": "The smallest quantity of items that need to be cleaned on daily basis",
"shape": []
"y": {
"description"; "Quantity of objects cleaned daily using a top-loading washer", "shape": []
"T": {
ddscrippion": "The quantity of objects cleaned daily with a front-loading washing machine.", "shap"": []
1, "variables":
"a": "descriptien"; "The quantity of top-loading appliances", "type"; "continuous",
"shape": []
)
"g": {
"description"; "The quantity of front-loading machines", "type": "continuous", "shape": II
raintstaints"
"description": "A top-loading washer cleans V items daily, while a front-loading washer cleans items daily. The combined total of items cleaned each day should fall below J.", "ormulationn; "J Vileq Wedot a Wedot g", "cod":
"gurcbipy"; IddCnns + T >= J)"
},
"objective"
"description"; "Reduce the everall quantity of washing machines bought.",
"formulation"; "Min \\ a",
"code":
"gurobipy"; "model. mrodel.setonn setobjetvett + g, MINIMIEE
Based on the data, please respond with exactly one of the following:
"Equivalent" if these two are the sane formulation. Be rigorous in your zeasoning. "Not Equivalent" if they are different. When you not sure, say "Not Equivalent".
14

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
Briefly explain the reasoning 1-2 sentences, then end with the word "Bquivalent or Not Equivalent" on its own line.
B.1.1. EquivaMap PROMPT
Listing 2: EquivaMap Prompt
You are language model assisting in mapping variables between optimization problems by ana analyzing their roles in constraints and the objective function.
*+Variable from Problem lit*
N*Name borrfemovingcheelllalbiiiie
**Desscriptin:: The number units of odor-removing chemical used per house
#CContraaints involving NorrRemviingheeicca calunits:**
Description: The total number of chemical units used per house cannot exceed MaxTotalUnits.
Formulation: CleansingChemicallhie
Vieq MaxTotalUnits
Description: The number of cleansing chemical units used cannot exceed
MaxcleanssiggToodortttt times the number of odor-rcmoving chemical units used. Formulation: ClcansingChemicallonno 0ddrRenoo.inghhemmccallli... ++In Objective Function:** Yes
Aleq MaxcleansingTooorrrattt \cdot
**Variables from Problem 2:**
**Name:** v_0
**Descriptien: Digit 0 of the The quantity of cleaning solution units utilized per household
* **Constraints involving v 0=**
Description: The quantity of cleansing chemical units applied must not surpass H times the quantity of odor-removing chemical units used.
Formulation: Aodot (f_0+10"0 f_1+10"1) \geg (v_0+10"0 v_i+10"1 v_2+10~2)
Descriptien: The cumulative quantity of chemical components utilized for each residence must not surpass T.
Formulation: T \geg (f_0x10"0= f_1+10"1) (v_0+10"0 v_1+10": - 2_
Descriptien: The company is required to utilize minimum of G units of the cleaning solution per household,
Formulation: G Aleq (v_0+10"0 + v_1+10"1 + v_2+1002)
*+In Objective Function:** Yes
Name v_1
**Description:w Digit of the The quantity of cleaning solution units utilized per household
* **Constraints involving v li**
Descriptien:
The quantity of cleansing chemical units applied must not surpass E odor-removing chemical units used.
times the quantity
Formulation: н Aedot (f_0+10"0 f_1*10"1) \geq (v_0+10"0 v_1+10"1 v_2+10"2)
Description: The cumulative quantity of chemical components utilized for each residence must not surpass T.
Formulation: \geq (f_0x10"0 f_1x10"1) (v_0x10"0 v_1x10"1 v_22x002)
Descriptien: The company is required to utilize minimum units the cleaning solution per household.
Formulaticn: G \leq (v_0+10"0 + v_1+10"1 + v_2+1002)
**In Objective Function:** Yes
Name:*** v_2
* <+Dscrrptiin:: Digit 2 of the The quantity of cleaning solution units utilized per household
**Constraints involving v 2=**
Descriptien: The quantity of cleansing chemical units applied must not surpass E times the quantity of odor-romoving chemical units used.
Formulation: и Aedot (f_0+10"0 + f_1+10"1) \geq (v_0+10"0- v_1+10"1 + v_2+10"2) Description: The cumulative quantity of chemical components utilized for each surpass T.
residence
Formulation: \geq (f_0x10"0- + f_1x10>1) (v_0x1010
v_1x1011 v_2x1012)
15

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
Descriptien: The company is required to utilize minimum units the cleaning solution per household.
Formulation: G Aleg (v_0+10"0 + v_1+10~1 + v_2+10"2)
++In Objective Function:*. Yes
**Name:** f_0
** **Descripticn: Digit 0 of the The quantity of odor-neutralizing chenical applied in each household
**Constraints involving f_0:**
Descriptien: The quantity of cleansing chemical units applied must not surpass E times the quantity of odor-removing chemi cal units used.
Cormulation; H Acdot (f_0+10"0 + f_1x1001) \geq (v_0x10"0 v_ix10"1 + v_2x10"2)
Description The cumulative quantity of chemica cal components utilized for each residence not surpass T.
Formulatien: \geq (E_0+10"0 =_1+10"1) (v_0+10"0 v_1=10 v 2=10"2)
*+In Objective Function:** Yes
Name::4 f_1
*+Descriptien:M Digit of the The quantity of odor-neutralizing chenical applied in each household
* **Constraints involving f_l:**
Description:
The quantity of cleansing chemical units applied must not surpass H times the quantity of odor-removing chemical units used.
Formulatien: Aedot (E_0+10"0 f_1+10"1) \geg (v_0+10"0 v_i+10"1 y_)+10 Description: The oumulative quantity of chemical components utilized for each residence must not surpass T.
Formulation: Ageq (f_0+10"0 + f_1+10"1) (v_0+10~0 v_1x1011 v_2x10-2)
Objective Function:**
Based the abeve information, find the best mapping from variables in Problem for the variable (oooReemoringchhmmccllllll from Froblem 1. The mapping be a linear conbination variables from Problem 2, possibly with constant multipliers. Your goal is to express "ddorecnooiighhcccaaalatts accurately as possible, based on their roles in the constraints and objective functions.
in terms of variables from Problem 2, as
Important Instructions:**
**Provide enly the mapping for "odrrtenoringghhemllallltttas as JSON object.** **Do not include any additional text, explanations, or formatting. **The JSON object follow this exact structure:**
"odbrleemviinghhhettlllllii
"constant"; constant_value_1
"variable"; "variable_name_j"
"constant"; constant_value_,, vvariable:; "variable_name_ ,
++If there is only one term in the mapping, the 1ist should contain. a single object.** ++Use numerical values for constants (decimals), and enclose variable names in double quotes (**).**
**Exampee::**
1. If the best mapping is 10.1*a' your response should be:
16

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
"constant"; 0.1,
"variable"; "a"
2. the best mapping is 10.1+a 0.01+b', your response should be:
"Odor Redovi hegmoriiccnn ca TUnits":
"constant; 0.1, "vrriable,; "s"
"constant"; 0.01, variable"; "b"
3. If the best mapping is single variable 'a' with coefficient of 1, your response should be:
"constant: 1,
"variable;; "a"
4. there is direct mapping, your response should be:
"constant"; "none", *variable"; "none"
Please ensure your response is a valid JSON object that can be parsed by standard JSON parsers.
17

---

EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations
C. Maximum Independent Set example
O
Vartables":
"Yoriables:
"Node[8]": ("typen: "binary"),
"lde""
"Node [1 ("type": *binary"),
"type": "binary",
'Node ("Sype": *binary"),
"shape": ["Nunkdees"]
"Node[3]": ("type": "binary"),
"oostrrttnts:
"Constraints" {
formulation's "Node[t] Node(3] U Edges(A](3)
*c1' (*formulation": "Node[0] Node[1] x-
CC2' (fformuaaioon: "Node[3] Node[2] 1)....
Set-based Representation
Individual Variable Representation
Figure 3: Comparison between set-based and individual-variale representations in JSON input formatting. EquivaMap
operates on sets variables, allowing the metadata and constraints to be described concisely (left) instead of expanding each variable individually, resulting longer and more redundant prompts (right).
Consider the maximum independent set example in Figure EquivaMap takes in set-based representations of input formulations (left). When the prompt iterates between variables of formulations and a', processes the entire 'Node" set input, rather than individual variables like Node 1, Node 2, etc. If variables in formulation alpha' are labeled as Node', the mapping discovered by the LLM will be Node Node' [i], Vi, instead of separate mappings for each indexed variable. This distinction is crucial for scalability, as it means our prompt size remains constant regardless of the number of nodes in the graph.
D. Runtime Analysis
To evaluate the computational overhead of EquivaMap and the baseline methods, measured the average runtime across all instances in dataset. The breakdown of time spent different components is presented in Table 5,
Table 5: Mean (+ std. dev.) runtime (seconds) per instance for different components of EquivaMap and baselines. Runtime is averaged across all instances in the EquivaFormulatin dataset.
Method
Solving Time
LLM Call Time
WL.-esst Time
Total
Execution Accuracy
0.12 + 0.02
0.12 0.02
WL-Test
0.38 + 0.07
0.38 + 0.07
EquivaMap
0.12 + 0.02
11.88 + 4.48
12.00 + 4.50
While EquivaMap exhibits higher total runtime compared to the baselines, this cost should be considered in light of its significantly improved accuracy and its ability to identify complex mappings that other methods miss (as shown in Section 4.2). The LLM interaction, though currently the bottleneck, enables a level of symbolic reasoning and mapping discovery previously unattainable.
also worth noting that this runtime for a single equivalence check. practice, formulation equivalence checking is often an offline analysis task where a higher runtime can be tolerated in exchange for reliable results. Furthermore, the LLM call time potentially be reduced with more optimized prompting strategies, the use of smaller fine-tuned models, or by leveraging future advancements in LLM efficiency. Additionally, discussed in Section 3.3, EquivaMap's prompt length scales with the number of sets of variables rather than individual variables, which helps manage the LLM interaction cost for larger, structured problems.
18


Reviews:
[{"review_id": "GGhYNOKZPW", "reviewer": "Reviewer_NwSG", "summary": "This paper discusses how LLMs (+ NLP) can help with automatic checking of equivalences in the context of combinatorial optimization reductions.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We sincerely thank the reviewer for their positive and thoughtful comments, and for recognizing the novelty of our work: \n\n> “The paper gives a novel connection between computational complexity and LLMs.”\n\nBelow, we address the specific questions and suggestions: \n\n---\n\n> **Q1**: \"Since you are mentioning cutting planes, do you see any connections of your work to proof complexity, etc.?\"\n\n**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.\n\n> **Q2**: \"Algorithm 1: I think you should elaborate on the LLM prompt. This step is a bit hand-wavy\"\n\n**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.\n\n> **Q3**: \"Why is it a reasonable assumption that LLM inference is in poly-time?\"\n\n**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.”\n\n\n\nMoreover, 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.\n\n> **Q4**: \"I think that in the Discussion, you should elaborate more on future work directions.\"\n\n**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.", "claims_and_evidence": "Yes, the experiments are convincing.", "methods_and_evaluation_criteria": "Yes.", "theoretical_claims": "N/A.", "experimental_designs_or_analyses": "Yes, the ones in the main body.", "relation_to_broader_scientific_literature": "They explore a novel direction in the use of LLMs, whereby LLMs are used as a copilot in checking equivalence between instances that are inputs/outputs of reductions.", "essential_references_not_discussed": "No.", "other_strengths_and_weaknesses": "Strengths:\nThe paper gives a novel connection between computational complexity and LLMs.\nEn route, the authors introduce a new kind of reductions, namely quasi-Karp reductions, which might be of independent interest.\n\nWeaknesses:\nTechnically, the paper is not so deep :)", "other_comments_or_suggestions": "None.", "questions_for_authors": "Page 4:\nSince you are mentioning cutting planes, do you see any connections of your work to proof complexity, etc.?\n\nPage 5:\nAlgorithm 1:\nI think you should elaborate on the LLM prompt.\nThis step is a bit hand-wavy :)\n\nPage 6:\nWhy is it a reasonable assumption that LLM inference is in poly-time?\n\nPage 8:\nI think that in the Discussion, you should elaborate more on future work directions.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "LwE7Jc5jqJ", "reviewer": "Reviewer_46ti", "summary": "The paper introduces EquivaMap, an LLM-based framework for automatically verifying equivalence between combinatorial optimization formulations (MILP). It defines a new theoretical criterion called quasi-Karp equivalence, enabling robust equivalence checks even under transformations like variable scaling or auxiliary variables. Additionally, the authors create EquivaFormulation, a benchmark dataset of equivalent formulations. Experiments show EquivaMap achieves high accuracy, significantly outperforming baseline methods.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "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. \n\nCompared 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.\n\nIn 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.", "claims_and_evidence": "The claims appear reasonably supported by the designed experiments.", "methods_and_evaluation_criteria": "Yes, both the proposed quasi-Karp equivalence and the designed dataset look reasonable to me.", "theoretical_claims": "There isn't any proof. The definitions look good to me.", "experimental_designs_or_analyses": "I appreciate the current design of the experiments. The only extra experiment/discussion I would love to see is the running time of the EquivaMap algorithm: since the algorithm heavily relies on a capable solver to establish the robust equivalence mapping between problem formulations, the running time of such solvers and its relationship with the size of input formula should be taken into account.", "relation_to_broader_scientific_literature": "I envision this paper could be beneficial to the operations research.", "essential_references_not_discussed": "N/A", "other_strengths_and_weaknesses": "The paper is well-written, with clear mathematical definitions and illustrative examples that effectively convey the key ideas.", "other_comments_or_suggestions": "N/A", "questions_for_authors": "N/A", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "5sDDMwaxsE", "reviewer": "Reviewer_FhjQ", "summary": "This paper proposes a new method to assess whether two mathematical MILP formulations of a combinatorial optimization problem are equivalent. To this end, it proposes a formal notion of equivalence inspired by standard Karp reductions, creates a new dataset called EquivaFormulation for assessment, and compares the proposed method against 3 common existing approaches and a naive LLM-based approach. It finds that the proposed method, EquivaMap, works perfectly on the dataset, while all other baselines struggle in some, if not all, categories.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "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.\n\n---\n\n>**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.” \n\n**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.  \n\n>**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.\"\n\n**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)\nunder 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.\n\n>**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?\"\n\n**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.\n\n>**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?\" \n\n**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**. \n\nHowever, 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. \n\nTo conclude, **the mapping is over formulations, while the verification check is over instances**. \n\n> **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.”\n\nA5: 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.” \n\n---\n\nWe 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.", "claims_and_evidence": "The main claim, that EquivaMap is more effective at recognizing problem formulation equivalence, seems sufficiently supported on the specific classes of transformations considered in EquivaFormulation and in Table 2. It's not clear whether EquivaMap will also work equally well in natural and real settings, such as the motivating one involving that the authors refer to as optimization copilot, or in scenarios where multiple transformations are stacked together. The evaluation does not assess these.", "methods_and_evaluation_criteria": "Yes", "theoretical_claims": "The way the authors formulate and pitch the notion of \"Quasi-Karp Equivalence\" seems to lack some precision (unless I misunderstood something). Overall, I like this formal way of defining when two problems are equivalent. However, the following is causing confusion:\n\n* While a reduction is naturally a one-way map (e.g., every \"simpler\" problem in the class NP reduces to an NP-complete problem, but not vice versa), I was naturally expecting *equivalence* to be a symmetric property. I am unclear why the authors didn't define problem formulations alpha and alpha' to be equivalent if alpha quasi-Karp reduce to alpha' AND alpha' quasi-Karp reduces to alpha. In fact, this is precisely how Karp equivalence is defined (two NP-complete problems are equivalent because they both reduce to each other).\n\n* I don't quite see how the 2nd and 3rd bullet are different. Isn't it the case that f found be polynomial if and only if (some well-chosen) A computing f runs in polynomial time?\n\n* In several places, the paper highlights the new notion being *instance-specific*. However, I really don't see how this is the case, after reading the description in section 3.2 and even after reading the detailed prompt in Appendix A. It seems to me a map from one problem formulation to another problem formulation. Just like in standard Karp reductions, it's a map from variables of one formulation to variables of another formulation. What is instance-specific about it? Wouldn't the transformation function be identical two different instances of, say, a traveling salesman problem? (I don't think this takes away anything from the findings, it's just confusing. E.g., the sentence \"our method aims to evaluation the equivalence.... for a given instantiation of the problem\" is confusing and doesn't seem to correctly represent what's being done)\n\n* In several places, the paper highlights the new notion is a mapping from *solutions* to solutions, suggesting that a Karp reduction is not. But this isn't quite accurate --- a standard Karp mapping is precisely from an instance of a problem (e.g., network flow) to an instance of another problem (e.g., 3-SAT). It's always a mapping from variables of one problem to variables of the other problem, exactly like the proposed quasi-Karp mapping is. The only relevant difference is that the two problems considered are the same in this case, it's just that one has two distinct MILP formulations for it. But the mapping is still from variables of one to variables of the other.", "experimental_designs_or_analyses": "Experiments seem justifiable. Results in Table 2 help clearly see which aspects of transformation (different rows) various methods struggle or excel at.\n\nHowever, as noted above, this evaluation dataset is synthetic and designed specifically around individual transformations. In practice, I suspect one will find combinations of various transformations from one formulation to another. The current evaluation does not test EquivaMap in such compositional transformation scenarios (or on actual instances of transformations seen in the motivating optimization copilot research).\n\nThe \"worst case\" line in Table 2 is a bit confusing and not very helpful. I would suggest dropping it, possibly replacing it with \"average\" line.", "relation_to_broader_scientific_literature": "To my limited knowledge of the area, the findings seem relevant, well-motivated, and novel. There are some concerns about clarity of the theoretical formalism and coverage of empirical findings, as discussed above.", "essential_references_not_discussed": "N/A", "other_strengths_and_weaknesses": "N/A", "other_comments_or_suggestions": "* page 6, line 303, LLM inference time being polynomial in the input length: Specific soft-quadratic time and linear space bounds are known for transformers, e.g., The Expressive Power of Transformers with Chain of Thought, ICLR-2024.\n\n* page 2, line 70: the Karp citation is presumably for the seminal paper where Karp shows dozens of problems to be equally NP-complete. That work was done in 1972, not 2010!\n\n* page 2, line 83: similarly, Cook's book was published earlier than 2011, around 2007 I believe. please double-check.", "questions_for_authors": "Please see some questions in the theoretical and empirical sections above.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "J8KoXN801s", "reviewer": "Reviewer_u5nU", "summary": "The submission proposed a new method for determining whether two optimization problem formulations are equivalent. The authors introduce Quasi-Karp Equivalence, based on Karp reductions, and propose EquivaMap, a framework that utilizes LLMs to identify mappings between decision variables of different formulations.  The paper also introduces EquivaFormulation, the first open-source dataset of equivalent optimization formulations. Experimental results demonstrate that EquivaMap outperforms existing equivalence-checking methods, including execution accuracy, canonical accuracy, and graph-based approaches. The contributions are positioned within the broader context of optimization copilots and automated mathematical modeling.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We sincerely thank the reviewer for the detailed feedback and for acknowledging the contribution of our work: \n\n> \"The introduction of Quasi-Karp Equivalence is an important conceptual contribution.\"\n\n>” The EquivaFormulation dataset is a valuable resource for future research.”\n\n>” The work is timely, given the increasing interest in AI-assisted optimization modeling.”\n\n---\n\nBelow, we address the questions raised:\n\n> **Q1**: \"... Could you provide a more challenging example that better demonstrates the depth of reasoning needed to discover a valid mapping?\" \n\n**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. \n\n> **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?\"\n\n**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).  \n\nWe 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.\n\n\n> **Q3**: \"... Have you explored or considered approaches that could ensure (or at least give stronger guarantees of) equivalence across all instances rather than one?\"\n\n**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. \n\n> **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?\"\n\n**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.\n\n\n>**C1**: “The methods…  partial equivalence … formulations align.”\n\n**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.", "claims_and_evidence": "The authors provide sufficient evidence to support their claims. However, I have some doubts about the scalability of EquivaMap in practical applications (mathematical modeling copilots), as it requires multiple calls to both the LLM and the solver for each problem instance. Furthermore, we typically seek a formulation that is correct for all problem instances, whereas EquivaMap can only demonstrate instance-specific equivalence, not a general equivalence.", "methods_and_evaluation_criteria": "The methods—embedding an LLM-based “mapping finder” plus a solver-based verification step—are straightforward and well-motivated. However, one drawback of the proposed approach is that it cannot account for partial equivalence between two formulations, which would be beneficial for more refined accuracy metrics. In contrast, methods like canonical accuracy and graph-edit distance do provide a measure of partial similarity, allowing more nuanced evaluations of how closely two formulations align.", "theoretical_claims": "Quasi-Karp Equivalence: Inspired by polynomial-time Karp reductions, but the formal proof of correctness or completeness is limited to a set of instance-specific transformations. There is no guarantee that every subtlety in modern MILP formulations (such as symmetries or problem-specific decomposition constraints) can be captured by a single linear mapping.", "experimental_designs_or_analyses": "- The new dataset is well-constructed, covering various equivalence-preserving transformations.\n- Baseline comparisons include execution accuracy, canonical accuracy, WL-test, and a naive LLM approach.", "relation_to_broader_scientific_literature": "The paper is well-situated within the broader research on LLM-based optimization modeling automation. The discussion on optimization copilots aligns with recent advancements in AI for mathematical modeling.", "essential_references_not_discussed": "The paper cites key relevant works.", "other_strengths_and_weaknesses": "- The introduction of Quasi-Karp Equivalence is an important conceptual contribution.\n- The EquivaFormulation dataset is a valuable resource for future research.\n- The work is timely, given the increasing interest in AI-assisted optimization modeling.", "other_comments_or_suggestions": "- A breakdown of computational costs (LLM inference time vs. solver time) would provide insights into practical deployment.", "questions_for_authors": "1 - The identity mapping in Figure 1 appears overly simple and may not effectively illustrate the complexity of the LLM-based mapping step. Could you provide a more challenging example that better demonstrates the depth of reasoning needed to discover a valid mapping?\n\n2 - Because EquivaMap relies on instance-specific mappings, 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?\n\n3 - EquivaMap verifies equivalence only for specific instances, not universally for the entire family of instances. Have you explored or considered approaches that could ensure (or at least give stronger guarantees of) equivalence across all instances rather than one?\n\n4 - The framework currently restricts the mapping function f to be linear. This effectively limits the kinds of transformations EquivaMap can capture. 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?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "r0uQe0erCl", "reviewer": "Reviewer_Nbcm", "summary": "This paper addresses the challenge of checking equivalence among modeling formulations. The authors introduce quasi-Karp as an equivalence criterion for determining model equivalence. The primary concept of this criterion involves verifying the existence of \"equivalence mapping\" (quasi-Karp) between models. The authors leverage GPT-based methods to automatically identify the existence of these equivalencies. The dataset used in experiments is derived from the NL4OPT dataset, further crafted by introducing equivalent and non-equivalent transformations. Experimental results indicate that Equivamap achieves 100% accuracy on this dataset.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "We sincerely thank the reviewer for the detailed feedback and for acknowledging the importance of our work: \n\n> \"This work tries to address an important challenge in modeling equivalence checking, where previous works have not provided sufficiently satisfying solutions.\"\n\nand for recognizing the soundness of our definition:\n\n> \"The definition of quasi-Karp equivalence is sound and reasonable.\"\n\nWe 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.\n\n---\n\n> **C1**: Generalizability to More Complex Datasets (e.g., MAMO (ComplexLP), IndustryOR)\n\n**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.  \n\nSpecifically, 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. \n\nThough 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.\n\nWe 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].\n\n[1] AhmadiTeshnizi, A., et al. (2024). Optimus-0.3: Using LLMs to model and solve optimization problems at scale. \n\n> **C2**: Scalability with the increase of the dimensionality of the problem and corresponding input prompt length\n\n**A2**: A key feature of EquivaMap is that it operates over **sets of variables**, rather than individual variables in a large-scale instance.\n\nFor 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.\n\nThis 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. \n\n > **C3**: Reliability on LLMs introduces a risk of hallucinations, where the model might generate plausible but incorrect equivalence mappings\n\n**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.\n\nThis 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.", "claims_and_evidence": "Not sufficiently clear and convincing.\n\nThe experiments are restricted to a dataset derived from the NL4OPT dataset, crafted by introducing equivalent and non-equivalent transformations. Broader experimentation or testing on diverse datasets would enhance result validity and generalizability.\n\nFurther, the experiments only show that", "methods_and_evaluation_criteria": "No, not enough.\n\nNL4OPT is a relatively simple dataset and there are more complex, and closer-to-reality ones, like MAMO (ComplexLP) and IndustryOR. The generalizability of EquivaMap to more challenging problems remains uncertain.", "theoretical_claims": "No proof is involved.\n\nThe definition of quasi-Karp equivalence is sound and reasonable. If the mapping defined in quasi-Karp equivalence exists, then the two optimization models are equivalent. This claim is true by definition, without the need for separate proof.", "experimental_designs_or_analyses": "See **Claims And Evidence** and **Methods And Evaluation Criteria**.", "relation_to_broader_scientific_literature": "The ideas of the equivalent transformations (used in the construction of the dataset) are from the optimization area (MILP).", "essential_references_not_discussed": "Not found yet.", "other_strengths_and_weaknesses": "Other Strengths:\n- This work tries to address an important challenge in modeling equivalence checking, where previous works have not provided sufficiently satisfying solutions.\n\nOther Weakness:\n- The method faces scalability issues. As the dimensionality of the problem increases, the input prompt length could significantly grow.\n- The method also faces reliability issues. The reliance on LLMs introduces a risk of hallucinations, where the model might generate plausible but incorrect equivalence mappings. Such inaccuracies can be challenging to detect, potentially impacting the reliability of Equivamap in more complex or realistic scenarios.", "other_comments_or_suggestions": "NA", "questions_for_authors": "In practice, when using the proposed method to benchmark LLMs for optimization modeling, can the proposed method provide better accuracies than the existing method? Specifically on more complex datasets like MAMO (ComplexLP) and IndustryOR.", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {"ethical_review_concerns": "NA"}}]

Author rebuttal:

Meta-review: This paper focuses on the problem of of automatically verifying equivalence between combinatorial optimization formulations (MILP) via LLMs and to this end, proposes the notion of quasi-karp like reductions. The reviewers found the paper's claims to be well motivated and supported: The writing at times appears imprecise and there is detailed feedback by reviewers. The reviewers who have provided feedback have deep expertise in computational complexity and therefore, I strongly recommend authors improve the final version by taking into the feedback of reviewers into account else authors risk the paper to be ignored by theoretical community.
Decision: Accept (poster)