精读笔记

Problem Setting

EvoPlan 处理的不是传统意义上的 task planning，而是自然语言目标、开放世界状态、离散符号动作和连续安全规范之间的耦合问题。真正困难点在于：任务目标通常只说明“要完成什么”，但机器人还必须满足没有显式写出的移动规范，例如红灯、避障、人际距离、速度舒适性等。

以前路线卡在两个极端。LLM/VLM planner 能读上下文、补语义、生成 plausible plan，但没有机器可检查的可执行性和安全性；PDDL planner 能验证 precondition/effect 和 goal reachability，但前提是 domain/problem 已经完整形式化，而且连续执行安全通常不在 PDDL 层里。行为克隆或 RL 可以吸收部分规范，但规范被埋进 policy 参数，难以验证、组合和迁移。

这篇论文的关键矛盾是：开放世界机器人需要 neural model 的语义弹性，但 safety/executability 需要 symbolic/temporal verifier 的硬边界。EvoPlan 的解法不是让一个模型同时学会二者，而是把生成和判定分离。

Motivation

已有路线缺的是一个可迁移的“执行合约”。PDDL 能约束离散动作是否合法，但不能自然表达连续轨迹上的 clearance、TTC、social distance、speed envelope；STL 能表达连续时序约束，但通常需要人工写规则或有 violation labels。机器人日志里有大量“可接受行为”，但通常只有正例，没有明确负例和符号规范。

作者的核心观察是：安全规范不一定要从任务 prompt 里来，也不一定要写进每个 action schema；它可以作为一个全局 mobility constraint 从历史轨迹中挖出来，然后对所有移动动作统一生效。这样，PDDL 解决“做什么顺序”，STL 解决“怎么移动才可接受”。

另一个动机是 LLM 最适合的位置不是最终决策者，而是 search operator。LLM 擅长根据失败反馈做局部修复，但它不擅长自证正确。因此把 LLM 放进 verifier-driven evolutionary loop，比 one-shot planning 或 self-reflection 更符合它的能力边界。

Core Idea

本文真正的核心不是“三个模块”，而是一个建模方式变化：把机器人 planning 从“生成一个完整计划”改成“反复生成候选，并用外部可计算约束筛选、修复和重规划”。LLM/VLM 只负责提出候选 plan、predicate mapping、violation pattern 或 repair；PDDL validator 和 STL robustness 才是系统的选择压力。

这个设计引入的 inductive bias 很明确：任务层可离散验证，移动层用全局时序约束验证，二者之间通过 waypoint trace 连接。相比把 safety 写进 prompt 或 reward，这种方式更 scalable，因为同一个 Φ_mob 可以跨任务、跨 policy、跨 action schema 复用；相比纯 symbolic planning，它又能用 LLM 处理 vocabulary mismatch、partial belief 和 plan repair。

和 prior 的本质区别在于，它不是只把 LLM 输出翻译成 PDDL，也不是只用 verifier 给 LLM 打分，而是把 learned temporal contract 放到了执行层。这个 contract 不是针对某个具体 skill，而是所有 mobility action 的全局约束，因此形成了一个跨任务的安全接口。

Method

第一，one-class demonstration 到 STL constraint。它解决的是“只有合格轨迹，没有违规标签”的问题。作者用 procedural perturbation 和 LLM violation generator 构造 counterfactual negatives，把规范学习变成正负轨迹分类，再用 evolutionary search 找 STL formula。核心变化是把隐含规范从 policy behavior 中抽离成显式、可监控、可迁移的 formula。

第二，LLM-guided evolutionary PDDL planning。它解决的是 LLM plan 不可靠、symbolic planner 对开放语义不灵活的问题。候选 plan 由 LLM mutation/repair 产生，但 survival 由 syntax check、VAL simulation、goal reachability 和可选 STL feasibility 决定。这里的关键不是 evolution 这个名字，而是 verifier feedback 变成 test-time curriculum：失败 action 和 unsatisfied precondition 直接塑造下一轮搜索。

第三，verified-prefix execution。它解决的是符号计划和连续执行之间的落差。每个 PDDL action 被 navigation layer 展开成 waypoint sequence，执行前检查 Φ_mob；若违反约束，则提交已验证前缀、刷新世界状态、重新规划。核心变化是 symbolic effect 不应在 plan 生成时无条件相信，而应在连续 trace 通过约束后才进入后续状态。

第四，vocabulary misalignment 处理。目标谓词和 action-model 词表不一致时，用一次 LLM predicate-symbol mapping 改写 goal predicates。这是实用工程点，解决 benchmark 中 hot/heated、clean/washed 这类 mismatch；但它更像 representation alignment glue，不是规划理论贡献。

Key Insight / Why It Works

最可能真正有效的部分是 verifier-driven test-time compute。LLM 的强项是从局部错误反馈中提出 plausible repair，而 VAL/STL 给出了明确、低噪声、机器可判定的错误信号。相比 self-critique，这种反馈更接近搜索中的 oracle；相比传统 symbolic search，它又能利用 LLM 在对象绑定、词表映射、动作重排上的语义先验。

STL shield 有效的原因不是它“理解安全”，而是它把 demonstration 中高度重复的低维运动 envelope 显式化了。速度、clearance、TTC、pedestrian distance 这类信号本来就有强结构，且很多 violation 可以用阈值公式捕捉。换句话说，核心贡献更像 better inductive bias + data-derived thresholds，而不是深层 reasoning。

PDDL planner 的增益很可能主要来自 test-time compute 和 validator feedback，而不是模型形成了新的长期规划能力。verified-prefix monotonic growth 是合理现象：一旦 validator 指出第一个失败位置，LLM 只需要修复 suffix 或插入 precondition action，搜索难度被局部化。这本质上是把 plan synthesis 转成 guided repair。

counterfactual negatives 是双刃剑。它们让 one-class learning 可行，但也把“什么算 violation”的边界悄悄注入了系统。若 perturbation modes 覆盖了 benchmark failure modes，shield 会显得很强；若真实世界 violation 超出这些模式，公式可能过窄或误拒。这里的增益来源不清，可能主要来自 data/negative generator 与评测场景的对齐。

所谓 spatio-temporal guarantees 需要谨慎理解。STL robustness 能保证被检查的 predicted/observed trace 满足 formula，但不能保证 perception 正确、未来动态可预测、navigation controller 精确跟踪，也不能保证 formula 等价于真实安全规范。因此它是 contract-monitoring guarantee，不是 full-stack safety guarantee。

Relation To Prior Work

这篇属于 LLM + formal methods + runtime monitoring 的技术谱系，接近 NL-PDDL、LLM+P、SafeGen-LLM、VLMFP、temporal logic learning 和 AlphaEvolve-style machine-gradable search 的交叉点。

和 NL-PDDL 的差异在于，NL-PDDL 主要扩展 symbolic planning 对自然语言 predicate 的处理能力；EvoPlan 额外引入了执行层 STL contract，关注连续轨迹是否满足隐含规范。两者解决的是不同断点：一个是 language-symbol alignment，一个是 symbol-continuous execution alignment。

和 SafeGen-LLM 的差异在于，SafeGen 更像在显式 safety constraints 上训练/优化 planner；EvoPlan 的 safety constraint 从 demonstration 中挖出来，并作用在 measured signals 上。这个差异是实质性的，因为它把 safety 从 PDDL3-style symbolic constraint 推到了 signal temporal logic 层。

和 temporal logic learning 的关系是复用思想而非纯创新。用 STL grammar、robustness score、complexity penalty 学公式并不新；新增点是把学到的公式作为所有 PDDL mobility action 的全局 runtime contract，并接入 LLM repair loop。

和 AlphaEvolve 类方法的关系也很直接：LLM 生成候选，外部 evaluator 决定保留。这里的新意不在 evolutionary search 本身，而在 evaluator 是 PDDL/VAL/STL 这种机器人规划与执行约束，并且搜索对象从程序/公式扩展到 grounded action sequence。

Dataset / Evaluation

评测覆盖三块：nuPlan 到 Bench2Drive 的 rule shield，SCAND 到 HA-VLN-CE 的 preference shield，ALFWorld/Text 与 Blocksworld 的 PDDL planning，以及 Gazebo Jackal 场景的 end-to-end 展示。覆盖面看起来宽，但每块验证的 claim 不同，不能合并理解为完整系统在真实世界中被充分验证。

STL shield 的跨场景结果支持“一个从 demonstration 中挖出的低维移动约束可以迁移到不同 policy/benchmark 上减少明显违规”。但这里主要验证的是约束过滤器，而不是完整 neuro-symbolic planner。并且 HA-VLN-CE 使用 ground-truth human positions，真实感知噪声被弱化。

PDDL planner 的 ALFWorld/Text 结果支持 verifier-guided LLM repair 在 benchmark 上优于 direct/reflective baselines，尤其在 vocabulary misalignment 下有优势。但 simulator 提供 ground-truth perception/affordance oracle，规划和真实感知执行的耦合没有被充分测试。Blocksworld variants 更像 stress test for lexical robustness，而不是机器人部署能力。

Gazebo end-to-end 是 proof-of-concept 级别。5 个 mission、仿真 Jackal、有限 crowd density 不能支撑强部署 claim；它主要说明接口能跑通，且 shield/replan 在局部拥挤下有预期行为。没有真机实验是核心缺口。

总体上，evaluation 支持“这种架构是可行的，且各子机制有局部收益”，但还不足以证明“学到的时空规范在真实开放世界中可靠泛化”。

Limitation

第一，方法把人工写规范的问题部分转移到了 grammar、signal selection 和 counterfactual generator。STL 只能表达预设信号空间里的约束；如果关键 safety factor 不在 signal dictionary 中，系统无法发现它。文中未充分说明信号选择的系统性原则。

第二，learned Φ_mob 的泛化依赖 demonstration 覆盖。若数据只覆盖常见道路/人群密度/操作风格，公式学到的是 demonstrator envelope，而不一定是因果安全规则。核心能力可能主要来自数据覆盖，而不是从少量数据中抽象出真实规范。

第三，counterfactual negatives 可能构成 hidden supervision。程序扰动模式和 LLM violation generator 实际定义了负类边界；如果这些模式与评测 violation 高度重合，结果会高估 constraint mining 的自然发现能力。增益来源不清。

第四，planner 没有真正解决开放世界长期状态建模。PDDL domain 仍然是输入，symbolic effects 仍由 domain assert；执行层虽然会检查 waypoint，但文中未充分说明 skill failure、partial observability、错误 perception、动态 agent prediction failure 如何系统性反馈到 domain-level belief。

第五，test-time token cost 高。EvoPlan 在很多任务上用 LLM 反复 repair，优势来自 verifier-guided search budget；在传统 symbolic planner 能直接求解的问题上，它明显不是更优解。这里可能主要是 scaling / test-time compute 换成功率。

第六，所谓 guarantee 有边界。它保证的是候选 trace 对 learned STL formula 的满足，不保证 formula 正确、不保证 rollout prediction 准确、不保证控制执行不偏离，也不保证感知输入可靠。因此标题中的 spatio-temporal guarantees 容易被过度解读。

第七，真实部署验证不足。Gazebo 中的 crowd、Nav2、ground-truth/近似信号和有限任务无法代表复杂物理世界。没有硬件实验时，很难判断该闭环在 latency、tracking noise、occlusion、controller saturation 下是否稳定。

Takeaway

• 1. 最值得迁移的 insight 是：不要让 LLM 直接承担 correctness；把它放在 machine-checkable loop 中作为 proposal/repair operator，外部 verifier 才是系统的可靠性来源。
• 2. 从 demonstrations 中抽取全局 execution contract，比把 safety 混进每个 skill/policy 更有组合性。
• 尤其在机器人系统中，低维可监控信号上的 STL shield 是一个实用接口。
• 3. 未来真正值得做的是把 learned constraint 的统计保证、uncertainty-aware monitoring、per-skill contract 和 real hardware feedback 接起来。

一句话总结

EvoPlan 是一篇把 LLM planning 从“直接生成计划”推进到“verifier-driven candidate evolution + learned STL execution contract”的系统型工作，真正贡献在于重新组织神经生成、符号验证和连续时空监控之间的信息流。