Total: 1
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 workwe introduce *Quasi-Karp equivalence*, a formal criterion for determining when two optimization formulations are equivalentbased 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, generatedby applying transformations such as adding slack variables or valid inequalitiesto existing formulations.Empirically, *EquivaMap*significantly outperforms existing methods, achieving substantial improvements in correctly identifying formulation equivalence.