SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
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 ε-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.
Related
- Aligning Information Theory and Formal Verification: A Lean Formalization of Rate-Distortion Theory
- Exact certification for conic optimization over quadratic modules: partitions of unity and recession directions
- Exact Risk-Complexity Laws for Projective Boundaries in Scenario Optimization and Distribution-Free Certification
- Agent4FreeFem: A Verification-Guided Framework for Autonomous Topology Optimization
- ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization
BibTeX
@misc{bhattacharyya2026sover,
title = {{SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification}},
author = {Swapnil Bhattacharyya and Mayank Baranwal},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.00728},
eprint = {2609.00728},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.00728},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
AU - Swapnil Bhattacharyya
AU - Mayank Baranwal
PY - 2026
DA - 2026/09/01
PB - arXiv
DO - 10.48550/arxiv.2609.00728
UR - https://arxiv.org/abs/2609.00728
AB - 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 ε-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.
ER -