VeriSimpl: 使用基于简化验证的自然语言鲁棒优化建模

# VeriSimpl: 基于简化验证的自然语言鲁棒优化建模 来源：https://arxiv.org/html/2607.20474 ###### 摘要 自然语言接口能够极大提升优化建模的可访问性和易用性，而近年来大语言模型（LLM）的进展显示出将文本问题描述自动翻译为可执行求解器公式的前景。然而，现有方法的一个关键挑战是确保推导出的公式正确实现了预期任务，即便它在执行时可能不报错。我们提出了 VeriSimpl，一个用于鲁棒自然语言到优化形式化的求解器-LLM 框架。我们的方法基于*基于简化的验证*这一思想，即利用优化求解器生成关于候选公式的简化诊断查询，从而使 LLM 能够可处理地推理该公式相对于任务描述的正确性。我们提出了沿着问题约束和决策变量不同维度的此类简化策略，使 LLM 能够在固定的全局上下文下进行局部推理。在一系列优化基准上的评估表明，我们的方法在准确率上相比现有方法有一致的提升，同时提供了一种新颖的高精度自验证信号。 机器学习，ICML ## 1 引言 优化在众多行业的决策中扮演核心角色，包括制造业、物流、供应链、能源系统、医疗保健和金融等（Sadana 等人，2025）。许多这类现实决策问题自然地被形式化为数学优化模型，例如混合整数线性规划（MILP）问题，这是最广泛使用且表达能力最强的范式之一（Williams 等人，2009）。 参见图 1：一个优化建模问题示例。对于给定的自然语言问题描述，LLM 可能生成正确的求解器公式，也可能生成看似非常相似但包含难以检测的微妙语义错误的错误公式。 尽管具有实际重要性，优化建模对于非专家用户而言仍然难以掌握。形式化一个正确的优化问题通常需要深厚的运筹学专业知识，以将现实场景转化为数学约束和目标，同时还需要编程专业知识，以使用特定于求解器的 API（如 Gurobi、CPLEX 或 SCIP）实现该公式。这种双重专业知识要求为许多潜在用户（包括小型企业、规划人员和领域专家）设置了巨大障碍，这些人可能非常了解自己的运营需求，但缺乏形式化这些需求所需的技术背景。 大语言模型的最新进展为降低这一障碍提供了有希望的途径。通过从优化问题的自然语言描述生成求解器代码，基于 LLM 的接口有潜力扩大优化技术的可访问性，并提高专家用户的可用性（Liu 等人，2024）。最初的方法基于直接提示（Yang 等人，2024），而更先进的技术，如智能体系统（Ahmaditeshnizi 等人，2024；Xiao 等人，2024）和微调后的领域特定模型（Tang 等人，2024；Jiang 等人，2025），在准确性上显示出显著提升。然而，一个关键挑战依然存在：即使基于 LLM 的系统生成了可能执行无错的求解器代码，所生成的公式也可能没有正确形式化预期问题，从而在所有情况下都将验证的负担完全留给用户。优化模型尤其容易出现微妙的语义错误：约束可能略微指定错误，索引处理不当，或目标聚合不正确。例如，图 1 展示了一个优化问题示例以及两个求解器代码公式：一个正确，一个错误。尽管两个公式看起来非常相似，但错误版本在目标函数和一个约束中包含微妙的语义错误，这些错误从根本上改变了模型的意义。此类错误难以检测，并可能导致无效的优化结果。 虽然标准代码生成方法通常利用从任务规范生成的单元测试或行为测试用例，但这类方法对于优化代码公式不可行：由于正确性取决于决策变量、约束和目标之间的全局交互，在高维空间中生成满足可行性或最优性条件的可靠测试实例本身就是一个困难的优化问题。 在这项工作中，我们通过引入一个新颖的求解器-LLM 框架来解决这个挑战，用于自然语言优化建模。我们的方法不仅提高了自然语言到求解器代码翻译的准确性，还提供了一个自验证信号，指示何时对生成的公式具有高置信度。我们的方法基于一种新的范式，即*基于简化的验证*。关键思想是，我们不依赖 LLM 生成验证测试，而是利用优化求解器构建关于原始问题的简化诊断查询。这些简化查询降低了复杂性，并探测特定性质，同时保留原始公式的全局语义结构。特别地，我们沿着由约束和决策变量表示的问题不同维度降低复杂性，从而能够探测可行性和最优性性质。因此从概念上讲，我们的方法颠覆了传统的验证工作流程：不是使用 LLM 提出测试场景然后由求解器检查，而是利用求解器在高维空间中构建可行和最优解的可靠性，以获得复杂度降低的问题实例，这些实例对于 LLM 来说是易于推理的。 我们在涵盖多个优化领域的四个基准数据集上的评估显示，与现有最先进基线方法相比，端到端形式化准确性有一致的提升。此外，我们新颖的自验证机制识别出一大部分情况，其中系统可以对生成的公式发出高置信度信号，这有助于在实践中许多情况下减少人工检查的负担。 总之，我们在这项工作中做出以下关键贡献：(1) 我们引入了*基于简化的验证*，一种通过求解器引导的诊断性问题简化来验证自然语言优化模型的框架，该框架探测语义正确性。(2) 我们提出了沿问题约束和决策变量维度表示的复杂性的具体简化策略，使 LLM 能够对可行性和最优性进行可处理的推理。(3) 我们在四个优化基准上进行了广泛的经验评估，证明了与现有自然语言到求解器系统相比准确率的一致提升，以及一种新颖的高置信度自验证信号。 ## 2 基于简化的验证 参见图 2：基于简化的验证流水线：利用求解器生成的简化查询进行有效的 LLM 推理 在本节中，我们介绍基于简化的验证方法的高层概述。给定一个优化问题的自然语言描述及相关输入数据，目标是计算最优解。标准方法通常遵循一个顺序过程，其中 LLM 或基于 LLM 的智能体系统首先将问题形式化为代码，然后由优化求解器执行以计算最优解。相比之下，我们的方法以更深入的方式整合求解器和 LLM，联合使用它们进行公式验证，而不是仅仅依靠求解器执行。 概述。图 2 展示了整体流水线。我们的系统首先使用 LLM 生成多个候选求解器程序，例如图 1 中木材示例所示的正确和不正确程序。每个程序都经过一个验证过程，该过程首先使用求解器从候选程序生成一组*简化查询*，其中每个简化问题孤立出完整问题的特定方面。对于每个简化查询，求解器计算一个真实结果，而 LLM 被要求仅基于自然语言问题描述独立推理该查询及其预期结果。因此，简化查询并非标准意义上的输入-输出测试用例（指定程序的预期行为），而是通过对程序使用求解器导出的性质，以使 LLM 能够根据任务描述推理预期的问题行为。LLM 的推理结果与求解器输出之间的一致性产生一个正面的验证信号。跨多个简化查询的验证结果被聚合为每个候选程序的最终验证分数，该分数反映了程序与自然语言规范的一致性程度。选择具有最高验证分数的程序，并在输入数据上执行以返回最优解。 简化过程。我们的方法使用求解器沿两个关键问题维度生成简化问题实例：约束和决策变量。*基于约束的简化*专注于验证候选程序中的单个约束是否捕捉了自然语言描述中的语义。关键思想是每次只考虑一个约束，同时保持其他约束固定，针对不同的语义可能性（严格满足、边界或违反）对其进行变异，并使用求解器为每种可能性生成具体估值。然后将这些具体估值与问题的自然语言描述一起呈现给 LLM，并要求 LLM 推理该估值的可行性。例如，对于图 1 中错误程序的存储容量约束，该公式错误地将容量（200000）除以 10000，实际上要求库存始终小于 20（这并不符合问题描述）。求解器将根据此公式为库存生成具体估值，例如库存 19 和 20 应是可行的，但 21 应不可行。当这些具有具体库存值的简单查询被发送给 LLM 时，它能够很容易地推理出所有三个库存值在问题描述下都是可以接受的，因此不可行性查询将无法通过验证。因此，带有具体值的简单查询使得 LLM 推理能够检测到这一差异，并对错误程序进行惩罚。 虽然基于约束的验证检查可行性违反，但它不评估候选程序的最优性公式。我们通过*基于变量的简化*来解决这一验证方面。虽然完整程序有许多相互作用的决策变量必须共同优化，但基于变量简化的关键思想是通过为其中许多变量提供具体值，并仅预测剩余的变量来降低复杂性。给定一个候选程序，我们首先运行求解器以获得所有决策变量（包括目标）的最优估值。然后，我们通过提供不同变量子集的值，并仅要求 LLM 预测剩余变量来生成简化查询。例如，对于图 1 中的木材示例，目标函数必须最大化总利润，但错误程序使用一个双重 for 循环错误地公式化了目标计算，这导致对同一库存多次添加存储成本。虽然直接要求 LLM 推理完整问题和所有未知决策变量非常复杂，但当我们为除总利润之外的所有决策变量提供具体值时，这实际上将任务复杂度降低到仅关注目标计算。当 LLM 在给定其他变量（采购、销售和库存）所有值的情况下进行具体推理时，它能够正确应用每个季度的存储成本一次。这在正确程序的情况下导致推断出的总利润值相同，但在错误程序的情况下导致不同的值。这种具体数值推理与符号公式评估之间的差异构成了一个强大的错误信号。通过这种方式，基于变量遮蔽的简化显著降低了 LLM 检测此类差异的推理复杂性。 总之，基于约束和基于变量的简化提供了互补的验证信号，探测候选求解器程序的可行性和最优性方面。通过系统地简化问题，并将求解器输出与基于自然语言描述的 LLM 推理进行比较，我们的方法有效检测了标准端到端生成方法未能捕捉的微妙公式错误。 ## 3 VeriSimpl 算法 本节将 VeriSimpl 呈现为一个抽象的、与求解器和 LLM 无关的算法，该算法实现了基于简化的验证，用于鲁棒的自然语言到优化形式化。 问题设置。我们假设给定一个优化问题的自然语言规范 \(x\) 以及关联的结构化输入数据 \(d\)，这些数据可能是表格数据和参数，以结构化格式（如 JSON 或 CSV）呈现。一个候选求解器程序 \(P\)（例如使用 Gurobi/CPLEX/SCIP API）在数据 \(d\) 上执行，实例化一个优化模型 \(M(P, d) = (\mathcal{V}, \mathcal{C}, \mathcal{O})\)，其中 \(\mathcal{V}\) 是决策变量集合，\(\mathcal{C} = \{c_1, \dots, c_m\}\) 是约束集合，\(\mathcal{O}\) 是目标函数。我们假设每个索引变量元素都作为原子变量包含在集合 \(\mathcal{V}\) 中，并且该集合还包含一个特殊变量 \(\mathsf{obj}\)，表示目标值。我们定义估值 \(v\) 为从变量到值的映射：\(v: \mathcal{V} \rightarrow \mathbb{R} \cup \mathbb{Z}\)。 我们的方法利用两个黑盒组件：一个优化求解器 \(\mathcal{S}\) 和一个大语言模型 \(\mathcal{L}\)。给定模型 \(M\)，求解器接口定义为 \(\textsc{Solve}(\mathcal{S}; M) \rightarrow (\texttt{status}, v)\)，返回一个状态和一个可能的估值 \(v\)（覆盖 \(\mathcal{V}\)）。状态 \(\texttt{status} \in \{\texttt{OPT}, \texttt{FEAS}, \texttt{INFEAS}\}\)