我们在做旅行规划时面对众多的目的地选择、复杂的交通连接、预算限制以及个人偏好等多重因素，即使是最有经验的旅行者也可能会陷入选择困境。传统的旅行规划方法往往依赖于人工操作，这不仅耗时耗力，而且难以保证计划的最优性和可执行性。

本文将探讨一个革命性的解决方案——将大型语言模型（LLMs）与形式化验证工具相结合，以解决传统旅行规划中存在的问题。这种方法不仅能够处理复杂的约束条件，还能够提供经过严格验证的旅行计划，确保每一项旅行安排都符合用户的具体要求。通过这一创新框架，我们能够实现更高效、更准确、更个性化的旅行规划，让每个人都能享受到定制化的旅行体验。

方法

究者们提出了一个框架，该框架利用LLMs来形式化地表述和解决旅行规划问题，将其视为一个可满足性模理论（SMT）问题。这一方法的核心在于，通过多次调用LLMs，完成从自然语言查询到JSON格式描述的转换、问题的公式化步骤生成，以及基于步骤的代码生成。当输入的查询不可满足时，LLMs还能够基于当前情况提出建议，并根据建议修改现有代码。

Figure 1框架是一个协作系统，涉及人类用户、大型语言模型（LLM）、SMT求解器以及生成的旅行计划。工作流程如下：

1. 人类用户提出查询：以自然语言的形式，用户提出他们的旅行计划需求。

2. LLM翻译：LLM将用户的自然语言查询转换为JSON格式，这是一种结构化的数据处理格式，便于计算机解析和处理。

3. 生成SMT问题步骤：LLM根据JSON格式的描述，生成解决问题所需的步骤，这些步骤将指导如何将旅行计划问题表述为一个SMT问题。

4. 代码生成：LLM根据生成的步骤，创建相应的代码。这些代码将作为SMT求解器的输入，用于编码问题。

5. SMT求解器调用：执行LLM生成的代码，以调用SMT求解器。SMT求解器是一个能够处理复杂逻辑和数学问题的算法工具，它尝试找到满足所有约束条件的解决方案。

6. 交互式查询修改：如果SMT求解器无法找到解决方案，表明当前的查询不可满足。此时，LLM将收集信息，分析当前情况，并与用户进行交互，提出修改查询的建议。

7. 代码更新与重新求解：根据用户的反馈和建议，LLM更新代码，并再次调用SMT求解器，以寻找可行的旅行计划。

8. 生成旅行计划：一旦找到满足所有约束条件的解决方案，SMT求解器将生成一个经过形式化验证的旅行计划，该计划以绿色区域表示。

研究者们定义了旅行规划问题：给定人类旅行计划的个人约束C的自然语言描述，系统应输出满足C的计划。这涉及到从起始城市出发，访问k个目的地城市，跨越n天的旅行，并采用k+1种交通方式。输出的计划应明确指定每天要访问的城市、交通方式、景点、餐厅和住宿。

然后研究者们对旅行规划问题进行了明确的定义。他们指出系统的目标是：基于用户提供的自然语言描述的个人约束C，生成一个满足这些约束条件的旅行计划。这包括从起始城市出发，访问若干目的地城市，整个旅程持续一定的天数，并涉及多种交通方式。

接下来LLMs的任务是将用户的自然语言输入转换成结构化的JSON格式。这一步是整个框架的基础，它确保了后续步骤能够准确理解用户的需求。

代码生成阶段是框架的关键部分，LLMs根据转换后的JSON描述和预先提供的示例，生成解决问题所需的具体步骤。这些步骤将指导如何将问题分解并逐步解决。LLMs进一步将这些步骤转化为可执行的代码。这些代码将被用来调用SMT求解器，是连接问题描述和求解器的桥梁。

最后框架执行生成的代码，将旅行规划问题编码为SMT问题，并提交给SMT求解器。求解器将尝试找到满足所有约束条件的解决方案。如果存在可行的计划，求解器将提供一个经过形式化验证的旅行计划。

当提出的查询不可满足时，LLMs利用其推理能力和常识知识来分析当前情况，并提出修改建议。这允许与人类用户进行交互式设置，用户可以同意、反对或对LLMs提出的建议提供反馈。LLMs然后根据不同的人类偏好输出个性化计划。

通过这种方法，研究者们展示了他们的框架如何有效地处理多样化的人类输入，提供经过形式化验证的计划，并在输入查询不可满足时与人类交互式地修改查询。

实验

为了测试框架的泛化能力和处理不可满足查询的交互式计划修复能力，研究者们提出了一个名为UnsatChristmas的数据集。这是专门为了评估他们提出的框架而设计的。该数据集包含39个在2023年圣诞节周制定的国际旅行计划的不可满足查询，覆盖了全球十大城市目的地，并从Metabase获取了景点信息，以及使用Google Flights收集了相关航班信息。UnsatChristmas数据集的独特之处在于它引入了与TravelPlanner不同的新约束，例如直飞规则、航空公司偏好和景点类别要求。这个数据集旨在测试框架对于未见过的约束类型是否具有良好的泛化能力，并通过交互式计划修复来适应用户的不同偏好。

研究者们在TravelPlanner和UnsatChristmas数据集上测试了他们的框架。他们使用GPT-4作为默认的LLM，并将其性能与其他两种LLM模型Claude 3 Opus和Mixtral-Large进行了比较。所有实验都使用了Z3求解器作为SMT求解器。

研究者们使用TravelPlanner数据集中的训练集来设计示例指令步骤和相应的代码，并使用这些训练查询来调整提示。然后在验证集（180个可满足的查询）和测试集（1000个可满足的查询）上评估了他们的方法。

评估指标：包括交付率（是否在限定时间内生成最终计划）、常识约束通过率、硬约束通过率和最终通过率。

基线比较：与研究者们（2024年）评估的传统基于规则的策略和各种LLM规划方法进行了比较。

结果分析：

• GPT-4的交付率在验证集上为99.4%，在测试集上为97.2%。
• 在最终通过率方面，GPT-4在验证集上达到了98.9%，在测试集上达到了97.0%，显示出框架在解决旅行规划问题上的强大能力。

研究者们还评估了框架在交互式计划修复方面的能力。他们修改了TravelPlanner的查询，使其不可满足，并使用UnsatChristmas数据集来测试框架的交互式计划修复性能。

评估指标：基于LLM最终是否能够修改约束条件以成功交付可行计划的成功率。

实现细节：定义了四种不可满足模式，并使用了模拟用户来测试框架。

结果分析：

• 框架在处理不同类型模拟用户时，平均成功率为78.6%至85.0%。
• 通过增加迭代次数，成功率可以进一步提高。

在框架对未见过的约束类型的泛化能力测试中。研究者们展示了通过在JSON-Step Generation提示中添加几行任务描述，LLM能够为UnsatChristmas中的新查询生成指令步骤，而无需添加新示例。

结论：

• 实验结果表明，提出的框架能够可靠地处理多样化的人类输入，提供经过形式化验证的计划，并能够根据不同的人类偏好交互式地修改不可满足的查询。

实验证明框架不仅在理论上是可行的，而且在实际应用中也是有效的。这些实验结果为LLMs在旅行规划领域的应用提供了有力的证据。然而，这项工作也存在一些局限性：框架的有效性依赖于精心设计的指令步骤和相应的代码，这可能需要大量的时间和专业知识来从零开始制定问题；对于包含大量目的地城市选择、多样化约束类型和只有少数可行计划的查询，求解器的运行时间可能会很长；框架目前还不能区分来自数据库的不安全或不正确信息，这可能带来基于不准确数据生成风险计划的潜在风险。

尽管存在这些挑战，研究者们的工作无疑为LLMs在旅行规划领域的应用开辟了新的道路。未来的工作可能会集中在简化问题制定过程、提高求解器效率以及增强对不安全信息的识别能力上。

论文链接：https://arxiv.org/abs/2404.11891