跳转至

文章背景与核心概要

在将复杂的数学优化问题在不同的建模语言之间进行翻译和重构时，大语言模型（LLM）展现出了巨大的应用潜力，然而完全依赖经验性的求解器执行结果是不可靠的。求解器的运行结果容易受到局部最优、结构化超时、数值计算畸变以及不同表述之间微妙的语义差异所干扰。

为了解决这一问题，作者推出了 SOVER（一种大模型辅助的 SMT 求解器验证框架），它将语义映射与形式化认证清晰地区分开来：Z3 用于处理混合整数线性表述，通过检查域的交叉可行性与全局目标函数顺序保持性来进行验证；dReal 则用于处理连续非线性表述，通过执行容差感知的可行性/范围检查以及 \(\epsilon\)-argmin 检查来完成验证。此外，作者还推出了 NLEquiv-150 公共基准测试集，包含 100 个等价的非线性重构对以及 50 个精心设计的、具挑战性的不等价重构对。利用大模型提取出的映射关系，SOVER 成功对 149/150 对样本（99.33%）进行了正确分类，其中包括全部 50 个困难负样本（唯一的错误源于不完整的映射提取）。

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

Authors: Swapnil Bhattacharyya, Mayank Baranwal
Published: September 1, 2026 (Accepted to EMNLP 2026 Findings)
Primary Subject: Artificial Intelligence (cs.AI)
arXiv: 2609.00728 [cs.AI]
DOI: 10.48550/arXiv.2609.00728

Authors: Swapnil Bhattacharyya, Mayank Baranwal
Published: September 1, 2026 (Accepted to EMNLP 2026 Findings)
Primary Subject: Artificial Intelligence (cs.AI)
arXiv: 2609.00728 [cs.AI]
DOI: 10.48550/arXiv.2609.00728

Summary

尽管大语言模型（LLM）在跨不同建模语言翻译和重构复杂数学优化问题方面展现出巨大前景，但纯粹依赖经验性求解器执行结果是不可靠的。求解器结果可能会被局部极小值、结构化超时、数值构件以及不同表述之间微妙的语义差异所扭曲。

While Large Language Models (LLMs) show great promise in translating and reformulating complex mathematical optimization problems across different modeling languages, relying purely on empirical solver executions is unreliable. Solver outcomes can be skewed by local minima, structural timeouts, numerical artifacts, and subtle semantic divergences between formulations.

为了解决这一问题，作者推出了 SOVER，这是一个将语义映射与形式化认证清晰分离的大模型辅助 SMT（可满足性模理论）框架： * Z3 通过检查域交叉可行性和全局目标顺序保持来处理混合整数线性表述。 * dReal 通过执行容差感知的可行性/范围检查以及 \(\epsilon\)-argmin 检查来处理连续非线性表述。

To address this, the authors introduce SOVER, an LLM-assisted SMT (Satisfiability Modulo Theories) framework that cleanly separates semantic mapping from formal certification: * Z3 handles mixed-integer linear formulations by checking domain cross-feasibility and global objective-order preservation. * dReal handles continuous nonlinear formulations by performing tolerance-aware feasibility/range checks and \(\epsilon\)-argmin checks.

此外，作者还提出了 NLEquiv-150，这是一个公开基准测试集，包含 100 个等价的和 50 个刻意设计且极具挑战性的不等价非线性重构对。利用大模型提取的映射，SOVER 成功对 149 个对中的 150 个（99.33%）进行了分类，其中包括所有 50 个困难负样本（唯一的错误源于不完整的映射提取）。

Additionally, the authors present NLEquiv-150, a public benchmark comprising 100 equivalent and 50 deliberately challenging non-equivalent nonlinear reformulation pairs. Utilizing LLM-extracted mappings, SOVER successfully classifies 149 out of 150 pairs (99.33%), including all 50 hard negatives (with the single error stemming from an incomplete mapping extraction).

Access Paper & Resources

Submission History

  • [v1] Tue, 1 Sep 2026, 05:05:12 UTC (501 KB)
  • [v1] Tue, 1 Sep 2026, 05:05:12 UTC (501 KB)