EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations

A fundamental problem in combinatorial optimization is identifying equivalent formulations. Despite the growing need for automated equivalence checks---driven, for example, byoptimization 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 workwe introduceQuasi-Karp equivalence, a formal criterion for determining when two optimization formulations are equivalentbased on the existence of a mapping between their decision variables. We proposeEquivaMap, 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 constructEquivaFormulation, the first open-source dataset of equivalent optimization formulations, generatedby applying transformations such as adding slack variables or valid inequalitiesto existing formulations.Empirically,EquivaMapsignificantly outperforms existing methods, achieving substantial improvements in correctly identifying formulation equivalence.