EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations

TL;DR

EquivaMap uses large language models to automatically and reliably verify the equivalence of different optimization problem formulations, improving over heuristic methods and supporting scalable applications.

Contribution

Introduces Quasi-Karp equivalence and EquivaMap framework, leveraging LLMs for automated, scalable, and reliable equivalence checking of optimization formulations.

Findings

Outperforms existing equivalence checking methods

Creates the first open-source dataset of equivalent formulations

Achieves high accuracy in identifying equivalent formulations

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.