精读笔记
Problem Setting
[Plan Right, Then Plan Tight: Symbolic RL for Efficient Embodied Reasoning]（arXiv preprint / 2026）
这篇论文解决的不是一般意义上的 embodied reasoning，而是高层 embodied planner 的可验证训练问题：给定语言指令和符号化场景，模型需要生成能被动作库执行、能达到 BDDL goal、且不违反 precondition 的计划。真正困难点在于训练信号：自然语言计划看起来合理不等于可执行，完整仿真又不适合作为 RL 内循环 reward。以前 LLM planner 卡在 fluent but unverifiable，classical planner 卡在 domain/action schema 扩展成本，simulation-based 方法卡在延迟和可扩展性。本文抓住的关键矛盾是：开放任务需要语言模型处理语义多样性，但训练优化需要一个确定、便宜、结构化的 verifier。
Motivation
作者的动机很清楚：现有路线缺的不是更长 CoT 或更复杂 prompt，而是一个能同时服务数据、执行检查和 RL reward 的共享语义接口。BDDL 正好处在一个有用的中间层：它保留 typed objects、initial predicates、goal predicates，可以被符号执行器快速检查；同时它比 PDDL domain 更贴近 BEHAVIOR 这类开放物体类别任务。核心观察是，如果把 BDDL 从 benchmark metadata 变成训练时的中心表示，就能避免三个常见错位：训练标签与评测目标错位、语言计划与世界状态错位、reward 与真实可执行性错位。
Core Idea
论文真正的核心不是“视频解析 + SFT + DAPO + Short-RL”的流水线，而是把 embodied planning 重新建模为 verifier-aligned generation。模型不再被要求直接从自然语言幻想一个计划，而是在一个 BDDL 定义的状态空间里生成可被 symbolic engine replay 的 action code；同一个 BDDL 同时定义输入、监督、reward 和 evaluation。
这个建模改变引入了强 inductive bias：计划必须以对象、谓词、前置条件、效果和目标满足为单位组织，而不是以自由文本 reasoning 为单位组织。相比 prior 的提示式 LLM planner，它的本质差异在于 verifier 进入训练内循环；相比 classical planning，它没有要求完整手写 domain，而是用 benchmark BDDL 和自动动作扩展降低工程门槛。它的 scalability 来自 verifier 低延迟和数据接口统一，而不是模型本身突然具备更强物理推理。
Method
关键机制可以压缩成三层。
第一层是 BDDL 对齐：把 curated BDDL 或视频解析得到的 draft BDDL 变成 verified task representation。它解决的是监督来源不稳定和语义漂移问题；必要性在于 planner 的输入、训练目标和评测器必须共享同一套对象/谓词，否则 RL reward 会优化到错误目标。
第二层是 symbolic verification：engine 执行动作序列，区分 Goal Completion、Engine-Pass 和 Strict-Pass。它解决的是二值成功信号过粗的问题；核心变化是 reward 能把“部分完成”“最终目标满足但中间非法”“真正可执行成功”分开，使 RL 有梯度而不是只做稀疏筛选。
第三层是 correctness-gated compression：先学会 plan right，再 plan tight。Short-RL 的长度惩罚只在正确性稳定后打开，GroupAdapt 用 group pass rate 判断当前 prompt 是否稳定，难样本给更宽 length tolerance。它解决的是 reasoning compression 中常见的过早截断问题；核心变化是长度优化从全局静态约束变成 verifier-conditioned curriculum。
Key Insight / Why It Works
最可能真正有效的部分是 verifier reuse，而不是 DAPO 本身。用同一个 symbolic engine 同时做 SFT rejection sampling、RL reward、evaluation 和 error diagnosis，会极大降低训练-评测 mismatch；这类 alignment 在结构化任务里通常比换一个更强 RL 算法更重要。
第二个有效点是 reward decomposition。GCR 给 hard prompt 保留连续信号，error penalty 避免模型通过非法动作投机，EP/SP 区分让模型知道“达到目标”和“可执行达到目标”不是一回事。这比 string-match 或 LLM judge 更像真正的 planning reward。
第三个有效点是 curriculum，而非长度优化本身。GroupAdapt 的本质是用 in-batch pass rate 做在线难度估计：会做的题压短，不会做的题先别压。这是一个低成本但合理的控制策略。它更像 difficulty-aware budget scheduling，不是新的 reasoning 能力。
需要直接判断的是：相当一部分增益可能主要来自 data / verifier alignment / teacher rejection sampling，而不是 8B 模型学到了通用 embodied reasoning。D-SFT 从 teacher 中选 shortest strict-pass trajectory，本身已经注入了强 hidden supervision；RL 更像把 sampled correct behaviors 提升为 one-sample consistency。所谓 symbolic reasoning 在 benchmark 内成立，但是否迁移到未覆盖谓词、未覆盖动作和真实物理约束，文中未充分说明。
Relation To Prior Work
这篇属于 LLM planner + symbolic verifier + verifier-guided RL 的谱系，接近 Code-as-Policies、ProgPrompt、LLM+P、neuro-symbolic planning，以及最近用 GRPO/DAPO 做 reasoning RL 的工作。它不是从零发明 symbolic planning，也不是发明 length-aware RL；真正新增的是把 BDDL 作为单一接口贯穿数据生成、执行验证和 RL reward。
和 prompting-based embodied planner 的本质差异是：prior 多数在 test time 依赖语言模型自洽或少量 affordance filter，本文把可执行性变成训练时优化目标。和 classical PDDL/TAMP 的差异是：本文不追求完整可证明的物理规划，而是在 benchmark action library 上做高速近似符号执行。和 Short-RL/DAPO 的关系则更像任务化改造：RL 框架是借来的，实质创新在于 reward source 是 symbolic engine，长度 schedule 被可执行性 gate 住。
Dataset / Evaluation
评测主要在 BEHAVIOR-100 / BEHAVIOR-1000 的 extended-BDDL setting 上，覆盖多任务、多物体、单臂/双臂配置，适合验证“BDDL-aligned symbolic planner 是否能在 benchmark 内变得准确且简洁”。实验确实支持这一点：小模型在 verifier-aligned 训练后能超过很多大模型的一次采样表现，并且长度大幅压缩。
但 evaluation 没有真正验证真实世界 embodied deployment。视频到 BDDL 只在 50 个视频上做了有限评估，而且最终主实验仍主要依赖 BDDL/BEHAVIOR 生态。由于训练、reward 和评测共享同一 symbolic engine，结果强烈证明了 engine-aligned optimization 的有效性，但不等价于证明模型具备开放世界物理可执行规划能力。prompt choice 也被作者承认是变量，说明 benchmark 表现可能对输入格式和规则表达较敏感。
Limitation
最核心的限制是前提很强：必须有足够准确的 BDDL、稳定的 predicate semantics、覆盖目标谓词的动作库，以及一个与评测一致的 symbolic engine。只要这些条件失效，planner 的高分可能迅速退化。
第二，方法可能把问题转移了。原问题是“模型如何理解场景并规划”，现在变成“系统如何构造正确 BDDL 并维护动作库”。视频到 BDDL、LLM verifier、action discovery 都可能成为实际瓶颈；文中未充分说明它们在长尾真实场景中的失败模式。
第三，泛化证据有限。BEHAVIOR 内的任务、谓词、动作和目标结构高度共享，模型提升可能主要来自 data coverage 与 benchmark-aligned rejection sampling。所谓 reasoning 更可能是 learned symbolic template / retrieval-like generation，而不是形成了稳健的长期状态建模。
第四，物理可行性被抽象掉了。Strict-Pass 是 symbolic strict，不是 robot strict；precondition/effect library 说可执行，不代表真实机器人能抓取、避障、操作或满足连续几何约束。
Takeaway
- 1. 值得迁移的核心 insight 是：在结构化决策任务中，先找到一个低延迟、可执行、训练-评测共享的中间表示，往往比直接扩大模型更有效。
- 2. verifier 不应只做评测器，而应进入数据筛选、reward shaping 和 curriculum；同一个 verifier 复用越多，训练目标越不容易漂。
- 3. 长度压缩的正确顺序是先建立可验证正确性，再压缩表达；对 hard prompt 施加统一短预算通常是错的，在线 group success rate 是一个便宜但有效的难度信号。
- 4. 未来真正值得做的是把这套 BDDL-centric verifier 从 benchmark-symbolic world 推到 noisy perception、partial observability 和真实 action feasibility；否则它更像 BEHAVIOR 上非常强的 symbolic-RL engineering system。
一句话总结
这篇论文的定位是把 embodied planning 从 free-form LLM generation 推向 verifier-aligned symbolic RL：真正贡献在于用 BDDL 统一表示和低延迟符号验证重组训练信息流，而不是发明新的 planner 或新的 RL 算法。