Mind the Refinement Gap: When Safe High-Level Robot Plans Produce Unsafe Executions

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.

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 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.

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.

References

1. [1] Y. Chen, J. Arkin, C. Dawson, Y. Zhang, N. Roy, and C. Fan (2024) AutoTAMP: autoregressive task and motion planning with LLMs as translators and checkers. In IEEE International Conference on Robotics and Automation,
2. [2] A. Desai, S. Ghosh, S. A. Seshia, N. Shankar, and A. Tiwari (2019) SOTER: a runtime assurance framework for programming safe robotics systems. In 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, pp. 138–150. External Links: Document
3. [3] B. Quartey, E. Rosen, S. Tellex, and G. Konidaris (2025) Verifiably following complex robot instructions with foundation models. In IEEE International Conference on Robotics and Automation,
4. [4] K. Rana, J. Haviland, S. Garg, J. Abou-Chakra, I. Reid, and N. Sünderhauf (2023) SayPlan: grounding large language models using 3d scene graphs for scalable robot task planning. In Proceedings of the 7th Conference on Robot Learning, Proceedings of Machine Learning Research, Vol. 229, pp. 23–72.
5. [5] Z. Ravichandran, V. Murali, M. Tzes, G. J. Pappas, and V. Kumar (2025) SPINE: online semantic planning for missions with incomplete natural language specifications in unstructured environments. In IEEE International Conference on Robotics and Automation,
6. [6] Z. Ravichandran, A. Robey, V. Kumar, G. J. Pappas, and H. Hassani (2026) Safety guardrails for LLM-enabled robots. IEEE Robotics and Automation Letters. External Links: Document
7. [7] Y. Yang, N. P. Bhatt, W. Ward, Z. Hu, J. Biswas, and U. Topcu (2024) Joint verification and refinement of language models for safety-constrained planning. arXiv preprint arXiv:2410.14865.
8. [8] Z. Yang, S. S. Raman, A. Shah, and S. Tellex (2024) Plug in the safety chip: enforcing constraints for LLM-driven robot agents. In IEEE International Conference on Robotics and Automation, pp. 14062–14069. External Links: Document