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

arXiv: https://arxiv.org/abs/2404.11891 · HTML: https://mlsanity.com/paper/2404.11891/

## Key facts

- Cited by 47 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 67 references that are in the map.
- First posted on arXiv 18 Apr 2024.

## Builds on (most cited first, 26 of 26)

- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Training language models to follow instructions with human feedback](https://mlsanity.com/paper/2203.02155/) (2022)
- [ReAct: Synergizing Reasoning and Acting in Language Models](https://mlsanity.com/paper/2210.03629/) (2022)
- [Self-Consistency Improves Chain of Thought Reasoning in Language Models](https://mlsanity.com/paper/2203.11171/) (2022)
- [Large Language Models are Zero-Shot Reasoners](https://mlsanity.com/paper/2205.11916/) (2022)
- [Toolformer: Language Models Can Teach Themselves to Use Tools](https://mlsanity.com/paper/2302.04761/) (2023)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [ToolLLM: Facilitating Large Language Models to Master 16000+ Real-world APIs](https://mlsanity.com/paper/2307.16789/) (2023)
- [Code as Policies: Language Model Programs for Embodied Control](https://mlsanity.com/paper/2209.07753/) (2022)
- [Inner Monologue: Embodied Reasoning through Planning with Language Models](https://mlsanity.com/paper/2207.05608/) (2022)
- [Measuring and Narrowing the Compositionality Gap in Language Models](https://mlsanity.com/paper/2210.03350/) (2022)
- [Language Models as Zero-Shot Planners: Extracting Actionable Knowledge for Embodied Agents](https://mlsanity.com/paper/2201.07207/) (2022)
- [Graph of Thoughts: Solving Elaborate Problems with Large Language Models](https://mlsanity.com/paper/2308.09687/) (2023)
- [Reasoning with Language Model is Planning with World Model](https://mlsanity.com/paper/2305.14992/) (2023)
- [Promptbreeder: Self-Referential Self-Improvement Via Prompt Evolution](https://mlsanity.com/paper/2309.16797/) (2023)
- [LLM+P: Empowering Large Language Models with Optimal Planning Proficiency](https://mlsanity.com/paper/2304.11477/) (2023)
- [Understanding the planning of LLM agents: A survey](https://mlsanity.com/paper/2402.02716/) (2024)
- [TravelPlanner: A Benchmark for Real-World Planning with Language Agents](https://mlsanity.com/paper/2402.01622/) (2024)
- [Check Your Facts and Try Again: Improving Large Language Models with External Knowledge and Automated Feedback](https://mlsanity.com/paper/2302.12813/) (2023)
- [PromptAgent: Strategic Planning with Language Models Enables Expert-level Prompt Optimization](https://mlsanity.com/paper/2310.16427/) (2023)
- [Large Language Models as Commonsense Knowledge for Large-Scale Task Planning](https://mlsanity.com/paper/2305.14078/) (2023)
- [Leveraging Pre-trained Large Language Models to Construct and Utilize World Models for Model-based Task Planning](https://mlsanity.com/paper/2305.14909/) (2023)
- [LLMs Can't Plan, But Can Help Planning in LLM-Modulo Frameworks](https://mlsanity.com/paper/2402.01817/) (2024)
- [EASYTOOL: Enhancing LLM-based Agents with Concise Tool Instruction](https://mlsanity.com/paper/2401.06201/) (2024)
- [AutoTAMP: Autoregressive Task and Motion Planning with LLMs as Translators and Checkers](https://mlsanity.com/paper/2306.06531/) (2023)

## Built on by (most cited first, 30 of 47)

- [ToolACE: Winning the Points of LLM Function Calling](https://mlsanity.com/paper/2409.00920/) (2024)
- [Evolving Deeper LLM Thinking](https://mlsanity.com/paper/2501.09891/) (2025)
- [Steering Large Language Models between Code Execution and Textual Reasoning](https://mlsanity.com/paper/2410.03524/) (2024)
- [TripCraft: A Benchmark for Spatio-Temporally Fine Grained Travel Planning](https://mlsanity.com/paper/2502.20508/) (2025)
- [Trust the PRoC3S: Solving Long-Horizon Robotics Problems with LLMs and Constraint Satisfaction](https://mlsanity.com/paper/2406.05572/) (2024)
- [TRIP-PAL: Travel Planning with Guarantees by Combining Large Language Models and Automated Planners](https://mlsanity.com/paper/2406.10196/) (2024)
- [Is Your LLM-Based Multi-Agent a Reliable Real-World Planner? Exploring Fraud Detection in Travel Planning](https://mlsanity.com/paper/2505.16557/) (2025)
- [R1-Code-Interpreter: LLMs Reason with Code via Supervised and Multi-stage Reinforcement Learning](https://mlsanity.com/paper/2505.21668/) (2025)
- [Teaching LLMs to Plan: Logical Chain-of-Thought Instruction Tuning for Symbolic Planning](https://mlsanity.com/paper/2509.13351/) (2025)
- [ConstraintLLM: A Neuro-Symbolic Framework for Industrial-Level Constraint Programming](https://mlsanity.com/paper/2510.05774/) (2025)
- [Verification-Aware Planning for Multi-Agent Systems](https://mlsanity.com/paper/2510.17109/) (2025)
- [ToolForge: A Data Synthesis Pipeline for Multi-Hop Search without Real-World APIs](https://mlsanity.com/paper/2512.16149/) (2025)
- [TripTide: A Benchmark for Adaptive Travel Planning under Disruptions](https://mlsanity.com/paper/2510.21329/) (2025)
- [Self-Guided Function Calling in Large Language Models via Stepwise Experience Recall](https://mlsanity.com/paper/2508.15214/) (2025)
- [Planner-R1: Reward Shaping Enables Efficient Agentic RL with Smaller LLMs](https://mlsanity.com/paper/2509.25779/) (2025)
- [Wide-Horizon Thinking and Simulation-Based Evaluation for Real-World LLM Planning with Multifaceted Constraints](https://mlsanity.com/paper/2506.12421/) (2025)
- [GroupTravelBench: Benchmarking LLM Agents on Multi-Person Travel Planning](https://mlsanity.com/paper/2605.25200/) (2026)
- [TAPE: Tool-Guided Adaptive Planning and Constrained Execution in Language Model Agents](https://mlsanity.com/paper/2602.19633/) (2026)
- [TourPlanner: A Competitive Consensus Framework with Constraint-Gated Reinforcement Learning for Travel Planning](https://mlsanity.com/paper/2601.04698/) (2026)
- [WorldTravel: A Realistic Multimodal Travel-Planning Benchmark with Tightly Coupled Constraints](https://mlsanity.com/paper/2602.08367/) (2026)
- [VASO: Formally Verifiable Self-Evolving Skills for Physical AI Agents](https://mlsanity.com/paper/2606.05395/) (2026)
- [Beyond the Leaderboard: A Synthesis of Tool-Use, Planning, and Reasoning Failures in Large Language Model Agents](https://mlsanity.com/paper/2607.05775/) (2026)
- [Urban Computing in the Era of Large Language Models](https://mlsanity.com/paper/2504.02009/) (2025)
- [Rethinking the Unsolvable: When In-Context Search Meets Test-Time Scaling](https://mlsanity.com/paper/2505.22290/) (2025)
- [Agent-Testing Agent: A Meta-Agent for Automated Testing and Evaluation of Conversational AI Agents](https://mlsanity.com/paper/2508.17393/) (2025)
- [ATA: A Neuro-Symbolic Approach to Implement Autonomous and Trustworthy Agents](https://mlsanity.com/paper/2510.16381/) (2025)
- [VeriTrans: Fine-Tuned LLM-Assisted NL-to-PL Translation via a Deterministic Neuro-Symbolic Pipeline](https://mlsanity.com/paper/2604.10341/) (2026)
- [TREK: A Travel Reasoning and Evaluation Kit for LLM Agents in Complex Trip Planning](https://mlsanity.com/paper/2607.26977/) (2026)
- [TripScore: Aligning LLMs for Real-World Travel Planning via Expert-Calibrated Reward](https://mlsanity.com/paper/2510.09011/) (2025)
- [TriFlow: A Progressive Multi-Agent Framework for Intelligent Trip Planning](https://mlsanity.com/paper/2512.11271/) (2025)

## Abstract (arXiv)

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.