Large Language Models Can Plan Your Travels Rigorously with Formal Verification Tools
arxiv(2024)
摘要
The recent advancements of Large Language Models (LLMs), with their abundant
world knowledge and capabilities of tool-using and reasoning, fostered many LLM
planning algorithms. However, LLMs have not shown to be able to accurately
solve complex combinatorial optimization problems. In Xie et al. (2024), the
authors proposed TravelPlanner, a U.S. domestic travel planning benchmark, and
showed that LLMs themselves cannot make travel plans that satisfy user
requirements with a best success rate of 0.6
framework that enables LLMs to formally formulate and solve the travel planning
problem as a satisfiability modulo theory (SMT) problem and use SMT solvers
interactively and automatically solve the combinatorial search problem. The SMT
solvers guarantee the satisfiable of input constraints and the LLMs can enable
a language-based interaction with our framework. When the input constraints
cannot be satisfiable, our LLM-based framework will interactively offer
suggestions to users to modify their travel requirements via automatic
reasoning using the SMT solvers. We evaluate our framework with TravelPlanner
and achieve a success rate of 97
contain international travel benchmarks and use both dataset to evaluate the
effectiveness of our interactive planning framework when the initial user
queries cannot be satisfied. Our framework could generate valid plans with an
average success rate of 78.6
according to diverse humans preferences.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要