arXiv cs.AI· Rui Zhang, Chenyu Zhou, Jianghao Lin, Yaoxin Wu, Dongdong Ge, Wen Song·· 12 小时前AI 评分31
ORSMT：用可满足性模理论为 LLM 优化建模提供语义验证与修复
ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization
AI 导读
ORSMT 通过类型化语义接口和精确 SMT 关系查询，对 LLM 生成的优化模型、求解器代码与报告做语义比对，可证明或反驳可行域与目标关系并定位到具体行或域。
正文 · AI 翻译
摘要：大型语言模型日益自动化地从自然语言问题中构建优化建模，产出书面数学、求解器代码和返回的报告。在这些产物之间验证同一个优化问题需要语义比较：不相等的模型可能达到相同目标，等价的模型可能使用不同的辅助变量，而彼此一致的产物可能遗漏相同的源需求。ORSMT 提供类型化语义接口和精确的 SMT 关系查询。它对齐可观测决策，投影辅助变量，证明或反驳可行域与目标关系，将反驳定位到相关行或域，并在可用时链接源文本。随后它从一种产物重建另一种产物，每个被采用的候选都通过所需的关系检查。在 3,034 个问题和六种生成器规模上，ORSMT 在全部 72 个基准与生成器组合中于选择前提升了模型-代码匹配率。受保护的选择将总体匹配率从 43.2% 提升至 88.2%，将既正确又匹配的比例从 25.2% 提升至 40.2%。在 1,905 个被反驳的输出上，共享回退下的认证投票使 50.9% 的输出正确且匹配，而 ReLoop 为 44.8%，Opt-Verifier 为 49.4%。单独进行一轮源修订后再进行精确重建，可为 84.4% 的被反驳配对恢复模型-代码匹配。
| 学科： | 优化与控制（math.OC）；人工智能（cs.AI）；软件工程（cs.SE） |
| 引用为： | arXiv:2610.29145 [math.OC] |
| （或 arXiv:2610.29145v1 [math.OC] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.29145 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Rui Zhang [查看电子邮件]
[v1]
2026年10月21日星期三 03:27:02 UTC（3,062 KB）
来源：arXiv cs.AI · arxiv.org