Large Language Models (LLMs) have demonstrated strong ability to translate and reformulate complex mathematical optimization problems across different modeling languages. Yet, relying solely on empirical solver runs to validate such transformations is fragile, because solver outcomes can be influenced by local minima, structural timeouts, numerical artifacts, and subtle semantic drift between formulations.
We introduce SOVER, an LLM‑assisted SMT framework that cleanly separates semantic mapping from formal certification. For mixed‑integer linear formulations, Z3 checks cross‑domain feasibility and preservation of the global objective ordering. For continuous nonlinear formulations, dReal provides tolerance‑aware feasibility/range analysis and $\epsilon$‑argmin verification.
We also release the public benchmark NLEquiv-150, comprising 100 equivalent nonlinear reformulation pairs and 50 deliberately hard non‑equivalent pairs. With mappings extracted by LLMs, SOVER correctly classifies 149 out of 150 pairs (99.33% accuracy), correctly handling all 50 hard negatives; the single mistake stems from an incomplete mapping extraction.
Review: SOVER’s division of labor—semantic extraction by LLMs and rigorous checking by mature SMT solvers—yields highly reliable certification of optimization reformulations, offering a verifiable safety net for automated modeling pipelines.