Extracting Forward Invariant Sets from Neural Network-Based Control Barrier Functions

TL;DR

This paper presents a sound and efficient algorithm to formally certify neural network-based barrier functions for safety in autonomous systems, ensuring provable safety guarantees.

Contribution

The authors introduce a novel certification method combining reachability analysis and hyperplane arrangement enumeration for shallow neural networks.

Findings

Successfully certifies neural network barrier functions in real-world case studies.

Demonstrates the algorithm's scalability and efficiency.

Provides formal safety guarantees for neural network controllers.

Abstract

Training Neural Networks (NNs) to serve as Barrier Functions (BFs) is a popular way to improve the safety of autonomous dynamical systems. Despite significant practical success, these methods are not generally guaranteed to produce true BFs in a provable sense, which undermines their intended use as safety certificates. In this paper, we consider the problem of formally certifying a learned NN as a BF with respect to state avoidance for an autonomous system: viz. computing a region of the state space on which the candidate NN is provably a BF. In particular, we propose a sound algorithm that efficiently produces such a certificate set for a shallow NN. Our algorithm combines two novel approaches: it first uses NN reachability tools to identify a subset of states for which the output of the NN does not increase along system trajectories; then, it uses a novel enumeration algorithm for hyperplane arrangements to find the intersection of the NN's zero-sub-level set with the first set of states. In this way, our algorithm soundly finds a subset of states on which the NN is certified as a BF. We further demonstrate the effectiveness of our algorithm at certifying for real-world NNs as BFs in two case studies. We complemented these with scalability experiments that demonstrate the efficiency of our algorithm.