LLM异步规划新基准，发现约束求解器远胜传统形式化方法。
Robust Asynchronous Planning via Auto-Formalization
- 用统一框架构建三个大规模异步规划基准，覆盖时序不均、并发与执行约束。
- 当任务依赖图从5增至100个动作时，CP-SAT形式化保持83%准确率，其他方法骤降至0%-5%。
- 引入状态感知修复策略，仅更新事件触发约束，使性能从46.1%回升至84.5%。
大语言模型（LLMs）可通过直接生成动作序列作为规划器，或将其转换为特定领域语言供外部求解器处理作为形式化器来实现规划。然而，现实任务常具异步性、非均匀时长、并发性和执行时间约束，现有基准极少涵盖此类场景。本文将这些异步规划挑战统一为单一范式，并提出首个三类规模化基准。结果表明，形式化表示的选择决定规划可扩展性：当依赖图规模从5增至100个动作时，规划器准确率由96%跌至5%，PDDL2.1形式化器从13%降至0%，而CP-SAT形式化器平均达94%，在100动作下仍保持83%。忠实度诊断显示，当需维持谓词、效果与目标一致性时，基于谓词的规划表示相比通用约束满足程序更易失效。执行时间约束动态更新进一步显著降低性能（规划器23.9%，PDDL2.1仅0.7%，CP-SAT为46.1%），但一种仅更新事件触发约束的状态感知修复策略，使CP-SAT形式化器恢复至84.5%。
原文摘要 · Abstract (English)
LLMs can plan by either generating action sequences directly as a Planner or translating tasks into domain specific language for an external solver as a Formalizer. While most real-world tasks are asynchronous with non-uniform durations, concurrency, and execution-time constraints, existing benchmarks hardly cover them. We unify these asynchronous planning challenges under a single formulation and introduce the first three benchmarks that address each at scale. We conclude that 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. Faithfulness diagnostics show that PDDL2.1's predicate-based planning representation becomes brittle compared to general constraint satisfaction programs, when LLMs must keep predicates, effects, and goals consistent. Execution-time updates of planning constraints further degrade performance sharply (Planner 23.9%, PDDL2.1 0.7%, CP-SAT 46.1%), but a state-aware repair strategy that updates only event-induced constraints recovers CP-SAT Formalizer to 84.5%.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。