@inproceedings{bhattacharyya-baranwal-2026-sover,
title = "{SOVER}: Formal Certification of Optimization Reformulations via {LLM}-Assisted {SMT} Verification",
author = "Bhattacharyya, Swapnil and
Baranwal, Mayank",
editor = "Lee, Hung-Yi and
Dev, Sunipa and
Li, Jessy and
Elliott, Desmond",
booktitle = "Findings of the {A}ssociation for {C}omputational {L}inguistics: {EMNLP} 2026",
month = oct,
year = "2026",
address = "Budapest, Hungary",
publisher = "Association for Computational Linguistics",
url = "https://aclanthology.org/2026.findings-emnlp.1886/",
doi = "10.18653/2026.findings-emnlp.1886",
pages = "40213--40230",
ISBN = "979-8-89176-462-0",
abstract = "Large Language Models (LLMs) have shown remarkable promise in translating and reformulating complex mathematical optimization problems across modeling languages. However, validating such transformations through empirical solver executions alone is unreliable, as solver outcomes may be affected by local minima, structural timeouts, numerical artifacts, and subtle semantic divergence between formulations. We introduce SOVER, an LLM-assisted SMT framework that separates semantic mapping from formal certification: Z3 checks domain cross-feasibility and global objective order preservation for mixed-integer linear formulations, while dReal provides tolerance aware feasibility/range and {\ensuremath{\varepsilon}}-argmin checks for continuous nonlinear formulations. We also introduce NLEQUIV-150, a public benchmark of 100 equivalent and 50 deliberately hard non-equivalent nonlinear reformulation pairs. With LLM-extracted mappings, SOVER classifies 149/150 pairs (99.33{\%}) correctly, including all 50 hard negatives; the sole error is an incomplete mapping extraction."
}<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="bhattacharyya-baranwal-2026-sover">
<titleInfo>
<title>SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification</title>
</titleInfo>
<name type="personal">
<namePart type="given">Swapnil</namePart>
<namePart type="family">Bhattacharyya</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Mayank</namePart>
<namePart type="family">Baranwal</namePart>
<role>
<roleTerm authority="marcrelator" type="text">author</roleTerm>
</role>
</name>
<originInfo>
<dateIssued>2026-10</dateIssued>
</originInfo>
<typeOfResource>text</typeOfResource>
<relatedItem type="host">
<titleInfo>
<title>Findings of the Association for Computational Linguistics: EMNLP 2026</title>
</titleInfo>
<name type="personal">
<namePart type="given">Hung-Yi</namePart>
<namePart type="family">Lee</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Sunipa</namePart>
<namePart type="family">Dev</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Jessy</namePart>
<namePart type="family">Li</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<name type="personal">
<namePart type="given">Desmond</namePart>
<namePart type="family">Elliott</namePart>
<role>
<roleTerm authority="marcrelator" type="text">editor</roleTerm>
</role>
</name>
<originInfo>
<publisher>Association for Computational Linguistics</publisher>
<place>
<placeTerm type="text">Budapest, Hungary</placeTerm>
</place>
</originInfo>
<genre authority="marcgt">conference publication</genre>
<identifier type="isbn">979-8-89176-462-0</identifier>
</relatedItem>
<abstract>Large Language Models (LLMs) have shown remarkable promise in translating and reformulating complex mathematical optimization problems across modeling languages. However, validating such transformations through empirical solver executions alone is unreliable, as solver outcomes may be affected by local minima, structural timeouts, numerical artifacts, and subtle semantic divergence between formulations. We introduce SOVER, an LLM-assisted SMT framework that separates semantic mapping from formal certification: Z3 checks domain cross-feasibility and global objective order preservation for mixed-integer linear formulations, while dReal provides tolerance aware feasibility/range and \ensuremathǎrepsilon-argmin checks for continuous nonlinear formulations. We also introduce NLEQUIV-150, a public benchmark of 100 equivalent and 50 deliberately hard non-equivalent nonlinear reformulation pairs. With LLM-extracted mappings, SOVER classifies 149/150 pairs (99.33%) correctly, including all 50 hard negatives; the sole error is an incomplete mapping extraction.</abstract>
<identifier type="citekey">bhattacharyya-baranwal-2026-sover</identifier>
<identifier type="doi">10.18653/2026.findings-emnlp.1886</identifier>
<location>
<url>https://aclanthology.org/2026.findings-emnlp.1886/</url>
</location>
<part>
<date>2026-10</date>
<extent unit="page">
<start>40213</start>
<end>40230</end>
</extent>
</part>
</mods>
</modsCollection>
%0 Conference Proceedings
%T SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
%A Bhattacharyya, Swapnil
%A Baranwal, Mayank
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Findings of the Association for Computational Linguistics: EMNLP 2026
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-462-0
%F bhattacharyya-baranwal-2026-sover
%X Large Language Models (LLMs) have shown remarkable promise in translating and reformulating complex mathematical optimization problems across modeling languages. However, validating such transformations through empirical solver executions alone is unreliable, as solver outcomes may be affected by local minima, structural timeouts, numerical artifacts, and subtle semantic divergence between formulations. We introduce SOVER, an LLM-assisted SMT framework that separates semantic mapping from formal certification: Z3 checks domain cross-feasibility and global objective order preservation for mixed-integer linear formulations, while dReal provides tolerance aware feasibility/range and \ensuremathǎrepsilon-argmin checks for continuous nonlinear formulations. We also introduce NLEQUIV-150, a public benchmark of 100 equivalent and 50 deliberately hard non-equivalent nonlinear reformulation pairs. With LLM-extracted mappings, SOVER classifies 149/150 pairs (99.33%) correctly, including all 50 hard negatives; the sole error is an incomplete mapping extraction.
%R 10.18653/2026.findings-emnlp.1886
%U https://aclanthology.org/2026.findings-emnlp.1886/
%U https://doi.org/10.18653/2026.findings-emnlp.1886
%P 40213-40230
Markdown (Informal)
[SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification](https://aclanthology.org/2026.findings-emnlp.1886/) (Bhattacharyya & Baranwal, Findings 2026)
ACL