论文
SOVER：通过大语言模型辅助的SMT验证，对优化问题重构进行形式化认证
SOVER: Formal Certification of Optimization Reformulations via LLM-Assisted SMT Verification
摘要
大语言模型 (LLM) 在跨建模语言转换和重新表述复杂的数学优化问题方面表现出了非凡的前景。然而，仅通过经验求解器执行来验证此类转换是不可靠的，因为求解器结果可能会受到局部最小值、结构超时、数值伪影和公式之间细微语义分歧的影响。我们引入了 SOVER，一个 LLM 辅助的 SMT 框架，它将语义映射与正式认证分开：Z3 检查混合整数线性公式的域交叉可行性和全局目标顺序保留，而 dReal 为连续非线性公式提供公差感知可行性/范围和 $ε$-argmin 检查。我们还引入了 NLEquiv-150，这是一个包含 100 个等效和 50 个特意硬非等效非线性重构对的公共基准。通过 LLM 提取的映射，SOVER 正确分类了 149/150 对 (99.33%)，包括所有 50 个硬负例；唯一的错误是映射提取不完整。
