ORSMT: Unleashing the Potential of Satisfiability Modulo Theories for Semantic Verification and Repair in LLM-Based Optimization

📄 arXiv: 2610.29145v1 📥 PDF

作者: Rui Zhang, Chenyu Zhou, Jianghao Lin, Yaoxin Wu, Dongdong Ge, Wen Song

分类: math.OC, cs.AI, cs.SE

发布日期: 2026-10-21

💡 一句话要点

提出ORSMT以解决大语言模型优化中的语义验证与修复问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大语言模型 优化建模 语义验证 SMT查询 模型修复 自动化决策 智能合约

📋 核心要点

  1. 现有方法在验证大语言模型生成的优化问题时，面临语义不一致和模型间关系复杂的问题。
  2. ORSMT通过提供类型化的语义接口和精确的SMT查询，解决了模型与代码之间的语义验证与修复问题。
  3. 在实验中，ORSMT在所有72个基准和生成器组合中提升了模型与代码的匹配率，保护性选择显著提高了整体正确率。

📝 摘要（中文）

随着大语言模型在自然语言问题优化建模中的应用日益广泛，如何验证这些模型生成的数学表达、求解代码和报告之间的语义一致性成为一个重要挑战。ORSMT提供了一种类型化的语义接口和精确的SMT关系查询，能够对可观察的决策进行对齐，投影辅助变量，证明或反驳可行区域和目标关系，并在可能的情况下链接源文本。通过在3034个问题和六种生成器规模上的实验，ORSMT显著提高了模型与代码的匹配率，保护性选择将整体匹配率从43.2%提升至88.2%。

🔬 方法详解

问题定义：论文要解决的问题是如何在大语言模型生成的优化问题中验证不同文档之间的语义一致性。现有方法在处理模型与代码之间的关系时，常常无法有效识别和修复语义不一致的问题。

核心思路：ORSMT的核心思路是通过类型化的语义接口和精确的SMT关系查询，来对不同文档进行语义比较和验证。这种设计使得能够对模型生成的不同输出进行有效的对齐和修复。

技术框架：ORSMT的整体架构包括几个主要模块：首先是类型化语义接口，其次是SMT关系查询模块，接着是决策对齐和辅助变量投影模块，最后是输出重构模块。整个流程通过这些模块的协同工作，实现了对模型与代码的语义验证与修复。

关键创新：ORSMT的关键创新在于其类型化的语义接口和精确的SMT查询能力，这与现有方法的主要区别在于能够更深入地分析和验证模型生成的不同输出之间的关系。

关键设计：在技术细节上，ORSMT采用了特定的参数设置和损失函数，以确保在语义验证过程中能够准确地识别和修复不一致的部分。

📊 实验亮点

实验结果显示，ORSMT在3034个问题和72个基准组合中均提升了模型与代码的匹配率，保护性选择将整体匹配率从43.2%提升至88.2%。在1905个被反驳的输出中，经过共享回退的认证投票使得50.9%的输出正确且匹配，相较于其他方法有显著提升。

🎯 应用场景

该研究的潜在应用领域包括自动化优化建模、智能合约验证和复杂系统的语义分析等。通过提高模型生成内容的语义一致性，ORSMT能够在实际应用中提升决策支持系统的可靠性和准确性，具有重要的实际价值和未来影响。

📄 摘要（原文）

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 and objective relations, localizes refutations to implicated rows or domains and links source texts when available. It then reconstructs one artifact from another, and each adopted candidate passes the required relation checks. Across 3,034 problems and six generator sizes, ORSMT improves the model-code match rate in all 72 benchmark and generator combinations before selection. Protected selection raises the aggregate rate from 43.2% to 88.2% and the share that are both correct and matched from 25.2% to 40.2%. On the 1,905 refuted outputs, certified voting under the shared fallback makes 50.9% of outputs correct and matched, compared with 44.8% for ReLoop and 49.4% for Opt-Verifier. A separate one-round source revision followed by exact reconstruction restores a model-code match for 84.4% of the refuted pairs.