高レベルロボット計画の安全判定が実行時不安全を見落とすrefinement gap、RoboGuardとSPINEで監査
本プレプリントは、ロボットの高レベル行動計画を検証する安全モニタが、グラフ上の経路や暗黙の行動効果を確認しないまま安全と判定するrefinement gapを監査した。制御された28ケース中12ケースで表面計画は安全、グラフ精緻化後は不安全となり、エンドツーエンド14ケースでもSPINEが目的地のみを提示した2ケースで同じ見落としを確認した。グラフ由来の実行トレースを検証前に展開する軽量な緩和策を提案し、形式検証と実APIのずれを診断する材料を提供する。
高レベル行動系列に対するRoboGuardの安全判定は、グラフ誘導のナビゲーションや文書化された暗黙の行動効果を明示した後も有効かという問い。
言語対応ロボットは意味グラフ計画と時相論理安全モニタを組み合わせるが、モニタが観測する行動トレースが実行時の経路や暗黙効果を含むという完全性を前提にしている。goto(safe_lab_1)のように目的地だけが提示され、実際にはgoto(construction_area_1)を経由する場合、禁止領域への侵入が表面トレースで検出されず不安全な実行が生じる。既存システムは検証対象の抽象化がロボットAPIの誘導する挙動と一致しないため失敗する。
従来のRoboGuardは保護された言語モデルで安全規則を意味グラフに接地し、LTL仕様を生成してロボットAPI行動列を検証する。しかし検証はリスト化された行動ごとにオートマトンを進め、未観測の命題は偽と扱うため、グラフ探索が生む中間的なgoto命題やinspect、map_regionの暗黙のナビゲーションが監視対象に含まれない。
本研究は新システムではなく、同一のLTL仕様を固定したまま表面計画とグラフ精緻化トレースを比較する監査手法を導入した。決定論的最短経路オラクルがgotoを実経路で展開し、inspectとmap_regionの文書化されたナビゲーション効果も明示する。このグラフベースのトレース精緻化は既存の意味グラフ情報を使うため、新たなLLMを信頼経路に追加しない。
制御監査では28ケース中12ケースがfalse-safe、14ケースが安全な対照として合格、2ケースが明示的不安全として正しく阻止され、エラーは0。12ケースすべてで予測どおり表面トレースは受理、グラフ精緻化トレースはconstruction_area_1への侵入を理由に拒否された。内訳は隠れ経由地位置3件、経路選択2件、行動精緻化4件、複数行動計画3件。goto7件、inspect3件、map_region2件。検証時間は平均0.54 msから0.69 msに増加した。エンドツーエンド14ケースではSPINEが全ケースで計画を生成し、RoboGuardの接地も4グラフすべてで成功し、全ケースでG(!goto(C))を生成した。固有の工事橋シナリオ5件中2件でfalse-safe、1件対照合格、2件インタフェースエラー。N2とN4ではSPINEが目的地Lのみを提示、精緻化でgC,gLが現れ不安全。N5とN7はCが表面に出て阻止。安全対照C2とC4は精緻化後も安全。inspectの5件は構造化引数とスカラー引数の不一致で構文エラーとなり、安全判定の分母から除外。
著者は静的な意味グラフとグラフ由来トレースのみを扱い、連続ロボット動力学、知覚誤差、衝突回避、物理実行をモデル化していないと述べる。エンドツーエンドは各ケース1試行で合計14件と小規模であり、inspectのインタフェース不整合が5件発生した。実機実験はなく、検証の健全性は文書化された高レベル実行意味論に対する相対的な主張に限定される。コード公開については論文で報告されていない。
自律移動ロボットや点検ドローンを開発する企業は、計画器と形式検証の間に実行トレース契約を設け、検証前に意味グラフから経路を展開する層を追加できる。既存のグラフ情報を使うため追加LLM不要で、計算コストも検証のみで0.15 ms増に留まる。実行経路が確定できない場合は全実行可能な精緻化を検証するか棄権する契約を満たす必要がある。現在のオフライン計画検証から1〜3年で物理AIシステムのランタイム保証に組み込むには、実機動力学や知覚を含む検証に拡張する必要がある。
論文全文
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.