形式语义测试揭示LLM智能体规划能力不足

该研究通过引入隐藏 PDDL 模型作为形式化验证器，对 LLM 智能体的规划能力进行了严格测试，发现现有主流评估方法存在严重缺陷。在五个领域、四种模型和六种提示策略的组合实验中，最佳配置在离线环境下仅能解决 78% 的可解任务，而在更接近真实场景的在线环境中，成功率骤降至 40%，且智能体大多在未检查状态的情况下盲目行动。 关键证据显示，对于不可解的任务，智能体仅在不到 10% 的回合中能够正确识别，这意味着它们无法有效区分“无解”与“未找到解”。此外，更复杂的提示策略（如思维链、自我反思等）导致 token 消耗量是直接提示的 5 到 22 倍，却未带来明显的性能提升。实验结果还表明，规划性能的差异主要源于模型本身的差异，而非提示策略或架构的变化。 事实层面，本研究证实了当前基于端到端成功率的评估无法反映真实的规划逻辑，且复杂提示策略存在严重的投入产出比失衡。推断层面，行业若继续依赖此类指标宣传 Agent 能力，将导致产品在实际部署中出现大量隐性失败。猜测层面，未来可能需要建立基于形式化验证的标准化基准来替代现有的黑盒评测，但这需要学术界与工程界共同推动新的评估范式。