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

Researchers introduced SOVER, an LLM-assisted SMT framework that formally certifies optimization reformulations using Z3 and dReal, achieving 99.33% accuracy (149/150) on the new NLEquiv-150 benchmark, which includes 100 equivalent and 50 hard non-equivalent nonlinear reformulation pairs. The framework separates semantic mapping from formal certification, addressing unreliability in empirical solver validation.

arXiv:2609.00728v1 Announce Type: new 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 $\epsilon$-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.