TriVAL: 一个用于忠实自动优化建模的三重验证框架

# TriVAL：一种面向忠实自动优化建模的三重验证框架  
来源：https://arxiv.org/html/2605.23966  
Ziyang Fang, JinXi Wang, Jinghui Zhong, , and Yew\-Soon Ong（通讯作者：Jinghui Zhong.）  
Ziyang Fang, JinXi Wang, Jinghui Zhong 任职于华南理工大学计算机科学与工程学院，广州 510000，中国（电子邮件：[email protected], [email protected], [email protected]）。  
Yew\-Soon Ong 任职于新加坡科技研究局前沿人工智能研究中心，新加坡 138632，同时任职于南洋理工大学计算与数据科学学院，新加坡 639798（电子邮件：[email protected]）。  

###### 摘要  
优化建模是连接自然语言问题描述与优化求解器之间的关键桥梁，也是将运筹学（OR）引入实际决策的基石。近年来，大语言模型（LLMs）的进展推动了自动优化建模的重大突破。然而，现有方法在建模过程中仍缺乏明确的验证机制，导致前期引入的错误沿着流水线传播，最终降低了建模的准确性。为应对这一挑战，我们提出了 TriVAL，一个三重验证框架，在自动优化建模的三个阶段（语义规范、数学建模和代码生成）执行显式验证。在每个阶段，TriVAL 遵循“构建-验证-修订”循环：根据阶段特定的标准评估当前结果，并在必要时进行修订。这种设计有助于在错误跨阶段累积之前识别并纠正它们，从而在整个建模过程中保持忠实性。为了在更具挑战性的组合问题上评估自动优化建模，我们进一步引入了 NL4COP 基准测试，包含 50 种不同问题类型的 150 个实例，其决策逻辑更复杂、约束耦合更紧密、建模要求也高于现有基准。在 NL4COP 和既定基准上的实验表明，TriVAL 始终优于最先进的方法，在最具挑战性的问题上提升最为显著。  

## I 引言  
优化建模是将现实世界决策问题转化为正式优化模型的关键通道；然而，它长期以来一直是阻止非专业用户大规模部署运筹学（OR）的主要瓶颈。这一瓶颈在供应链规划[21 (https://arxiv.org/html/2605.23966#bib.bib2)]、生产调度[34 (https://arxiv.org/html/2605.23966#bib.bib3)]和交通运输[25 (https://arxiv.org/html/2605.23966#bib.bib4)]等领域尤为突出，因为这些领域对优化建模的需求远远超出专家建模者的供给[33 (https://arxiv.org/html/2605.23966#bib.bib8)]。在实践中，优化问题很少以完全形式化的数学规划形式呈现。它们通常用自然语言描述，往往包含复杂的决策逻辑、紧密耦合的需求以及隐含的假设。从这样的描述中构建正确的数学模型，需要的远不止直接形式化——还需要抽象、语义理解和细致的建模判断。提升这一能力对自动优化建模的研究以及将运筹学扩展到专家建模者之外的实际应用都具有重要意义[35 (https://arxiv.org/html/2605.23966#bib.bib32),29 (https://arxiv.org/html/2605.23966#bib.bib33)]。  

自动优化建模之所以困难，是因为正确性必须在相互依赖的建模阶段序列中保持：理解问题、形式化问题、生成代码[11 (https://arxiv.org/html/2605.23966#bib.bib19),2 (https://arxiv.org/html/2605.23966#bib.bib9),20 (https://arxiv.org/html/2605.23966#bib.bib13)]。每个阶段产生的结果都约束着下一个阶段；任何早期阶段的缺陷都可能向前传播；后续结果可能仍然内部一致，却与原始问题脱节。因此，自动优化建模的真正瓶颈已不再是代码生成本身，而是在相互依赖的建模阶段中稳健地遏制错误，以保持对原始问题的忠实性。  

近年来，大语言模型（LLMs）显著推进了自动优化建模[35 (https://arxiv.org/html/2605.23966#bib.bib32),29 (https://arxiv.org/html/2605.23966#bib.bib33),32 (https://arxiv.org/html/2605.23966#bib.bib30)]。随着优化建模任务变得更加复杂，现有工作越来越多地采用多步策略来提升建模能力。当前方法大致可分为两条主线：基于学习的方法和基于提示的方法。基于学习的方法通过大规模数据合成和模型训练来增强优化建模能力[9 (https://arxiv.org/html/2605.23966#bib.bib23),11 (https://arxiv.org/html/2605.23966#bib.bib19),16 (https://arxiv.org/html/2605.23966#bib.bib22),4 (https://arxiv.org/html/2605.23966#bib.bib24)]，而基于提示的方法则通过多步分解和融入建模知识来提升推理时的建模质量[30 (https://arxiv.org/html/2605.23966#bib.bib18),36 (https://arxiv.org/html/2605.23966#bib.bib10),2 (https://arxiv.org/html/2605.23966#bib.bib9),27 (https://arxiv.org/html/2605.23966#bib.bib12),40 (https://arxiv.org/html/2605.23966#bib.bib16)]。这两个方向都提高了生成模型的质量。然而，尽管这些方法增强了多步生成，它们通常将较早阶段的中间结果视为天然可靠，很少在结果用于后续阶段之前对其进行显式验证。没有显式验证，早期的幻觉、误解或错误推理很容易嵌入阶段结果中。由于后续阶段直接建立在这些输入之上，它们仅仅将已有缺陷的建模决策转化为代码。因此，最终程序可能完美执行，但解决的却是错误的问题。  

为了减轻语义漂移，自动优化建模必须显式验证关键阶段的结果，在缺陷变得难以后期纠正之前将其捕获。认识到保持忠实性需要在每个阶段捕捉缺陷，以免其变得难以后期纠正，我们提出了 TriVAL，一个专门用于自动优化建模的三重验证框架，它将建模过程组织成围绕中间建模结果的显式验证。它引入了针对建模过程三个不同阶段的三重验证：语义验证、公式验证和代码验证。对于每个目标，TriVAL 遵循“构建-验证-修订”循环：首先构建当前的建模结果，然后根据该阶段特定风险定制的标准进行验证，并在必要时进行修订，然后才继续推进。通过这种设计，TriVAL 在早期错误传播之前就将其遏制，在整个建模过程中保护从问题到解决方案的正确映射。  

在现有的 LP 和 MILP 基准测试中，错误传播的有害影响在很大程度上被掩盖了，因为这些基准的问题逻辑和公式化要求相对简单。然而，在建模难度更大的复杂组合场景中，问题理解和公式化中的错误变得更为普遍，因此显式验证变得至关重要。为了在忠实性难以保持的场景下评估优化建模，我们引入了 NL4COP，一个新的基准测试，包含 50 种不同组合问题类型的 150 个实例，其决策逻辑更复杂，建模难度也高于现有基准。在 NL4COP 和既定基准上的实验表明，TriVAL 始终优于最先进的方法，在最具挑战性的任务上提升最大。  

本文的主要贡献有三方面：  
1. 1. 我们提出了 TriVAL，一个专门用于自动优化建模的三重验证框架，它将建模过程组织成围绕三个关键建模结果（语义规范、数学公式和生成代码）的显式验证。每个结果在流程继续之前都经过评估，必要时进行修订，有助于遏制错误传播并在整个建模过程中保持忠实性。  
2. 2. 我们引入了 NL4COP，一个新的自动优化建模基准测试，针对具有挑战性的组合问题。它包含 50 种问题类型和 150 个实例，具有复杂的决策逻辑和紧密耦合的约束，比现有基准提供了更具挑战性和区分度的评估。  
3. 3. 通过在 NL4COP 和既定基准上的广泛实验，我们表明 TriVAL 始终优于最先进的优化建模方法，在最具挑战性的问题上提升最大。结果进一步凸显了 NL4COP 作为一个具有挑战性和区分度的基准测试，能够展示显式验证的优势。  

本文其余部分组织如下。第 II 节 (https://arxiv.org/html/2605.23966#S2) 回顾相关工作并阐明我们的定位。第 III 节 (https://arxiv.org/html/2605.23966#S3) 介绍提出的 TriVAL 框架。第 IV 节 (https://arxiv.org/html/2605.23966#S4) 介绍 NL4COP 基准测试并报告实验评估。最后，第 V 节 (https://arxiv.org/html/2605.23966#S5) 总结本文。  

## II 相关工作  
自动优化建模将自然语言问题描述转化为数学建模框架和求解器（如 CVXPY[6 (https://arxiv.org/html/2605.23966#bib.bib7)]、Gurobi[8 (https://arxiv.org/html/2605.23966#bib.bib5)] 和 OR-Tools[23 (https://arxiv.org/html/2605.23966#bib.bib6)]）的形式化公式和可执行代码。近期将 LLMs 应用于此任务的文献通常追求两个主要方向。第一个方向通过数据合成、监督微调或对齐训练来训练专用模型。第二个方向通过提示工程、推理框架或外部知识注入来指导通用模型。在回顾这些基础方法之后，我们将讨论与我们贡献最密切相关的文献：生成输出的评估和显式优化验证。  

### II-A 基于学习的优化建模方法  
基于学习的方法主要通过监督微调或对齐训练来推进自动优化建模，利用面向优化的数据和反馈。一条突出的工作线集中于构建结构化数据集，以教会模型生成准确的公式。例如，ORLM[9 (https://arxiv.org/html/2605.23966#bib.bib23)] 和 LLMOPT[11 (https://arxiv.org/html/2605.23966#bib.bib19)] 设计了连接自然语言描述、数学公式和代码的多元素模式，从而能够对优化建模进行指令微调。或者，ReSocratic[37 (https://arxiv.org/html/2605.23966#bib.bib20)] 和 OptMATH[16 (https://arxiv.org/html/2605.23966#bib.bib22)] 采用以公式为中心的合成方法，在数学表达式和问题描述之间双向生成数据，以可控复杂性扩展训练多样性。  

一个互补的方向将可验证的求解器信号直接纳入模型对齐和推理中。SIRL[4 (https://arxiv.org/html/2605.23966#bib.bib24)] 将优化求解器视为奖励源，使用可执行代码和形式化模型来指导基于强化学习的对齐。基于这一可验证反馈循环，OptiMind[41 (https://arxiv.org/html/2605.23966#bib.bib21)] 在测试时应用求解器信号，将基于类的错误摘要与自一致性相结合，以减少常见的建模错误。虽然这些学习驱动的方法成功生成了更高质量的公式和可执行代码，但它们本质上仍以生成为中心。它们往往将较早阶段的结果视为天然可靠，缺乏在中间建模结果用于后续阶段之前对其进行审查的显式机制。  

### II-B 基于提示的优化建模方法  
第二个主要方向通过任务分解、多智能体协作和结构化搜索来指导推理时的优化建模。鉴于单步生成往往难以应对复杂的问题结构[28 (https://arxiv.org/html/2605.23966#bib.bib34)]，一条突出的工作线将建模工作流分解为专门的职责。例如，Chain-of-Experts[36 (https://arxiv.org/html/2605.23966#bib.bib10)]、OptiMUS[1 (https://arxiv.org/html/2605.23966#bib.bib14)]、OptimAI[27 (https://arxiv.org/html/2605.23966#bib.bib12)] 和 OR-LLM-Agent[40 (https://arxiv.org/html/2605.23966#bib.bib16)] 等框架协调不同的智能体或角色，分别处理数学公式、代码生成和执行修复。通过模块化工作流，这些方法允许模型一次专注于建模任务的一个特定部分。  

一条互补的工作线通过搜索轨迹和语义基础来保证结构一致性。OptiTree[13 (https://arxiv.org/html/2605.23966#bib.bib15)] 通过分层树搜索组织生成过程，将复杂问题分解为更简单的子问题，以合成全局建模策略。与树搜索并行，通过上下文学习检索相关建模知识在约束编程中显示出前景[18 (https://arxiv.org/html/2605.23966#bib.bib27)]。为了进一步夯实生成过程，SAC-Opt[42 (https://arxiv.org/html/2605.23966#bib.bib17)] 专注于结构对齐，从生成的代码中重建语义锚点，并针对原始问题描述纠正不匹配的组件。  

虽然这些结构化方法和多智能体方法使推理更加可靠，但它们的反馈循环仍然集中在代码阶段，通常通过代码生成后的执行和调试进行。由于它们很少对早期建模结果（如初始语义提取或数学公式）施加显式验证门控，因此早期误解仍然可以自由传播到最终的代码结构中。  

### II-C 生成输出的评估与显式优化验证  
认识到纯生成的局限性，近期机器学习文献越来越多地利用 LLMs 作为评估者来批评和改进输出[17 (https://arxiv.org/html/2605.23966#bib.bib39),12 (https://arxiv.org/html/2605.23966#bib.bib40),3 (https://arxiv.org/html/2605.23966#bib.bib38),7 (https://arxiv.org/html/2605.23966#bib.bib41),31 (https://arxiv.org/html/2605.23966#bib.bib31)]。在优化建模领域，近期工作探索了验证引导的搜索和测试。例如，AutoFormulation[2 (https://arxiv.org/html/2605.23966#bib.bib9)] 引入正确性评分来探索和筛选候选公式。其他工作则侧重于生成后验证：OptiVer[14 (https://arxiv.org/html/2605.23966#bib.bib43)] 通过对结构和解的双面验证来检查最终模型，而一种基于智能体的方法使用生成的测试和突变形式化模型检查[39 (https://arxiv.org/html/2605.23966#bib.bib42)]。尽管取得了这些进展，现有的优化验证器