Awesome World Models / OpenReview

Plan Verification for LLM-Based Embodied Task Completion Agents

作者：作者信息待提取 · 单位：University of Illinois Urbana-Champaign · 来源：General Approaches to World Models · 发布日期：2025 · 分类：5. Building World Models by Bridging Language and Vision Intelligence

具身智能语言先验

精读笔记

Problem Setting

论文标题：Plan Verification for LLM-Based Embodied Task Completion Agents（Awesome World Models / 2025）。

这篇论文真正处理的是 embodied AI 数据和计划中的“轨迹级语义噪声”问题，而不是在线机器人规划问题。输入是自然语言目标和一串动作，目标是判断哪些动作应该删、哪些步骤缺失，并把轨迹整理成更适合训练或执行的形式。

关键矛盾在于：人类 demonstration 不是 gold expert policy。TEACh 这类数据里有大量误操作、重复操作、绕路、未完成目标和临时 recovery。如果直接 imitation，模型会学习到错误动作；如果简单过滤，又可能丢掉有价值的 error-recovery pattern。以前方法要么专注于生成更好的 plan，要么依赖规则、simulator feedback 或 formal constraints；它们对已有 noisy trajectories 的低成本清洗能力不足。

真正困难点不是动作 token 是否合法，而是动作在目标和上下文中是否“有必要”。这要求模型理解长程依赖、物体用途、任务阶段、动作前后因果关系，以及有时非常模糊的“效率”标准。论文的选择是接受这个模糊性，把它交给 LLM 的语言先验和判断能力，而不是构造完整 symbolic world model。

Motivation

作者的核心动机可以概括为：embodied agents 的训练瓶颈不只是缺数据，而是 demonstration 质量低且错误结构复杂。TEACh 里的 human-authored actions 包含许多非专家行为，这些行为对 policy learning 是噪声，但对学习 recovery 又可能是信号。

已有路线的不足在于它们多数试图让 LLM 更好地产生 plan：给 action space、给 object list、给 simulator error、给 Python-like prompt。这些工作解决的是 generation grounding，却没有充分解决“已有轨迹是否值得模仿”。Formal verification 类方法能检查一致性，但需要规则、LTL 或环境假设，难以覆盖开放式 household 行为中的软错误。

这篇论文的关键缺口判断是：在 embodied pipeline 中缺一个轻量、模型无关、可扩展的 post-hoc plan verifier。也就是说，不把 LLM 当 planner 的唯一来源，而把它当 dataset curator / semantic auditor。

Core Idea

核心思想是把计划质量控制拆成两个较容易的语言任务：Judge 负责批判现有动作序列，Planner 负责根据批判做最小编辑。这个重构很重要，因为 LLM 通常比“从零生成正确长期计划”更擅长“比较、指出不一致、解释局部错误”。论文本质上是在利用 LLM-as-a-Judge 的优势，而不是声称 LLM 已经具备可靠 embodied planning。

这种方法引入的 inductive bias 是 conservative revision：保留原轨迹结构，只在 Judge 指出的地方删改或补充。这比完全重新规划更适合 demonstration curation，因为它不会把 human recovery pattern 全部 collapse 成一个理想化 plan，也避免了 planner hallucination 出全新动作链。

和 prior 的本质区别不是多 agent 本身，而是信息流的方向发生了变化：不是 goal → plan，而是 goal + existing plan → critique → edited plan。已有轨迹成为强条件，LLM 的作用从 generator 变成 verifier/editor。这使方法更 scalable：不需要为每个 domain 写 exhaustive rules，只要动作和目标可语言化，就能尝试审计。

Method

方法上可以抽象成一个 verification operator：Judge 对动作序列产生 step-level critique，Planner 将 critique 应用到原计划，循环直到无 critique 或达到上限。

第一，Judge 的作用是把隐式质量判断显式化。它输出 REMOVE / MISSING，并附理由。这解决的是“错误不可见”的问题：下游不仅知道最终计划，还知道哪些动作被认为是噪声。这个设计也让评估可以转成 precision / recall，而不是只看最终任务成功。

第二，Planner 的作用不是重新规划，而是执行受约束编辑。这解决的是 LLM 生成漂移问题。若每轮都让模型重新写完整计划，改动来源不可控；而 critique-conditioned editing 把搜索空间压缩到局部修改。

第三，迭代循环的必要性在于一次 Judge 往往只能看到显著错误；删除某些动作后，新的缺失或冗余可能暴露出来。多轮机制本质上是 test-time compute：用反复审查换 recall，而不是训练一个更强模型。

文中的形式化假设是 verification operator 在期望上减少 error count，并导致几何收敛。但这更像解释性假设，不是被严格证明的性质；实际是否单调依赖 Judge 和 Planner 的稳定性。

Key Insight / Why It Works

这篇论文最值得关注的 insight 是：在 embodied plan 场景里，LLM 的语言先验对“常见 household script 的合理性”非常强，足以捕捉大量 demonstration noise。比如 microwave toggle 顺序、无关 remote control、sandwich 未组装等错误，本质上是 commonsense script violation，不需要视觉或物理模拟就能发现。

方法有效的第一原因是任务被降维了。Judge 不需要求解完整 POMDP，也不需要建模连续空间，只需要判断给定动作是否在自然语言目标下合理。这比在线规划容易得多。

第二个原因是已有轨迹提供了强上下文。LLM 不必枚举所有可能计划，而是在一个具体 sequence 上做局部对比；这会显著降低 hallucination 空间，也让大模型的 pattern matching 能发挥作用。

第三个原因是迭代带来的 test-time compute。论文中的 recall 提升很可能主要来自多轮审查和编辑后重新暴露错误，而不是 Planner 产生了新的长期规划能力。换句话说，这不是学到了更好的 world model，而是用 LLM prior + repeated auditing 做了 dataset cleaning。

最可能的核心贡献是“语言化 verifier 用于 embodied trajectory curation”的 framing，而不是具体 prompt 或双 agent 架构。Judge-Planner loop 本身并不新，更多是已有 Reflexion / LLM-as-a-Judge 思路在 TEACh demonstration cleaning 上的直接重组。

需要警惕的是，所谓 spatial coherence 的证据并不强。模型没有视觉输入、地图、对象坐标或可达性约束，因此它改善的是动作叙事顺序和常识一致性，而不是严格空间规划。长程依赖失败案例也说明它更擅长表层逻辑错误，对真正依赖状态跟踪的冗余判断仍然弱。

Relation To Prior Work

它最接近三条路线：LLM embodied planning、LLM verification/refinement、LLM-as-a-Judge。和 PROGPROMPT、LLM-PLANNER、TAPA 等 planner-centric 方法相比，它不试图提升 initial plan generation，而是做 post-hoc verification。这个区别是实质性的：它把主要问题从“生成可执行动作”转成“清洗已有动作”。

和 Reflexion / AutoGen 类多 agent loop 相比，新意不在 agent 对话机制，而在把 critique 目标具体化为 embodied trajectory 的 REMOVE / MISSING 标注，并用人工 annotation 做 precision-recall 评估。它比一般 self-reflection 更可量化。

和 VerifyLLM 这类 formal verification 方法相比，它放弃 LTL / symbolic intermediate representation，完全依赖自然语言 prompt。这带来更好的部署便利和更宽的错误覆盖，但也牺牲了可验证性和 grounding。它不是更严格的 verifier，而是更 flexible 的 semantic filter。

因此，这篇论文属于“LLM-as-semantic-data-curator for embodied AI”的谱系。真正新增的信息是：在 TEACh 这类 noisy human demonstration 上，零样本 LLM Judge 已经能提供有用的错误定位，而且多轮 critique 可以稳定提升 recall。

Dataset / Evaluation

评估集中在 TEACh 的一个小规模 curated subset：100 个 episode、15 类 household goals、约 1.4k actions。任务覆盖了常见室内家务，但不是跨域验证，也没有真机、在线 simulator execution 或视觉 grounding。

实验支持的 claim 是有限但清楚的：LLM Judge 能在语言化动作序列上比规则 baseline 更好地识别人工标注的错误；不同 LLM 的保守/激进风格会影响 precision-recall；迭代 refinement 能提高错误发现率。

但实验并没有充分验证几个更强 claim：第一，清洗后的轨迹是否真的提升 imitation learning policy；第二，是否提升真实 embodied task completion；第三，是否保留并有效利用 error-recovery pattern；第四，是否能泛化到非 household 或更长时程任务。

人工 annotation 是必要的，但也引入 evaluation bias：什么叫 redundant、什么时候 early pickup 算低效、multi-object reuse 是否合理，都带有主观性。Judge 与 annotator 之间的一致性可能更多反映 household script 的共享先验，而非真正任务正确性。

Limitation

核心前提是：动作序列的正确性可以主要从自然语言目标和动作文本中判断。这个前提在 TEACh household script 上大体成立，但在需要视觉状态、几何约束、物理可达性、对象实例区分的任务中会迅速失效。

方法把 grounding 问题转移给了 LLM 的语言先验。没有环境状态时，Judge 不知道物体是否已经存在、是否可见、是否被另一个 agent 移动、是否有多个同类对象，也无法判断导航是否真的冗余。因此 planner 实际没有形成长期状态建模，更多是在做 script-level plausibility checking。

泛化性文中未充分说明。TEACh household task 与大模型预训练中的常识分布高度重合，效果可能主要来自 data coverage 和 implicit script memorization。若换到工业装配、医疗护理、户外搜索救援，错误类型和动作语义未必可由通用语言先验覆盖。

增益归因不清。迭代提升可能来自 Judge 多次采样式审查、Planner 重写导致表达更规整、模型自一致性，还是单纯更多 token budget，文中没有充分 ablation。所谓 multi-agent collaboration 也可能只是 prompt chaining。

scalability 上限在成本和一致性。一方面大规模数据集多轮调用 LLM 成本不低；另一方面 Judge 的 false positive 会污染轨迹，尤其是把必要的准备动作或多对象重复操作误删时，cleaning 反而破坏任务完成。

Takeaway

  • 1. 这篇论文最有价值的不是提出新 planner，而是把 embodied demonstration cleaning 明确建模为 LLM-based plan verification；这是一个值得独立出来的 pipeline stage。
  • 2. 对已有轨迹做 critique/edit，通常比从零生成计划更可靠。
  • 这一 insight 可以迁移到机器人数据清洗、web agent trace auditing、tool-use trajectory refinement 等场景。
  • 3. LLM Judge 的主要能力来自语言先验和局部一致性检查，不应过度解读为 grounded world model。

一句话总结

这篇论文把 LLM 从 embodied planner 转向 embodied trajectory verifier，用自然语言 critique-and-edit 循环做低成本 demonstration curation，是 LLM-as-a-Judge 思路在具身任务数据清洗上的一个直接但有用的实例。