Source-linked AI summary
Mind the Refinement Gap: When Safe High-Level Robot Plans Produce Unsafe Executions
Stabak Das, Priyesh Ranjan, Xiangfang Li, Lijun Qian
TL;DR
Language-enabled robot systems combine semantic-graph planning with temporal-logic monitors, but a high-level action trace may omit navigation or implicit effects induced during execution. This paper compares RoboGuard’s verdicts on surface plans and graph-refined traces under the same LTL specification; all 12 targeted controlled cases show the predicted discrepancy, while all 16 controls behave as expected.
Problem
It is unclear whether a safety verdict on a high-level action trace remains valid when graph-induced navigation and documented implicit action effects are made explicit.
Source: §1 · p. 1Method
The audit compares RoboGuard’s verdicts on surface plans and graph-refined traces under the same LTL specification, using controlled and end-to-end evaluations.
Source: §1 · p. 2Results
All 12 targeted controlled cases showed the predicted surface-versus-refined discrepancy, while all 16 controls behaved as expected.
Source: §3 · p. 4Takeaways & Limitations
The controlled suite shows the discrepancy is systematic under the tested abstraction, while end-to-end occurrence depends on planner trace granularity.
Source: §4 · p. 4The experiments use static semantic graphs and graph-derived traces, not continuous dynamics, perception errors, collision avoidance, or physical execution.
Source: §1 · p. 2
Abstract
from arXiv · showhide
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 [1] 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.
1 Introduction
The introduction asks whether a monitor’s verdict on a high-level action trace remains valid when graph-induced navigation and implicit action effects are made explicit. It proposes comparing surface and graph-refined traces under the same LTL specification, while distinguishing action-abstraction discrepancies from other system failures.
1 Introduction
- A monitor can miss an unsafe route when navigation is represented only by its destination or hidden inside a higher-level action.A surface plan may list only goto(safe lab 1), while graph execution passes through goto(construction area 1), violating the prohibition.Source: §1 · p. 1
- The central question is whether a verdict on a high-level trace remains valid after graph-induced navigation and documented implicit effects are made explicit.The comparison holds the LTL specification fixed, separating trace mismatch from LTL-generation or scene-grounding errors.Source: §1 · pp. 1–2
- The evaluation pairs 28 controlled fixed-plan cases with 14 end-to-end cases using natural-language tasks, semantic graphs, and RoboGuard safety rules.The controlled cases cover negative examples and controls; the end-to-end protocol records planning, contextual grounding, verification, graph-oracle, and interface failures separately.Source: §1 · p. 2
- The proposed diagnostic compares surface and graph-refined traces under the same LTL rule, while graph-based refinement exposes safety-relevant events already encoded in the semantic graph.The study treats action-abstraction failures separately from specification-generation failures.Source: §1 · p. 2
- The experiments use static semantic graphs and graph-derived traces, not continuous dynamics, perception errors, collision avoidance, or physical execution.The claims concern action-level monitoring relative to documented high-level execution semantics, not complete real-world robot safety.Source: §1 · p. 2
2 Related Work
Related work combines language-enabled planning with structured world models and formal safety methods. This paper focuses on whether intermediate navigation events represented in semantic graphs remain visible to downstream verification.
2 Related Work
- SayPlan combines hierarchical 3D scene graphs, classical path planning, and simulator feedback, while SPINE plans navigation, inspection, and mapping over an incrementally updated semantic graph [3] [1].The study asks whether safety-relevant navigation events in these graphs remain visible to downstream verification.Source: §2 · p. 3
- Related safety approaches combine language models with symbolic planning or task-and-motion reasoning [4] [5], encode prohibitions as LTL constraints [6], or verify generated robot programs [7].Runtime-assurance systems such as SOTER rely on observable system states to detect hazards and activate verified fallbacks [8].Source: §2 · p. 3
- This study examines whether high-level action traces omit intermediate navigation or implicit action effects already recoverable from the semantic graph.Its focus is the abstraction boundary between planning and verification.Source: §2 · p. 3
3 Experimental Results
The controlled audit found the predicted surface-versus-refined discrepancy in every targeted case, while controls behaved as expected. End-to-end outcomes depended on whether SPINE exposed unsafe intermediate regions in its plan; inspect cases also revealed interface failures.
Protocol and test scenarios
- The controlled audit used fixed plans and manually specified LTL across five action-abstraction families; the end-to-end audit covered 14 cases across four graph scenarios.False-safe results required surface acceptance, oracle-identified forbidden entry, and rejection of the refined trace under the same specification; checker errors were reported separately.Source: §3 · p. 3
Controlled audit
- All 12 targeted cases showed the predicted discrepancy, while all 16 controls behaved correctly; there were no checker errors or mismatches with surface predictions.The outcomes distinguish false-safe abstraction cases, correctly blocked unsafe challenges, control passes, and checker errors.Source: Table 1 · p. 3, §3 · pp. 3–4
End-to-end audit
- In N2 and N4, graph refinement exposed forbidden-region traversal hidden by benign destinations; in N5 and N7, plans exposed the region directly and were rejected.Matched safe controls C2 and C4 remained safe after refinement; Table 2 reports representative surface/refined traces.Source: Table 2 · p. 4, §3 · p. 4
- SPINE produced task-attempting plans in all 14 cases, and RoboGuard grounded the intended G(!goto(C)) prohibition for all four graphs.The audit used static semantic graphs, one trial per case, and cross-checked realized routes against an independent BFS oracle.Source: §3 · pp. 3–4
- Five inspect cases produced interface syntax errors because structured object-and-question arguments did not match the scalar arguments expected by the RoboGuard–Spot interface.Three challenge cases and two safe controls were retained as interface failures, outside the safety-outcome denominators.Source: §3 · p. 4
4 Conclusion
The experiments locate false-safe outcomes at hidden graph-induced intermediate states, rather than showing uniform monitor failure. The conclusion proposes execution-aware trace refinement, with verification of feasible refinements or abstention when the route is unknown.
4 Conclusion
- RoboGuard blocks forbidden regions when the planner exposes them, but may accept a surface trace when a forbidden intermediate state is hidden behind a benign destination.The controlled discrepancy was systematic under the tested abstraction, while its end-to-end occurrence depended on planner trace granularity.Source: §4 · p. 4
- 0.54 to 0.69 ms was the increase in mean verifier time when checking refined traces in the controlled evaluation.The proposed refinement expands goto actions using the executor-selected route and exposes documented navigation effects of inspect and map region.Source: §4 · p. 4
- When the executed route cannot be determined, the proposed system should verify all feasible refinements or abstain.The refinement layer uses information already present in the semantic graph rather than adding another LLM to the trusted path.Source: §4 · p. 4