Large Language Models Can Solve Real-World Planning Rigorously with Formal Verification Tools
作者: Yilun Hao, Yongchao Chen, Yang Zhang, Chuchu Fan
分类: cs.AI, cs.CL, cs.HC
发布日期: 2024-04-18 (更新: 2025-01-29)
备注: 50 pages, 6 figures, 8 tables
💡 一句话要点
提出基于LLM的规划框架以解决复杂多约束规划问题
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 大型语言模型 规划问题 约束满足 形式化验证 零-shot 泛化 智能决策 旅行规划
📋 核心要点
- 现有的LLM在处理复杂多约束规划问题时成功率低，难以生成正确的计划。
- 本文提出的框架将复杂规划问题形式化为约束满足问题，利用满足性求解器进行求解。
- 实验结果显示，框架在TravelPlanner上成功率达到93.9%，并能有效处理未见约束和不满足的查询。
📝 摘要（中文）
大型语言模型（LLMs）在直接生成复杂多约束规划问题的正确计划时面临挑战，即使使用自我验证和自我批评。例如，在Xie等人（2024）提出的美国国内旅行规划基准TravelPlanner中，最佳LLM OpenAI o1-preview仅能以10%的成功率找到可行的旅行计划。本文提出了一种基于LLM的规划框架，将复杂的多约束规划问题形式化为约束满足问题，并由健全且完整的满足性求解器进行求解。以TravelPlanner为主要用例，我们的框架成功率达到93.9%，并在多样化的改写提示下表现良好。此外，我们的框架具有强大的零-shot 泛化能力，能够处理新创建的国际旅行数据集中未见的约束，并在新的根本不同领域中良好泛化。
🔬 方法详解
问题定义：本文旨在解决大型语言模型在复杂多约束规划问题中生成正确计划的困难。现有方法在处理此类问题时，成功率普遍较低，且难以适应多样化的用户输入。
核心思路：论文提出了一种新的LLM规划框架，通过将复杂的多约束规划问题形式化为约束满足问题，从而利用成熟的满足性求解器进行求解。这种方法能够有效提高成功率，并增强模型的泛化能力。
技术框架：该框架主要包括三个模块：首先是输入处理模块，将用户查询转化为约束满足问题；其次是求解模块，使用满足性求解器进行问题求解；最后是反馈模块，识别不满足的查询并提供修改建议。
关键创新：框架的核心创新在于将LLM与形式化验证工具结合，形成了一种新的求解思路。这一方法与传统的基于规则或启发式的方法本质上不同，能够更系统地处理复杂约束。
关键设计：在设计中，框架采用了高效的约束表示方式，并通过多样化的提示进行训练，以增强模型的适应性。同时，针对不满足的查询，框架能够识别出不满足核心，并提供个性化的修改建议。
🖼️ 关键图片
📊 实验亮点
实验结果表明，提出的框架在TravelPlanner基准上成功率达到93.9%，显著高于现有最佳LLM的10%。此外，框架能够有效处理未见约束，成功修改和解决81.6%和91.7%的不满足查询，展示了其强大的实用性和泛化能力。
🎯 应用场景
该研究的潜在应用领域包括旅行规划、项目管理和资源分配等复杂决策场景。通过提高规划的准确性和效率，能够为用户提供更优质的服务，未来可能在智能助手和自动化决策系统中发挥重要作用。
📄 摘要（原文）
Large Language Models (LLMs) struggle to directly generate correct plans for complex multi-constraint planning problems, even with self-verification and self-critique. For example, a U.S. domestic travel planning benchmark TravelPlanner was proposed in Xie et al. (2024), where the best LLM OpenAI o1-preview can only find viable travel plans with a 10% success rate given all needed information. In this work, we tackle this by proposing an LLM-based planning framework that formalizes and solves complex multi-constraint planning problems as constrained satisfiability problems, which are further consumed by sound and complete satisfiability solvers. We start with TravelPlanner as the primary use case and show that our framework achieves a success rate of 93.9% and is effective with diverse paraphrased prompts. More importantly, our framework has strong zero-shot generalizability, successfully handling unseen constraints in our newly created unseen international travel dataset and generalizing well to new fundamentally different domains. Moreover, when user input queries are infeasible, our framework can identify the unsatisfiable core, provide failure reasons, and offers personalized modification suggestions. We show that our framework can modify and solve for an average of 81.6% and 91.7% unsatisfiable queries from two datasets and prove with ablations that all key components of our framework are effective and necessary. Project page: https://sites.google.com/view/llm-rwplanning.