Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation

Safe control is of great importance in online decision making for robot learning through filtering out unsafe explorative actions [1, 2, 3, 4], guaranteeing safety during sim-to-real transfer in a hierarchical manner [5]. As an effective tool of safe control, control barrier functions (CBFs) have been studied for years on both verification and synthesis [6, 7, 8, 9, 10]. A valid CBF guarantees safety by ensuring the function values non-positive for any states along the safe trajectory, implicitly enforcing the non-trivial forward invariance that feasible control inputs always exist to maintain the following non-positive energy values once the state is safe. To ensure forward invariance, polynomial-based CBFs have been proposed based on hand-crafted parametric functions [11, 12, 13], which can be verified through algebraic geometry techniques like sum-of-squares (SOS) optimization [14, 15, 16]. However, polynomial-based CBFs cannot encode complicated safety constraints [17], and the generic parameterization of non-conservative safe control for various nonlinear dynamics and nonconvex safety specifications is needed. Neural network parameterized CBFs (neural CBFs) have shown promising results due to their powerful expressiveness in modeling complex dynamics with bounded control inputs [18, 19, 20, 21, 22]. But it is challenging to guarantee that the learned neural CBF is valid because of its poor mathematical interpretability. One way to ensure the safety/stability of the dynamic system is to learn neural barrier/Lyapunov certificates [23, 24, 25, 26, 27, 28], but it may be too conservative and cause false negatives if the formal verification only relies on a specific control policy [17, 29]. Recent works to directly verify the forward invariance of learned neural CBFs are based on SMT-based counterexample falsification [30, 31], mixed integer programming [32], Lipschitz neural networks [33], and CROWN-based linear bound propagation [34, 35, 36].