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

• URL: http://arxiv.org/abs/2510.12985v1
• Date: Tue, 14 Oct 2025 20:53:51 GMT
• Title: SENTINEL: A Multi-Level Formal Framework for Safety Evaluation of LLM-based Embodied Agents
• Authors: Simon Sinong Zhan, Yao Liu, Philip Wang, Zinan Wang, Qineng Wang, Zhian Ruan, Xiangyu Shi, Xinyu Cao, Frank Yang, Kangrui Wang, Huajie Shao, Manling Li, Qi Zhu,
• Abstract summary: We present Sentinel, the first framework for formally evaluating the physical safety of Large Language Model(LLM)-based embodied agents.<n>We apply Sentinel in VirtualHome and ALFRED, and formally evaluate multiple LLM-based embodied agents against diverse safety requirements.
• Score: 25.567593463613388
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Evaluating Implicit Regulatory Compliance in LLM Tool Invocation via Logic-Guided Synthesis [18.51135049856393]
  We introduce LogiSafetyGen, a framework that converts unstructured regulations into Linear Temporal Logic oracles and employs logic-guided fuzzing to synthesize valid, safety-critical traces.<n>Building on this framework, we construct LogiSafetyBench, a benchmark comprising 240 human-verified tasks that require LLMs to generate Python programs that satisfy both functional objectives and latent compliance rules.<n> Evaluations of 13 state-of-the-art (SOTA) LLMs reveal that larger models, despite achieving better functional correctness, frequently prioritize task completion over safety, which results in non-compliant behavior.
  arXiv  Detail & Related papers  (2026-01-13T03:55:18Z)
• Bridging Natural Language and Formal Specification--Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs [10.958536923155101]
  Req2LTL is a modular framework that bridges NL and Linear Temporal Logic.<n>It achieves 88.4% semantic accuracy and 100% syntactic correctness on real-world aerospace requirements.
  arXiv  Detail & Related papers  (2025-12-19T08:25:54Z)
• Taxonomy-Adaptive Moderation Model with Robust Guardrails for Large Language Models [3.710103086278309]
  Large Language Models (LLMs) are typically aligned for safety during the post-training phase.<n>They may still generate inappropriate outputs that could potentially pose risks to users.<n>This challenge underscores the need for robust safeguards that operate across both model inputs and outputs.
  arXiv  Detail & Related papers  (2025-12-05T00:43:55Z)
• Reasoning with Confidence: Efficient Verification of LLM Reasoning Steps via Uncertainty Heads [104.9566359759396]
  We propose a lightweight alternative for step-level reasoning verification based on data-driven uncertainty scores.<n>Our findings suggest that the internal states of LLMs encode their uncertainty and can serve as reliable signals for reasoning verification.
  arXiv  Detail & Related papers  (2025-11-09T03:38:29Z)
• Visual Backdoor Attacks on MLLM Embodied Decision Making via Contrastive Trigger Learning [89.1856483797116]
  We introduce BEAT, the first framework to inject visual backdoors into MLLM-based embodied agents.<n>Unlike textual triggers, object triggers exhibit wide variation across viewpoints and lighting, making them difficult to implant reliably.<n>BEAT achieves attack success rates up to 80%, while maintaining strong benign task performance.
  arXiv  Detail & Related papers  (2025-10-31T16:50:49Z)
• TypePilot: Leveraging the Scala Type System for Secure LLM-generated Code [46.747768845221735]
  Large language Models (LLMs) have shown remarkable proficiency in code generation tasks across various programming languages.<n>Their outputs often contain subtle but critical vulnerabilities, posing significant risks when deployed in security-sensitive or mission-critical systems.<n>This paper introduces TypePilot, an agentic AI framework designed to enhance the security and robustness of LLM-generated code.
  arXiv  Detail & Related papers  (2025-10-13T08:44:01Z)
• Towards Reliable and Practical LLM Security Evaluations via Bayesian Modelling [1.0266286487433585]
  It is critical to understand vulnerabilities accurately before adopting a new large language model (LLM) architecture.<n>Existing evaluations can be difficult to trust, often drawing conclusions from LLMs that are not meaningfully comparable.<n>We propose a principled and practical end-to-end framework for evaluating LLM vulnerabilities to prompt injection attacks.
  arXiv  Detail & Related papers  (2025-10-07T09:22:22Z)
• Evaluating LLM Generated Detection Rules in Cybersecurity [0.3469154896502103]
  The benchmark employs a holdout set-based methodology to measure the effectiveness of LLM-generated security rules.<n>It provides three key metrics inspired by the way experts evaluate security rules.<n>This methodology is illustrated using rules from Sublime Security's detection team and those written by Sublime Security's Automated Detection Engineer.
  arXiv  Detail & Related papers  (2025-09-20T17:21:51Z)
• AgentAuditor: Human-Level Safety and Security Evaluation for LLM Agents [41.000042817113645]
  sys is a universal, training-free, memory-augmented reasoning framework.<n>sys constructs an experiential memory by having an LLM adaptively extract structured semantic features.<n>data is the first benchmark designed to check how well LLM-based evaluators can spot both safety risks and security threats.
  arXiv  Detail & Related papers  (2025-05-31T17:10:23Z)
• Subtle Risks, Critical Failures: A Framework for Diagnosing Physical Safety of LLMs for Embodied Decision Making [31.555271917529872]
  We introduce SAFEL, the framework for systematically evaluating the physical safety of large language models (LLMs) in embodied decision making.<n>We introduce EMBODYGUARD, a PDDL-grounded benchmark containing 942 LLM-generated scenarios covering both overtly malicious and contextually hazardous instructions.<n>Our results highlight critical limitations in current LLMs and provide a foundation for more targeted, modular improvements in safe embodied reasoning.
  arXiv  Detail & Related papers  (2025-05-26T13:01:14Z)
• Fundamental Safety-Capability Trade-offs in Fine-tuning Large Language Models [92.38300626647342]
  Fine-tuning Large Language Models (LLMs) on some task-specific datasets has been a primary use of LLMs.<n>This paper presents a theoretical framework for understanding the interplay between safety and capability in two primary safety-aware LLM fine-tuning strategies.
  arXiv  Detail & Related papers  (2025-03-24T20:41:57Z)
• Embodied Agent Interface: Benchmarking LLMs for Embodied Decision Making [85.24399869971236]
  We aim to evaluate Large Language Models (LLMs) for embodied decision making.<n>Existing evaluations tend to rely solely on a final success rate.<n>We propose a generalized interface (Embodied Agent Interface) that supports the formalization of various types of tasks.
  arXiv  Detail & Related papers  (2024-10-09T17:59:00Z)
• SCANS: Mitigating the Exaggerated Safety for LLMs via Safety-Conscious Activation Steering [56.92068213969036]
  Safety alignment is indispensable for Large Language Models (LLMs) to defend threats from malicious instructions.<n>Recent researches reveal safety-aligned LLMs prone to reject benign queries due to the exaggerated safety issue.<n>We propose a Safety-Conscious Activation Steering (SCANS) method to mitigate the exaggerated safety concerns.
  arXiv  Detail & Related papers  (2024-08-21T10:01:34Z)
• DECIDER: A Dual-System Rule-Controllable Decoding Framework for Language Generation [57.07295906718989]
  Constrained decoding approaches aim to control the meaning or style of text generated by pre-trained large language (Ms also PLMs) for various tasks at inference time.<n>These methods often guide plausible continuations by greedily and explicitly selecting targets.<n>Inspired by cognitive dual-process theory, we propose a novel decoding framework DECIDER.
  arXiv  Detail & Related papers  (2024-03-04T11:49:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.