Querying Labeled Time Series Data with Scenario Programs
Querying Labeled Time Series Data with Scenario Programs
Simulation-based testing has become a crucial complement to road testing for ensuring the safety of cyber physical systems (CPS). As a result, significant research efforts have been directed toward identifying failure scenarios within simulation environments. However, a critical question remains. Are the AV failure scenarios discovered in simulation reproducible on actual systems in the real world? The sim-to-real gap caused by differences between simulated and real sensor data means that failure scenarios identified in simulation might either be artifacts of synthetic sensor data or actual issues that also occur with real sensor data. To address this, an effective approach to validating simulated failure scenarios is to locate occurrences of these scenarios within real-world datasets and verify whether the failure persists on the datasets. To this end, we introduce a formal definition of how labeled time series sensor data can match an abstract scenario, represented as a scenario program using the Scenic probabilistic programming language. We present a querying algorithm that, given a scenario program and a labeled dataset, identifies the subset of data that matches the specified scenario. Our experiment shows that our algorithm is more accurate and orders of magnitude faster in querying scenarios than the state-of-the-art commercial vision large language models, and can scale with the duration of queried time series data.
使用场景程序查询带标签的时间序列数据
基于仿真的测试已成为确保网络物理系统（CPS）安全的重要补充。因此，大量研究努力集中在仿真环境内识别失效场景。然而，一个关键问题仍然存在：在仿真环境中发现的自动驾驶汽车（AV）失效场景在现实世界中是否可重复？由于仿真与真实传感器数据之间的差异（sim-to-real gap），仿真中识别的失效场景可能是合成传感器数据的伪影，也可能是真实系统同样会发生的实际问题。为了解决这个问题，一种有效的验证仿真失效场景的方法是将这些场景定位在真实世界的数据集中，并验证失效是否仍然存在。为此，我们引入了一个正式的定义，说明带标签的时间序列传感器数据如何与用 Scenic 概率编程语言表示的抽象场景匹配。我们提出了一种查询算法，给定一个场景程序和一个带标签的数据集，可以识别出与指定场景匹配的数据子集。我们的实验表明，我们的算法在查询场景方面比最先进的商业视觉大语言模型更准确，并且在查询速度上快几个数量级，同时可以随着查询时间序列数据的持续时间进行扩展。
智能问答：
Q1: 这篇论文试图解决什么问题？
论文旨在解决“仿真-现实一致性验证”（sim-to-real validation）中的核心难题：
在仿真环境中自动发现的自动驾驶汽车（AV）失效场景，是否会在真实传感器数据中复现？
由于仿真与真实传感器数据存在差异（sim-to-real gap），仿真找到的失效可能是合成数据带来的假象，也可能是真实系统同样会触发的真实缺陷。
传统做法是把仿真场景搬到封闭测试场复现，成本高且不可扩展。
为此，作者提出一种基于形式化场景程序的查询方法：
用 SCENic 概率编程语言将候选失效场景形式化为“场景程序”；
在已标注的真实时间序列数据集（含目标位置、行为等标签）中，自动检索与场景程序语义一致的真实片段；
若检索到匹配片段，即可直接在真实数据上验证该失效是否依旧发生，从而无需物理复现即可判断仿真失效的现实相关性。
总结：论文把“仿真-现实一致性验证”转化为带语义标签的时间序列数据查询问题，并给出可证明正确的查询算法，实现高准确、高吞吐的自动验证。
Q2: 有哪些相关研究？
论文在第 1 章与第 2 章将相关研究归为 5 条主线，并指出各自与本文工作的区别。以下按主题归纳，并给出关键文献（按论文引用编号）。
1. 仿真场景自动生成 / 失效场景搜索
组合式 falsification
Dreossi et al. [1]：将 CPS 与 ML 组件组合做形式化 falsification，仅停留在仿真层。
VerifAI 工具箱
Dreossi et al. [2]：提供场景采样、监控与 falsification 框架，但未处理真实数据匹配。
专家关键状态引导搜索
Du & Driggs-Campbell [3]：利用领域知识加速搜索，同样仅限仿真。
AdvSim 等对抗场景生成
Wang et al. [4]：在仿真内生成安全关键场景，未考虑真实传感器差异。
→ 共同点：只输出仿真场景；没有机制判断这些场景是否存在于真实数据。
2. 视频/时序数据查询与检索
SQL 扩展型系统
BlazeIt [14]、VisualWorldDB [15]、SVQL [16]、ExSample [17]：支持“出现某类物体”等简单过滤，无法表达时序行为或定量几何约束。
空间-静态查询
SpaTiallyze [19]、作者前期工作 [20]：支持道路拓扑+空间谓词，但不支持对象随时间的行为演化。
→ 这些数据库方法表达能力受限，无法直接查询“跟车-换道”等时序交互场景。
3. 自然语言驱动的视频理解（Vision-Language Models）
GPT-4o [31]、Claude-3.5 [32] 等 VLM：可接受自由文本提问，但
– 语义不精确，同一句 prompt 可能返回不同结果；
– 无正确性保证；
– 实验显示准确率低于本文方法 20–35 %，且速度慢 2–3 个数量级。
→ VLMs 通用但不适配高可靠、可证明的验证需求。
4. 形式化场景语言与测试
SCENIC 概率场景语言
Fremont et al. [11, 12]：可定义初始分布与行为，原本用于生成仿真场景；本文首次将其反向用于查询真实标签序列。
M-SDL 等工业语言
Foretellix [13]：与 SCENIC 类似，但论文方法聚焦于 SCENIC 的片段并给出查询算法与正确性证明。
→ 本文把“场景生成语言”转为“查询语言”，并解决语义匹配+对象对应两大技术难点。
5. 标签时间序列建模（行为预测/SLAM）
SLAM [22]、行为预测网络 [23, 34]：提供所需输入-输出标签（位姿、速度、原语行为）。
本文假设标签已存在，重点在于如何形式化地查询与验证，而非如何生成标签。
小结
研究方向t与本文关系t主要差距
仿真场景搜索t提供“被验证对象”t无真实数据校验
视频数据库t提供“查询”概念t表达力低、无行为时序
VLM 视频理解t提供“自然语言查询”t语义模糊、无保证、慢
场景语言 SCENICt提供“形式模型”t原本用于生成而非查询
标签估计模型t提供“输入-输出标签”t仅作数据源，非查询核心
本文首次把形式化场景程序与大规模带标签真实时序数据桥接起来，给出可证明正确的查询算法，从而在无物理复现的情况下完成 sim-to-real 验证。
Q3: 论文如何解决这个问题？
论文将“仿真-现实一致性验证”转化为一个带标签时间序列的查询问题，并给出完整技术路线，可概括为 “形式建模 → 语法翻译 → 对象对应 → 符号仿真 → 正确性保证” 五步。核心内容如下（按方法论章节顺序）。
1. 形式建模：用 SCENIC 描述候选失效场景
将仿真中发现的失效场景写成 SCENIC 程序
初始条件：nP.Initn𝑃n.n𝐼n𝑛n𝑖n𝑡n 给出对象初始位姿分布
行为：nP.nbnon𝑃n.n𝑏n𝑜n 为每个对象定义输入→输出原语集合的映射
语义：程序 nPn𝑃n 定义轨迹集合 nTnPn={σ=⟨(nin0n,non0n),…,(ninmn,nonmn)⟩n∣n∣nin0n∈Supp(P.Init),nonjn∈P.b(nin0n..ninjn)}n𝑇n𝑃n=n{n𝜎n=n⟨n(n𝑖n0n,n𝑜n0n)n,n…n,n(n𝑖n𝑚n,n𝑜n𝑚n)n⟩n|n𝑖n0n∈nSnunpnpn(n𝑃n.n𝐼n𝑛n𝑖n𝑡n)n,n𝑜n𝑗n∈n𝑃n.n𝑏n(n𝑖n0n.n.n𝑖n𝑗n)n}n 查询目标即判断真实标签轨迹是否与 nTnPn𝑇n𝑃n 有交集。
2. 语法翻译：SCENIC → 层次有限状态机 (HFSM)
对表 1 所列片段，语法导向地将每个行为编译成 HFSM
状态 nsn𝑠n 可嵌套子机 nμ(s)n𝜇n(n𝑠n)n迁移守卫 ngn𝑔n 用非线性实数算术 SMT 公式编码
未观测参数（如 Range(1,15)）作为存在量词变量进入守卫公式
结果：得到对象级 HFSM 字典 nMn𝑀n，与程序 nPn𝑃n 语义等价但可执行符号仿真。
3. 对象对应：SMT 编码 + 迭代阻断
问题：程序里叫 ego、otherCar，标签里只有 car1, car2, …
做法：
按类型与最短观测时长剪枝，生成部分注入映射集合
用线性整数算术 SMT 公式 nϕn𝜙n 一次性枚举可能对应
每失败一次，加一条阻断子句 nϕn′n𝜙n′n 排除该映射，直至找到匹配或 nϕn𝜙n 不可满足
保证：最终会尝试所有可行对应，无漏检。
4. 符号仿真：滑动窗口 + ValidStep 剪枝
算法 2 给出单对应+单窗口验证流程：
滑动窗口长度 nmn𝑚n 遍历标签轨迹
InitialInputMatch：用前工作[20]的 SMT 例程检查窗口首帧是否落在 nP.Initn𝑃n.n𝐼n𝑛n𝑖n𝑡n 支撑集
初始化各 HFSM 至基态集合（叶子状态）
对窗口内每一步：
ValidStep 自底向上重建当前层次状态
用当前观测值求解守卫，得到所有可迁移基态
与标签给出的观测原语取交集，剪掉不一致状态
若任一对象基态集为空 → 当前窗口不匹配
若整窗口走完仍非空 → 存在程序轨迹与标签轨迹一致，返回 True
复杂度：
时间序列长度 nTn𝑇n → 线性 nO(T)n𝑂n(n𝑇n)n对象数 nnn𝑛n → 对应空间 nn!n𝑛n!n，实验中用剪枝+SMT 仍呈指数，但 8 对象内可接受（10 s 超时）
5. 正确性保证
定理 1（概要）：
算法输出 Truen⇔ 存在长度-nmn𝑚n 窗口及对象对应，使得n(1) 窗口首帧在 nP.Initn𝑃n.n𝐼n𝑛n𝑖n𝑡n 支撑集，且n(2) 窗口输出序列 n∈nTnPn∈n𝑇n𝑃n
证明思路：
枚举所有对应与窗口 → 完备
InitialInputMatch + ValidStep 按 NFA 模拟标准论证，每步保持“当前基态集合 = 与观测一致的所有可达状态” → 归纳可得等价性
守卫仅依赖当前输入（片段无赋值语句）→ 无历史依赖，保证符号仿真与程序语义一致
6. 实验验证
准确性：nuScenes 400 段 20 s 视频，4 个失效场景，平均准确率nClaude 0.45，GPT-4o 0.60，本文算法 0.80；运行时间 0.06 s vs 6–41 s
规模：
视频时长 20–100 帧 → 查询时间线性增长
对象数 2–8 → 随 n𝑛!n𝑛n!n 指数增长，但 6 对象内仍<2 s
结论
通过“SCENIC→HFSM→SMT 符号仿真” pipeline，论文首次实现了nn形式语义保证n毫秒级查询n直接作用于已有标签数据集nn无需物理复现即可判断仿真失效场景是否真实存在，从而解决 sim-to-real 验证的可扩展性与准确性瓶颈。
Q4: 论文做了哪些实验？
论文围绕 “准确性” 与 “可扩展性” 两个假设共设计 2 组实验，全部在 带标签的 nuScenes 视频 与 CARLA 合成标签序列 上完成。实验细节与结果如下（均取自原文第 5 章及附录）。
1. 准确性实验（Accuracy Experiment）
维度t设置
数据tnuScenes 波士顿城区 RGB 视频 400 段（20 s，40 帧/段）；已含 3D 边框、车道、类别等标签
场景t4 个安全关键场景（SCENIC 程序手工编写）
1. 跟车→遇静止车辆→换道
2. 无保护左转等待对向车
3. 同车道前方行人→减速跟随
4. 右转前让行对向车
查询集t每场景 5 段正例 + 若干负例（共 20 段）；正例经人工肉眼确认
基线t当前最强视觉-语言模型：GPT-4o [31]、Claude-3.5 [32]
评价指标t准确率 = 正确数 / 5；运行时间（秒）
VLM 提示t附录 B 给出 200+ 词细粒度 prompt，要求
① 判断视频是否包含场景 ≥ ½ 时长；
② 给出对象对应截图，防止乱猜
主要结果（表 4）
方法t平均准确率t平均耗时
Claude-3.5t0.45 ± 0.19t6.33 ± 1.04 s
GPT-4ot0.60 ± 0.28t41.19 ± 27.57 s
本文算法t0.80 ± 0.23t0.06 ± 0.07 s
速度：比 GPT-4o 快 3 个数量级（×685），比 Claude 快 100×
精度：绝对提升 +20 %（vs GPT-4o）、+35 %（vs Claude）
误差来源：全部为标签端行为预测错误（附录 B），算法本身无假阴性/阳性。
2. 可扩展性实验（Scalability Experiment）
在 CARLA 内批量生成已知匹配的标签序列，排除标签噪声，单独观察算法随规模增长的时间开销。
2.1 随视频时长增长
变量t设置
程序t图 1 两车场景（固定 2 对象）
序列长度t20、40、60、80、100 帧（10 条/点）
窗口参数 mt½ 序列长度
结果t图 5 左：运行时间 vs 帧数 线性增长，R²≈0.98
2.2 随对象数量增长
变量t设置
程序t复制图 1 行为，得到 2、4、6、8 个对象（n! 对应空间）
序列长度t固定 100 帧
结果t图 5 右：运行时间随 n 呈指数增长
8 对象时 8! = 40 320 种对应，超时阈值 10 s
3. 附加微观实验（在附录）
守卫求解微基准：cvc5 求解 Range/距离等非线性守卫，平均 2.1 ms/调用
标签噪声敏感度：向行为标签注入 5 %、10 % 错误，准确率分别下降 3 %、8 %，仍高于 VLM 基线
结论性数字
0.06 s：查询 20 段 20 s 视频总耗时
685×：相比 GPT-4o 的速度倍率
100 帧：线性缩放上限（时长维度）
6 对象：指数缩放可接受上限（对应维度）
实验覆盖 真实公开数据 + 合成可控数据，验证了论文提出的两条核心假设：
高准确性（显著优于现有 VLM）
可扩展性（时长线性，对象指数但可接受）
Q5: 有什么可以进一步探索的点？
以下问题与方向可直接在论文框架上继续深入，按“短期可扩展”与“长期挑战性”两级列出，并给出可能方法或预期收益。
一、短期可扩展（1–2 年内可验证）
#t探索点t现状局限t可能做法t预期收益
1t更大 SCENIC 片段t表 1 禁止赋值→行为无记忆t引入“局部变量+冻结语义”或“有限历史抽象”t支持跟车加速度积分、红绿灯记忆等场景
2t快速对象对应t对象数 n>8 时 n! 爆炸t① 基于轨迹相似度的剪枝 ② 贪心+局部搜索 ③ 图匹配启发式t将指数→多项式平均复杂度，支持 ≥12 对象
3t多模态标签融合t仅用 3D 边框+行为t引入 LiDAR/Radar 语义分割、HD-Map 元素t可查询“湿滑路面+低能见度”等跨模态场景
4t在线流查询t当前只支持离线批处理t采用增量 SMT+滑动窗口缓存t实时发现路测日志中的危险片段，无需等待上传
5t标签噪声鲁棒t行为预测错 5 % 即降精度t① 概率观测模型 ② 最大容忍交集准则 ③ 贝叶斯更新t准确率从 0.80→0.90，降低人工重标成本
二、长期挑战性（3–5 年研究）
#t探索点t现状局限t可能做法t预期收益
6tsim-to-real 差距量化t仅二值“匹配/不匹配”t引入 Wasserstein 距离或最大均值差异，计算“场景级差距”t给出“仿真失效在真实世界发生概率”数值估计
7t场景程序自动合成t手工编写 SCENICt反例引导的归纳合成（CEGIS）+ LLM 辅助t从仿真失效轨迹直接生成查询程序，零人工
8t对抗式标签攻击t标签被恶意篡改可绕过验证t结合区块链签名+可信硬件时间戳t保证路测数据与标签不可抵赖，满足法规审计
9t连续状态+时间语义t当前离散时间步t引入混成自动机或信号时序逻辑（STL）t支持“0.3 s 内碰撞时间<1.5 s”的连续时序查询
10t联邦查询t数据分散在 OEM 无法集中上传t使用隐私保护的联邦 SMT（同态加密+OBDD 共享）t各车企联合验证共性失效，无需泄露原始数据
三、交叉领域衍生方向
与生成式模型互补
用本文算法检索“稀有正例”，再送入扩散模型做数据增强，可缓解真实危险场景样本不足问题。
法规认证接口
将查询结果直接输出为 ISO 26262 / UL 4600 所需的“场景覆盖度”证据包，减少安全审核人工工作量。
闭环自动修复
一旦查询确认真实存在失效，立即触发仿真再训练→生成补丁→OTA 更新，形成“发现-验证-修复”闭环。
可立即着手的“最小可行”下一步
在现有代码库上把对象对应模块替换成“相似度剪枝 + 贪心匹配”，用 6–10 对象场景跑消融实验，即可在 1–2 个月内拿到第一条“指数→线性”改进曲线，作为后续论文的突破口。
Q6: 总结一下论文的主要内容
论文提出并解决“仿真-现实一致性验证”的核心难题：
“仿真里发现的自动驾驶失效场景，能否在真实传感器数据中复现？”
1. 问题定义
仿真-真实传感器差异（sim-to-real gap）使仿真失效可能仅为“合成数据假象”。
传统物理复现成本高、不可扩展。
→ 需要自动、可证明、可扩展的手段，在已标注真实数据里查找与仿真场景语义一致的片段，再验证系统是否同样失效。
2. 技术路线（四步）
形式建模
用 SCENIC 概率编程语言将候选失效场景写成“场景程序”P，定义初始分布与对象行为。
语法翻译
把 P 自动编译为**层次有限状态机(HFSM)**网络，守卫用 SMT 公式编码，保持语义等价。
对象对应 + 滑动窗口
未知对象映射：SMT 一次性枚举所有类型-兼容注入，失败即阻断，直至穷尽。
对每条长度 m 窗口：n– 检查首帧是否落在 P 初始分布支撑集；n– 符号仿真每一步，只保留与标签观测一致的 HFSM 基态；n– 任一对象基态集为空 → 窗口不匹配。
正确性保证
算法输出 True 当且仅当存在窗口与对象对应，使得窗口轨迹属于程序轨迹集 T_P（定理 1，归纳法证明）。nn3. 实验结果n准确性：nuScenes 400 段视频 × 4 安全场景n– 相比 GPT-4o / Claude，平均准确率提升 20–35 %，运行时间快 2–3 个数量级（0.06 s vs 6–41 s）。n可扩展性：n– 视频时长 20–100 帧 → 查询时间线性增长；n– 对象数 2–8 → 对应搜索呈指数，但 6 对象内仍<2 s（10 s 超时）。n4. 贡献一句话nn首次把“仿真失效场景”转化为“对带标签时间序列的形式化查询”，给出可证明正确、毫秒级、适用于任意传感器模态的查询算法，实现无需物理复现的 sim-to-real 验证。
来源：Arxiv2025-11-13 18:52:27 UTC
