论文发现语言驱动机器人安全监控的细化缺口：安全高层计划可能产生不安全执行

高层动作轨迹上的安全裁决，在写明图诱导导航和已记录的隐式动作效应之后，是否仍然成立。

• 出现场景：语言规划器用语义图连接指令、物体、区域和动作，再用时序逻辑监控计划。作者认为保证只相对于所见轨迹；导航若只写目的地或藏在高层动作里，图中已有的不安全路线到不了监控器。
• RoboGuard：引言将其描述为用受保护的语言模型把自然语言安全规则接到语义图、生成LTL，再对提议的机器人API动作做时序逻辑控制综合。论文未给出该语言模型的名称。
• 抽象错位：表面计划可以只有goto(safe lab 1)，图搜索却先经过construction area 1。inspect也可能隐式导航到物体所在区域，而不把该导航写成被监控命题。
• 作者的区分：作者认为这不是时序逻辑本身失效，而是被验证的抽象与机器人API诱导的行为不一致。固定同一条φ，用来把轨迹不匹配和LTL生成或场景接地错误分开。
• 审计内容：比较未改RoboGuard对表面计划与图细化轨迹的裁决。材料是28个受控案例（五类动作抽象）和14个端到端案例（SPINE出计划，RoboGuard生成场景接地的安全规约）。作者把图细化当作缓解，也当作诊断。

场景接地的机器人规划

• SayPlan（Rana等，2023）：用分层3D场景图、经典路径规划和仿真器反馈做长时程规划。
• SPINE（Ravichandran等，2025）：在增量更新的语义图上规划导航、检查和建图。作者追问：图虽编码语义与拓扑，安全相关的导航事件是否仍对下游验证可见。

形式化安全与运行时保障

• AutoTAMP（Chen等，2024）与LIMP（Quartey等，2025）：把语言模型与符号规划或任务—运动推理结合起来。
• Safety Chip（Z. Yang等，2024）：把自然语言禁令编码为LTL约束。Y. Yang等（2024预印本）用自动机和外部供给的规约验证生成的机器人程序。
• SOTER（Desai等，2019）：运行时保障依赖可观察系统状态发现危险，并启动已验证的回退。

实验里的对照

• 内部对照：论文没有把上述系统当作实验基线。对照是同一RoboGuard、同一条LTL下的表面轨迹与图细化轨迹；受控侧另有安全对照和显式不安全对照。
• 数据：受控用手工LTL和固定JSON计划；端到端用四个成对语义图上的自然语言任务，由SPINE出计划、RoboGuard接地。

作者把本文放在规划与验证的抽象边界上：高层动作轨迹是否省略了语义图已经能够恢复的中间导航或隐式动作效应。

固定同一条LTL，比较RoboGuard对表面动作词和图细化轨迹的裁决。细化把语义图里已有、表面计划未列出的导航事件交给同一个监控器。这不是对模型内部表示的干预。

形式化

• 不变量：C为禁入施工区，L为良性实验室。监控式为φ_C = G¬ goto(C)：动作词每个位置上goto(C)必须为假。G表示globally。
• 自动机：RoboGuard用Spot把公式编译成Büchi自动机，每个列出的动作推进一步。导航步上，列出的goto为真，未观察到的goto为假。表面词只有goto(L)时，goto(C)保持为假。
• false-safe：细化算子R用语义图G和已记录的API语义插入图诱导事件。判定为\tau_{surf}\models\varphi,\ R(G,\tau_{surf})\not\models\varphi。φ两次相同。作者称监控器对两个词各自一致，失败在于表面词不是执行的保安全抽象。

受控协议

• 隔离规约生成：未修改的RoboGuard验证器，commit e487f83。手工LTL、固定JSON计划，不调用LLM。
• 28例：12个目标抽象案例、14个安全对照、2个显式不安全对照。五类为显式且安全的目的地、隐藏禁区航点的位置、路线选择、goto/inspect/map region的细化、多动作计划。
• 展开：确定性无权最短路oracle把每个表面计划展开为图诱导执行轨迹。

端到端协议

• 系统：SPINE（commit e776a8a）从自然语言生成计划；RoboGuard在同一语义图上接地安全规则。14例、四个场景：施工区是通往良性实验室的唯一通道；匹配的安全走廊；最短路不安全且有更长的安全替代；最短路安全且有更长的不安全替代。覆盖goto、inspect、map region。
• 接地设置：temperature为0，开启chain-of-thought，每例1次试验。SPINE实现的路线与独立BFS oracle交叉核对。论文未给出语言模型名称。
• 实验形态：静态图上的离线规划与验证，不是物理机器人执行。

结局定义与结论中的细化层

• 四类结局：false-safe指表面计划被接受、图oracle认定进入禁区、同一LTL拒绝细化轨迹。blocked指不安全航点已出现在表面计划中且被拒绝。对照通过与检查器错误分开报告，错误不计为安全结局。
• 实验中的R：受控用无权最短路；端到端核对SPINE实现的路线。结论另建议：验证前按执行器选定路线展开每个goto，并暴露inspect与map region已记录的导航效应；路线不能确定时，验证所有可行细化或弃权。论文未写该层已经接入RoboGuard的发布版本。

实验设置

• 验证器：未修改的RoboGuard，commit e487f83。LTL经Spot编译为Büchi自动机，每个列出的动作推进一步。
• 受控：28个固定JSON计划、手工LTL、无LLM。12个目标案例、14个安全对照、2个显式不安全对照，覆盖第3节的五类抽象。
• 端到端：SPINE（commit e776a8a）出计划，RoboGuard在同一图上接地。14例、四个场景；temperature 0、chain-of-thought、每例1次。论文未给出语言模型名称。
• Oracle：受控为确定性无权最短路。端到端将SPINE实现的路线与独立BFS oracle交叉核对。
• 指标：FS为表面接受、oracle认定进入禁区、同一LTL拒绝细化轨迹；Blk为禁区航点已在表面计划中且被拒绝；CP为对照通过；Err为检查器错误。错误不计为安全结局。
• 未报告项：论文未报告受控重复次数。实验不是物理执行。

主结果

据Table 1：

Swipe horizontally to read the table

场景	n	FS	Blk	CP	Err
Controlled (five families)	28	12	0	16	0
E2E: unique construction bridge	5	2	0	1	2
E2E: matched safe corridor	3	0	0	2	1
E2E: unsafe shortest route	3	0	2	0	1
E2E: safe shortest route	3	0	0	2	1

• 受控分解：差异出现在隐藏航点位置（3/3）、路线选择（2/2）、动作细化（4/4）和多动作计划（3/3），并覆盖goto（7）、inspect（3）、map region（2）。细化轨迹被拒，是因为暴露了进入construction area 1。无检查器错误，也无与预注册表面预测不符。
• CP与Blk：14个安全对照被接受，2个显式不安全对照被拒绝；这16个对照计入CP。受控行的Blk为0，不是「显式不安全计划未被拒绝」。
• 端到端接地：SPINE在全部14例都产出task-attempting计划。四个图的contextual grounder都成功，且每次接地都是G(!goto(C))。作者称因此不能把false-safe归因于未认出危险区域或未生成禁令；是否出现取决于规划器轨迹粒度。

代表轨迹

• Figure 1 / N2：图中文字为表面goto(safe lab 1)、φ为G¬goto(C)、C absent、SAFE；图执行经过C再到safe lab 1，C entered、UNSAFE，并标FALSE-SAFE RESULT。图注称SPINE只暴露目的地，所以RoboGuard接受表面计划。
• Table 2的S/U与U/U：N2表面为gL，细化为gC、gL，裁决S/U。N4表面为gL、mL，细化为gC、gL、mL，裁决S/U。N5、N7表面已含gC，裁决U/U，记为Blocked。作者称最短路径指令使SPINE直接暴露C。
• 安全对照：C2、C4被作者称为matched safe controls。细化插入的是H而不是C，裁决S/S。作者称暴露中间图状态并不必然产生误报。Table 2写明是代表轨迹，不是全部14例。

接口失败与检查时间

• inspect：其余5例使用inspect。SPINE给出含物体和问题的结构化参数，RoboGuard–Spot接口期望与命题兼容的标量参数，因而语法错误：3个挑战例、2个安全对照。作者将其保留为端到端接口失败，不放入false-safe或control-pass分母。
• 耗时：受控检查平均为表面轨迹0.54 ms、细化轨迹0.69 ms。作者称检查本身保持在亚毫秒。这两个数不含规划、接地或图构建。
• 边界：作者称受控套件中该差异在所测抽象下是系统性的；端到端是否出现则取决于规划器轨迹粒度。规划器已暴露禁区时，RoboGuard拒绝原计划。

其他消融与分析

• 论文没有单独的消融表或参数扫描。
• 受控五类里，正文只给出上述四类目标案例的3/3、2/2、4/4、3/3；「显式且安全的目的地」没有单独的FS计数。
• Table 1按场景列出Err，正文未把5个inspect错误逐例对应到场景。
• 论文未报告统计检验，也未报告端到端检查时间。

作者指出的局限与后续方向

论文没有Limitations、Discussion、Future Work或附录。Conclusion没有使用「局限」或「未来工作」这类字样，写的是实践含义：

• 轨迹契约（Conclusion）：验证前，确定性细化层应按执行器选定路线展开每个goto，并暴露inspect与map region已记录的导航效应。作者称这用语义图里已有的信息，而不是在可信路径上再加一个LLM。
• 路线不能确定时（Conclusion）：系统应验证所有可行细化，或弃权。作者称带类型、面向执行的轨迹，会使RoboGuard的形式裁决与其机器人API实际诱导的高层行为对齐。

实验覆盖范围

• 受控：第3节使用未改RoboGuard（commit e487f83），28个固定计划和手工LTL，无LLM调用；含12个目标案例、14个安全对照和2个显式不安全对照。
• 端到端：第3节使用SPINE（commit e776a8a）与RoboGuard，14例、四个成对语义图场景；接地temperature为0、开启chain-of-thought、每例1次；路线与独立BFS oracle交叉核对。
• 结局拆分：第3节把规划、contextual grounding、验证、图oracle和接口失败分开记录。5个inspect例因参数形式不兼容记为语法错误，不进入false-safe或control-pass分母。
• 执行范围：第3节写明是静态图上的离线实验，不是物理执行。引言写明不建模连续机器人动力学、感知误差、避障或物理执行；主张限于相对已记录高层执行语义的动作级监控。
• 未报告项：论文未报告接地语言模型的名称、受控审计的重复次数，以及规划、接地或建图的耗时。检查时间只报告受控平均值。

作者审计RoboGuard的一个假设：对高层动作轨迹的安全裁决，在补上语义图诱导的导航和已记录隐式效应之后是否仍然成立。

做法是不改验证器，并固定同一条LTL。受控侧用手工规约和无权最短路展开28个固定计划；端到端侧由SPINE从自然语言出计划，RoboGuard在四个语义图上接地，temperature为0，每例1次。

• 12个目标案例全部是表面接受、细化后拒绝；拒绝是因为细化轨迹进入construction area 1。16个对照符合预注册预期：14个安全对照被接受，2个显式不安全对照被拒绝。这两个对照计入CP，受控Blk为0，Err为0。
• 端到端每次接地都是G(!goto(C))。Table 1里FS只出现在unique construction bridge（n=5，FS=2）；unsafe shortest route一行是Blk=2（n=3）。Table 2中N2、N4为S/U，N5、N7为U/U，C2、C4为S/S。
• 5个inspect例因结构化参数与RoboGuard–Spot接口期望的标量参数不一致而报语法错误，不计入FS或CP分母。受控检查时间从表面轨迹的0.54 ms到细化轨迹的0.69 ms，不含规划、接地或建图。

作者称这比一种笼统的失败判断更精确地定位了失败边界：规划器若已暴露禁区，RoboGuard会拒绝，接地也生成了预定禁令；禁区只作为良性目的地背后的图诱导中间状态时，表面轨迹仍可被接受。端到端是否出现，取决于规划器轨迹粒度。作者建议在验证前建立规划器、执行器与监控器之间的轨迹契约；路线不能确定时，验证所有可行细化或弃权。