Technical Summary: SENTINEL

Problem Statement

The integration of Foundation Models (FMs) into embodied agents has expanded capabilities in planning and human-robot interaction but has simultaneously magnified safety risks. Existing evaluation benchmarks for FM-based agents primarily focus on task completion metrics (e.g., success rates) and often treat physical hazards merely as task failures rather than distinct safety violations. Current safety evaluation methods rely heavily on heuristic rules or subjective FM-based judges (LLM-as-Judge), which lack rigorous definitions and fail to distinguish between failures occurring at different stages of the agent pipeline: semantic misunderstanding, unsafe plan generation, or unsafe physical execution. Furthermore, these methods often cannot localize the specific level at which a safety violation originates.

Methodology

The authors propose SENTINEL (Safety EvaluatioN framework with Temporal logics for INterpretable Embodied foundation modeL-based agents), a multi-level formal framework that grounds physical safety in temporal logic specifications. The framework operates within simulation environments (VirtualHome and AI2-THOR) and evaluates agents across three progressive levels:

1. Formal Safety Specification

SENTINEL encodes natural language safety constraints into Temporal Logic formulas, specifically Linear Temporal Logic (LTL) and Computation Tree Logic (CTL).

• State Invariants: Constraints forbidding unsafe states at all times (e.g., $G(\neg p)$ for collision avoidance).
• Ordering Constraints: Constraints enforcing proper action sequencing (e.g., $G(p \to F q)$ for "eventually turn off").
• Classification: Safety rules are categorized into state invariants and ordering constraints, mapped to atomic propositions derived from object properties in the simulation.

2. Multi-Level Evaluation Pipeline

The framework employs a three-stage pipeline to progressively filter failures and localize violations:

• Semantic-Level Evaluation:

  • Goal: Assess the FM's ability to translate natural language safety requirements into formal LTL formulas.
  • Method: The agent is prompted with safety constraints and generates candidate LTL formulas. These are compared against ground-truth LTL specifications using syntactic checks and semantic equivalence verification (via Büchi automata and language containment).
  • Output: Metrics on syntax errors, semantic non-equivalence, and successful interpretation.

• Plan-Level Evaluation:

  • Goal: Verify high-level action plans and subgoals against the LTL constraints before execution.
  • Method: The agent generates a high-level plan (milestone subgoals). This plan is checked against the LTL formulas to detect unsafe symbolic orderings or missing preconditions. A Breadth-First Search (BFS) is used to validate the executability of the plan within the action space.
  • Output: Identification of unsafe plans that satisfy task goals but violate safety constraints.

• Trajectory-Level Evaluation:

  • Goal: Evaluate the physical execution of plans, accounting for branching outcomes and environment dynamics.
  • Method: Multiple execution trajectories are sampled from the simulator based on the high-level plan. These trajectories are merged into a Computation Tree ($T$). Safety requirements are lifted from LTL to CTL to evaluate branching-time properties.
  • Verification: A CTL model checker verifies properties (e.g., $AG \phi$ for "all paths always satisfy $\phi$") against the tree.
  • Output: Detection of execution-dependent violations and generation of counterexample paths (specific states or sequences causing failure).

3. Feedback-Driven Refinement

SENTINEL utilizes the counterexamples generated during trajectory-level checking to provide verifiable feedback to the agent. This feedback loop allows the agent to refine its plans iteratively, aiming to improve safety without modifying the underlying agent architecture.

Key Contributions

1. Formal and Interpretable Safety Specifications: The work grounds intuitive safety requirements in LTL and CTL, enabling explicit categorization (state invariants, temporal dependencies) and formal verification rather than heuristic judgment.
2. Unified Multi-Level Formal Safety Evaluation: SENTINEL is the first framework to formally evaluate safety progressively across semantic interpretation, plan generation, and physical execution. This design allows for the localization of failures to specific stages (comprehension vs. reasoning vs. execution).
3. Cross-Level Empirical Analysis: The authors apply SENTINEL to VirtualHome and AI2-THOR, extending tasks with safety-focused requirements. They demonstrate that safety violations often stem from different levels (e.g., semantic misinterpretation vs. low-level controller errors) and that formal evaluation exposes failure modes invisible to task-success-only benchmarks.

Experimental Results

The authors evaluated multiple Closed-Source (GPT-5, Claude-Opus, Gemini) and Open-Source (DeepSeek, Qwen, Mistral, Llama) LLMs, as well as Vision-Language Models (VLMs).

• Semantic-Level: Larger models demonstrated significantly higher performance in translating natural language to LTL compared to smaller open-source models. However, even strong models struggled with conditional prohibitions compared to global prohibitions.
• Plan-Level: Models with higher semantic equivalence rates generally maintained higher safety rates at the plan level. However, adding explicit safety guidance (LTL prompts) improved safety metrics but did not eliminate all violations.
• Trajectory-Level:
  • LLMs vs. VLMs: VLM-based agents generally achieved higher safety rates than text-only LLMs, likely due to visual grounding helping detect physical hazards. However, VLMs often exhibited lower task success rates, indicating a safety-capability trade-off.
  • Execution Failures: A significant drop in "Success & Safety" was observed from plan-level to trajectory-level results, suggesting that many failures originate from low-level action arguments and the lack of safety mechanisms in controllers.
• Safety Improvement: In a refinement loop experiment, SENTINEL's verifiable counterexample feedback led to significantly greater improvements in safety metrics (approx. double the improvement of an LLM-as-Judge baseline) while maintaining comparable task success gains. Analysis showed that LLM-as-Judge baselines often missed truly unsafe trajectories (83% miss rate in one study), whereas SENTINEL's formal checks were more reliable.
• Efficiency: CTL-based verification over a merged computation tree was found to be more efficient than independent LTL checking, with speedups increasing as the number of trajectories grew.

Significance and Claims

The paper claims that SENTINEL provides a rigorous foundation for systematically evaluating the safety of FM-based embodied agents. By moving beyond heuristic or subjective judgments, the framework offers:

• Localization: The ability to pinpoint whether a safety failure stems from misunderstanding instructions, generating unsafe plans, or executing actions unsafely.
• Actionable Feedback: The generation of verifiable counterexamples that can drive meaningful safety improvements through refinement loops.
• Scalability: The use of CTL over sampled computation trees offers a practical trade-off, providing scalable empirical detection of violations without the infeasibility of full-state model checking in complex physical environments.

The authors emphasize that SENTINEL offers empirical detection rather than certified verification, as it operates on a finite computation tree assembled from sampled trajectories. They acknowledge that missed violations remain possible if the sample count is insufficient, but argue that this approach is closer to statistical model checking and is necessary given the black-box nature of FMs and the complexity of physical environments. The framework is presented as a step toward verifiable safety benchmarks and safety-aware reinforcement learning rewards.