通过深度强化学习和PAC验证为自动驾驶提供一种可证明的安全性度量方法

《TRANSPORTATION RESEARCH PART C-EMERGING TECHNOLOGIES》：A provable safety metric for autonomous driving via deep reinforcement learning and PAC verification

自动驾驶安全评估中，现有定量指标缺乏可证明可靠性，而定性指标过度保守。本文提出Provable Minimum Collision Time（PMCT）安全指标，通过DRL构建风险基状态集划分并采用PAC验证，实现碰撞时间下限的可证明预测，同时降低误报率。

　　

范凌翔|何林轩|冯硕

清华大学自动化系，北京，100084，中国

摘要

实时安全指标对自动驾驶的安全至关重要，它们可以在存在碰撞风险时触发警告，以便人类驾驶员接管控制或激活紧急系统。由于在高维驾驶环境中安全关键事件的罕见性，大多数现有的定量指标缺乏对其可靠性的正式保证，而一些定性指标虽然可以被证明，但只能提供具有高度保守性的二元安全判断。为了克服这些限制，我们提出了一种可证明的定量安全指标，该指标能够实时预测碰撞时间下限，并具有理论保证和可接受的保守性，称为“可证明的最小碰撞时间”（Provable Minimum Collision Time，简称PMCT）。我们将PMCT的计算表述为一个基于风险的最优状态集划分问题，并通过结合深度强化学习进行划分构建和基于概率近似正确性（PAC）的验证来确保PMCT的可靠性。广泛的实验证实了PMCT的可证明性，并展示了其在识别危险情况方面的更高召回率，同时显著减少了误报。

引言

自从深度学习出现以来（LeCun等人，2015年），自动驾驶技术发展迅速。尽管数据驱动的模型为自动驾驶车辆（AVs）提供了增强的决策能力，但大规模模型的黑箱性质使得它们的决策不可靠，可能在未经训练的场景中导致严重事故。为了解决自动驾驶安全方面的挑战，采用了安全指标（Committee，2021年）来监控实时驾驶状况。通过收集关于AV及其周围背景车辆（BVs）的观测数据来计算实时安全性评估，这些指标可以在存在碰撞风险时触发警告，以便人类驾驶员接管控制或激活紧急系统。鉴于实时安全指标在确保大规模部署中AV安全方面的关键作用，确保它们在实时碰撞预测和警告方面的可靠性能至关重要。为了实现这种可靠性，实时安全指标应该是可证明的，即对其安全性评估提供正式保证。例如，正式保证可以采取碰撞预测失败率有界且可接受的形式（He等人，2025年）。

现有的安全指标主要是定量的且没有可证明性，它们基于车辆的显式模型预测与自动驾驶系统相关的碰撞风险。这些指标大致可以分为三类：基于时间的、基于规避动作的以及结合多种指标的（Cheng等人，2025年；Wang等人，2021年）。基于时间的指标通过时间接近度来衡量交互风险。这类指标在之前的车辆性能研究中得到了广泛应用，包括碰撞时间（TTC）（Hayward，1972年）和侵入后时间（PET）（Hayward，1972年）。后续的发展引入了变体，如暴露时间TTC（Minderhoud和Bovy，2001年）、积分时间TTC、穿越车道时间（van Winsum等人，2000年）、修改后的TTC（Ozbay等人，2008年）和时间优势（TA）（Laureshyn等人，2010年），这些变体在早期指标的基础上进行了各种改进。基于规避动作的指标，如避免碰撞所需的减速率（Cooper和Ferguson，1976年）、临界性指数函数（Chan，2006年）和碰撞潜力指数（Cunto，2008年），侧重于避免碰撞所需的规避操作，作为冲突情况下制动需求的直接指标。结合多种指标的方法将多维动态和不同的安全指标（包括时间和规避动作）整合到一个层次化的安全评估中，用于2D冲突，例如扩展的TTC（Ward等人，2015年）、预期碰撞时间（ACT）、规避动作时间（Venthuruthiyil和Chunchu，2022年）以及2D-TTC（Guo等人，2023年）。最近提出的先进指标提供了新的概念和更全面、更整体的评估框架。值得注意的例子包括责任敏感的安全模型，它为AV定义了安全距离的计算原则（Shalev-Shwartz等人，2017年）；PEGASUS临界性指标，它提供了一个量化场景风险水平的框架（Junietz等人，2018年）；以及模型预测瞬时安全指标（MPrISM），它使用极小极大优化来量化最坏情况下的碰撞时间（Weng等人，2020年）。

然而，这些定量指标存在几个固有的挑战。首先，自动驾驶系统涉及复杂的车辆动态和众多交通参与者，导致高维的环境变量和大量可能的场景。因此，很难确保这些指标在所有可能的情况下都能可靠地检测到碰撞。其次，安全关键事件很少发生，因此评估这些指标在所有这些罕见事件上的性能极具挑战性，这导致预测边缘情况风险的失败率不确定（Feng等人，2023年；Liu和Feng，2024年）。这些挑战在现有的定量指标中基本上没有得到解决，导致它们在安全关键事件中的可靠性有限，从而限制了它们在现实世界中的使用。

与定量指标相比，第二类是定性安全指标，它们通过可证明的方法提供正式保证。这些方法通常将给定场景分类为安全或不安全，并为被确定为安全的场景提供正式保证。例如，基于可达性分析的指标（Althoff，2010年；Althoff和Dolan，2014年；Orzechowski等人，2019年；Zhao等人，2023年）推导出AV和BV在时间范围内的可达集，并通过检查这些集合是否有非空交集来确定安全性。此外，基于不变集的指标（Kianfar等人，2013年；Weng等人，2022年）构建了AV操作状态空间的一个子集，确保除了极少数状态之外的所有状态的安全性或几乎安全性，并通过概率验证（Weng等人，2021年）。然而，这些指标无法量化其正式保证的安全集之外的区域的碰撞风险水平。因此，这些指标将AV限制在狭义定义的安全区域内运行，通常导致高度保守性（Liu等人，2021年）。

为了克服这些挑战并量化碰撞风险，本文提出了一种可证明的定量安全指标，称为“可证明的最小碰撞时间”（Provable Minimum Collision Time，简称PMCT）。PMCT提供了碰撞时间下限的实时可证明预测。本文的总体框架如图1所示。我们的目标不仅是预测任何给定状态的碰撞时间的严格下限，还要最小化此类预测中的过度保守性。具体来说，我们将碰撞时间离散化为几个“最小步骤到碰撞”（Minimum Steps to Collision，简称MSC）类别，这些类别代表碰撞所需的最小步骤数。这种离散化将无限状态空间映射到有限数量的MSC类别上，使其可以被划分为有限数量的子集，每个子集都与特定的MSC值相关联。因此，可以在子集级别执行下限预测的验证和保守性的优化，使得这一过程在计算上是可行的。通过这种方式，我们将PMCT的计算表述为一个最优状态集划分问题。

为了捕捉子集之间的转换关系并在高维状态空间中构建这种划分，使用了深度强化学习（DRL）方法。网络的价值函数将状态映射到相应的MSC类别，从而提供了划分的可行构建。在网络训练期间明确优化了划分，以减少其固有的保守性。此外，在网络训练过程中采用了基于PAC的方法（Valiant，2013年）来验证构建的集合划分。然后，将这种验证过的划分实例化为实时安全指标PMCT，确保碰撞时间的可证明下限。此外，该划分还能够推导出系统在有限时间范围内的总体碰撞风险的上限，支持离线安全评估。在与现有指标的比较实验中，PMCT展示了其在识别危险情况方面的更高召回率，同时显著减少了误报。本文的主要贡献总结如下。

•

基于风险的状态集划分：我们提出了一种基于风险的状态集划分及其可证明性定理。该框架基于碰撞风险对自动驾驶系统中所有可能的状态进行了可证明的分类，并进一步将其实例化为称为PMCT的安全指标。该指标预测碰撞时间下限，并对其成功率提供了正式保证。实验表明，PMCT在识别危险情况方面的能力更强，召回率更高，同时显著减少了误报。

•

基于DRL的构建和基于PAC的验证算法：我们提出了一种基于深度强化学习框架的算法来解决状态划分问题。该算法结合了使用基于概率近似正确性（PAC）方法的严格验证，为高维自动驾驶系统中的可证明安全性评估提供了可行的实现。

•

系统碰撞风险的可证明上限：在划分的基础上，我们推导出了系统在有限时间范围内的形式验证的上限。这为系统的安全性能提供了概率保证，有可能实现符合相关工业标准的离线安全评估。

本文的其余部分组织如下：第2节介绍了本文中使用的符号、场景定义、状态集和模拟运行。第3节描述了我们提出的方法论，包括不安全子集划分及其验证理论、我们使用的DRL网络、我们提出的可证明安全指标以及特定自动驾驶系统中总碰撞风险的计算。第4节介绍了所提指标的可证明性实验结果以及与其他安全指标的实时实验结果比较。最后，第5节总结了本文。缩写和符号列在表1和表2中。

章节片段

初步

我们首先正式化了本文中使用的符号，包括自动驾驶场景、状态集和模拟运行。

场景被建模为一个离散时间序列，在该序列中，交通参与者表现出非线性运动动态。让$\Delta t\in R$表示时间间隔，$K\in N_{+}$表示步骤总数。所有参与者在时间t的状态向量（例如AV及其周围的BVs）表示为$x_t\in R^n$，$u_t\in R^a$表示时间t的动作向量，其中t∈{0, 1, ..., K。

方法

为了可证明地量化可行集合内每个状态的实时碰撞风险，我们将碰撞风险预测表述为一个最优状态集划分问题（如问题1所示），并引入了一个基于风险的划分，称为ε-Unsafe Subset Partition（ε-USP）来解决这个问题。该划分将状态分组为子集，每个子集代表一个特定的风险水平，由其最小步骤到碰撞来量化。随后，建立了定理1来验证构建的ε-USP

实验

在本节中，我们在SUMO（Lopez等人，2018年）构建的微观交通模拟器和TeraSim（Sun等人，2025年）构建的复杂城市道路系统中评估了所提出的方法。我们进行了网络训练和验证实验来验证所提出的方法论。我们部署了PMCT进行实时安全评估，并实验性地验证了其可证明性，同时比较了性能

结论

总之，本文提出了一种用于自动驾驶车辆的可证明安全指标PMCT。通过使用基于PAC的验证方法和基于DRL的网络进行最优状态集划分，PMCT提供了可证明的最小碰撞时间预测和系统碰撞风险的可证明上限。前者实现了可靠的实时碰撞警报和碰撞避免辅助，后者促进了符合相关工业标准的离线安全评估。

代码可用性

代码可在https://github.com/THU-AI-Testing/PMCT-master获取。

CRediT作者贡献声明

范凌翔：写作 – 审稿与编辑，撰写原始草稿，可视化，软件，方法论，形式分析，数据整理。何林轩：写作 – 审稿与编辑，方法论，调查，形式分析，概念化。冯硕：写作 – 审稿与编辑，撰写原始草稿，验证，监督，项目管理，形式分析，概念化。