Exact Verification of ReLU Neural Control Barrier Functions
Exact Verification of ReLU Neural Control Barrier Functions
复制标题
DOI：
10.48550/arxiv.2310.09360
复制
发表时间：
2023-10
期刊：
影响因子：
--
通讯作者：
Hongchao Zhang;Junlin Wu;Yevgeniy Vorobeychik;Andrew Clark
中科院分区：
文献类型：
--
作者：
Hongchao Zhang;Junlin Wu;Yevgeniy Vorobeychik;Andrew Clark
控制障碍函数（CBFs）是一种常用的非线性系统安全控制方法。在基于CBF的控制中，系统所需的安全特性被映射到CBF的非负性，并选择控制输入以确保CBF始终保持非负。最近，将cbf表示为神经网络（神经控制障碍函数，或ncbf）的机器学习方法由于神经网络的普遍可表征性而显示出很大的前景。然而，验证习得的CBF是否能保证安全性仍然是一个具有挑战性的研究问题。本文提出了验证具有ReLU激活函数的前馈ncbf安全性的新的精确条件和算法。这样做的关键挑战是，由于ReLU函数的分段线性，NCBF在某些点上是不可微的，从而使假设平滑屏障函数的传统安全验证方法无效。利用证明非光滑边界集合不变性的Nagumo定理的推广，推导出安全的充分必要条件，从而解决了这个问题。基于此，我们提出了一种NCBF的安全性验证算法，该算法首先将NCBF分解为分段线性段，然后求解非线性程序来验证每个段以及线性段的交叉点的安全性。通过只考虑安全区域的边界，利用区间界传播（IBP）和线性松弛对区段进行剪枝，降低了复杂度。我们通过数值研究来评估我们的方法，并与最先进的基于smt的方法进行比较。我们的代码可在https://github.com/HongchaoZhang-HZ/exactverif-reluncbf-nips23上获得。
Control Barrier Functions (CBFs) are a popular approach for safe control of nonlinear systems. In CBF-based control, the desired safety properties of the system are mapped to nonnegativity of a CBF, and the control input is chosen to ensure that the CBF remains nonnegative for all time. Recently, machine learning methods that represent CBFs as neural networks (neural control barrier functions, or NCBFs) have shown great promise due to the universal representability of neural networks. However, verifying that a learned CBF guarantees safety remains a challenging research problem. This paper presents novel exact conditions and algorithms for verifying safety of feedforward NCBFs with ReLU activation functions. The key challenge in doing so is that, due to the piecewise linearity of the ReLU function, the NCBF will be nondifferentiable at certain points, thus invalidating traditional safety verification methods that assume a smooth barrier function. We resolve this issue by leveraging a generalization of Nagumo's theorem for proving invariance of sets with nonsmooth boundaries to derive necessary and sufficient conditions for safety. Based on this condition, we propose an algorithm for safety verification of NCBFs that first decomposes the NCBF into piecewise linear segments and then solves a nonlinear program to verify safety of each segment as well as the intersections of the linear segments. We mitigate the complexity by only considering the boundary of the safe region and by pruning the segments with Interval Bound Propagation (IBP) and linear relaxation. We evaluate our approach through numerical studies with comparison to state-of-the-art SMT-based methods. Our code is available at https://github.com/HongchaoZhang-HZ/exactverif-reluncbf-nips23.