Runtime Monitoring of Perception-Based Autonomous Systems via Embedding Temporal Logic¶
会议: NeurIPS 2026
arXiv: 2605.12651
OpenReview: https://openreview.net/forum?id=JGbC5dLr5b
代码: https://github.com/ETLMonitoringAuthors/ETLMonitoring
领域: 其他
关键词: 运行时监控, 嵌入时序逻辑, 形式化规约, 保形预测, 具身智能
一句话总结¶
提出直接在预训练视觉编码器嵌入空间中定义并监控时序规约的嵌入时序逻辑（ETL），结合保形校准提供无分布假设的召回率安全保障，实现免目标检测与无符号标注的端到端自主系统感知运行时监控。
研究背景与动机¶
现代自主系统（如自动驾驶车辆、具身机器人操纵臂）日益依赖从原始高维传感器观测（RGB 图像、点云等）到紧凑隐表示的预训练视觉表征进行规划与决策。为了保障高安全关键场景下的行为正确性，传统的运行时监控方法依赖于时序逻辑（如信号时序逻辑 STL 或度量时序逻辑 MTL），在每个控制周期评估系统的执行轨迹是否满足形式化安全规约并在违规时告警。然而，传统时序逻辑的原子谓词是建立在显式低维状态空间之上的（例如障碍物三维坐标、机械臂末端速度、抓夹接触力）。当面对以端到端或感知驱动的自主系统时，这类低维物理状态往往无法直接获取，通常需要额外堆叠专门的目标检测器、关键点估计器或手工设计的概念分类器。
依赖额外感知模块将传感器流离散化为符号命题的做法存在严重的根本缺陷：一方面，训练与部署额外的分类器引入了计算开销、领域迁移脆弱性与感知标定误差；另一方面，一旦任务要求演进（例如需要从监测“抓取物体”扩充到监测“平稳放置到指定容器”），系统必须重新设计或微调专用检测模型，难以应对开放环境中动态扩展的概念词表。形式化规约所依赖的低维符号空间与现代感知系统实际运作的连续高维潜空间之间存在难以调和的表征鸿沟。
受预训练视觉编码器（如 CLIP、DINOv2、World Model 潜空间）几何特性的启发，语义相似的物理场景在潜空间中天然聚类且距离相近。若能将预训练潜向量作为形式化规约的“一等公民”，直接将感知概念表述为观测嵌入与参考目标嵌入之间的几何测度，便能彻底省去中间符号检测模块。核心 idea：提出嵌入时序逻辑（ETL），直接在预训练嵌入空间中将感知概念定义为观测潜向量与目标潜向量之间的几何距离谓词，结合布尔与鲁棒性时序算子评估有限轨迹，并引入基于保形预测的数据驱动阈值校准机制，为安全关键自主系统提供免符号标注且具备统计召回率保证的在线感知监控。
方法详解¶
整体框架¶
ETL 将感知驱动的自主系统形式化为嵌入时序结构（Embedding Temporal Structure），其核心流程是：在系统运行过程中，传感器采集的高维连续观测通过固定的预训练编码器实时映射到潜向量序列；监控器通过度量当前观测潜向量与离线给定的目标观测嵌入集合之间的几何距离，判定原子嵌入谓词是否满足；进而利用时序逻辑算子（如 Always、Eventually、Until）计算整条有限轨迹的前缀鲁棒性度量，并在出现违反规约时输出报警信号。
%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
A["传感器实时观测 o_t + 参考目标图像 O_G"] --> B["预训练视觉编码器<br/>提取嵌入向量 z_t 与目标集 Z_target"]
B --> C["原子嵌入谓词评估<br/>计算几何距离与目标集聚合测度 δ_ap(z_t)"]
C --> D["保形阈值校准<br/>确定安全判定边界 ε_F1 / ε_CP"]
D --> E["有限轨迹时序监控器<br/>评估 ETL 鲁棒性与布尔报警信号 M_φ(σ_≤t)"]关键设计¶
1. 嵌入时序结构与原子嵌入谓词：直接在连续隐空间中具象化高层感知语义
传统时序逻辑将系统建模为离散状态转移系统，而 ETL 构建了嵌入时序结构 \(\mathcal{M} \equiv (\mathcal{S}, \mathcal{O}, \mathcal{Z}, \phi_{obs}, \psi_{enc}, D_{\mathcal{Z}}, AP_z)\)，通过表征映射 \(\eta \equiv \psi_{enc} \circ \phi_{obs}: \mathcal{S} \to \mathcal{Z}\) 将底层物理真实状态转换为隐空间轨迹 \(\sigma = (z_i)_{i \in \mathbb{N}}\)。针对传统方法难以表达“位于物体附近”或“呈现目标外观”等模糊感知概念的问题，ETL 定义原子嵌入谓词为五元组 \(ap \equiv (\mathcal{Z}_{target}, d, \epsilon, \bowtie, a)\)，其中 \(\mathcal{Z}_{target}\) 为专家提供的参考观测集合（例如目标姿态的参考图像嵌入），\(d\) 为匹配编码器训练特性的距离度量（如对比学习表征采用余弦距离、世界模型重构表征采用 \(L_2\) 范数），\(a\) 为集合聚合算子（如 \(\min\) 或 \(\max\)），\(\bowtie \in \{\le, <, \ge, >\}\) 为比较关系，\(\epsilon\) 为距离阈值。当前观测嵌入 \(z_t\) 对目标概念的偏离度被量化为：
当聚合算子选取 \(a = \min\) 且 \(\bowtie = \le\) 时，\(\delta_{ap}(z_t) \le \epsilon\) 直观表示当前画面在潜空间中与任意一个目标正例参考帧的距离不超过安全容差，无需预先训练分类器即可即插即用地完成视觉语义判定。
2. 嵌入时序逻辑监控器与定量鲁棒性语义：支持复杂长程时序行为的在线判定
为了对包含阶段性子任务、避免危险区域、严格先后次序（如“先抓取物体再移动至托盘”）的长程任务进行全程监控，ETL 沿用线性时序逻辑（LTL）与信号时序逻辑（STL）的语法结构，递归定义公式 \(\varphi ::= ap \mid \neg \varphi \mid \varphi_1 \land \varphi_2 \mid \varphi_1 \mathbf{U} \varphi_2\)，并派生出最终算子 \(\mathbf{F}\varphi = \text{True} \mathbf{U} \varphi\) 与全局算子 \(\mathbf{G}\varphi = \neg \mathbf{F} \neg \varphi\)。在有限前缀轨迹 \(\sigma_{\le t} = (z_0, \dots, z_t)\) 上，ETL 引入定量鲁棒性语义 \(\rho(ap, \sigma, i, b)\)：对于距离上限谓词（\(\bowtie \in \{\le, <\}\)），单步鲁棒度为 \(\rho(ap, \sigma, i, b) = \epsilon - \delta_{ap}(z_i)\)；对于逻辑与及全局算子则取区间下确界 \(\inf\)。在线监控器定义为符号序列 \(M_\varphi(\sigma_{\le t}) = (r_0^\varphi, \dots, r_t^\varphi) \in \{-1, +1\}^{t+1}\)，其中 \(r_i^\varphi = \operatorname{sgn}(\rho(\varphi, \sigma_{\le i}, 0, i))\)。只要在某个时间步鲁棒性转负，监控器立即触发警报，向底层控制器反馈规约违背信息。
3. 数据驱动的阈值校准机制：兼顾经验最优与无分布假设的召回率统计保障
连续隐空间中几何距离阈值 \(\epsilon\) 的取值直接决定了谓词的严格程度。过小的阈值会导致漏检，过大的阈值则会导致虚警。针对不同应用对精度的要求，本文提出两类校准机制：第一类是 \(F_1\) 最优阈值 \(\epsilon_{F1}\)，在留出校准轨迹集 \(\mathcal{D}_{cal} = \{(d_t, y_t)\}_{t=1}^N\) 上，通过遍历经验距离集合选择使 \(F_1\) 分数最大化的候选阈值，适用于对精确率与召回率平衡要求严苛的通用监测；第二类是面向高危安全场景的保形预测校准阈值 \(\epsilon_{CP}\)。针对单条校准轨迹 \(\varsigma^i\)，提取所有满足真实正例条件的时刻中距离目标最远（即最难检测）的帧构建不符度得分：
给定允许的漏检错误界 \(\alpha \in (0, 1)\)，基于独立同分布或可交换性假设，取各校准轨迹得分的升序排列第 \(k = \lceil (1 - \alpha)(n_{cal} + 1) \rceil\) 个分位数作为 \(\epsilon_{CP}\)。该校准方法无需假设隐空间距离的具体分布形式，在有限样本下从理论上严格保证新轨迹全时步正例被完全检出的边际概率不低于 \(1 - \alpha\)。
损失函数 / 训练策略¶
ETL 属于免微调（zero-shot / inference-only）的形式化监控框架，不涉及对预训练视觉编码器参数的梯度反向传播。编码器采用冻结权重的通用视觉模型（如 DINOv2、SVD VAE）或基于 RSSM 结构预训练的世界模型（Dreamer）。阈值校准完全在由 \(n_{cal}\) 条带真值轨迹构成的离线校准集上以非参数统计方式进行，部署时仅需执行前向推理与一维距离比较，单步监控开销极小，能够满足实时控制回路的要求。
实验关键数据¶
主实验¶
论文在三个互补的实验基准上进行了系统评估：（1）带有二维特权真实状态的 Dubins 小车导航避障与序列规划任务；（2）包含接触丰富与阶段性长程交互的 MetaWorld 与 D3IL 仿真机械臂操纵任务；（3）跨视角、非结构化真实环境的大规模机器人操纵数据集 DROID。对比基线包括基于隐空间密度估计的最新监控方法 logpZO、主成分聚类基线 PCA-kmeans 以及前沿视觉语言模型 Qwen2-VL-2B。
| 实验基准 / 任务 | 评测指标 | ETL (本文, \(F_1\)-optimal) | 核心对比基准 | 优势幅度 / 对比表现 |
|---|---|---|---|---|
| Dubins Car (到达 \(F A\)) | \(F_1\) / 准确率 (Agree) | 0.85 / 98.6% | Ground-Truth State Monitor | 极度逼近特权物理状态监控器 |
| Dubins Car (避障 \(G \neg C\)) | \(F_1\) / 准确率 (Agree) | 0.80 / 96.5% | Ground-Truth State Monitor | 成功识别障碍物语义隐边界 |
| Dubins Car (序列 \(A \to B\)) | 轨迹级时序一致性 | 100% (精确率/召回率均 1.0) | Ground-Truth State Monitor | 完美捕捉多子目标先后时序 |
| D3IL Stacking 堆叠操纵 | 谓词监测 \(F_1\) | 0.897 | 0.852 (PCA-kmeans) | 领先 +0.045 |
| D3IL Sorting 分类推块 | 谓词监测 \(F_1\) | 0.593 | 0.585 (PCA-kmeans) | 领先 +0.008 (分布漂移最难任务) |
| MetaWorld Pick-Place-Wall | 谓词监测 \(F_1\) | 0.961 | 0.992 (logpZO) | 极高水平 (logpZO 贴合流模型先验) |
| 三大仿真操纵环境综合平均 | 平均 \(F_1\) 分数 | 0.817 | 0.790 (logpZO) / 0.751 (PCA-kmeans) | 综合性能达最优，高出 +0.027 |
| DROID 真实环境多阶段任务 | 平均 \(F_1\) / 帧准确率 | 0.813 / 94.0% | 0.390 / 56.7% (Qwen2-VL-2B) | \(F_1\) 提升超一倍 (+0.423)，准确率显著优异 |
| DROID 真实环境时序阶段顺序 | 完整序列正确率 | 4/5 任务 (80%) | 2/5 任务 (40%) (Qwen2-VL-2B) | 序列辨识稳定性大幅超越多模态大模型 |
消融实验¶
为了验证阈值校准机制在安全监控中的精度-召回率权衡效果，研究人员在 Dubins Car 导航和三大仿真操纵环境中对 \(F_1\) 最优阈值 \(\epsilon_{F1}\) 与保形预测阈值 \(\epsilon_{CP}\)（设定标称错误率 \(\alpha = 0.10\)）进行了详细对比。
| 配置 / 任务 | 阈值方案 | 精确率 (Prec.) | 召回率 (Rec.) | 帧级一致性 (Agree) | 说明 |
|---|---|---|---|---|---|
| Dubins Car (到达 A) | \(\epsilon^*\) (\(F_1\)-optimal) | 0.87 | 0.83 | 98.6% | 平衡模式：查准与查全兼顾 |
| Dubins Car (到达 A) | \(\epsilon_{CP}\) (\(\alpha=0.10\)) | 0.79 | 0.93 | 98.5% | 安全保形：召回率大幅上升 (+0.10)，一致性无损 |
| Dubins Car (避障 C) | \(\epsilon^*\) (\(F_1\)-optimal) | 0.69 | 0.94 | 96.5% | 避障模式下高召回 |
| Dubins Car (避障 C) | \(\epsilon_{CP}\) (\(\alpha=0.10\)) | 0.70 | 0.92 | 96.5% | 保持稳定安全边界 |
| MetaWorld (Grasp A) | \(\epsilon^*\) (\(F_1\)-optimal) | 0.971 | 0.999 | 97.3% | 抓取检测接近饱和 |
| MetaWorld (Place B) | \(\epsilon^*\) (\(F_1\)-optimal) | 0.901 | 1.000 | 91.4% | 放置检测全召回 |
| 三环境操纵综合 (Avg) | \(\epsilon_{F1}\) vs \(\epsilon_{CP}\) | - | - | - | \(\epsilon_{F1}\) 平均 \(F_1\) 为 0.817，\(\epsilon_{CP}\) 为 0.789 |
关键发现¶
- 形式化时序追踪表现出色：在 Dubins 导航和 MetaWorld Pick-Place 任务中，ETL 的时序规约监控器在子目标先后执行顺序（如抓取后放置、先到达 A 后到达 B）的轨迹级符合率均达到了 100%，证明在潜空间中时序距离特征的演化能够高度精确地映射物理世界的离散阶段转移。
- 保形校准有效消除漏检风险：消融数据显示，采用保形阈值 \(\epsilon_{CP}\) 能够在精确率仅发生微小让步的前提下，将关键事件（如目标到达）的召回率从 0.83 显著提高到 0.93，完全符合安全关键控制系统“宁可轻度虚警、绝不漏报危险”的工程设计原则。
- 远优于直接使用通识 VLM 提问：真实世界 DROID 数据表明，通用 VLM（Qwen2-VL）面对视觉特征相似但物理接触状态迥异的细粒度操作阶段（如机械臂靠近物体 vs 刚刚完成接触抓取）极易产生幻觉与时序错判，导致平均 \(F_1\) 仅有 0.390；而 ETL 借助领域匹配的表征距离，展现出强韧的鲁棒性（\(F_1 = 0.813\)）。
亮点与洞察¶
- 将表征距离重塑为时序逻辑谓词：摆脱了以往为每个命题单独训练分类器或目标检测器的传统范式，将预训练大模型的潜空间度量直接提升为一等公民的逻辑谓词，实现了零样本或少样本参考图驱动的高层概念监控。
- 统计形式化双轮驱动的保形安全边界：创造性地将无需分布假设的有限样本保形预测（Conformal Prediction）理论适配到时序轨迹的极值距离校准上，为黑盒神经网络驱动的自主系统赋予了严谨的概率安全召回保障。
- 即插即用的低开销部署特性：监控器仅需轻量的前向特征提取与标量距离运算，避开了密集目标检测与大模型多轮自回归生成的推理延迟，能够直接插入 20Hz 以上的高频机器人闭环控制循环。
局限与展望¶
- 作者承认的局限：隐空间谓词缺乏人类可直观理解的符号可解释性，决策边界受编码器隐空间的特征分布支配；当不同物理状态在特征空间发生表征重叠时（如 DROID 中张开夹爪接近物体与释放物体后的画面具有相似性），谓词判别精度会出现退化。
- 拓展与改进方向：未来的演进路径包括引入概念瓶颈模型（Concept Bottleneck Models）以增强隐空间谓词的可解释性、结合对比适应学习（Encoder Fine-tuning / Adaptation）进一步拉大细粒度语义状态在潜空间中的几何间距，以及探索在线自适应动态阈值调整算法。
相关工作与启发¶
- vs STPL (Hekmatnejad et al., 2024)：STPL 扩展了时空感知逻辑，但依然强依赖于目标检测边界框与 2D/3D 几何估计模块；本文 ETL 彻底打破了符号与边界框依赖，直接在预训练向量连续隐空间进行形式化监控。
- vs logpZO / PCA-kmeans (Xu et al., 2025; Liu et al., 2024)：纯表征异常检测方法仅能给出系统是否发生 OOD 偏离的标量不确定性分数，无法解析复杂的阶段演进；ETL 融合了时序逻辑算子，能够严密验证包含前后依赖、死锁与分支选择的时序组合任务。
- vs VLM-as-a-Monitor (Wang et al., 2024)：直接通过提示词让多模态大语言模型评判视频帧存在高推理延迟、时序不一致与细粒度接触幻觉；ETL 在冻结表征上通过几何测度与保形校准兼顾了高效性与确定性。
评分¶
- 新颖性: ⭐⭐⭐⭐⭐ 首次提出将连续表征空间几何距离形式化为时序逻辑原子谓词，并引入轨迹级保形校准。
- 实验充分度: ⭐⭐⭐⭐⭐ 覆盖从 2D 物理模型、3D 复杂接触仿真到真实世界多阶段机械臂操纵的全谱系验证。
- 写作质量: ⭐⭐⭐⭐⭐ 概念形式化严谨，从定义、语法语义到统计定理推导脉络清晰。
- 价值: ⭐⭐⭐⭐⭐ 成功连接了现代感知表征学习与高可信形式化验证两大领域，为端到端具身智能的安全落地开辟了新途径。