Exact Verification of ReLU Neural Control Barrier Functions
Hongchao Zhang Junlin Wu Yevgeniy Vorobeychik Andrew Clark
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.