Are LLMs Better Formalizers than Solvers on Complex Problems?
作者: Rikhil Amonkar, May Lai, Ronan Le Bras, Li Zhang
分类: cs.CL
发布日期: 2025-05-19 (更新: 2025-09-19)
💡 一句话要点
针对复杂约束满足问题，LLM作为形式化器性能不如直接求解器
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大型语言模型 形式化器 约束满足问题 逻辑推理 少样本学习
📋 核心要点
- 现有研究表明LLM作为形式化器在逻辑推理问题上优于直接求解器，但该结论在实际约束满足问题中是否成立仍需验证。
- 该论文系统评估了不同规模的LLM在四个约束满足问题领域中，作为形式化器和直接求解器的性能差异。
- 实验结果表明，在少样本设置下，LLM作为形式化器的性能低于直接求解器，并且存在扩展性差、易硬编码等问题。
📝 摘要（中文）
最近的研究趋势提倡使用大型语言模型（LLM）作为形式化器，而不是作为逻辑推理问题的端到端求解器。形式化器不直接生成解决方案，而是生成一个形式化程序，通过外部求解器推导出解决方案。尽管LLM作为形式化器相对于LLM作为求解器在性能上的提升已被广泛报道，但我们表明，这种优越性在实际的约束满足问题中并不成立。在四个领域中，我们系统地评估了六个LLM，包括四个具有推理时扩展的大型推理模型，并结合了五个pipeline，包括两种类型的形式化方法。结果表明，在少样本设置下，LLM作为形式化器的性能不如LLM作为求解器。虽然LLM作为形式化器有望提高准确性、鲁棒性、忠实性和效率，但我们观察到，目前的LLM尚未实现这些目标，因为它们生成形式化程序的能力有限，导致无法随复杂性扩展、硬编码解决方案以及过多的推理token。我们提出了详细的分析和可行的补救措施，以推动未来改进LLM作为形式化器的研究。
🔬 方法详解
问题定义：论文旨在研究在解决复杂约束满足问题时，使用大型语言模型（LLM）作为形式化器（生成形式化程序，再由外部求解器求解）是否优于直接使用LLM作为求解器。现有方法的痛点在于，虽然有研究表明LLM作为形式化器在某些逻辑推理任务上表现更好，但在实际约束满足问题上的效果尚不明确，且可能存在扩展性、鲁棒性等问题。
核心思路：论文的核心思路是通过在多个实际约束满足问题领域中，系统地比较LLM作为形式化器和直接求解器的性能，来验证LLM作为形式化器的有效性。通过控制实验变量（如LLM模型、形式化方法、少样本示例等），分析两种方法的优缺点，并找出影响LLM作为形式化器性能的关键因素。
技术框架：整体框架包括以下几个主要步骤：1）选择四个具有代表性的约束满足问题领域；2）选择多个不同规模的LLM模型，包括具有推理时扩展能力的模型；3）设计不同的形式化pipeline，包括不同的形式化语言和外部求解器；4）在少样本设置下，使用不同的LLM模型和pipeline，分别作为形式化器和直接求解器，解决约束满足问题；5）评估两种方法的性能指标，如准确率、鲁棒性、推理token数量等；6）分析实验结果，找出LLM作为形式化器的优势和不足。
关键创新：论文的关键创新在于对LLM作为形式化器在实际约束满足问题上的有效性进行了系统性的评估和分析。之前的研究主要集中在逻辑推理任务上，而该论文将研究范围扩展到更具实际意义的约束满足问题，并发现了LLM作为形式化器在这些问题上的局限性。此外，论文还提出了改进LLM作为形式化器的可行性建议。
关键设计：论文的关键设计包括：1）选择具有代表性的约束满足问题领域，以保证实验结果的泛化性；2）选择不同规模的LLM模型，以研究模型规模对性能的影响；3）设计不同的形式化pipeline，以研究形式化方法对性能的影响；4）使用少样本设置，以模拟实际应用场景；5）采用多种性能指标，以全面评估两种方法的优缺点。
🖼️ 关键图片
📊 实验亮点
实验结果表明，在少样本设置下，LLM作为形式化器在四个约束满足问题领域中的性能均不如LLM作为直接求解器。研究发现，LLM作为形式化器存在扩展性差、易硬编码解决方案、推理token数量过多等问题。例如，在某些领域，LLM倾向于生成针对特定输入的硬编码程序，而不是通用的形式化程序，导致泛化能力较差。
🎯 应用场景
该研究成果可应用于优化AI在约束满足问题中的应用，例如资源调度、任务分配、产品配置等。通过深入理解LLM作为形式化器和直接求解器的优劣势，可以指导开发者选择更合适的解决方案，并针对性地改进LLM在形式化方面的能力，提升问题求解效率和准确性。未来的研究可以探索更有效的形式化方法和更强大的LLM模型，以实现更智能、更高效的约束满足问题求解。
📄 摘要（原文）
A trending line of recent work advocates for using large language models (LLMs) as formalizers instead of as end-to-end solvers for logical reasoning problems. Instead of generating the solution, the LLM generates a formal program that derives a solution via an external solver. While performance gain of the seemingly scalable LLM-as-formalizer over the seemingly unscalable LLM-as-solver has been widely reported, we show that this superiority does not hold on real-life constraint satisfaction problems. On 4 domains, we systematically evaluate 6 LLMs including 4 large reasoning models with inference-time scaling, paired with 5 pipelines including 2 types of formalism. We show that in few-shot settings, LLM-as-formalizer underperforms LLM-as-solver. While LLM-as-formalizer promises accuracy, robustness, faithfulness, and efficiency, we observe that the present LLMs do not yet deliver any of those, as their limited ability to generate formal programs leads to failure to scale with complexity, hard-coded solutions, and excessive reasoning tokens. We present our detailed analysis and actionable remedies to drive future research that improves LLM-as-formalizer.