SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2609.00728
curl -X POST /api/v1/records/arxiv/2609.00728/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2609.00728/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'