Control barrier functions (CBFs) are a popular tool for safety certification of nonlinear dynamical control systems. Recently, CBFs represented as neural networks have shown great promise due to their expressiveness and applicability to a broad class of dynamics and safety constraints. However, verifying that a trained neural network is indeed a valid CBF is a computational bottleneck that limits the size of the networks that can be used. To overcome this limitation, we present a novel framework for verifying neural CBFs based on piecewise linear upper and lower bounds on the conditions required for a neural network to be a CBF. Our approach is rooted in linear bound propagation (LBP) for neural networks, which we extend to compute bounds on the gradients of the network. Combined with McCormick relaxation, we derive linear upper and lower bounds on the CBF conditions, thereby eliminating the need for computationally expensive verification procedures. Our approach applies to arbitrary control-affine systems and a broad range of nonlinear activation functions. To reduce conservatism, we develop a parallelizable refinement strategy that adaptively refines the regions over which these bounds are computed. Our approach scales to larger neural networks than state-of-the-art verification procedures for CBFs, as demonstrated by our numerical experiments.

翻译：控制屏障函数（CBFs）是非线性动态控制系统安全认证的常用工具。近年来，以神经网络表示的控制屏障函数因其表达能力强大且适用于广泛的动力学模型与安全约束而展现出巨大潜力。然而，验证训练后的神经网络是否为有效的控制屏障函数是一个计算瓶颈，限制了可使用的网络规模。为克服这一限制，我们提出了一种基于分段线性上下界的新型验证框架，用于检验神经网络满足控制屏障函数所需的条件。该方法植根于神经网络的线性边界传播（LBP）技术，我们将其扩展至计算网络梯度的边界。结合麦考密克松弛方法，我们推导出控制屏障函数条件的线性上下界，从而避免了计算成本高昂的验证过程。本方法适用于任意控制仿射系统及广泛的非线性激活函数。为降低保守性，我们开发了一种可并行化的精细化策略，自适应地优化计算这些边界的区域划分。数值实验表明，相较于控制屏障函数验证领域的最先进方法，本方案能够扩展到更大规模的神经网络。