SENTINEL: A Multi-Level Formal Framework for Safety Evaluation of Foundation Model-based Embodied Agents
Simon Sinong Zhan, Philip Wang, Yao Liu, Yiyan Peng, Zinan Wang, Qineng Wang, Zhian Ruan, Xiangyu Shi, Xinyu Cao, Frank Yang, Zhenyang Ni, Kangrui Wang, Ruohan Zhang, Huajie Shao, Manling Li, Qi Zhu
Why It Matters
What makes this one worth your time
As AI systems increasingly operate in physical environments, ensuring their safety through formal methods is crucial for real-world applications and public trust.
SENTINEL offers a rigorous multi-level framework for ensuring the safety of embodied agents.
Summary
The paper introduces SENTINEL, a formal framework for evaluating the safety of foundation model-based embodied agents through a multi-level verification process that includes semantic interpretation, plan generation, and physical execution.
Key contributions
- Development of a multi-level safety evaluation framework for FM-based embodied agents.
- Formalization of safety requirements using temporal logic for improved clarity and precision.
- Implementation and evaluation of SENTINEL in simulation environments, demonstrating its effectiveness in identifying safety violations.
Notable insights
- The use of temporal logic to ground safety requirements provides a precise and formal basis for evaluating agent behavior.
- The multi-level verification pipeline allows for early detection of safety violations, potentially reducing risks before execution.
Possible limitations
- Not stated in the abstract.
Abstract
arXiv:2510.12985v3 Announce Type: replace Abstract: We present SENTINEL, a framework for formally evaluating the physical safety of foundation model (FM)-based embodied agents. SENTINEL is the first to provide multi-level safety evaluation across semantic interpretation, plan generation, and physical execution within a unified formal framework. Unlike prior methods that rely on heuristic rules or subjective FM judgments, SENTINEL grounds practical safety requirements in formal temporal logic (TL) semantics that can precisely specify state invariants, temporal dependencies, and timing constraints. It employs a multi-level verification pipeline where (i) at the semantic level, intuitive natural language safety requirements are formalized into TL formulas and the 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 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 AI2-THOR, and formally evaluate multiple FM-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 the safety of FM-based embodied agents in simulation-based physical environments, and can effectively expose potential safety violations in interpreting, planning, and executing the tasks.