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

• LLMs achieve only 10.0% on TravelPlanner with pre-collected information, while GPT-4 and LLM-Modulo reach 0.6% and 20% respectively.These results motivate external formal solving for multi-constraint planning.Source: §1 · p. 1
• The framework combines LLM natural-language processing with SMT-based formalization and solving, guaranteeing a plan when the encoded constraints are satisfiable.The LLM generates instruction steps and solver code, while the SMT solver handles the full constraint set.Source: §1 · p. 2
• 93.9% final pass rate on TravelPlanner test queries, substantially exceeding LLM-Modulo’s 65% with o1-preview.The framework also reaches 93.3% on validation queries.Source: §1 · p. 2
• 81.6% and 91.7% of unsatisfiable queries from two datasets become solvable through solver feedback and modification suggestions.The framework supports autonomous suggestions and interactive incorporation of user preferences.Source: §1 · p. 2
• Zero-shot evaluations show 89.0% average optimal rates across four new combinatorial planning domains, alongside robustness to paraphrased prompts.The framework also generalizes to unseen constraint types beyond the travel-planning examples.Source: §1 · p. 2

• Existing LLM planning methods commonly decompose tasks, generate alternatives, refine plans, or use external planners, but evaluations largely target simpler constraint settings.TravelPlanner exposed the difficulty of realistic multi-constraint planning.Source: §2 · p. 2
• Algorithmic planning methods provide structured search or constraint solving but do not generalize well to diverse natural-language inputs.The proposed framework uses LLMs to formalize such inputs for sound and complete SMT solvers.Source: §2 · p. 3
• The framework extends LLM tool use by generating code that encodes all constraints and invokes an SMT solver, addressing LLM omissions during direct generation.This differs from tools used only to retrieve information or provide generic feedback.Source: §2 · p. 3
• Prompt design uses offline in-context examples, while experiments report robustness to wording changes and generalization beyond task-specific prompt designs.The authors frame this as reducing dependence on exact prompt formulations for end users.Source: §2 · p. 3

3.1 Problem Formulation

• The travel-planning formulation requires a multi-day itinerary satisfying user constraints over cities, transportation, attractions, restaurants, and accommodations.Users can add requirements such as the number of attractions visited per day.Source: §3.1 · pp. 3–4

3.2 Framework Overview

• For satisfiable queries, the framework parses the request into formalization steps, converts those steps into code, calls the SMT solver, and renders the solver output in natural language.This pipeline combines LLM processing with external formal verification.Source: §3.2 · p. 4

3.4 Interactive Plan Repair

• For unsatisfiable queries, the LLM analyzes solver reasons, gathers information, proposes constraint changes, and iterates with user feedback until a satisfiable plan is found or the process times out.Users can accept, reject, or customize suggestions, enabling personalized plan repair.Source: §3.2 · p. 4, §3.4 · p. 5

3.3.1 Query-Step Generation

• Query-Step Generation converts natural-language constraints into executable procedural instructions, learned from three human-crafted examples and generalized to unseen constraints.Examples are organized by constraint subjects, while optional JSON preprocessing is excluded from the main comparison.Source: §3.3.1 · p. 4

3.3.2 Step-Code Generation

• Step-Code Generation maps generated instructions to Python calls for information APIs and the SMT solver using demonstrations covering the relevant operations.The examples enable code generation for new instruction steps without separate API documentation.Source: §3.3.2 · pp. 4–5

3.3.3 SMT Solver

• The sound and complete SMT solver returns a formally verified plan for satisfiable constraints or unsatisfiable reasons extracted with get_unsat_core.These solver outputs determine whether the framework proceeds to plan generation or repair.Source: §3.3.3 · p. 5

• UnsatChristmas introduces international Christmas-week travel queries with constraints not included in TravelPlanner, especially flight and attraction preferences.The dataset uses ten worldwide cities and flight data collected for December 24–30, 2023.Source: §4 · p. 5
• The dataset contains 39 unsatisfiable queries caused by unmet nonstop-flight, airline, attraction-category, or budget requirements.Queries contain between one and four simultaneous failure reasons.Source: §4 · p. 5
• The unsatisfiable queries are balanced across one, two, and three destination cities, with 13 queries in each group.The construction also includes 12 modified TravelPlanner training queries for interactive-repair evaluation.Source: §4 · p. 5

5.1 Satisfiable Plan Solving Evaluation

• 93.3% and 93.9% final pass rates on TravelPlanner validation and test sets show strong satisfiable-plan performance, while comparable results hold across LLMs.The validation set contains 180 queries and the test set 1000 queries; Mistral-Large remains effective despite lower pass rates than Claude-3.Source: Figure 3 · p. 6, §5.1 · p. 6, Table 1 · p. 7
• 97.0% test-set pass rate is achieved after optionally converting natural-language queries into JSON descriptions, with an average 9.4% validation improvement across three LLMs.The corresponding validation pass rates are 98.9%, 98.3%, and 84.4%.Source: §5.1 · p. 6

5.2.1 New Prompts

• 86.7% final pass rate under GPT-4-paraphrased Query-Step and Step-Code prompts indicates robustness to substantial prompt rewording.The paraphrasing covers the full prompts, including their examples, across all 180 validation queries.Source: §5.2.1 · pp. 6–7

5.2.2 New Travel Plan Constraints

• Adding concise descriptions of unseen constraint types enables zero-shot generation of encoding steps for UnsatChristmas without adding new prompt examples.Figure 3 illustrates how unseen constraints are encoded through generated steps.Source: Figure 3 · p. 6, §5.2.2 · p. 7

5.2.3 New Multi-Constraint Planning Tasks

• 92%, 92%, 100%, and 72% optimal rates across Block Picking, Task Allocation, TSP, and Warehouse demonstrate zero-shot transfer to four new combinatorial tasks.Each task includes 25 scenarios, and the evaluation also measures delivery rate.Source: Table 2 · p. 7, §5.2.3 · p. 8

5.3 Interactive Plan Repair Evaluation

• 81.6% and 91.7% success rates with 20 iterations show that iterative feedback and solver verification improve repair of unsatisfiable queries across two datasets.The standard approach reaches 78.6% and 85.0%; removing the solver lowers performance by averages of 53.4% and 60.0%.Source: Table 3 · p. 7, Table 4 · p. 7, §5.3 · p. 8

• The framework uses LLMs with SMT solvers to formalize and solve complex realistic planning problems as constrained satisfiability problems.Source: §6 · p. 8

7 Limitation

• Careful instruction-step and code design is required to encode each planning problem from scratch.The authors note that task-specific formulation is time-consuming, although zero-shot generalization may reduce future effort.Source: §7 · p. 9
• SMT runtime can increase with problem complexity, especially for large databases, many constraint types, or queries with few feasible plans.The authors suggest heuristics or alternative solvers such as MILP for some problem classes.Source: §7 · p. 9
• The framework may generate risky plans because it cannot distinguish unsafe or incorrect information in its databases.Source: §7 · p. 9

A Description of constraints

• Table 5 distinguishes constraints unique to TravelPlanner, constraints unique to the authors’ dataset, and constraints common to both.Source: Table 5 · p. 15

• The TravelPlanner database creates an extremely large combinatorial solution space, and some queries have few feasible plans.The SMT solver is capped at 30 minutes per query.Source: B Runtime and cost analysis · p. 16
• Runtime and cost analysis covers satisfiable plan solving and interactive plan repair within the framework.Source: B Runtime and cost analysis · p. 16

B.1 Satisfiable Plan Solving

• 245.66 seconds per query is the average total runtime across 179 delivered plans in the validation set.The average GPT-4 cost across 180 queries is $0.74 per query.Source: §B.1 · p. 16
• Step-Code generation takes most of the runtime because it uses multiple LLM calls for different constraint types.Source: §B.1 · p. 16
• Table 6 reports runtime in seconds for each stage of satisfiable plan solving.Source: Table 6 · p. 16
• One of 180 validation queries produces no plan because its runtime exceeds the 30-minute limit.The authors use heuristics that prioritize cities with available transportation to reduce SMT overhead in some multi-city queries.Source: §B.1 · p. 16

B.2 Interactive Plan Repair

• $0.65 per iteration and 33.68 seconds per iteration are the reported average cost and total runtime for successful UnsatChristmas repairs.Among 39 queries, 23 succeeded, with an average of 2.22 successful modification iterations per query.Source: §B.2 · p. 16, Table 7 · p. 16

C Example input queries and output plans

• A five-day Atlanta-to-Minnesota query specifies group size, destinations, dates, budget, accommodation rules, and preferences as planning constraints.The example requests travel from Atlanta to two Minnesota cities for three people from March 3rd to March 7th, 2022, with a $7,900 budget.Source: C Example input queries and output plans · p. 17
• The generated itinerary represents each day with travel, meals, attractions, and accommodation, including movement between Minneapolis and St. Cloud before returning to Atlanta.The example output spans five daily records and includes transportation, restaurants, attractions, and lodging entries.Source: C Example input queries and output plans · pp. 17–18

D.1 Result of Ours+JSON on TravelPlanner

• 98.9%, 98.3%, and 84.4% validation final pass rates are achieved by GPT-4, Claude-3-Opus, and Mistral-Large, while GPT-4 reaches 97.0% on test.Relative to Ours, validation performance improves by 5.6%, 5.0%, and 17.7%, and test performance improves by 6.8%.Source: §D.1 · p. 19, Table 8 · p. 19
• JSON translation helps LLMs extract and summarize key query information into a fixed-format representation, improving problem understanding and representation.The result comparison attributes the performance improvement to clearer structured input before planning.Source: §D.1 · p. 19, Figure 4 · p. 19

D.2 Description of other evaluation metrics

• Delivery Rate measures timely plan generation, while micro and macro commonsense or hard-constraint pass rates measure individual-constraint and whole-plan compliance.Hard constraints include budget, room rules and types, cuisine requirements, and transportation requirements.Source: §D.2 · p. 19

E Interactive Plan Repair: Iteration versus Performance

• 81.6% of 39 UnsatChristmas queries and 91.7% of 12 modified TravelPlanner queries become satisfiable within 20 iterations.The corresponding three-iteration success rates are 63.7% and 65.0%, respectively.Source: E Interactive Plan Repair: Iteration… · p. 20, Figure 5 · p. 20
• Performance rises quickly during the first five iterations, while later iterations solve a limited number of more difficult queries.For UnsatChristmas, success reaches 74.8% within five iterations; for TravelPlanner, it reaches 73.3%.Source: E Interactive Plan Repair: Iteration… · p. 20

F.1 Task Setup

• The four new domains are Block Picking, Task Allocation, Travelling Salesman Problem, and Warehouse routing.Figure 6 identifies the four new multi-constraint tasks used in the setup.Source: Figure 6 · p. 21

F.1.1 Block Picking

• Block Picking selects ten unique blocks of required colors while maximizing score across randomized scenes of 50–200 blocks.Each block has a random score from 1 to 20, and queries specify one to three required colors.Source: §F.1.1 · p. 21

F.1.2 Task Allocation

• Task Allocation assigns tasks among three heterogeneous robots working in parallel while minimizing the time until the last robot finishes.The setup randomizes task counts and robot-task completion times between 10 and 100.Source: §F.1.2 · p. 21

F.1.3 TSP

• The TSP task visits ten cities exactly once while minimizing travel distance, using randomly generated coordinates.The setup evaluates 25 scenarios and does not count the return distance to the first city.Source: §F.1.3 · p. 21, §F.2 · p. 22

F.1.4 Warehouse

• Warehouse routing completes a sequential task list by selecting stations and minimizing travel from origin through the stations and back to origin.The task uses 50 stations and requires accounting for the initial, intermediate, and return distances.Source: §F.1.4 · p. 21, Warehouse · p. 22

F.2 Added task description in prompt

• The added task prompts expose APIs for searching feasible objects, retrieving scores or distances, and enforcing index, allocation, or station-selection constraints.Task-specific descriptions define BlockSearch, TimeSearch, DistanceSearch, and StationSearch interfaces.Source: §F.2 · pp. 21–22, Warehouse · p. 22

Block Picking

• 2 of 25 Block Picking plans were non-optimal because the generated code repeatedly selected the same high-scoring blocks despite requiring distinct blocks.The error was failure to explicitly enforce distinctness among selected block indices.Source: §F.3 · pp. 22–23

Cross-task findings

• The failures show that generated plans can remain incorrect when code omits task-specific constraints or misrepresents solver inputs.Observed errors included missing uniqueness checks, invalid function arguments, contradictory variable assertions, and incorrect identifier mapping.Source: §F.3 · p. 23

Task Allocation

• 2 of 25 Task Allocation scenarios failed because the generated code passed individual variables to Max(variable_list) instead of supplying a list.This misuse caused runtime errors and prevented plan delivery.Source: §F.3 · p. 23

Warehouse

• 4 of 25 Warehouse scenarios failed to deliver plans, while 3 of 21 delivered plans were non-optimal because the generated code mishandled station variables and station IDs.The failures involved conflicting origin variables and distance calculations based on station-list indices rather than station IDs.Source: §F.3 · p. 23

G.1.1 Query-Step prompt

• The Query-Step prompt directs the model to decompose travel requests into step-by-step encodings of destinations, dates, transportation, flights, driving, restaurants, attractions, accommodations, and budget constraints.The examples instantiate these structures for 3-, 5-, and 7-day trips with varying cities, travelers, cuisines, accommodation rules, transport preferences, and budgets.Source: §G.1.1 · pp. 24–25
• The prompts connect search outputs to itinerary variables by retrieving flight, driving, restaurant, attraction, and accommodation data and constraining indices, timing, prices, availability, and repetition.Restaurant and attraction choices are tied to the current or next city based on arrival times, while accommodation constraints include room type, minimum nights, parties, pets, and children.Source: §G.1.1 · pp. 24, 25, 27
• The examples encode accommodation constraints, including entire homes or apartments with no parties and private rooms, while adding transportation, restaurant, and accommodation costs and asserting spending stays within budgets of $7,900, $15,100, and $1,100.Source: §G.1.1 · pp. 25, 29
• The example travel plans enforce destination selection, ordered transportation dates, and consistent transportation-mode constraints across all itinerary legs.They require distinct destination indices, fix the first and last transport dates to the trip boundaries, constrain intermediate dates, and prevent incompatible combinations such as mixing self-driving with flight or taxi.Source: §G.1.1 · pp. 26, 28

G.1.2 Step-Code prompt

• The Step-Code prompt asks the model to translate each instruction block into Python code for testing constraint satisfiability, using a prescribed instruction-and-code format.The destination example calls CitySearch, iterates over candidate cities, initializes a Z3 Optimize solver, creates integer variables, and tracks assertions linking variables to selected cities.Source: §G.1.2 · pp. 29–30
• The generated code represents departure-date constraints with integer variables and tracked assertions that place transportation at trip boundaries and order intermediate departures.The illustrated constraints include day 0 and day 6 boundaries for a longer trip and day 0 and day 2 boundaries for a shorter trip.Source: §G.1.2 · p. 30
• The transportation-code example uses Boolean flight, self-driving, and taxi variables, asserts an available mode for each leg, prevents simultaneous modes, and forbids self-driving when any leg uses flight.The constraints are tracked separately for the first, second, and third transportation legs and include a global implication disallowing self-driving after flight selection.Source: §G.1.2 · p. 30
• The Step-Code prompt translates travel-planning instructions into satisfiability-testing code with explicit response delimiters and constraint-specific scripts.Separate prompts cover transportation, flights, driving, restaurants, attractions, accommodation, and budget constraints.Source: §G.1.2 · pp. 31–33
• Transportation and flight code retrieves route data, constrains transportation choices and flight indices, and computes prices and arrival times for three legs.Non-flight choices receive index -1, while flight indices must be valid when flights are selected.Source: §G.1.2 · p. 31
• Driving code retrieves distances and durations, requires feasible routes for driving choices, and computes self-driving and taxi costs for three travelers.The cost formulas use distance and vehicle-capacity adjustments.Source: §G.1.2 · p. 31
• Restaurant constraints assign 15 meals to permissible cities based on arrival times, prevent repeated restaurants, calculate prices, and require each requested cuisine type.Breakfast, lunch, and dinner use different arrival-time thresholds for selecting the dining city.Source: §G.1.2 · p. 32
• Attraction constraints assign one attraction per day according to arrival times, validate attraction indices, and prevent repeated attractions in the same city.An attraction is assigned to the current or next city depending on whether arrival occurs after 18:00.Source: §G.1.2 · p. 33
• Accommodation and budget code validates lodging indices, room counts, prices, minimum-night requirements, house rules, and total spending against a 7900 budget limit.The budget aggregates transportation, restaurant, and accommodation costs.Source: §G.1.2 · p. 33

G.1.3 Prompt difference of GPT-4, Claude 3, and Mistral-Large

• Mistral-Large requires more prompt adjustments because it produces more code-generation errors than GPT-4 and Claude-3.Its revisions add explanations and examples beyond the starting GPT-4 prompt.Source: §G.1.3 · p. 34
• Prompt revisions are tailored by model: Claude-3 receives clarification for interpreting house rules, while Mistral-Large receives stricter JSON completeness instructions and additional examples and anti-loop guidance.The added examples cover city loops, travel-date assertions, and transportation-method assertions; variable names using i and for-loops are explicitly discouraged.Source: §G.1.3 · p. 34

G.1.4 Failure cases of Mistral-Large

• Mistral-Large’s major failure is an unseen “no shared room” type, which causes an incorrect instruction and accounts for 7.8% of failed delivered plans, within a 15.0% total failure rate.The remaining failures result from runtime issues or occasional code-generation errors.Source: §G.1.4 · p. 34

G.2.1 Suggestion prompt

• The Suggestion prompt guides the LLM to collect information, analyze unsatisfiable constraints, and propose one minimal, high-confidence modification within 15 iterations.It supports flight, airline, attraction, and category searches for one travel setting, and driving, flight, accommodation, and type tools for another.Source: §G.2.1 · pp. 35–36
• For accommodation-oriented queries, the Suggestion prompt permits removing house-type or transportation constraints, changing destinations, or raising the budget while preserving other fields.Suggestions are made only after sufficient information is collected and should maintain the original constraints with minimal necessary changes.Source: §G.2.1 · pp. 37–38

G.2.2 Suggestion-No Reason prompt

• The Suggestion-No Reason prompt removes descriptions of unsatisfiability reasons from the original Suggestion prompt.Its modification is described as removing all reason-related descriptions rather than changing the broader prompt structure.Source: §G.2.2 · p. 38

G.2.3 Suggestion-No Sovler prompt

• The Suggestion-No Sovler prompt removes iterative solver calling and directly guides the LLM to generate one or more information-grounded suggestions.It retains tool-assisted analysis, restricts allowable constraint changes, requests minimal modifications, and separates multiple suggestions with semicolons.Source: §G.2.3 · pp. 38–39

G.2.4 Code modify prompt

• The Code modify prompt asks the LLM to update only code portions required by changed constraints and return the complete modified code in a prescribed wrapper.The response must contain code only, beginning with "########## response ##########" and ending with "########## response ends ##########."Source: §G.2.4 · p. 41

G.3 Prompts for Generalization Evaluation

• The generalization prompt appends a task for producing steps from JSON constraints with varied fields, while fixing restaurant and accommodation prices and excluding their information.It specifies flight-only transportation, flight and airline constraints, attraction categories, and conditional date semantics for five- or seven-day trips.Source: §G.3 · pp. 41–42

G.4 Paraphrased Prompt Examples

• The paraphrased-prompt examples provide an alternative natural-language formulation of a travel-itinerary query for evaluating prompt robustness.The example is specifically introduced as a paraphrased prompt for Query-Step.Source: §G.4 · p. 42
• Paraphrased prompts translate travel requirements such as cities, dates, group size, budget, accommodations, dining, transportation, and activities into step-by-step code instructions.The examples span trips with different durations, party sizes, destinations, budgets, cuisines, accommodation rules, and transportation preferences.Source: §G.4 · pp. 42, 44, 46
• Destination constraints use CitySearch, exclude the departure city, iterate over candidate cities, and constrain distinct destination variables through a Z3 solver.The examples instantiate this pattern for selecting two, three, or one destination cities.Source: §G.4 · pp. 42, 44, 46, 48
• Travel schedules constrain transportation dates to trip boundaries, enforce intermediate-day placement and distinctness, and restrict transportation modes such as excluding flights or self-driving.Transportation variables encode flights, self-driving, and taxis while linking valid modes to corresponding search and cost calculations.Source: §G.4 · pp. 42, 44, 46
• Flight and driving instructions call external searches, bind route and date variables to prices and arrival times, and calculate transportation costs for the traveling group.Driving constraints additionally require nonempty distance data, while flight indexes use a sentinel value when flights are not selected.Source: §G.4 · pp. 43–46
• Restaurant and attraction constraints assign activities to feasible cities based on arrival times, prevent repeated selections, and enforce required cuisines where specified.The examples model 3 meals per day and 1 attraction per day, with cuisine variables checked against restaurant options.Source: §G.4 · pp. 43, 45, 47
• Accommodation constraints select one lodging per destination, check minimum stays and room types, and enforce rules such as entire homes, party allowances, pet access, and child access.The examples also calculate required rooms and accommodation prices for each group and city.Source: §G.4 · pp. 43–47
• Budget instructions aggregate transportation, restaurant, and accommodation costs and assert that total spending remains within the requested budget.The examples use budget limits of $7,900, $15,100, and $1,100 for different itineraries.Source: §G.4 · pp. 44, 46, 47, 48
• The final paraphrased-prompt instructions require preserving the original step structure, using the examples’ code structure and variable names, and returning only delimited code.Lines beginning with '#' mark instructions, while following lines contain the corresponding code until the next instruction marker.Source: §G.4 · p. 48

H Example input query and output step for generalization evaluation

• The input specifies Hong Kong, New York City, Bangkok, five days, three travelers, flight travel, nonstop flights, United or Emirates, and attraction categories.Source: H Example input query and output step… · p. 49
• The generated plan decomposes the query into solver steps for destinations, departure dates, transportation methods, flights, attractions, restaurants, accommodation, and budget.The example organizes constraints by subject and represents each subject with corresponding variables, searches, calculations, or assertions.Source: H Example input query and output step… · pp. 49–50
• Flight steps search available connections, constrain flight indices and rules, and calculate prices and arrival times for three travelers across three transports.Source: H Example input query and output step… · p. 49
• Attraction steps assign five daily attractions to cities based on arrival times, prevent repeated attractions within a city, and check required categories.Source: H Example input query and output step… · p. 50
• Restaurant and accommodation steps calculate costs using fixed per-person rates, while the budget step aggregates transportation, restaurant, and accommodation spending under a 5000 limit.Source: H Example input query and output step… · p. 50