Robust Asynchronous Planning via Auto-Formalization

arXiv:2606.00981 · cs.CL · Submitted 2026-05-31 · Read on arXiv

Listen

Transcript

Introduction to the show: ident: AI Radio. Generated commentary on the latest Artificial Intelligence papers.

Tom: I'm Tom.

Jane: And I'm Jane, here with Lu, Meng and our in-house large language model, Lalam.

Tom: Today's paper: "Robust Asynchronous Planning via Auto-Formalization".

Jane: The gist The choice of formal representation primarily determines whether planning scales: as dependency graphs grow from 5 to 100 actions,

Tom: First, who's behind it and why it matters.

Title and authors: Tom: We've established that there are three main ways to handle these planning problems, and this paper focuses on comparing the direct planning method against two different ways of translating tasks into a solver: using a direct Planner and using a Formalizer.

Jane: And what this paper does is look at how crucial that choice of formal representation is for scaling up those systems. It’s not just about getting one way to work, it’s about understanding which way actually works when the problem gets complicated.

Lu: They set up three specific benchmarks to test different types of challenges: action-constrained problems with non-uniform durations and precedence, state-constrained problems involving grounded states and resources, and online planning where the task changes while you're executing it.

Meng: I’m interested in the online planning part because that’s where most real systems break when things change during execution. How does this paper handle that dynamic stuff?

Lalam: The results show they test all three settings at scale, and they introduce one specific dataset for each one, like AsyncPlan-XXL, which scales AsyncHow style duration and precedence tasks to graphs with up to one hundred actions <ref:2606.00981#pg1>.

The paper's summary: Tom: So what’s the core finding here? It seems the paper unifies these different asynchronous planning challenges under one formulation, which is a key step because it lets them compare things fairly across those three distinct settings.

Jane: That unification allows them to see how different formal representations perform differently when facing action constraints, state constraints, or online planning scenarios. They’re showing that the choice of formal representation primarily determines whether planning actually scales.

Lu: They highlight a major difference in faithfulness diagnostics between PDDL2 point 1 and general constraint satisfaction programs when you have an AI model keeping track of predicates, effects, and goals consistently <ref:2606.00981#pg1,general constraint satisfaction programs when>. PDDL2 point 1 becomes really brittle there compared to the more general constraint satisfaction approach they are using for comparison <ref:2606.00981#pg1>.

Meng: So if I’m building a system that needs to handle lots of complex constraints, this suggests I should probably be looking at something more robust than just sticking to PDDL2 point 1 syntax when using an LLM as the translator <ref:2606.00981#pg1>.

Lalam: And the CP-SAT Formalizer is substantially more robust than the direct Planner when the formal representation matches what’s in the task structure, which they found was a key factor in their success.

The paper's improvements: Tom: The paper suggests that by using a formalizer approach, you can combine the LLM’s language understanding with the solver’s correctness guarantees, which is a pretty powerful combination for building reliable planning systems.

Jane: It seems like the improvement isn't just about getting a slightly better plan; it’s about achieving much higher faithfulness when translating natural language into something the computer can actually solve correctly.

Lu: They also show that they study multiple formal languages instead of assuming one representation is enough, which means they are testing different ways to translate those natural-language tasks into formal ones.

Meng: If you’re deploying this, the idea that CP-SAT Formalizer can maintain eighty-three percent accuracy even at step one hundred is a tangible number we can use to judge if it’s worth the engineering lift of using a formalizer instead of just trying to generate sequences directly <ref:2606.00981#pg1>.

Lalam: And they introduced a state-aware repair strategy specifically for online planning, which helps recover accuracy from forty-six point one percent up to eighty-four point five percent when tasks change during execution.

Conclusion: Tom: So, to wrap things up on Robust Asynchronous Planning via Auto-Formalization, the main implication is that matching the formal representation to the task structure is what lets these planning systems scale effectively when complexity grows.

Jane: It means we can stop relying solely on one method and start choosing a translation path based on whether we need high accuracy under extreme scaling or if we are dealing with dynamic execution events.

Lu: The work points toward a foundation where you use LLMs as formalizers to get the language understanding plus the solver’s guarantee, but you have to be careful because richer formalisms can introduce syntactic and semantic errors.

Meng: From a deployment standpoint, it suggests that for safety-critical domains, we need more than just makespan accuracy; we need verification of those fidelity diagnostics they found.

Lalam: And they confirmed that the unified formulation and representation alignment principle provide a solid foundation for asynchronous planning systems that scale where direct generation simply doesn't work anymore.

Jiayi Zhang, Jianing Yin, Ben Zhou Li Zhang

Drexel University · Arizona State University

cs.CL

Submitted: 2026-05-31

Updated: 2026-10-14

Comments: 31 pages, 20 figures, 15 tables

Code: https://github.com/jiayizx/async_planning

License: http://creativecommons.org/licenses/by-nc-nd/4.0/

Importance score: 88/100

The gist: The gist The choice of formal representation primarily determines whether planning scales: as dependency graphs grow from 5 to 100 actions, Planner collapses from 96% to 5% plan accuracy and PDDL2.1

Key concepts

Planner: This approach has the LLM directly generate a complete action schedule or sequence of steps based on the task description. It is fast but struggles significantly with complex, long-running tasks because it lacks a formal structure to ensure correctness and consistency.
Formalizer: This method translates the natural language task into a formal mathematical specification that an external solver (like CP-SAT) can understand. This approach is more robust for complex problems because the external solver handles the intricate logic, leading to much higher accuracy at scale.
Asynchronous Planning: This involves planning tasks where actions have unpredictable durations and execution happens over time, often involving concurrency. The paper tests how well different planning methods handle these real-world complexities, including changes during execution.
Faithfulness Diagnostics: These are checks used to see how accurately the formal representation (the translation from language to code) reflects the original task. Poor faithfulness causes errors like missing dependencies or incorrect action effects, which lead to failed plans.

Terminology

Benchmark — 2× in this paper · explained in 2 episodes
Accuracy — 1× in this paper · explained in 1 episode

Summary

The gist The choice of formal representation primarily determines whether planning scales: as dependency graphs grow from 5 to 100 actions, Planner collapses from 96% to 5% plan accuracy and PDDL2.1 Formalizer from 13% to 0%, while CP-SAT Formalizer averages 94% and still achieves 83% at 100 actions

How it works

The paper unifies asynchronous planning challenges under a single formulation and introduces three benchmarks that address action-constrained, state-constrained, and online settings at scale. The core comparison involves two approaches: an end-to-end Planner that generates action sequences directly from natural language, and a Formalizer that translates the task into a formal representation for an external solver.

The three problem categories tested are:

Action-Constrained (PA): where actions have non-uniform, non-zero durations and precedence constraints. This is tested by AsyncHow and AsyncPlan-XXL.
State-Constrained (PS): which involves grounded states, resources, and agents. This is tested by Robo Challenge.
Online Planning (PO): which includes execution-time events that revise the task specification during planning. This is tested by Online Robo Challenge.

Formal Representation and Scalability

The choice of formal representation is highlighted as the dominant factor in determining scalability. Specifically, when dependency graphs grow from 5 to 100 actions, Planner collapses from 96% to 5% plan accuracy and PDDL2.1 Formalizer from 13% to 0%, while CP-SAT Formalizer averages 94% and still achieves 83% at step S100.

Faithfulness diagnostics reveal critical differences between formalisms. PDDL2.1’s predicate-based planning representation becomes brittle compared to general constraint satisfaction programs when LLMs must keep predicates, effects, and goals consistent. CP-SAT Formalizer is substantially more robust than Planner when the formal representation matches the task structure.

Performance Across Settings

The performance of the methods varies significantly across settings and problem scales.

** Action-Constrained:**

Planner achieves above 94% on AsyncHow and above 97.5% on AsyncPlan-XXL N=5, but drops sharply as graph size grows. CP-SAT Formalizer maintains an average of 94% across all graph sizes and reaches 83% at S100.

** State-Constrained:**

All three methods score near zero on Robotouille, but Robo Challenge shows that CP-SAT Formalizer reaches 98.8% average plan accuracy and 94.2% on AsyncPlan-XXL.

** Online Planning:**

Online planning exposes the limits of oneshot formalization, as CP-SAT Formalizer drops to 46.1% when tasks change during execution, but a state-aware repair strategy that updates only event-induced constraints recovers accuracy to 84.5%.

Error Analysis and Robustness

Error analysis shows that PDDL2.1 Formalizer failures are dominated by structural and symbolic consistency errors, including missing dependencies, incomplete goals, and action-effect mismatches. CP-SAT Formalizer has fewer than 6% residual errors across all settings.

Specific failure modes include:

** Action-effect mismatch:**

PDDL2.1 Formalizer frequently produces specifications with missing dependencies (94.08%), incomplete goals (99.50%), or action effect mismatches that may lead to the solver returning plans with the correct makespan but an invalid execution structure.

** Dependency recall:**

Dependency recall differs by 88.81 points between PDDL2.1 and CP-SAT Formalizer (10.35% vs. 99.16%) on AsyncPlan-XXL.

** Online replanning:**

In the Online Robo Challenge, the state-aware repair variant recovers accuracy from 46.1% to 84.5%, identifying execution-state preservation as the binding constraint.

Conclusion and Recommendations

Robust asynchronous planning depends on matching the formal representation to the task structure. Greater expressivity helps only when the LLM can use it consistently. For safety-critical domains, human-in-the-loop verification and faithfulness-level validation beyond makespan accuracy are recommended. The Robo Challenge and Online Robo Challenge benchmarks introduce executable action semantics, station capacities, multi-agent assignment, deadlines, and execution-time events.

Limitations

The study notes limitations regarding dataset scale, domain coverage (centering on cooking-style grounded tasks), and the potential for biases embedded in LLMs used for data construction. The framework is an abstraction of full embodied systems, omitting continuous dynamics and sensor noise. The dataset generation relies on a commercial LLM, Gemini 3 Flash, which introduces potential biases in task framing or duration assignments.

Data and Methodology

The experiments compare three methods: Planner (direct plan generation), PDDL2.1 Formalizer (translation to OPTIC solver), and CP-SAT Formalizer (translation to scheduling JSON for CP-SAT). The evaluation metric is plan accuracy, defined as an instance being correct iff π = C ∧ g and Ttotal(π) = T⋆.

The controlled analysis on AsyncPlan-XXL confirms that the NL IR step lifts all models to 79.3%, showing that direct PDDL generation is the dominant bottleneck. The Gold IR → CP-SAT path reaches 100.0% for all four models at all scales, confirming that the ground-truth task graph is always sufficient for exact scheduling.

The paper provides detailed prompt templates for each interface, including specific instructions to ensure consistency between the LLM's output and the solver's requirements. The prompts guide the LLM to use exact item names and adhere strictly to required output schemas for different formalization targets. The results demonstrate that CP-SAT’s advantage comes from both easier faithful extraction and a more stable compilation-to-solution path. The state-aware CP-SAT repair variant improves average Online Robo Challenge accuracy from 46.1% to 84.5%, an 83.3% relative improvement over the base CP-SAT Formalizer. The paper concludes that the unified formulation, three datasets, and representation alignment principle provide a foundation for asynchronous planning systems that scale where direct generation does not.

Improvements for AI systems

Robust Asynchronous Planning via Auto-Formalization: The improved system can maintain plan accuracy even when problem complexity grows from 5 to 100 actions by choosing a formal representation that primarily determines whether planning scales. This addresses the collapse of Planner and PDDL2.1 Formalizer accuracy, as CP-SAT Formalizer averages 94% across all graph sizes and maintains 83% at step 100.
Faithfulness Diagnostics for Formalization: The system can detect specific failures in formal representations, such as PDDL2.1's predicate-based planning representation becomes brittle compared to general constraint satisfaction programs, when LLMs must keep predicates, effects, and goals consistent. This allows the system to distinguish between structural and semantic errors.
State-Aware Repair for Online Planning: For dynamic environments where constraints change during execution, the system can recover performance by employing a state-aware repair strategy that updates only event-induced constraints, which recovers CP-SAT Formalizer to 84.5% on the Online Robo Challenge when compared to one-shot re-formalization's 46.1%.

Abstract

LLMs can plan by generating schedules directly as a Planner, or by translating a task into a formal specification for a solver as a Formalizer. Most real-world tasks are asynchronous, with non-uniform durations, concurrency, and execution-time changes, yet existing benchmarks hardly cover them. We unify asynchronous planning under one formulation and release three benchmarks spanning task-graph scale, grounded state and resource constraints, and execution-time events. Surprisingly, PDDL2.1, the formalism built for temporal planning, is the weakest pipeline. On AsyncPlan-XXL it averages 30.8% plan accuracy, against 81.7% for the Planner and 94.0% for a CP-SAT Formalizer. The gap widens with scale, and at 100 actions the three pipelines reach 9.0%, 44.5%, and 82.5%, respectively. The formalism is not to blame. Compiled from the same model-extracted intermediate representation, PDDL2.1 and CP-SAT reach nearly identical accuracy (81.6% vs. 81.5%), and gold task graphs reach 100% for both. What remains is a bottleneck shared by every pipeline: recovering the task graph from language. Execution-time events further degrade every pipeline, yet updating only event-induced constraints reaches 81.6% versus 41.6% for full regeneration. Robust asynchronous planning thus hinges not on the expressiveness of the target formalism but on how reliably a model can write and edit it, and a well-chosen interface can let a weaker model match a stronger one.