Mind the Refinement Gap: RoboGuard übersieht unsichere Ausführungsrouten
Der Preprint untersucht, ob Sicherheitsurteile von RoboGuard über High-Level-Aktionsspuren gültig bleiben, wenn graph-induzierte Navigation und implizite Aktionseffekte explizit gemacht werden. In 28 kontrollierten Fällen akzeptierte RoboGuard alle 12 gezielten Abstraktionsfälle, obwohl die verfeinerte Spur einen verbotenen Bereich durchquerte, während alle 16 Kontrollen korrekt waren. Die Ergebnisse zeigen, dass eine deterministische Spurverfeinerung aus dem semantischen Graphen nötig ist, um false-safe Sicherheitsurteile zu vermeiden.
Bleibt ein Sicherheitsurteil über eine High-Level-Aktionsspur gültig, wenn die durch den semantischen Graphen induzierte Navigation und dokumentierte implizite Aktionseffekte explizit gemacht werden?
Sprachgesteuerte Robotersysteme stellen Aktionen wie goto(safe_lab_1) oft nur durch ihren Zielort dar und verbergen Zwischenregionen oder implizite Navigationseffekte. Ein Sicherheitsmonitor wie RoboGuard prüft diese Oberflächenspur gegen LTL-Spezifikationen, aber die tatsächliche Graph-Suche kann durch einen verbotenen Bereich führen. Dadurch ist das Monitor-Urteil nur relativ zur beobachteten Abstraktion gültig; der Abgleich zwischen verifizierter Spur und ausgeführtem Verhalten fehlt.
Bisherige Ansätze wie RoboGuard erden Sicherheitsregeln in semantischen Graphen, erzeugen LTL-Spezifikationen und setzen temporallogische Synthese auf vorgeschlagene Roboter-API-Aktionen ein. SPINE plant Navigation, Inspektion und Kartierung, gibt aber häufig nur Zielorte aus. Diese Systeme prüfen nicht, ob die dem Monitor übergebene Spur alle graph-induzierten Zwischenschritte und dokumentierten Aktionsfolgen enthält. Andere formale Systeme wie AutoTAMP, LIMP oder Safety Chip verlassen sich ebenfalls auf beobachtbare Zustände, ohne die Abstraktionsgrenze zwischen Planung und Verifikation systematisch zu adressieren.
Die Autoren führen ein kontrolliertes Audit ein, das dieselbe LTL-Spezifikation auf Oberflächen- und graph-verfeinerte Spuren anwendet, um Abstraktionsfehler von Spezifikationsfehlern zu trennen. Ein deterministischer ungewichteter Kürzeste-Pfade-Orakel expandiert jeden Plan; dabei werden Zwischenknoten aus dem semantischen Graphen sowie dokumentierte Navigationseffekte von inspect und map_region sichtbar gemacht. Als minimales Mitigationsverfahren wird eine deterministische Verfeinerungsschicht vor der Verifikation vorgeschlagen, die bereits im Graphen vorhandene Informationen nutzt, ohne ein weiteres Sprachmodell in den vertrauenswürdigen Pfad aufzunehmen.
Im kontrollierten Audit mit 28 Fällen erzeugten alle 12 gezielten Abstraktionsfälle die vorhergesagte Diskrepanz: die Oberflächenspur wurde akzeptiert, die verfeinerte Spur abgelehnt. Dies galt für versteckte Wegpunkte (3/3), Routenwahl (2/2), Aktionsverfeinerung (4/4) und Multi-Aktions-Pläne (3/3), über goto (7), inspect (3) und map_region (2). Alle 16 Kontrollen verhielten sich korrekt (14 sichere akzeptiert, 2 unsichere abgelehnt). Die mittlere Verifikationszeit stieg von 0,54 ms auf 0,69 ms. Im End-to-End-Audit mit SPINE und RoboGuard über 14 Fälle und vier Szenarien erzeugte SPINE in allen Fällen einen Plan, und RoboGuard erzeugte in allen vier Graphen die Spezifikation G(!goto(C)). Zwei Fälle (N2, N4) waren false-safe, zwei (N5, N7) wurden korrekt blockiert, fünf Fälle führten zu einem Kontroll-Pass, und fünf Fälle mit inspect verursachten Syntaxfehler durch nicht skalare Argumente. Die kontrollierten und End-to-End-Ergebnisse zeigen, dass die Diskrepanz systematisch von der Granularität der Planerspur abhängt.
Die Experimente arbeiten ausschließlich über statischen semantischen Graphen und offline erzeugten Spuren; kontinuierliche Roboterdynamik, Wahrnehmungsfehler, Kollisionsvermeidung und physische Ausführung werden nicht modelliert. Die Zahl der End-to-End-Fälle ist mit 14 relativ gering, und die Audit-Ergebnisse gelten nur für die unveränderten Versionen von RoboGuard (Commit e487f83) und SPINE (Commit e776a8a) sowie für die gewählten deterministischen Orakel. Die fünf Interface-Fehler bei inspect zeigen, dass die Schnittstellen zwischen Planer und Monitor noch nicht robust sind. Im Paper nicht berichtet: Veröffentlichung von Code oder Daten sowie Tests auf realer Hardware.
Unternehmen, die sprachgesteuerte Robotik mit formalen Sicherheitsmonitoren entwickeln, können die vorgeschlagene deterministische Spurverfeinerung kurzfristig (1 bis 3 Jahre) in ihre Verifikationspipelines integrieren, sofern der ausführende Router die gewählte Route meldet. Für den Einsatz in sicherheitskritischen Umgebungen mit dynamischen Graphen und Echtzeit-Wahrnehmung sind zusätzliche Arbeiten zu kontinuierlicher Dynamik und Fehlerbehandlung nötig (mehr als 3 Jahre). Voraussetzung ist ein expliziter Trace-Vertrag zwischen Planer, Executor und Monitor; ohne diesen bleibt die formale Garantie unvollständig.
Vollständige Studie
Mind the Refinement Gap: When Safe High-Level Robot Plans Produce Unsafe Executions
Veröffentlicht unter CC BY 4.0. Wiedergabe mit Namensnennung, Original unter 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.