EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations

Haotian Zhai, Connor Lawless, Ellen Vitercik, Liu Leqi
Proceedings of the 42nd International Conference on Machine Learning, PMLR 267:74288-74305, 2025.

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.

Cite this Paper

BibTeX
@InProceedings{pmlr-v267-zhai25a, title = {{E}quiva{M}ap: Leveraging {LLM}s for Automatic Equivalence Checking of Optimization Formulations}, author = {Zhai, Haotian and Lawless, Connor and Vitercik, Ellen and Leqi, Liu}, booktitle = {Proceedings of the 42nd International Conference on Machine Learning}, pages = {74288--74305}, year = {2025}, editor = {Singh, Aarti and Fazel, Maryam and Hsu, Daniel and Lacoste-Julien, Simon and Berkenkamp, Felix and Maharaj, Tegan and Wagstaff, Kiri and Zhu, Jerry}, volume = {267}, series = {Proceedings of Machine Learning Research}, month = {13--19 Jul}, publisher = {PMLR}, pdf = {https://raw.githubusercontent.com/mlresearch/v267/main/assets/zhai25a/zhai25a.pdf}, url = {https://proceedings.mlr.press/v267/zhai25a.html}, 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.} }
Endnote
%0 Conference Paper %T EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations %A Haotian Zhai %A Connor Lawless %A Ellen Vitercik %A Liu Leqi %B Proceedings of the 42nd International Conference on Machine Learning %C Proceedings of Machine Learning Research %D 2025 %E Aarti Singh %E Maryam Fazel %E Daniel Hsu %E Simon Lacoste-Julien %E Felix Berkenkamp %E Tegan Maharaj %E Kiri Wagstaff %E Jerry Zhu %F pmlr-v267-zhai25a %I PMLR %P 74288--74305 %U https://proceedings.mlr.press/v267/zhai25a.html %V 267 %X 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.
APA
Zhai, H., Lawless, C., Vitercik, E. & Leqi, L.. (2025). EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations. Proceedings of the 42nd International Conference on Machine Learning, in Proceedings of Machine Learning Research 267:74288-74305 Available from https://proceedings.mlr.press/v267/zhai25a.html.

Related Material