SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification

📄 arXiv: 2609.00728v1 📥 PDF

作者: Swapnil Bhattacharyya, Mayank Baranwal

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

发布日期: 2026-09-01

备注: Accepted to EMNLP 2026 Findings

💡 一句话要点

提出SOVER框架以实现优化重构的形式验证

🎯 匹配领域: 支柱三：空间感知与语义 (Perception & Semantics) 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 优化重构 形式验证 大型语言模型 SMT求解器 非线性优化 可行性检查 语义映射 机器学习

📋 核心要点

  1. 现有方法在验证优化问题的重构时，依赖经验求解器执行，容易受到多种因素的影响，导致结果不可靠。
  2. SOVER框架通过将语义映射与形式认证分离，利用Z3和dReal进行不同类型公式的可行性和目标顺序检查。
  3. 实验结果显示，SOVER在149/150对重构对中正确分类，准确率达到99.33%，有效提升了验证的可靠性。

📝 摘要（中文）

大型语言模型（LLMs）在复杂数学优化问题的翻译和重构方面展现出显著潜力。然而，仅依靠经验求解器执行来验证这些变换是不可靠的，因为求解器的结果可能受到局部最小值、结构超时、数值伪影和细微语义差异的影响。我们提出了SOVER，一个LLM辅助的SMT框架，旨在将语义映射与形式认证分离：Z3检查混合整数线性公式的领域交叉可行性和全局目标顺序保持，而dReal则提供容忍度感知的可行性/范围和ε-argmin检查。我们还引入了NLEquiv-150，这是一个包含100对等效和50对故意难度较大的非等效非线性重构对的公共基准。通过LLM提取的映射，SOVER正确分类了149/150对（99.33%），包括所有50个难负样本，唯一的错误是映射提取不完整。

🔬 方法详解

问题定义：本论文旨在解决优化问题重构的形式验证问题，现有方法依赖求解器执行，易受局部最小值和语义差异影响，导致验证不可靠。

核心思路：SOVER框架的核心思想是将语义映射与形式认证分离，通过LLM提取映射，并利用SMT求解器进行形式验证，以提高验证的准确性和可靠性。

技术框架：SOVER的整体架构包括两个主要模块：首先，使用LLM提取优化问题的语义映射；其次，利用Z3和dReal进行形式认证，分别处理混合整数线性和连续非线性公式。

关键创新：SOVER的最大创新在于将语义映射与形式认证分离，采用不同的求解器针对不同类型的优化问题进行验证，这一方法与传统的依赖单一求解器的方式本质上不同。

关键设计：在设计中，SOVER使用了LLM提取的映射进行分类，并通过Z3和dReal进行可行性和目标顺序检查，确保了对复杂优化问题的高效处理。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

在实验中，SOVER成功地将149对重构对中的99.33%正确分类，包括所有50个难负样本，显示出其在优化重构验证中的高效性和准确性。唯一的错误源于映射提取的不完整性，表明该方法在实际应用中仍有进一步优化的空间。

🎯 应用场景

SOVER框架具有广泛的应用潜力，尤其在工业优化、资源调度和金融建模等领域。通过提供可靠的优化重构验证工具，SOVER可以帮助研究人员和工程师更有效地解决复杂的优化问题，提升决策的准确性和效率。

📄 摘要（原文）

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 mixed-integer linear formulations, while dReal provides tolerance-aware feasibility/range and $ε$-argmin checks for continuous nonlinear formulations. We also introduce NLEquiv-150, a public benchmark of 100 equivalent and 50 deliberately hard non-equivalent nonlinear reformulation pairs. With LLM-extracted mappings, SOVER classifies 149/150 pairs (99.33%) correctly, including all 50 hard negatives; the sole error is an incomplete mapping extraction.