大型语言模型（LLM）在将复杂的数学优化问题从一种建模语言翻译或重构为另一种语言方面表现出色。然而，仅凭求解器的实验运行来验证这些转换并不可靠，因为求解器结果可能受到局部最优、结构性超时、数值误差以及两种表述之间细微语义差异的影响。
我们提出 SOVER，这是一套基于 LLM 的 SMT（可满足性模理论）框架，明确分离语义映射与形式化认证两个环节。对混合整数线性模型，使用 Z3 检查跨域可行性以及全局目标顺序是否保持；对连续非线性模型，借助 dReal 完成容差感知的可行性/范围检查以及 $\epsilon$‑argmin 验证。
此外，我们构建了公开基准 NLEquiv-150，包含 100 对等价的非线性重构以及 50 对刻意设计的非等价难例。利用 LLM 自动抽取的映射信息，SOVER 能够在 150 对中正确分类 149 对（准确率 99.33%），其中所有 50 条硬负例均被正确识别，唯一一次错误来源于映射抽取不完整。
点评：SOVER 通过将语义抽取交给 LLM、将形式化检查交给成熟 SMT 求解器，实现了对优化重构的高可靠性认证，为自动化建模工具提供了可验证的安全保障。