精化差距审计：RoboGuard 安全高层计划为何产生不安全执行
本文为一篇预印本，作者审计了 RoboGuard 安全监视器对高层动作序列的验证假设。通过对比表面计划与基于语义图的精化执行轨迹，在 28 个受控案例中发现 12 个目标案例全部出现表面安全但精细化后不安全的假安全结果，并在 14 个端到端案例中复现 2 例。作者提出轻量级图驱动轨迹精化层作为缓解，将验证时间仅从 0.54 毫秒增至 0.69 毫秒。
在语言驱动的机器人系统中，高层动作序列的安全验证结论是否在加入图诱导导航和隐式动作效果后仍然成立？
RoboGuard 等安全监视器验证的是高层动作列表，但实际执行时 goto、inspect 等动作会触发隐式的导航步骤或中间区域，这些安全相关事件未出现在被监视的表面轨迹中。例如，goto(safe_lab_1) 可能在图中先经过禁止的施工区，但监视器只看到目的地区域，因而错误接受违反安全规则的计划。
既有安全验证方法（如 RoboGuard、AutoTAMP、LIMP、Safety Chip、SOTER）假设可观的高层状态足以代表执行行为，没有检查动作抽象层是否掩盖了图诱导的中间导航或隐式动作效果。RoboGuard 自身仅对列出的动作逐项推进自动机，不展开隐藏的路径。
作者设计了一套受控审计方法，固定 LTL 规范不变，将同一表面计划与经过确定性 BFS 最短路径预言机扩展后的图精化轨迹分别送入 RoboGuard 验证，从而隔离动作抽象故障与规范生成故障。在此基础上，提出最小缓解方案：在验证前加入一个确定性轨迹精化层，利用语义图中已有的路径信息和文档化的动作语义，展开每个 goto 的选定路径，并暴露 inspect 和 map_region 的导航效果，无需引入额外 LLM。
受控评估包含 28 个案例，其中 12 个目标抽象案例全部出现表面轨迹安全、精化轨迹不安全的假安全结果，16 个对照案例全部符合预期（14 个安全通过、2 个显式不安全被拒绝），零检查器错误。RoboGuard 检查平均耗时表面 0.54 毫秒、精化 0.69 毫秒。端到端评估使用 SPINE 规划、RoboGuard 接地的 14 个案例中，SPINE 全部生成尝试性计划，RoboGuard 在四张图上均成功接地并生成规范 G(!goto(C))；结果为 2 个假安全（仅出现在唯一施工桥场景，案例 N2、N4）、2 个显式不安全被阻止（不安全最短路径场景）、5 个控制通过、5 个检查器错误（均由 inspect 结构化参数接口不匹配引起）。安全对照在精化后仍安全，未产生误报。
作者明确说明实验基于静态语义图和图推导执行轨迹，未建模连续动力学、感知误差、碰撞避免或物理执行，结论仅针对动作级监控相对文档化高层执行语义的可靠性。端到端评估每个案例仅进行一次试验，离线进行且非真机。inspect 动作的接口不匹配导致 5 个检查器错误，未被计入假安全或控制通过。论文未报告代码开源情况或缓解方案在端到端系统中的完整实现。
使用语言驱动规划和形式化安全监视器的机器人公司（如仓储、巡检、服务机器人）可立即将图驱动轨迹精化作为诊断工具，检测 RoboGuard 类系统的假安全漏洞。1 至 3 年内，可在现有 RoboGuard 部署中加入确定性精化层，消除由动作抽象引起的假安全。前提是语义图包含完整可达路径、执行器路由可确定、动作语义文档完整。3 年以上，若结合感知与动力学验证，该思路可支撑更严格的安全认证流程。
论文全文
Mind the Refinement Gap: When Safe High-Level Robot Plans Produce Unsafe Executions
本文依据 CC BY 4.0 许可发布，经署名转载，原文见 arXiv:2610.02662（PDF）。
Abstract
Language-enabled robot systems increasingly combine semantic-graph planning with temporal-logic safety monitors. We investigate a trace-completeness assumption in these systems: whether the high-level action sequence checked by a monitor represents the navigation and implicit action effects induced during execution. We audit this assumption in RoboGuard by comparing its verdict on a surface plan with its verdict on a graph-refined trace under the same Linear Temporal Logic (LTL) specification. Our evaluation comprises 28 controlled cases spanning five action-abstraction families and 14 end-to-end cases in which SPINE [5] generates plans from natural-language instructions while RoboGuard generates scene-grounded safety specifications. In the controlled evaluation, all 12 targeted abstraction cases exhibit the predicted surface-versus-refined discrepancy while all 16 controls behave as expected, motivating graph-based trace refinement as a lightweight mitigation and a diagnostic tool for physical-AI safety monitors.
Keywords: Physical AI Safety, Runtime Verification, Semantic Graphs
1 Introduction
Language-enabled robot planners increasingly use semantic graphs to connect natural-language instructions with objects, regions, and executable robot actions. Formal safety monitors can then evaluate the resulting plans against temporal-logic requirements. However, the guarantees provided by such a monitor are necessarily relative to the action trace that it observes. A semantic graph may contain enough information to identify an unsafe route, yet that information may never reach the monitor if navigation is represented only by its destination or is hidden inside a higher-level action.
For example, a surface plan may contain only goto(safe_lab_1), although graph search realizes the action as goto(construction_area_1) followed by goto(safe_lab_1). Similarly, an action such as inspect(sensor_1) may implicitly navigate to the object’s associated region without exposing that navigation as a monitored proposition. A prohibition against entering a construction area can therefore be satisfied by the surface trace while being violated by the graph-induced execution trace. This is not a failure of temporal logic itself; it is a mismatch between the abstraction verified by the monitor and the behavior induced by the robot API.
RoboGuard [6] provides a suitable system for studying this boundary. It uses a protected language model to ground natural-language safety rules in a semantic graph, generates LTL specifications, and applies temporal-logic control synthesis to proposed robot API actions. Our central question is:
Does a safety verdict over a high-level action trace remain valid after graph-induced navigation and documented implicit action effects are made explicit?
Let C be a forbidden construction region. RoboGuard grounds the corresponding safety rule as the LTL invariant
\varphi_{C}=\mathbf{G}\neg\texttt{goto}(C),where \mathbf{G} means “globally”: at every position in the monitored action word, the atomic proposition goto(C) must be false. RoboGuard compiles this formula into a Büchi automaton with Spot and advances the automaton once per listed action. At a navigation step, the listed goto proposition is true and unobserved goto propositions are false. Thus, in the surface word \tau_{\mathrm{surf}}, only goto(L) occurs; goto(C) remains false and Eq. (1) is satisfied. Yet the navigation backend may realize that action along the graph path C\rightarrow L. Let \mathcal{R} expose graph-induced events using semantic graph G and the documented API semantics. In this example, it inserts goto(C) before goto(L); the first refined valuation therefore violates the invariant. More generally, we call a case an action-abstraction false-safe when
\tau_{\mathrm{surf}}\models\varphi\quad\text{but}\quad\mathcal{R}(G,\tau_{\mathrm{surf}})\not\models\varphi.Thus, the monitor is internally consistent on both words; the failure arises because the surface word is not a safety-preserving abstraction of execution. Holding \varphi fixed separates this trace mismatch from errors in LTL generation or scene grounding. Figure 1 instantiates this condition using the observed N2 end-to-end failure.
C is the forbidden construction region. SPINE exposes only the destination, so RoboGuard accepts the surface plan. Graph execution traverses C and violates the same LTL rule.We investigate this question at two levels. First, a controlled suite contains 28 fixed-plan cases with manually specified LTL constraints: 12 targeted abstraction cases and 16 safe or explicitly unsafe controls. The cases cover direct-action controls, hidden-waypoint position, route selection, action refinement, and multi-action plans. Second, a 14-case end-to-end suite provides natural-language tasks to SPINE and safety rules to RoboGuard over four paired semantic-graph scenarios. It covers goto, inspect, and map_region, including unique unsafe bridges, matched safe corridors, and graphs containing both safe and unsafe alternative routes.
Our contributions are:
- A controlled methodology for distinguishing action-abstraction failures from specification-generation failures by evaluating surface and graph-refined traces under the same LTL specification.
- A collection of paired negative cases and controls covering explicit navigation, hidden intermediate regions, implicit navigation, route choice, action refinement, and multi-action plans.
- An end-to-end SPINE–RoboGuard evaluation that records planning, contextual grounding, verification, graph-oracle, and interface failures as separate outcomes rather than conflating them with safety verdicts.
- An evaluation of graph-based trace refinement as a minimal mitigation that exposes safety-relevant execution events already represented in the semantic graph.
Our experiments operate over static semantic graphs and graph-derived execution traces. They do not model continuous robot dynamics, perception errors, collision avoidance, or physical execution. Accordingly, our claims concern the soundness of action-level monitoring relative to documented high-level execution semantics, rather than complete real-world robot safety.
2 Related Work
Scene-grounded robot planning.
Language-enabled robot planners increasingly use structured world models to ground instructions. SayPlan combines hierarchical 3D scene graphs, classical path planning, and simulator feedback for long-horizon planning [4], while SPINE plans navigation, inspection, and mapping actions over an incrementally updated semantic graph [5]. Although these graphs encode semantic and topological information, our study asks whether safety-relevant navigation events remain visible to downstream verification.
Formal safety and runtime assurance.
AutoTAMP and LIMP combine language models with symbolic planning or task-and-motion reasoning [1, 3]. The Safety Chip encodes natural-language prohibitions as LTL constraints [8], while related work verifies generated robot programs using automata and externally supplied specifications [7]. Runtime-assurance systems such as SOTER similarly rely on observable system states to detect hazards and activate verified fallbacks [2]. In contrast, we examine the abstraction boundary between planning and verification: whether high-level action traces omit intermediate navigation or implicit action effects already recoverable from the semantic graph.
3 Experimental Results
Protocol and test scenarios.
We evaluate the unmodified RoboGuard verifier at commit e487f83 using two complementary protocols. The controlled audit uses manually specified LTL and fixed JSON plans, requires no LLM calls, and isolates the action-abstraction boundary from specification generation. Its 28 cases comprise 12 targeted cases, 14 safe controls, and two explicitly unsafe controls. They span five families: explicit and safe destinations, the position of a hidden forbidden waypoint, route choice, refinement of goto/inspect/map_region, and multi-action plans. A deterministic unweighted shortest-path oracle expands each surface plan into its graph-induced execution trace. Below, C denotes the forbidden construction region and L the benign laboratory.
The end-to-end audit uses SPINE (commit e776a8a) to generate plans from natural-language instructions and RoboGuard to ground the safety rule in the same semantic graph. We evaluate 14 cases over four scenarios: a construction area forming the unique bridge to a benign laboratory, a matched safe corridor, an unsafe shortest route with a longer safe alternative, and a safe shortest route with a longer unsafe alternative. The suite covers goto, inspect, and map_region. Grounding used temperature zero with chain-of-thought enabled; one trial was run per case. SPINE’s realized route was cross-checked against an independent BFS oracle. These are offline planning-and-verification experiments over static graphs, not physical robot executions.
For both protocols, a false-safe action-abstraction result means that RoboGuard accepts the surface plan, the graph oracle identifies forbidden entry, and the same LTL specification rejects the refined trace. A blocked result means that the unsafe waypoint is already exposed in the surface plan and RoboGuard rejects it. Control passes and checker errors are reported separately; errors are never counted as safety outcomes.
- 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
Controlled audit.
All 12 targeted cases produced the predicted discrepancy: the surface trace was accepted, whereas the graph-refined trace was rejected after exposing entry into construction_area_1. The result held across hidden waypoint position (3/3), route choice (2/2), action refinement (4/4), and multi-action plans (3/3), and across goto (7 cases), inspect (3), and map_region (2). All 16 controls behaved correctly: all 14 safe controls were accepted and both explicit unsafe controls were rejected. There were no checker errors or mismatches with the preregistered surface predictions. RoboGuard checking itself remained sub-millisecond on average (0.54 ms for surface traces and 0.69 ms for refined traces); these figures do not include planning, grounding, or graph construction.
End-to-end SPINE–RoboGuard audit.
SPINE successfully produced a task-attempting plan in all 14 cases, and RoboGuard’s contextual grounder succeeded for all four graphs. Importantly, every grounding produced the intended specification G(!goto(C)). Thus, the observed false-safe cases cannot be attributed to failure to recognize the hazardous region or to generate its prohibition.
Table 2 exposes the role of planner trace granularity. In N2 and N4, SPINE represents navigation only by the benign destination L, while graph refinement reveals traversal through the forbidden region C. RoboGuard consequently accepts the surface trace and rejects the refined trace. In N5 and N7, the shortest-route instruction causes SPINE to expose C directly, allowing RoboGuard to reject the original plan. The matched safe controls C2 and C4 remain safe after refinement, indicating that exposing intermediate graph states does not inherently produce false alarms.
- N2
- g_{L}
- g_{C},g_{L}
- S/U
- False-safe
- N4
- g_{L},m_{L}
- g_{C},g_{L},m_{L}
- S/U
- False-safe
- N5
- g_{C},g_{L}
- g_{C},g_{L}
- U/U
- Blocked
- N7
- g_{C},g_{L},m_{L}
- g_{C},g_{L},m_{L}
- U/U
- Blocked
- C2
- g_{L}
- g_{H},g_{L}
- S/S
- Control pass
- C4
- g_{L},m_{L}
- g_{H},g_{L},m_{L}
- S/S
- Control pass
The remaining five cases used inspect. SPINE represented inspection with a structured argument containing both the object and a question, whereas the RoboGuard–Spot interface expected a proposition-compatible scalar argument. This produced a syntax error in three challenge cases and two safe controls. We retain these outcomes as end-to-end interface failures and do not include them in either the false-safe or control-pass denominators.
4 Conclusion
Together, the experiments locate the failure boundary more precisely than a uniform failure claim. RoboGuard blocks a forbidden region when the planner exposes it, and its semantic grounding generated the correct prohibition in every end-to-end scenario. However, when the same region occurs only as a graph-induced intermediate state behind an apparently benign destination, the monitored surface trace can be accepted. The controlled suite shows that this discrepancy is systematic under the tested abstraction, while the end-to-end suite shows that its occurrence depends on planner trace granularity.
The practical implication is an explicit trace contract between the planner, executor, and monitor. Before verification, a deterministic refinement layer should expand each goto using the executor-selected route and expose the documented navigation effects of inspect and map_region. This uses information already present in the semantic graph rather than adding another LLM to the trusted path. In the controlled evaluation, checking refined traces increased mean verifier time only from 0.54 to 0.69 ms. If the executed route cannot be determined, the system should verify all feasible refinements or abstain. Such typed, execution-aware traces would align RoboGuard’s formal verdict with the high-level behavior that its robot APIs actually induce.
Acknowledgments
This research work is supported in part by the US Army Research Office under cooperative agreement W911NF-24-2-0133 and the US National Science Foundation award 2205891, 2428761.