LLM（大语言模型）驱动的智能体近年来被赋予了实用推理能力，包括规划、监控以及自我纠正。其成功常归因于链式思考、基于搜索的提示、自我精炼、反思、批评者以及工具使用循环等提示策略和代理架构。然而，这些主张大多依赖于端到端的成功率（仅表明任务是否完成）或由 LLM 充当的评审者，而非真正的验证器。\ \ 本文采用形式语义对 LLM 规划能力进行检验：任务以自然语言描述，但背后隐藏一个 PDDL（规划域描述语言）模型，用以判定每一步动作的适用性、目标是否达成以及是否存在可行计划。实验覆盖五个领域（其中两项为新领域，随论文公开），使用四种模型、六种提示策略和三种代理架构。离线评估中，最佳配置在可解任务上解出 78%，而在线评估（智能体在执行时几乎不检查状态）仅为 40%。不可解任务的识别率不足 10%。更复杂的提示策略消耗的 token 数是直接提示的 5 到 22 倍，却未带来明显提升。实验表明，规划性能在不同模型之间的差异大于提示策略或代理架构之间的差异。\ \ 结论：声称智能体具备规划能力必须基于经验证的动作轨迹，而非仅凭成功率或 LLM 评审。\ \ 点评