Formalize, Don't Optimize: The Heuristic Trap in LLM-Generated Combinatorial Solvers

📄 arXiv: 2605.12421v1 📥 PDF

作者: Haoyu Wang, Yuliang Song, Tao Li, Zhiwei Deng, Yaqing Wang, Deepak Ramachandran, Eldan Cohen, Dan Roth

分类: cs.AI

发布日期: 2026-05-12

💡 一句话要点

形式化而非优化：LLM生成组合求解器中的启发式陷阱

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大型语言模型 组合优化 神经符号系统 约束求解 程序合成

📋 核心要点

  1. 现有LLM在解决复杂组合问题时，直接推理能力不足，依赖神经符号系统生成求解器。
  2. 论文提出保守设计原则，利用LLM形式化变量、约束和目标，交由验证过的求解器处理，避免过度优化。
  3. 实验表明，Python + OR-Tools正确性最高，优化提示仅带来微小加速，并可能导致正确性下降。

📝 摘要（中文）

大型语言模型(LLM)在通过直接推理解决复杂的组合问题时面临挑战。因此，最近的神经符号系统越来越多地使用LLM来合成可执行的求解器。一个核心的设计问题是LLM应该如何表示求解器，以及它是否应该尝试优化搜索。我们引入了CP-SynC-XL，这是一个包含100个组合问题（4,577个实例）的基准，并评估了三种求解器构建范式：原生算法搜索（Python）、通过Python求解器API进行约束建模（Python + OR-Tools）和声明式约束建模（MiniZinc + OR-Tools）。我们发现了一种一致的表示差异：Python + OR-Tools在LLM中获得了最高的正确性，而MiniZinc + OR-Tools尽管使用相同的OR-Tools后端，但绝对覆盖率较低。原生Python最有可能返回一个模式有效的解决方案，但验证失败，而求解器支持的路径保持更高的条件保真度。在启发式轴上，提示进行搜索优化仅产生较小的中位数加速（1.03-1.12倍），并且具有强烈的双峰效应：许多实例减慢，并且在长尾问题上正确性急剧下降。配对的代码级审计将这些回归追溯到重复出现的启发式陷阱。在以效率为导向的提示下，LLM可能会用局部近似代替完整的搜索（Python），注入未经验证的边界（Python + OR-Tools），或者添加冗余的声明式机制，从而压倒或过度约束模型（MiniZinc + OR-Tools）。这些发现支持LLM生成的组合求解器的保守设计原则：主要使用LLM来形式化变量、约束和经过验证的求解器的目标，并在使用前单独检查任何LLM编写的搜索优化。

🔬 方法详解

问题定义：论文旨在解决LLM在生成组合问题求解器时，如何有效利用LLM的能力，并避免因过度优化导致的性能下降问题。现有方法要么依赖LLM直接推理，效果不佳；要么过度优化搜索策略，反而降低求解器的正确性和效率。

核心思路：论文的核心思路是形式化优先，优化滞后。即首先利用LLM将组合问题形式化为变量、约束和目标函数，然后交给成熟的求解器（如OR-Tools）进行求解。避免LLM直接参与搜索优化，以减少引入错误启发式的风险。

技术框架：论文构建了一个名为CP-SynC-XL的基准测试集，包含100个组合问题。然后，评估了三种求解器构建范式：1) 原生Python算法搜索；2) Python + OR-Tools，利用Python API进行约束建模；3) MiniZinc + OR-Tools，采用声明式约束建模。通过对比这三种方法在不同LLM上的表现，分析LLM在求解器生成过程中的优势和不足。

关键创新：论文的关键创新在于提出了“形式化而非优化”的设计原则，强调LLM在求解器生成过程中应侧重于问题建模，而非搜索优化。这种方法能够有效利用LLM的建模能力，同时避免因引入不正确的启发式信息而导致的性能下降。

关键设计：论文的关键设计包括：1) CP-SynC-XL基准测试集，用于评估不同求解器构建范式的性能；2) 三种求解器构建范式的对比实验，分析LLM在不同范式下的表现；3) 代码级审计，用于追踪因优化提示导致的性能回归，并识别LLM引入的错误启发式。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，Python + OR-Tools方法在LLM中获得了最高的正确性。优化提示虽然能带来微小的中位数加速（1.03-1.12倍），但具有强烈的双峰效应，许多实例反而减慢，并且在长尾问题上正确性急剧下降。代码级审计发现，LLM在优化过程中容易引入错误的启发式信息，导致性能回归。

🎯 应用场景

该研究成果可应用于自动化程序生成、智能规划、运筹优化等领域。通过形式化问题描述，并结合成熟的求解器，可以更有效地利用LLM解决复杂的组合优化问题，提高问题求解的效率和可靠性。未来，该方法有望应用于工业生产调度、资源分配、路径规划等实际场景。

📄 摘要（原文）

Large Language Models (LLMs) struggle to solve complex combinatorial problems through direct reasoning, so recent neuro-symbolic systems increasingly use them to synthesize executable solvers. A central design question is how the LLM should represent the solver, and whether it should also attempt to optimize search. We introduce CP-SynC-XL, a benchmark of 100 combinatorial problems (4,577 instances), and evaluate three solver-construction paradigms: native algorithmic search (Python), constraint modeling through a Python solver API (Python + OR-Tools), and declarative constraint modeling (MiniZinc + OR-Tools). We find a consistent representational divergence: Python + OR-Tools attains the highest correctness across LLMs, while MiniZinc + OR-Tools has lower absolute coverage despite using the same OR-Tools back-end. Native Python is the most likely to return a schema-valid solution that fails verification, whereas solver-backed paths preserve higher conditional fidelity. On the heuristic axis, prompting for search optimization yields only small median speed-ups (1.03-1.12x) and a strongly bimodal effect: many instances slow down, and correctness drops sharply on a long tail of problems. A paired code-level audit traces these regressions to a recurring heuristic trap. Under an efficiency-oriented prompt, the LLM may replace complete search with local approximations (Python), inject unverified bounds (Python + OR-Tools), or add redundant declarative machinery that overwhelms or over-constrains the model (MiniZinc + OR-Tools). These findings support a conservative design principle for LLM-generated combinatorial solvers: use the LLM primarily to formalize variables, constraints, and objectives for verified solvers, and separately check any LLM-authored search optimization before use.