协同单形：面向安全关键自主系统的协作式运行时保障

# 安全关键自主系统的协同运行时保证 ⋆同等贡献。本材料基于美国国家航空航天局（NASA）根据合作协议 80NSSC20M0229 和大学领导倡议拨款编号 80NSSC22M0070 以及美国国家科学基金会（NSF）根据拨款编号 CNS 1932529 和 ECCS 2311085 支持的工作。本材料中表达的任何观点、发现、结论或建议均为作者所有，不一定反映赞助方的观点。来源：https://arxiv.org/html/2605.08190 Ayoosh Bansal⋆\\star,1Mikael Yeghiazaryan⋆\\star,1Artyom Khachatryan2Tianyi Zhu3 Hunmin Kim4Naira Hovakimyan1Lui Sha1 ###### 摘要 自主系统日益依赖机器学习（ML）组件来执行安全关键任务，例如自动驾驶汽车（AV）中的感知和控制。虽然 ML 使能了基本能力，但它不可避免地表现出长尾故障，使其不适合用于安全关键任务。运行时保证（RTA）通过将 ML 组件与可验证的安全监控器配对来缓解此问题，例如 Control Simplex 和 Perception Simplex 架构。然而，安全监控器的性能有限仍然是一个主要瓶颈。协同 Simplex（SS$\mathcal{SS}$）架构通过实现 ML 组件与安全监控器之间的双向集成，同时保持形式化安全保证，从而提高系统性能。此处的关键创新是允许安全监控器使用 ML 输出，这通常在 RTA 系统中是被禁止的。我们形式化推导了这种集成保持安全的条件，并展示了性能优势。我们介绍了用于 AV 障碍物检测的 SS$\mathcal{SS}$ 的设计、分析和评估。 ## I 引言 自主系统正在迅速进步，由机器学习（ML）在实现复杂自主任务方面的突破所驱动。在这些系统中，自动驾驶汽车（AV）体现了对 ML 的依赖，用于对车辆安全目标至关重要的功能，例如感知。尽管具有巨大的潜力，但这种基于 ML 的系统提出了重大的安全挑战，因为部署用于安全关键任务的 ML 组件中的故障可能产生严重后果。虽然基于 ML 的组件取得了令人印象深刻的实证性能，但它们本质上是不可验证的，因此容易受到意外故障的影响\[45 (https://arxiv.org/html/2605.08190#bib.bib110),18 (https://arxiv.org/html/2605.08190#bib.bib111),35 (https://arxiv.org/html/2605.08190#bib.bib112),56 (https://arxiv.org/html/2605.08190#bib.bib115),10 (https://arxiv.org/html/2605.08190#bib.bib113)\]。Suet al.\[50 (https://arxiv.org/html/2605.08190#bib.bib83)\]表明，即使是人类无法察觉的单个像素扰动，也可能 drastic 改变 ML 输出。这种脆弱性引发了人们对建立在根本不可靠的 ML 组件之上的自主系统安全的严重担忧\[25 (https://arxiv.org/html/2605.08190#bib.bib105),55 (https://arxiv.org/html/2605.08190#bib.bib103),38 (https://arxiv.org/html/2605.08190#bib.bib104),1 (https://arxiv.org/html/2605.08190#bib.bib101),44 (https://arxiv.org/html/2605.08190#bib.bib100),41 (https://arxiv.org/html/2605.08190#bib.bib106),42 (https://arxiv.org/html/2605.08190#bib.bib109),43 (https://arxiv.org/html/2605.08190#bib.bib108),40 (https://arxiv.org/html/2605.08190#bib.bib95)\]。 解决这一问题的方案是运行时保证（RTA）设计，其中简单的可验证组件监控并约束复杂的高性能组件，确保系统保持在安全操作区域内。这一想法由 Sha 作为控制系统的 Simplex 架构率先提出\[49 (https://arxiv.org/html/2605.08190#bib.bib45)\]。此后，RTA 设计日益突出，激发了许多改进和适应\[13 (https://arxiv.org/html/2605.08190#bib.bib46),4 (https://arxiv.org/html/2605.08190#bib.bib47),17 (https://arxiv.org/html/2605.08190#bib.bib99),46 (https://arxiv.org/html/2605.08190#bib.bib78),47 (https://arxiv.org/html/2605.08190#bib.bib84),37 (https://arxiv.org/html/2605.08190#bib.bib85),14 (https://arxiv.org/html/2605.08190#bib.bib86)\]。安全关键系统中基于 ML 的感知的日益使用促进了感知 Simplex（PS$\mathcal{PS}$）的开发\[5 (https://arxiv.org/html/2605.08190#bib.bib10),6 (https://arxiv.org/html/2605.08190#bib.bib36)\]。PS$\mathcal{PS}$将 RTA 设计适应于感知系统，在 AV 的基于 ML 的感知中存在障碍物检测故障的情况下为 AV 提供安全护栏。虽然PS$\mathcal{PS}$在特定约束下保证安全，但由于保守性，即使在没有 ML 故障的情况下，它也可能导致性能大幅下降。请参阅标题图 1：协同 Simplex（SS$\mathcal{SS}$）架构概述，扩展自 Perception Simplex\[6 (https://arxiv.org/html/2605.08190#bib.bib36)\]。与传统运行时保证设计一样\[49 (https://arxiv.org/html/2605.08190#bib.bib45),13 (https://arxiv.org/html/2605.08190#bib.bib46),4 (https://arxiv.org/html/2605.08190#bib.bib47),17 (https://arxiv.org/html/2605.08190#bib.bib99)\]，ML 层执行系统任务，安全层强制执行确定性护栏。协同 Simplex通过利用层之间的双向通信改进了先前的设计。 这项工作通过引入两个互补层之间的整体双向集成来解决 PS$\mathcal{PS}$等 RTA 设计的性能限制：经过广泛验证但不可验证的基于 ML 的层，负责尽最大努力执行任务；以及可验证的安全层，负责强制实施确定性安全属性。在本协同 Simplex（SS$\mathcal{SS}$）设计中，如图 1 (https://arxiv.org/html/2605.08190#S1.F1) 所示，这两个部分冗余的层合作以提高系统性能，而不违反安全保证。安全认证标准禁止安全层使用不可验证的 ML 生成的信息\[23 (https://arxiv.org/html/2605.08190#bib.bib116),15 (https://arxiv.org/html/2605.08190#bib.bib117)\]，例如，在 PS$\mathcal{PS}$中，在安全层中使用由 ML 组件生成的车道边界信息进行障碍物检测和碰撞避免。SS$\mathcal{SS}$在形式化陈述的条件下克服了这一限制（第三节-B (https://arxiv.org/html/2605.08190#S3.SS2)），在提高性能的同时保持安全保证（第六节 (https://arxiv.org/html/2605.08190#S6)）。 这项工作的主要贡献是： - •协同 Simplex（SS$\mathcal{SS}$）架构，利用安全层和 ML 层之间的协同交互*以提高整体系统性能，同时保持形式化安全保证*（第三节 (https://arxiv.org/html/2605.08190#S3)）。 - •SS$\mathcal{SS}$的形式化安全分析，推导双向 ML-安全通信保持 PS$\mathcal{PS}$的确定性安全保证的条件（第三节-A (https://arxiv.org/html/2605.08190#S3.SS1)和第三节-B (https://arxiv.org/html/2605.08190#S3.SS2)）。 - •用于 AV 的参考 SS$\mathcal{SS}$设计（第四节 (https://arxiv.org/html/2605.08190#S4)）。 ## II 相关工作 本节回顾相关的前期工作，并将我们的贡献置于安全自主研究之中。 ### II-A 控制 Simplex 冗余长期以来一直用于通过复制或不同实现来实现安全关键信息物理系统（CPS）中的容错性\[22 (https://arxiv.org/html/2605.08190#bib.bib59),31 (https://arxiv.org/html/2605.08190#bib.bib64),7 (https://arxiv.org/html/2605.08190#bib.bib75)\]。然而，传统的计算冗余仍然容易受到学习启用组件中常见的关联和设计级故障的影响\[53 (https://arxiv.org/html/2605.08190#bib.bib71),54 (https://arxiv.org/html/2605.08190#bib.bib74),26 (https://arxiv.org/html/2605.08190#bib.bib66)\]。这种局限性促进了功能冗余，其中异构算法或传感模式减少了共享故障模式。Simplex 架构基于这一理念。Simplex 架构\[49 (https://arxiv.org/html/2605.08190#bib.bib45),13 (https://arxiv.org/html/2605.08190#bib.bib46),4 (https://arxiv.org/html/2605.08190#bib.bib47)\]是我们工作的基础。它将高性能但未经过验证的控制与简单、可验证的备份配对，在运行时进行监控。当系统接近不安全区域时，控制权会切换给安全控制器。Control Simplex 已广泛应用于 CPS 和自主性，包括诸如 R-Simplex\[52 (https://arxiv.org/html/2605.08190#bib.bib76)\]、SL1-Simplex\[36 (https://arxiv.org/html/2605.08190#bib.bib77)\] 和其他扩展\[39 (https://arxiv.org/html/2605.08190#bib.bib79)\]。Neural Simplex\[46 (https://arxiv.org/html/2605.08190#bib.bib78)\]引入了从安全控制器到复杂控制器的有限通信，以减少不必要的回退，但这种交互仅限于低级控制。相比之下，SS$\mathcal{SS}$在感知层运行，并支持更丰富的 ML-安全合作。我们将在第二节-B (https://arxiv.org/html/2605.08190#S2.SS2) 中讨论其感知层前身 Perception Simplex\[6 (https://arxiv.org/html/2605.08190#bib.bib36)\]。 ### II-B 感知 Simplex 请参阅标题图 2：基于激光雷达的障碍物检测的可检测区域，改编自\[5 (https://arxiv.org/html/2605.08190#bib.bib10)\]。虚线上方的障碍物根据其高度和距离保证被检测到。感知 Simplex（PS$\mathcal{PS}$）\[6 (https://arxiv.org/html/2605.08190#bib.bib36)\]通过将自主栈分离为不可验证的 ML 层和可验证的安全层，为 AV 提供确定性安全保证。安全层实现了一个基于经典激光雷达的障碍物存在检测器，该检测器建立在可验证障碍物检测（VOD）\[5 (https://arxiv.org/html/2605.08190#bib.bib10)\] 之上，VOD 推导了深度聚类算法\[8 (https://arxiv.org/html/2605.08190#bib.bib80),9 (https://arxiv.org/html/2605.08190#bib.bib81)\] 保证检测到障碍物的几何条件。如图 2 (https://arxiv.org/html/2605.08190#S2.F2) 所示，只要距离为 $x$ 的障碍物的高度 $y$ 满足 $y \geq kx+b$，其中 $k$ 和 $b$ 取决于传感器和算法参数，检测就得到保证。此边界实现了可证明安全的最大速度：ML 层提供高性能感知和规划，而安全层确保在车辆在此限制内运行时避免碰撞。在运行时，安全层监控 ML 层，并在检测到后者遗漏的安全关键障碍物时进行覆盖，确保在障碍物存在检测出现故障的情况下避免碰撞。然而，PS$\mathcal{PS}$仅涵盖障碍物存在（而非分类），其覆盖操作仅限于完全停止，这可能导致保守行为。SS$\mathcal{SS}$通过在这两个层之间启用经过仔细约束的双向通信来扩展 PS$\mathcal{PS}$，在保持其形式化保证的同时减少保守性。 ### II-C ML 感知的安全方法 除了基于运行时保证的设计之外，还提出了几种互补的方向来提高自主系统中基于 ML 的感知的安全性。基于 ML 的感知中的优先级反转发生在网络在整个输入上分配均匀计算时，延迟了对安全关键区域的處理\[48 (https://arxiv.org/html/2605.08190#bib.bib87)\]。之前的工作通过外部提议或启发式区域划分来缓解这一问题：Liuet al.\[34 (https://arxiv.org/html/2605.08190#bib.bib22),33 (https://arxiv.org/html/2605.08190#bib.bib23)\]、Huet al.\[19 (https://arxiv.org/html/2605.08190#bib.bib48),20 (https://arxiv.org/html/2605.08190#bib.bib49)\] 和 Chenet al.\[12 (https://arxiv.org/html/2605.08190#bib.bib13)\] 使用外部代理对摄像机或激光雷达区域进行排名。Tunget al.\[51 (https://arxiv.org/html/2605.08190#bib.bib52)\] 在聚焦卷积之前去除无关像素，Kanget al.\[27 (https://arxiv.org/html/2605.08190#bib.bib50)\] 和 Liuet al.\[32 (https://arxiv.org/html/2605.08190#bib.bib51)\] 使用感兴趣区域来聚焦 DNNs。不确定性估计提供了另一条途径，使 ML 模型能够量化其对感知输出的置信度。Kendall 和 Gal\[29 (https://arxiv.org/html/2605.08190#bib.bib118)\] 区分了深度学习中感知任务的偶然不确定性和认知不确定性，而 Lakshminarayananet al.\[30 (https://arxiv.org/html/2605.08190#bib.bib119)\] 提出了深度集成作为预测不确定性估计的可扩展方法。Araujoet al.\[2 (https://arxiv.org/html/2605.08190#bib.bib120)\] 特别在自动驾驶感知背景下调查不确定性方法。虽然这些方法可以标记可能不可靠的输出，但它们不提供确定性安全保证。神经网络的正式验证试图通过证明网络行为的属性来提供更强的正确性保证。Katzet al.\[28 (https://arxiv.org/html/2605.08190#bib.bib121)\] 引入了 Reluplex，这是一种基于 SMT 的求解器，用于验证深度神经网络，而 Huanget al.\[21 (https://arxiv.org/html/2605.08190#bib.bib122)\] 开发了 DNNs 的安全验证方法。然而，这些技术计算成本高昂，并且无法扩展到现代自主栈中使用的大型网络。相比之下，SS$\mathcal{SS}$ 不尝试直接验证或约束 ML 层。相反，它通过将 ML 层与可验证的安全层配对来保持形式化安全保证，在运行时容忍 ML 故障，而不是在设计时消除它们。 ## III 方法 我们现在提出所提出的 SS$\mathcal{SS}$ 框架的设计。我们强调 SS$\mathcal{SS}$ 不是一个独立的自主栈。它是一种架构增强，在现有、完全功能化的 ML 层之上运行，提供可验证的安全协调，而不替换任何自主组件。重要的是，SS$\mathcal{SS}$ 对底层 ML 模型是无关的，不对 ML 层的架构或算法做出假设，可以在提出动作的任何模块之上运行。在其核心，SS$\mathcal{SS}$ 扩展了 PS$\mathcal{PS}$ 架构\[6 (https://arxiv.org/html/2605.08190#bib.bib36)\]，将其单向监督结构概括为任务层和安全层之间的*双向*信息交换，如图 1 (https://arxiv.org/html/2605.08190#S1.F1) 所示。经典 Simplex 设计依赖于单向监督链接，其中安全层通过*故障处理器*监控 ML 层动作，并且仅在*安全层软件*定义的安全条件被违反时才进行干预。相比之下，SS$\mathcal{SS}$ 建立了安全层和 ML 层之间的双向信息交换架构，允许两层的软件合作，在保持形式化安全保证的同时，提高整体性能，超越 PS$\mathcal{PS}$ 所达到的水平。以下子节形式化了安全到 ML（S2M）和 ML 到安全（M2S）通信链路，并建立在其各自的假设下，这两个扩展都保留了原始 PS$\mathcal{PS}$ 架构的安全保证。 ### III-A 安全层到 ML 层通信 安全到 ML（S2M）链路，如图 1 (https://arxiv.org/html/2605.08190#S1.F1) 所示，使安全层能够传达验证过的信息