可达多面体行进 (RPM)：一种用于含深度神经网络组件机器人系统的安全验证算法

我们提出了一种计算具有修正线性单元 (ReLU) 激活的深度神经网络精确可达集的方法。我们的方法非常适用于对含深度神经网络组件的机器人感知与控制系统进行严格的安全性分析。我们的算法能够计算在机器人系统感知-动作回路中出现的、跨多个时间步迭代的 ReLU 网络的前向与后向可达集。我们的算法独特之处在于，它通过增量式枚举输入空间中的多面体单元来构建可达集，而非像其他方法那样逐层遍历网络。若发现不安全单元，我们的算法可在未完成完整可达性计算的情况下返回该结果，从而具备加速安全验证的 anytime 特性。此外，与现有方法中内存可能成为限制因素的情况相比，我们的方法在执行过程中所需内存更少。我们在 ACAS Xu 飞机告警系统的安全验证上演示了我们的算法。我们发现不安全动作的速度比最快的现有方法快许多倍，并在约两倍于现有方法的时间内证明了不存在不安全动作。我们还在笔记本电脑上以 87 秒计算了摆动力学学习模型在 50 个时间步范围内的前向与后向可达集。算法源代码：https://github.com/StanfordMSL/Neural-Network-Reach。