{"id":"arxiv/2609.00728","url":"https://arxiv.org/abs/2609.00728","tags":["cs.AI","cs.LG","math.OC"],"score":0,"title":"SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification","domain":"cs.AI","source":"arxiv","authors":["Swapnil Bhattacharyya","Mayank Baranwal"],"reviews":0,"subject":"cs.AI","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-09-01","reactions":{}}