{"id":"arxiv/2610.29145","url":"https://arxiv.org/abs/2610.29145","tags":["math.OC","cs.AI","cs.SE"],"score":0,"title":"ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization","domain":"math.OC","source":"arxiv","authors":["Rui Zhang","Chenyu Zhou","Jianghao Lin","Yaoxin Wu","Dongdong Ge","Wen Song"],"reviews":0,"subject":"math.OC","summary":"Large language models increasingly automate optimization modeling from natural language problems, producing written mathematics, solver code and a returned report. Verifying one optimization problem across these artifacts requires semantic comparison: unequal models can attain the same objective, equivalent models can use different auxiliary variables, and mutually consistent artifacts can omit the same source requirement. ORSMT provides a typed semantic interface and exact SMT relation queries. It aligns observable decisions, projects auxiliary variables, proves or refutes feasible region…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-10-21","reactions":{}}