SENTINEL: A Multi-Level Formal Framework for Safety Evaluation of LLM-based Embodied Agents

TL;DR

SENTINEL addresses the critical need for formal physical-safety evaluation of LLM-based embodied agents. It introduces a multi-level framework that grounds safety in temporal logic and verifies behavior across semantic interpretation, plan generation, and trajectory execution. The approach formalizes safety as $LTL$/$CTL$ constraints, constructs computation trees from multiple trajectories, and applies model-checking to detect violations and provide counterexamples. Empirical results in VirtualHome and ALFRED reveal safety violations overlooked by prior benchmarks and highlight the benefits of formal grounding, while also exposing challenges in planning under safety constraints and in controller-level execution. This work provides a rigorous, scalable foundation for designing safer embodied AI systems with actionable feedback across stages of decision-making and execution.

Abstract

We present Sentinel, the first framework for formally evaluating the physical safety of Large Language Model(LLM-based) embodied agents across the semantic, plan, and trajectory levels. Unlike prior methods that rely on heuristic rules or subjective LLM judgments, Sentinel grounds practical safety requirements in formal temporal logic (TL) semantics that can precisely specify state invariants, temporal dependencies, and timing constraints. It then employs a multi-level verification pipeline where (i) at the semantic level, intuitive natural language safety requirements are formalized into TL formulas and the LLM agent's understanding of these requirements is probed for alignment with the TL formulas; (ii) at the plan level, high-level action plans and subgoals generated by the LLM agent are verified against the TL formulas to detect unsafe plans before execution; and (iii) at the trajectory level, multiple execution trajectories are merged into a computation tree and efficiently verified against physically-detailed TL specifications for a final safety check. We apply Sentinel in VirtualHome and ALFRED, and formally evaluate multiple LLM-based embodied agents against diverse safety requirements. Our experiments show that by grounding physical safety in temporal logic and applying verification methods across multiple levels, Sentinel provides a rigorous foundation for systematically evaluating LLM-based embodied agents in physical environments, exposing safety violations overlooked by previous methods and offering insights into their failure modes.

Figures (15)

• Figure 1: Multi-level, progressive formal safety evaluation pipeline of SENTINEL. The process begins with semantic-level evaluation, where intuitive natural language safety requirements are interpreted into formal safety semantics. These interpretations then guide plan-level generation of high-level action plans by LLM agents, which are verified through LTL checking. Finally, at the trajectory-level, physical execution trajectories are generated based on the action plans and simulated, and verified through CTL checking. At every level, evaluation is automated and grounded in temporal-logic–based safety semantics. Further details are in \ref{['fig:example_subgoal', 'fig:trajectory_safety_pipeline']}, and \ref{['sec:sentinel_framework']}.
• Figure 2: Pipeline overview of Semantic-level safety checking and downstream plan generation. We ground natural language safety constraints into an LTL semantics, applying it to high-level plan generation for \ref{['example::ltl_def_simplified']} with extensive constraints. Red highlights indicate the impact of enforcing safety constraints during plan generation.
• Figure 3: An illustrative walkthrough of trajectory safety evaluation of \ref{['example::ltl_def_simplified']} using our framework. With given subgoals, the agent generates candidate action sequences in top left which are executed in the simulator with low-level controllers/planners to produce state transitions. These trajectories are organized into a trajectories tree with multiple branches. CTL-based evaluation pipeline is then applied to the computation tree to verify whether safety constraints are violated across all paths. In this example, all branch violates safety constraints: one violates oven nearby paper in \ref{['example::ltl_def_simplified']} and the other violates the knife-holding constraint listed in \ref{['example::ltl_def']}, and the violation is flagged with a counterexample path.
• Figure 4: Correlation analysis between semantic safety interpretation and plan-level safety.
• Figure 5: Some examples of detailed physical safety violations, which can only be evaluated at trajectory level. Demo videos can be found in Supp. Material and detailed analysis is in \ref{['subsec:case_studies']}.

Theorems & Definitions (6)

• Remark 2.1
• Example 2.2
• Example 2.3
• Remark 2.4
• Remark 2.5
• Example B.1