面向神经反馈环路安全验证的约束感知细化策略

神经网络（NN）正越来越多地被用于自主系统控制管道的设计中。然而，由于在非分布数据或对抗性攻击存在时，NN 的性能可能恶化，包含 NN 的系统即神经反馈环路（NFL），在应用于安全关键场景前需要获得安全保障。可达性分析提供了解决方案，通过计算 NFL 的可达集来界定其未来状态的可能范围，可用于检查状态空间中的危险区域，以验证系统是否满足安全约束。由于精确的可达集通常难以计算，通常使用可达集近似（RSOA）。RSOA 的问题在于其可能过于保守，尤其是在长时间尺度或高度非线性 NN 控制策略下，更难以验证安全约束的满足。分区或符号传播等细化策略通常用于限制 RSOA 的保守性，但这些方法计算成本高，往往只能用于验证简单的可达性问题。本文提出了用于验证的约束感知细化策略（CARV）：一种高效的细化方法，通过显式利用 NFL 对安全约束的约束，仅在必要时对 RSOA 进行细化，从而减少其保守性。我们展示，CARV 能够验证 NFL 的安全性，而其他方法要么失败，要么需要最长高达 60 倍、内存高达 40 倍。