# SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification

arXiv: https://arxiv.org/abs/2609.00728 · HTML: https://mlsanity.com/paper/2609.00728/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 16 of its 34 references that are in the map.
- First posted on arXiv 1 Sep 2026.

## Builds on (most cited first, 16 of 16)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [Large Language Models as Optimizers](https://mlsanity.com/paper/2309.03409/) (2023)
- [A Survey of Optimization Methods from a Machine Learning Perspective](https://mlsanity.com/paper/1906.06821/) (2019)
- [Large Language Model Safety: A Holistic Survey](https://mlsanity.com/paper/2412.17686/) (2024)
- [LLMs for Mathematical Modeling: Towards Bridging the Gap between Natural and Mathematical Languages](https://mlsanity.com/paper/2405.13144/) (2024)
- [Solver-Informed RL: Grounding Large Language Models for Authentic Optimization Modeling](https://mlsanity.com/paper/2505.11792/) (2025)
- [StepORLM: A Self-Evolving Framework With Generative Process Supervision For Operations Research Language Models](https://mlsanity.com/paper/2509.22558/) (2025)
- [An overview of model uncertainty and variability in LLM-based sentiment analysis. Challenges, mitigation strategies and the role of explainability](https://mlsanity.com/paper/2504.04462/) (2025)
- [A Systematic Survey on Large Language Models for Evolutionary Optimization: From Modeling to Solving](https://mlsanity.com/paper/2509.08269/) (2025)
- [EquivaMap: Leveraging LLMs for Automatic Equivalence Checking of Optimization Formulations](https://mlsanity.com/paper/2502.14760/) (2025)
- [EvoCut: Strengthening Integer Programs via Evolution-Guided Language Models](https://mlsanity.com/paper/2508.11850/) (2025)
- [Teaching Networks to Solve Optimization Problems](https://mlsanity.com/paper/2202.04104/) (2022)
- [Large Language Models in Operations Research: Methods, Applications, and Challenges](https://mlsanity.com/paper/2509.18180/) (2025)
- [Fact-checking AI-generated news reports: Can LLMs catch their own lies?](https://mlsanity.com/paper/2503.18293/) (2025)
- [Defining Functions on Equivalence Classes](https://mlsanity.com/paper/1907.07591/) (2019)
- [FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving](https://mlsanity.com/paper/2608.25220/) (2026)

## Abstract (arXiv)

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.