Large Language Models Can Plan Your Travels Rigorously with Formal Verification Tools

最近大型语言模型（LLM）的进展，凭借其丰富的世界知识和工具使用和推理能力，促进了许多LLM计划算法的发展。然而，LLM还没有显示出能够准确解决复杂组合优化问题的能力。在Xie等人（2024年）的论文中，作者提出了美国国内旅行规划基准TravelPlanner，并表明LLM本身无法制定满足用户要求的旅行计划，最佳成功率仅为0.6％。在这项工作中，我们提出了一个框架，使LLM能够将旅行计划问题正式制定和解决为满足模理论（SMT）问题，并使用SMT求解器交互式地自动解决组合搜索问题。SMT求解器保证输入约束的可满足性，而LLM可以使我们的框架具有基于语言的交互。当输入约束无法满足时，我们的LLM框架将通过使用SMT求解器进行自动推理，与用户互动地提供修改旅行要求的建议。我们使用TravelPlanner评估我们的框架，并实现了97％的成功率。我们还创建了一个包含国际旅行基准的单独数据集，并使用两个数据集来评估当初始用户查询无法满足时我们的交互式规划框架的有效性。根据不同人的喜好，我们的框架可以生成有效的计划，平均成功率为我们的数据集为78.6％，TravelPlanner为85.0％。

这篇论文旨在解决LLMs在解决复杂组合优化问题时的准确性问题，提出了一个旅行规划框架，使用SMT求解器与LLMs交互式地解决旅行规划问题。

论文提出了一个框架，将旅行规划问题转化为SMT问题，并使用SMT求解器与LLMs交互式地解决问题，当输入约束不可满足时，框架会根据SMT求解器的自动推理，与用户交互地提出修改旅行需求的建议。

论文使用TravelPlanner和一个国际旅行数据集对框架进行了评估，成功率分别为97%和78.6%（国际旅行数据集），并且成功率较高（85%）地满足了各种人的偏好。该框架可以为用户提供合理的旅行规划建议，并且可以为未来的研究提供一个新的思路。

在最近的相关研究中，还有一些研究致力于将SMT求解器与其他AI技术（如深度学习）结合使用来解决组合优化问题，例如“DeepSMT”（ICML 2019）和“Neural-guided SAT solving”（ICLR 2020）等。