Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

Nikolaus Vertovec, Frederik Baymler Mathiesen, Thom Badings, Luca Laurenti, Alessandro Abate

TL;DR

This work tackles the bottleneck of verifying neural control barrier functions (CBFs) for safety in nonlinear control systems. It replaces expensive SMT-based nonlinear reasoning with a scalable framework that derives linear upper and lower bounds on the CBF condition by extending linear bound propagation (LBP) to network gradients and coupling these with McCormick relaxations, yielding a linear surrogate $\phi_{\mathrm{linear}}$ whose satisfaction implies a valid CBF. The method supports arbitrary control-affine dynamics and a wide range of activations, and introduces a parallelizable, adaptive simplicial refinement to reduce conservatism. Experimental results show substantial speedups over SMT-based verification and the ability to certify larger neural CBFs across multiple benchmarks, including the incorporation of control input terms in the invariance condition. This framework advances practical safety certification for neural CBFs and opens paths toward certificates for reachability and avoidance.

Abstract

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.

Scalable Verification of Neural Control Barrier Functions Using Linear Bound Propagation

TL;DR

This work tackles the bottleneck of verifying neural control barrier functions (CBFs) for safety in nonlinear control systems. It replaces expensive SMT-based nonlinear reasoning with a scalable framework that derives linear upper and lower bounds on the CBF condition by extending linear bound propagation (LBP) to network gradients and coupling these with McCormick relaxations, yielding a linear surrogate whose satisfaction implies a valid CBF. The method supports arbitrary control-affine dynamics and a wide range of activations, and introduces a parallelizable, adaptive simplicial refinement to reduce conservatism. Experimental results show substantial speedups over SMT-based verification and the ability to certify larger neural CBFs across multiple benchmarks, including the incorporation of control input terms in the invariance condition. This framework advances practical safety certification for neural CBFs and opens paths toward certificates for reachability and avoidance.

Abstract

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.

Paper Structure

This paper contains 28 sections, 4 theorems, 49 equations, 12 figures, 1 table.

Table of Contents

  1. Introduction
  2. Our approach
  3. Problem Formulation
  4. Neural Control Barrier Functions
  5. Problem Statement: Certification of a Valid Control Barrier Function
  6. Overview of our approach
  7. Linear Bound Propagation for Neural CBF Verification
  8. Verification Procedure
  9. First-Order Model of the System Dynamics
  10. Linear Bounds on the CBF Constraint
  11. Counterexamples
  12. Refinement of the Domains for Linear Bounds
  13. Batching simplices
  14. Experimental Results
  15. Results
  16. ...and 13 more sections

Key Result

theorem 1

[DBLP:journals/tac/AmesXGT17] If $\mathcal{B}$ is a CBF for the dynamical system in eq:nonlnsys and the safe set $\mathcal{S}$, then the superlevel set $\mathcal{C}$ is control invariant with respect to eq:nonlnsys.

Figures (12)

  • Figure 1: Verification flowchart illustrating the refinement and validation procedure for each simplex.
  • Figure 2: Illustration of the neural control barrier function $\mathcal{B}_{\theta}(x)$, the CBF invariance condition from \ref{['eq:cbf']}, and the resulting verification regions after adaptive mesh refinement.
  • Figure 3: ReLU Relaxation.
  • Figure 4: Leaky ReLU Relaxation.
  • Figure 5: Sigmoid Relaxation.
  • ...and 7 more figures

Theorems & Definitions (9)

  • definition 1
  • theorem 1
  • definition 2
  • theorem 4: Linear bounds on Jacobian
  • proof
  • proposition 1: Certified first-order Taylor expansion
  • theorem 5
  • definition 3: Simplex crane2018discrete
  • proof