🤖 AI

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

SENTINEL 是一个新颖的多层形式化框架，通过在语义、规划和轨迹层面，系统地验证针对形式化时序逻辑规范的语义理解、规划与执行，从而确保基于基础模型的具身智能体的物理安全性。

原作者： 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

发布于 2026-07-22

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： 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

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在教一个全新的机器人帮你在家里干活。你希望它能给你做个三明治、整理房间，或者只是递给你一杯水。这就是“具身智能体”（embodied agents）的精彩世界——这些机器人能够观察、思考并在现实（或虚拟）世界中移动。为了让这些机器人足够聪明，能够理解你那些凌乱的指令，科学家们正赋予它们“基础模型”（foundation models），这就像是拥有了巨大的、超级聪明的脑子，并接受了几乎人类写过的所有内容的训练。但问题在于，仅仅有聪明并不意味着安全。一个超智能的机器人可能会找到为你拿饮料最快的方法，但如果它没意识到把水倒在笔记本电脑旁边是个坏主意，它可能会导致电路短路。科学家们提出的核心问题是：我们如何确保这些聪明的机器人不会在试图提供帮助时，不小心烧掉房子或弄坏我们的东西？

这正是名为 SENTINEL 的新框架大显身手的地方。把 SENTINEL 想象成一个非常严格、逻辑极其严密的机器人大脑安全检查员。它不是简单地问机器人：“你觉得这安全吗？”（这就像问一个小孩觉得从屋顶跳下去是否安全一样——他们可能会说可以，因为他们不理解重力），SENTINEL 使用了一种特殊的“数学语言”，叫做“时序逻辑”（temporal logic）。这种语言就像一套不可打破的规则，精确地描述了什么必须发生，什么绝不能发生，以及发生的先后顺序。例如，与其说“小心火源”，SENTINEL 会写下一条规则，规定：“如果炉灶开着，那么纸张绝不能出现在距离它一米以内的范围内。”

研究人员建立了一个测试系统，用于在三个不同阶段检查机器人的安全性，就像机场的三层安检口一样。首先，在语义层面（Semantic Level），他们检查机器人是否真正理解了你给出的安全规则。它是否将你的话（如“不要混合漂白剂和氨水”）转化成了正确的数学规则？其次，在规划层面（Plan Level），他们在机器人开始移动前检查它的待办事项清单。如果计划写着“打开微波炉，然后把金属勺放进去”，SENTINEL 会立即捕捉到这个错误，就像老师在学生交卷前发现了一道错题一样。最后，在轨迹层面（Trajectory Level），他们在模拟器中观察机器人实际执行任务的过程。即使计划看起来没问题，但也可能出现机器人手臂挥动幅度过大，撞倒花瓶的情况。SENTINEL 会观看机器人动作的整部“电影”，以确保实时过程中不出差错。

在实验中，团队在数字厨房和客厅里的虚拟机器人身上测试了这个系统。他们发现，虽然大型、强大的 AI 模型在思考“如何做”某项任务方面表现出色，但除非使用这些严格的数学规则进行检查，否则它们往往会忽略安全细节。当 SENTINEL 给机器人提供关于计划为何不安全的具体反馈时（例如指出金属勺即将进入微波炉的那一瞬间），机器人学习纠正错误的效果比仅被另一个 AI 告知“这不安全”时要好得多。这项研究表明，要让机器人成为真正安全的小助手，我们需要从“猜测”转向在机器人思考过程的每一步都使用这些精确的数学检查。这不仅仅关乎聪明，更关乎谨慎，而 SENTINEL 正是帮助我们教会机器人如何做到兼而有之的工具。

技术摘要：SENTINEL

问题陈述

将基础模型（Foundation Models, FMs）集成到具身智能体中扩展了其在规划和人机交互方面的能力，但同时也放大了安全风险。现有的基于基础模型的智能体评估基准主要关注任务完成指标（如成功率），并且通常仅将物理危害视为任务失败，而非独立的安全性违规。目前的安全性评估方法过度依赖启发式规则或主观的基础模型评判（LLM-as-Judge），这些方法缺乏严谨的定义，且无法区分发生在智能体流水线不同阶段的失败：语义理解错误、不安全的规划生成，或是不安全的物理执行。此外，这些方法往往无法定位安全性违规究竟起源于哪个层级。

方法论

作者提出了 SENTINEL（基于时序逻辑的可解释具身基础模型安全性评估框架），这是一个将物理安全性建立在时序逻辑规范基础上的多层级形式化框架。该框架在模拟环境（VirtualHome 和 AI2-THOR）中运行，并从三个递进的层级对智能体进行评估：

1. 形式化安全性规范

SENTINEL 将自然语言安全性约束编码为时序逻辑公式，具体包括线性时序逻辑（LTL）和计算树逻辑（CTL）。

状态不变性（State Invariants）： 禁止在所有时刻出现不安全状态的约束（例如，用于避障的 $G(\neg p)$ ）。
顺序约束（Ordering Constraints）： 强制执行正确动作序列的约束（例如，用于“最终关闭”的 $G(p \to F q)$ ）。
分类： 安全规则被分为状态不变性和顺序约束两类，并映射到源自模拟环境中物体属性的原子命题。

2. 多层级评估流水线

该框架采用三阶段流水线，通过逐步过滤失败情况来定位违规行为：

语义层级评估（Semantic-Level Evaluation）：
- 目标： 评估基础模型将自然语言安全性要求转化为形式化 LTL 公式的能力。
- 方法： 向智能体提供安全性约束，并让其生成候选 LTL 公式。这些公式通过语法检查和语义等价性验证（通过 Büchi 自动机和语言包含关系）与地面真值（ground-truth）LTL 规范进行对比。
- 输出： 关于语法错误、语义非等价性和成功解释率的指标。
规划层级评估（Plan-Level Evaluation）：
- 目标： 在执行前验证高层动作规划和子目标是否符合 LTL 约束。
- 方法： 智能体生成一个高层规划（里程碑子目标）。该规划通过检查 LTL 公式，以检测是否存在不安全的符号化顺序或缺失的前置条件。使用广度优先搜索（BFS）来验证该规划在动作空间内的可执行性。
- 输出： 识别出虽然满足任务目标但违反安全性约束的不安全规划。
轨迹层级评估（Trajectory-Level Evaluation）：
- 目标： 评估规划的物理执行情况，考虑分支结果和环境动态。
- 方法： 根据高层规划从模拟器中采样多个执行轨迹。这些轨迹被合并为一个计算树（ $T$ ）。安全性要求从 LTI 提升到 CTL，以评估分支时间属性。
- 验证： 使用 CTL 模型检测器针对该树验证属性（例如，针对“所有路径始终满足 $\phi$ ”的 $AG \phi$ ）。
- 输出： 检测执行相关的违规行为，并生成反例路径（导致失败的具体状态或序列）。

3. 驱动反馈的精炼（Feedback-Driven Refinement）

SENTINEL 利用在轨迹层级检查过程中生成的反例，向智能体提供可验证的反馈。这种反馈循环允许智能体迭代地精炼其规划，旨在提高安全性而不修改底层的智能体架构。

核心贡献

形式化且可解释的安全性规范： 本工作将直观的安全性要求落实到 LTL 和 CTL 中，实现了显式的分类（状态不变性、时序依赖）和形式化验证，而非启发式判断。
统一的多层级形式化安全性评估： SENTINEL 是首个在语义理解、规划生成和物理执行这三个阶段对安全性进行递进式形式化评估的框架。这种设计允许将失败定位到特定阶段（理解问题 vs. 推理问题 vs. 执行问题）。
跨层级的实证分析： 作者将 SENTINEL 应用于 VirtualHome 和 AI2-THOR，并扩展了带有安全性要求的任务。他们证明了安全性违规往往源于不同的层级（例如，语义误解 vs. 低层控制器错误），并且形式化评估能够揭示仅关注任务成功率的基准测试所无法发现的失效模式。

实验结果

作者评估了多种闭源模型（GPT-5, Claude-Opus, Gemini）和开源模型（DeepSeek, Qwen, Mistral, Llama），以及视觉语言模型（VLMs）。

语义层级： 与较小的开源模型相比，较大的模型在将自然语言转化为 LTL 方面的表现显著更高。然而，即使是强大的模型，在处理条件性禁止（conditional prohibitions）时也比处理全局性禁止（global prohibitions）更为吃力。
规划层级： 具有较高语义等价率的模型通常在规划层级保持较高的安全性。然而，添加显式的安全性引导（LTL 提示词）虽然提高了安全性指标，但并未能消除所有违规。
轨迹层级：
- LLMs vs. VLMs： 基于 VLM 的智能体通常比纯文本 LLM 实现了更高的安全性，这可能是由于视觉接地（visual grounding）有助于检测物理危害。然而，VLMs 通常表现出较低的任务成功率，表明存在安全性与能力之间的权衡。
- 执行失败： 从规划层级到轨迹层级的“成功与安全”指标观察到了显著下降，这表明许多失败源于低层动作参数以及控制器中缺乏安全性机制。
安全性提升： 在精炼循环实验中，SENTINEL 的可验证反例反馈带来了显著的安全性指标提升（约为 LLM-as-Judge 基准提升幅度的两倍），同时保持了相当的任务成功率增益。分析显示，LLM-as-Judge 基准经常遗漏真正的危险轨迹（在一项研究中漏检率为 83%），而 SENTINEL 的形式化检查则更加可靠。
效率： 研究发现，在合并的计算树上进行 CTL 验证比独立的 LTL 检查更高效，且随着轨迹数量的增加，加速效果愈发明显。

重要性与主张

本文声称 SENTINEL 为系统性评估基于基础模型的具身智能体的安全性提供了严谨的基础。通过超越启发式或主观判断，该框架提供了：

定位能力： 能够精准定位安全性失败是源于指令误解、生成了不安全规划，还是执行动作时不安全。
可操作的反馈： 生成可验证的反例，从而通过精炼循环驱动有意义的安全性改进。
可扩展性： 通过在采样的计算树上使用 CTL，提供了一种实用的统计检测方式，解决了在复杂物理环境中进行全状态模型检测的不可行性问题。

作者强调，SENTINEL 提供的是经验性检测而非经过认证的验证，因为它是在由采样轨迹组成的有限计算树上运行的。他们承认，如果样本量不足，仍可能存在漏检情况，但他们认为这种方法更接近于统计模型检测，并且鉴于基础模型的黑盒性质及物理环境的复杂性，这是必经之路。该框架被呈现为迈向可验证安全性基准和安全性感知强化学习奖励的重要一步。