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

arXiv: https://arxiv.org/abs/2501.15189 · HTML: https://mlsanity.com/paper/2501.15189/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 21 references that are in the map.
- First posted on arXiv 25 Jan 2025.

## Builds on (most cited first, 7 of 7)

- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [How to Train Your Neural Control Barrier Function: Learning Safety Filters for Complex Input-Constrained Systems](https://mlsanity.com/paper/2310.15478/) (2023)
- [Fast BATLLNN: Fast Box Analysis of Two-Level Lattice Neural Networks](https://mlsanity.com/paper/2111.09293/) (2021)
- [Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees](https://mlsanity.com/paper/2403.07308/) (2024)
- [Simultaneous Synthesis and Verification of Neural Control Barrier Functions through Branch-and-Bound Verification-in-the-loop Training](https://mlsanity.com/paper/2311.10438/) (2023)
- [DeepBern-Nets: Taming the Complexity of Certifying Neural Networks using Bernstein Polynomial Activations and Precise Bound Propagation](https://mlsanity.com/paper/2305.13508/) (2023)

## Abstract (arXiv)

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.