在不同规格下使用语义潜在表示的基于视觉运行时监控

# 基于视觉的运行时监控：利用语义潜表征适应变化的规范
来源: https://arxiv.org/html/2605.13923
Bardh Hoxha¹, Oliver Schön², Hideki Okamoto¹, Lars Lindemann², Georgios Fainekos¹  
¹B. Hoxha, H. Okamoto, 和 G. Fainekos 就职于 Toyota NA R&D  
²Oliver Schön 和 Lars Lindemann 就职于 ETH Zürich

###### 摘要

本文研究在部分可观测条件下，基于视觉观测对过去时间信号时态逻辑（ptSTL）进行认证的运行时监控。监控器需要从图像中推断安全相关量，并提供有限样本保证，同时具备**可重用性**：一旦训练并校准，它应能在目标片段中认证任意公式，而无需针对每个公式重新训练。对于由有限时态原子字典诱导的片段，我们证明**语义基**（一组原子鲁棒度得分向量）是单调、1-Lipschitz 可重用接口类中的最小预测目标：任何公式均可通过解析树导出的确定性解码器求值，单次共形校准即可认证整个片段，无需联合界。我们还引入了一种**滚动预测监控器**，它仅预测当前谓词值并在线重建时态历史；该监控器更易学习，但在长时域下会变得保守。在行人交叉路口基准测试中，滚动监控器在短时域下获得更紧的认证界，而语义基监控器在长时域下紧致性高达 4 倍。我们在真实世界的 Waymo 驾驶数据上验证了所提出的监控器，实验证明两种监控器均能经验性地满足共形覆盖保证。

## I. 引言

运行时监控提供了一种机制，用于评估自主系统在部署过程中是否满足指定的安全条件。在实践中，这些条件通常并非一成不变：不同的任务可能需要不同的安全性和性能规范，操作员也可能在部署时更新所使用的规范。因此，一个实用的运行时监控器应具备**可重用性**（见图1 (https://arxiv.org/html/2605.13923#S1.F1)）：经过训练和校准后，它应支持对目标片段中一系列规范的认证，而无需为每个新规范重新训练。这促使在观测和规范之间建立一种**语义接口**：预训练的编码器产生固定的中间表示，而公式特定的值则在查询时通过确定性的、解析推导的解码器计算，无需额外学习。

部分可观测性带来了额外的挑战。监控器只能访问视觉观测，而安全谓词定义在潜物理量上（例如距离、速度和间隙），但监控器只能观测图像。因此，必须从像素中推断安全相关量，并且在证书中必须考虑由此产生的预测不确定性。本文结合了可重用规范监控和部分可观测下的认证学习这两个问题。

一个公式特定的认证基线是预测固定公式的满足度量，并应用共形预测获得认证的下界[1 (https://arxiv.org/html/2605.13923#bib.bib1)]。这种方法可行，但无法重用：当规范改变时，预测器和校准都与该公式绑定。为避免这一限制，监控器必须预测一个**可重用的中间表示**。表示的选择决定了可重用的范围、视觉预测的难度以及由此产生的共形界的紧致性。

参见说明
参见说明
encθ\\operatorname\{enc\}\_{\\theta}
参见说明
decφ1\\operatorname\{dec\}\_{\\varphi\_{1}}
参见说明
decφ2\\operatorname\{dec\}\_{\\varphi\_{2}}
ρ\(φ1,x,t\)\\rho\(\\varphi\_{1},x,t\)
A: 谓词窗口历史

ρ\(φ2,x,t\)\\rho\(\\varphi\_{2},x,t\)
参见说明：公式特定解码器
参见说明
μ1,t−K⋯μ1,t\\small\\mu\_{1,t-K}\\,\\cdots\\,\\mu\_{1,t}
μm,t−K⋯μm,t\\small\\mu\_{m,t-K}\\cdots\\mu\_{m,t}
BtP=\\small\{\\mathcal\{B\}\}\_{t}^{\{\\mathcal\{P\}\}}=
参见说明
BtP=\\small\{\\mathcal\{B\}\}\_{t}^{\{\\mathcal\{P\}\}}=
图1: *左:* 一个训练好的编码器 encθ\\operatorname\{enc\}\_{\\theta} 将视觉输入映射到潜接口 Bt\{\\mathcal\{B\}\}\_{t}，从该接口出发，公式特定解码器可以评估目标片段 F\\mathcal\{F\} 中的任意公式 φ∈F\\varphi\\in\\mathcal\{F\}。*右:* 两种接口基的选择。

我们研究两种可重用的监控接口。第一种在每个时间步预测规范回溯窗口内的所有安全相关量。这具有最大的灵活性，因为任何时态属性都可以由此求值，但编码器必须回归一个高维输出，其维度随窗口长度增长。对于一组固定时态运算符上的规范片段，例如“在过去 K 步内始终安全”或“在 K 步内最终达到目标”，我们证明存在一个更小的表示——**语义基**——足以评估该族中的所有规范，并且不存在更小的表示。

我们使用**共形预测**（CP）[1 (https://arxiv.org/html/2605.13923#bib.bib1), 2 (https://arxiv.org/html/2605.13923#bib.bib2), 3 (https://arxiv.org/html/2605.13923#bib.bib3)] 将预测残差转换为认证下界，并证明这些界的紧致性关键取决于校准是在解码器中的时态聚合之前还是之后应用。

贡献:

1. 1. **语义基作为可重用接口（第IV节 (https://arxiv.org/html/2605.13923#S4)）：** 对于任何由有限原子字典诱导的 ptSTL 片段，我们证明语义基是单调、1-Lipschitz 可重用接口类中的最小表示。
2. 2. **组合共形认证（第V节 (https://arxiv.org/html/2605.13923#S5)）：** 由于每个公式都由单调、1-Lipschitz 函数解码，单次逐原子共形界即可同时认证整个片段（定理2 (https://arxiv.org/html/2605.13923#Thmtheorem2)）。
3. 3. **滚动预测监控器：** 我们引入了一种滚动预测监控器，在线更新谓词基。这大大降低了编码器维度，使学习问题显著简化。我们提供经验证据表明，这在短时域下能获得更高的预测精度和更紧的共形界。

## II. 相关工作

信号时态逻辑（STL）提供了一个框架，用于指定和评估连续值信号的时态属性，其鲁棒性语义量化了与违反的距离[4 (https://arxiv.org/html/2605.13923#bib.bib4), 5 (https://arxiv.org/html/2605.13923#bib.bib5)]。过去时间 STL 的高效在线监控算法已得到很好的建立[6 (https://arxiv.org/html/2605.13923#bib.bib6), 7 (https://arxiv.org/html/2605.13923#bib.bib7)]。我们在此基础上构建，通过学习的视觉模型处理部分可观测性。

共形预测（CP）已被用于 STL 监控中，以提供有限样本覆盖保证[1 (https://arxiv.org/html/2605.13923#bib.bib1), 2 (https://arxiv.org/html/2605.13923#bib.bib2), 3 (https://arxiv.org/html/2605.13923#bib.bib3)]。除了监控，CP 也被用于安全规划和预测[8 (https://arxiv.org/html/2605.13923#bib.bib8), 9 (https://arxiv.org/html/2605.13923#bib.bib9)]；与这些工作不同，我们研究通过单次校准实现可重用的片段级认证。

在部分可观测性下的神经监控已针对固定属性和小型模板族进行了研究[10 (https://arxiv.org/html/2605.13923#bib.bib10), 11 (https://arxiv.org/html/2605.13923#bib.bib11)]。我们将这一设置扩展为从单个预测器认证整个 ∧/∨\\wedge/\\vee 封闭的片段，并描述了实现这一目标所需的最小接口。

在部分和不确观测下，组合的不确定性感知 STL 语义已被研究。部分轨迹的鲁棒满足区间在[5 (https://arxiv.org/html/2605.13923#bib.bib5)]中引入；通过 STL 算子传播不确定性的区间值语义在[12 (https://arxiv.org/html/2605.13923#bib.bib12), 13 (https://arxiv.org/html/2605.13923#bib.bib13)]中开发；基于仿射算术和 SMT 的相关设置则在[14 (https://arxiv.org/html/2605.13923#bib.bib14)]中研究。我们的滚动和语义基监控器建立在这种组合观点之上，增加了预测目标的最小性结果以及显式的校准权衡分析。在[15 (https://arxiv.org/html/2605.13923#bib.bib15), 16 (https://arxiv.org/html/2605.13923#bib.bib16)]中，论文提出了针对感知系统的监控，但未提供基于学习到的潜在视觉表示的 ptSTL 鲁棒性的有限样本认证界。

*预测状态表示*（PSRs）为部分可观测系统构建最小充分统计量[17 (https://arxiv.org/html/2605.13923#bib.bib17), 18 (https://arxiv.org/html/2605.13923#bib.bib18)]：线性 PSR 识别最小秩基，从该基可以线性解码任何可观测测试，而无需显式建模潜在信念状态。最近，时态逻辑规范通过*嵌入时态逻辑*（ETL）直接嵌入到潜在空间中，并通过学习到的距离阈值检查满足性，但没有认证覆盖界[19 (https://arxiv.org/html/2605.13923#bib.bib19)]。概念嵌入模型将潜在表示扩展到概率概念成员资格，用于并发概念推理，同样没有形式化保证[20 (https://arxiv.org/html/2605.13923#bib.bib20)]。我们的语义基是 ptSTL 监控的 PSR 模拟：对于所有信号，单调、1-Lipschitz 解码器足以满足的最小统计量，而这种 Lipschitz 限制正是第V节 (https://arxiv.org/html/2605.13923#S5) 中实现共形认证的关键。

自适应共形方法提供了在分布偏移下对轨迹级紧致性的正交改进；将它们与我们的组合认证结构相结合是未来工作的一个可能方向[21 (https://arxiv.org/html/2605.13923#bib.bib21)]。

## III. 问题形式化

### III-A 动力学系统与观测

我们考虑离散时间动力学系统，其状态 xt∈X⊂Rdxx\_{t}\\in\\mathbb\{X\}\\subset\\mathbb\{R\}^{d\_{x}} 演化如下：

xt+1\\displaystyle x\_{t+1} = fX(xt,ut,vt), ot = fO(xt,wt),\\displaystyle = f\_{X}(x\_{t},u\_{t},v\_{t}),\\qquad o\_{t}=f\_{O}(x\_{t},w\_{t}), (1)

其中 ut∈Rduu\_{t}\\in\\mathbb\{R\}^{d\_{u}} 是控制输入，vt,wtv\_{t},w\_{t} 是噪声项。在每个时刻 t∈Z≥0t\\in\\mathbb\{Z\}\_{\\geq 0}，状态生成一个观测 ot∈O⊂Rdoo\_{t}\\in\\mathbb\{O\}\\subset\\mathbb\{R\}^{d\_{o}}；例如，oto\_{t} 可能是在不同传感器干扰下的俯视摄像机图像。在本文中，监控器只能访问观测序列 {oτ}τ≤t\\{o\_{\\tau}\\}\_{\\tau\\leq t}；状态 xtx\_{t} 从未被直接观测。

### III-B 时态逻辑规范

令 P={μ1,...,μm}\\mathcal\{P\}=\\\{\\mu\_{1},\\dots,\\mu\_{m}\\\} 为关于信号 x:Z≥0→X\\{x\\}\\colon\\mathbb\{Z\}\_{\\geq 0}\\to\\mathbb\{X\} 的一组有限**原子谓词**，其中每个 μk:X×Z≥0→{⊤,⊥}\\mu\_{k}\\colon\\mathbb\{X\}\\times\\mathbb\{Z\}\_{\\geq 0}\\to\\{\\top,\\bot\\} 通过标量谓词函数 hk:X→Rh\_{k}\\colon\\mathbb\{X\}\\to\\mathbb\{R\} 定义为：

(μk(x,t)=⊤) ⇔ hk(xt)≥0.\\big\(\\mu\_{k}(x,t)=\\top\\big\)\\Leftrightarrow h\_{k}(x\_{t})\\geq 0.

我们将 ρ(μk,x,t):=hk(xt)\\rho(\\mu\_{k},\\{x\\},t):=h\_{k}(x\_{t}) 称为 μk\\mu\_{k} 的**鲁棒度**。

###### 定义1（ptSTL 语法和定量语义）

**过去时间 STL**（ptSTL）[22 (https://arxiv.org/html/2605.13923#bib.bib22)] 公式，基于谓词集 P\\mathcal\{P\}，采用**正范式**（PNF），由以下文法生成：

φ::=μk ∣ φ1∧φ2 ∣ φ1∨φ2 ∣ ⊡[a,b]φ ∣ ⟐[a,b]φ,\\displaystyle\\varphi::=\\mu\_{k}\\mid\\varphi\_{1}\\wedge\\varphi\_{2}\\mid\\varphi\_{1}\\vee\\varphi\_{2}\\mid\\boxdot\_{[a,b]}\\,\\varphi\\mid\\Diamonddot\_{[a,b]}\\,\\varphi,

其中 μk∈P\\mu\_{k}\\in\\mathcal\{P\}，φ1,φ2\\varphi\_{1},\\varphi\_{2} 是 ptSTL 公式，且 [a,b]⊆Z≥0[a,b]\\subseteq\\mathbb\{Z\}\_{\\geq 0}。**鲁棒度** ρ(φ,x,t)∈R\\rho(\\varphi,\\{x\\},t)\\in\\mathbb\{R\} 在时刻 t∈Z≥0t\\in\\mathbb\{Z\}\_{\\geq 0} 关于信号 x:Z≥0→X\\{x\\}\\colon\\mathbb\{Z\}\_{\\geq 0}\\to\\mathbb\{X\} 递归定义如下：

ρ(μk,x,t)\\displaystyle\\rho(\\mu\_{k},x,t) = hk(xt),\\displaystyle= h\_{k}(x\_{t}),  
ρ(φ1∧φ2,x,t)\\displaystyle\\rho(\\varphi\_{1}\\wedge\\varphi\_{2},\\{x\\},t) = min{ρ(φ1,x,t),ρ(φ2,x,t)},\\displaystyle= \\min\\big\\{\\rho(\\varphi\_{1},\\{x\\},t),\\,\\rho(\\varphi\_{2},\\{x\\},t)\\big\\},  
ρ(φ1∨φ2,x,t)\\displaystyle\\rho(\\varphi\_{1}\\vee\\varphi\_{2},\\{x\\},t) = max{ρ(φ1,x,t),ρ(φ2,x,t)},\\displaystyle= \\max\\big\\{\\rho(\\varphi\_{1},\\{x\\},t),\\,\\rho(\\varphi\_{2},\\{x\\},t)\\big\\},  
ρ(⊡[a,b]φ,x,t)\\displaystyle\\rho(\\boxdot\_{[a,b]}\\varphi,\\{x\\},t) = inft′∈[t−b,t−a]ρ(φ,x,t′),\\displaystyle= \\inf\_{t^{\\prime}\\in[t-b,t-a]}\\rho(\\varphi,\\{x\\},t^{\\prime}),  
ρ(⟐[a,b]φ,x,t)\\displaystyle\\rho(\\Diamonddot\_{[a,b]}\\varphi,\\{x\\},t) = supt′∈[t−b,t−a]ρ(φ,x,t′).\\displaystyle= \\sup\_{t^{\\prime}\\in[t-b,t-a]}\\rho(\\varphi,\\{x\\},t^{\\prime}).

信号 x\\{x\\} 在时刻 tt 满足公式 φ\\varphi 当且仅当 ρ(φ,x,t)≥0\\rho(\\varphi,\\{x\\},t)\\geq 0。

我们将**公式时域** hor(φ)∈N\\mathrm\{hor\}(\\varphi)\\in\\mathbb\{N\} 定义为在时刻 tt 求值 φ\\varphi 所需的最大向后时间延迟，使得 ρ(φ,x,t)\\rho(\\varphi,\\{x\\},t) 仅依赖于 xt−hor(φ):t∈Rdx×(hor(φ)+1)\\{x\\}\_{t-\\mathrm\{hor\}(\\varphi):t}\\in\\mathbb\{R\}^{d\_{x}\\times(\\mathrm\{hor\}(\\varphi)+1)}。

### III-C 诱导的规范片段

我们现在定义本文所处理的一类规范。关键思想是固定一个有限的**时态原子**字典，即作为不可约生成元的基础 ptSTL 公式，并将其在合取和析取下封闭（见图2 (https://arxiv.org/html/2605.13923#S3.F2)）。其结果是 ptSTL 的一个片段，具有丰富的代数结构，能够通过第IV节 (https://arxiv.org/html/2605.13923#S4) 中引入的语义基实现紧致组合共形认证。

μ1\\mu\_{1} μ2\\mu\_{2} μk\\mu\_{k} μm\\mu\_{m} ⋯\\cdots 谓词集 P\\mathcal\{P\}:
⊡Iμ1\\boxdot\_{I}\\mu\_{1} ⟐Iμ1\\Diamonddot\_{I}\\mu\_{1} ⊡I′μk\\boxdot\_{I^{\\prime}}\\\!\\mu\_{k} ⋯\\cdots 时态原子 A\\mathcal\{A\}:
a1∧a2a\_{1}\\wedge a\_{2} a2∨a3a\_{2}\\vee a\_{3} ⋯\\cdots 片段 F(A)\\mathcal\{F\}(\\mathcal\{A\}): ∧\\wedge ∨\\vee
图2: 片段结构。*上*: 谓词 μk∈P\\mu\_{k}\\in\\mathcal\{P\}。*中*: 时态原子 aq∈Aa\_{q}\\in\\mathcal\{A\}，例如每个原子对一个谓词应用单个过去时间算子（⊡I\\boxdot\_{I} 或 ⟐I\\Diamonddot\_{I}）。*下*: 诱导的片段 F(A)\\mathcal\{F\}(\\mathcal\{A\})，通过将 A\\mathcal\{A\} 在合取（实线，∧\\wedge）和析取（虚线，∨\\vee）下封闭得到。

###### 定义2（原子字典与诱导片段）

一组有限的 ptSTL 公式 A={a1,...,ar}\\mathcal\{A\}=\\\{a\_{1},\\dots,a\_{r}\\\} 是一个**原子字典**。其**诱导片段** F(A)\\mathcal\{F\}(\\mathcal\{A\})