Large Language Models Can Solve Real-World Planning Rigorously with Formal Verification Tools

TL;DR

This paper introduces a formal verification-based framework that enables large language models to solve complex multi-constraint planning problems with high success rates and strong generalizability, surpassing previous limitations.

Contribution

The authors propose a novel LLM-based planning framework that formalizes planning as satisfiability problems and integrates sound solvers, achieving significant improvements in success rate and generalization.

Findings

Achieves 93.9% success rate on TravelPlanner benchmark

Successfully generalizes to unseen constraints and domains

Effectively identifies unsatisfiable queries and suggests modifications

Abstract

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.