A fundamental problem in combinatorial optimization is identifying equivalent formulations, which can lead to more efficient solution strategies and deeper insights into a problem's computational complexity. The need to automatically identify equivalence between problem formulations has grown as optimization copilots--systems that generate problem formulations from natural language descriptions--have proliferated. However, existing approaches to checking formulation equivalence lack grounding, relying on simple heuristics which are insufficient for rigorous validation. 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, enabling scalable and reliable equivalence verification. To evaluate our approach, we construct 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.

该研究解决了组合优化领域中识别等价公式的问题，进而提升解决策略的效率和对计算复杂性的理解。本文提出了一种基于决策变量映射的准卡普等价性标准，并开发了EquivaMap框架，利用大型语言模型自动发现这些映射，显著提高了等价性验证的准确性和可扩展性。研究结果表明，EquivaMap在识别公式等价性方面优于现有方法，具有重要的理论和实际影响。

EquivaMap：利用大型语言模型进行优化公式的自动等价性检查