# Verification-Aided Learning of Neural Network Barrier Functions with Termination Guarantees

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

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- Builds on 20 of its 39 references that are in the map.
- First posted on arXiv 12 Mar 2024.

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

- [Convex optimization](https://mlsanity.com/paper/2106.01946/) (2021)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Neural Lyapunov Control](https://mlsanity.com/paper/2005.00611/) (2020)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Learning Control Barrier Functions from Expert Demonstrations](https://mlsanity.com/paper/2004.03315/) (2020)
- [Learning Safe Multi-Agent Control with Decentralized Neural Barrier Certificates](https://mlsanity.com/paper/2101.05436/) (2021)
- [Lyapunov-stable neural-network control](https://mlsanity.com/paper/2109.14152/) (2021)
- [Neural Certificates for Safe Control Policies](https://mlsanity.com/paper/2006.08465/) (2020)
- [Safe Control Under Input Limits with Neural Control Barrier Functions](https://mlsanity.com/paper/2211.11056/) (2022)
- [Learning Hybrid Control Barrier Functions from Data](https://mlsanity.com/paper/2011.04112/) (2020)
- [Learning Lyapunov Functions for Hybrid Systems](https://mlsanity.com/paper/2012.12015/) (2020)
- [Learning Control Lyapunov Functions from Counterexamples and Demonstrations](https://mlsanity.com/paper/1804.05285/) (2018)
- [Lyapunov-Net: A Deep Neural Network Architecture for Lyapunov Function Approximation](https://mlsanity.com/paper/2109.13359/) (2021)
- [Learning Region of Attraction for Nonlinear Systems](https://mlsanity.com/paper/2110.00731/) (2021)
- [ReachLipBnB: A branch-and-bound method for reachability analysis of neural autonomous systems using Lipschitz bounds](https://mlsanity.com/paper/2211.00608/) (2022)
- [Compositional Neural Certificates for Networked Dynamical Systems](https://mlsanity.com/paper/2303.14564/) (2023)
- [Exponential-Condition-Based Barrier Certificate Generation for Safety Verification of Hybrid Systems](https://mlsanity.com/paper/1303.6885/) (2013)

## Built on by (most cited first, 7 of 7)

- [Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes](https://mlsanity.com/paper/2501.00200/) (2024)
- [Verification of Neural Control Barrier Functions with Symbolic Derivative Bounds Propagation](https://mlsanity.com/paper/2410.16281/) (2024)
- [Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification](https://mlsanity.com/paper/2512.11087/) (2025)
- [TorchLean: Formalizing Neural Networks in Lean](https://mlsanity.com/paper/2602.22631/) (2026)
- [Extracting Forward Invariant Sets from Neural Network-Based Control Barrier Functions](https://mlsanity.com/paper/2501.15189/) (2025)
- [Sample Efficient Certification of Discrete-Time Control Barrier Functions](https://mlsanity.com/paper/2509.03899/) (2025)
- [Efficient Verification of Neural Control Barrier Functions with Smooth Nonlinear Activations](https://mlsanity.com/paper/2605.07757/) (2026)

## Abstract (arXiv)

Barrier functions are a general framework for establishing a safety guarantee for a system. However, there is no general method for finding these functions. To address this shortcoming, recent approaches use self-supervised learning techniques to learn these functions using training data that are periodically generated by a verification procedure, leading to a verification-aided learning framework. Despite its immense potential in automating barrier function synthesis, the verification-aided learning framework does not have termination guarantees and may suffer from a low success rate of finding a valid barrier function in practice. In this paper, we propose a holistic approach to address these drawbacks. With a convex formulation of the barrier function synthesis, we propose to first learn an empirically well-behaved NN basis function and then apply a fine-tuning algorithm that exploits the convexity and counterexamples from the verification failure to find a valid barrier function with finite-step termination guarantees: if there exist valid barrier functions, the fine-tuning algorithm is guaranteed to find one in a finite number of iterations. We demonstrate that our fine-tuning method can significantly boost the performance of the verification-aided learning framework on examples of different scales and using various neural network verifiers.