Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation

TL;DR

A new efficient verification framework for ReLU-based neural CBFs through symbolic derivative bound propagation by combining the linearly bounded nonlinear dynamic system and the gradient bounds of neural CBFs is proposed.

Abstract

Control barrier functions (CBFs) are important in safety-critical systems and robot control applications. Neural networks have been used to parameterize and synthesize CBFs with bounded control input for complex systems. However, it is still challenging to verify pre-trained neural networks CBFs (neural CBFs) in an efficient symbolic manner. To this end, we propose a new efficient verification framework for ReLU-based neural CBFs through symbolic derivative bound propagation by combining the linearly bounded nonlinear dynamic system and the gradient bounds of neural CBFs. Specifically, with Heaviside step function form for derivatives of activation functions, we show that the symbolic bounds can be propagated through the inner product of neural CBF Jacobian and nonlinear system dynamics. Through extensive experiments on different robot dynamics, our results outperform the interval arithmetic based baselines in verified rate and verification time along the CBF boundary, validating the effectiveness and efficiency of the proposed method with different model complexity. The code can be found at https://github.com/intelligent-control-lab/ verify-neural-CBF.

Figures (6)

• Figure 1: Overview of the verification pipeline with symbolic bound propagation, from input specifications of boundary state and control to the output specification of the CBF condition.
• Figure 2: Illustration of the verification results for Dubins car using (a) NNCB-IBP mazouz2022safety, (b) BBV wang2023simultaneous and (c) ours. The obstacle is in gray. The state boundary of $\phi(\boldsymbol{\mathbf{x}})=0$ given orientation $-14^\circ$ is over-approximated by boxes. Green boxes denote the results of "hold" while red ones denote the results of "unknown" to verify $\dot \phi + 0.5 \phi\leq 0$, whose value is shown as heatmap in Fig. (d).
• Figure 3: Verified Rate under different number of boundary hyper-rectangles under different grid sizes. The grid number per dimension for each figure (from left to right): 10, 20, 50, 100. The dashed line denotes the results of falsification by counterexample as upper bounds.
• Figure 4: Comparison of verification time using branch-and-bound to achieve 100% Verified Rate with different model complexity with regular training. The more hyper-rectangles the boundary set contains, the finer the state input specification will be.
• Figure 5: Verified rate with different $\alpha$ in the neural CBF verification condition using different grid sizes (different number of boundary hyper-rectangles) for Dubins Car.

Theorems & Definitions (13)

• Definition 1
• Theorem 1: from ames2019controlliu2014control
• Proposition 1
• Example 1
• Theorem 2
• Example 2
• Lemma 1: Interval Arithmetic, restated from Section 4.1 in liu2021algorithms.
• proof
• Proposition 2
• proof