# Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 12 of its 56 references that are in the map.
- First posted on arXiv 4 May 2026.

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

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Control Barrier Functions: Theory and Applications](https://mlsanity.com/paper/1903.11199/) (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)
- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [SEEV: Synthesis with Efficient Exact Verification for ReLU Neural Barrier Functions](https://mlsanity.com/paper/2410.20326/) (2024)
- [Advances in the Theory of Control Barrier Functions: Addressing Practical Challenges in Safe Control Synthesis for Autonomous and Robotic Systems](https://mlsanity.com/paper/2312.16719/) (2023)
- [Set-Based Training for Neural Network Verification](https://mlsanity.com/paper/2401.14961/) (2024)
- [Out of the Shadows: Exploring a Latent Space for Neural Network Verification](https://mlsanity.com/paper/2505.17854/) (2025)
- [Abstraction of Elementary Hybrid Systems by Variable Transformation](https://mlsanity.com/paper/1403.7022/) (2014)
- [Barrier Certificates Revisited](https://mlsanity.com/paper/1310.6481/) (2013)
- [Verification of Quantum Systems using Barrier Certificates](https://mlsanity.com/paper/2307.07307/) (2023)

## Abstract (arXiv)

Barrier certificates are scalar functions over the state space of dynamical systems that separate all unsafe states from all reachable states. The existence of a barrier certificate formally verifies the safety of the dynamical system. Recent approaches synthesize barrier certificates by iteratively training a neural network. In each iteration, the candidate is formally verified - if successful, the barrier certificate is found. Instead, we propose a set-based training approach that tightly integrates verification into training via a set-based loss function that soundly encodes all barrier certificate properties. A loss of zero formally proves the validity of the barrier certificate, collapsing the iterative training and verification into a single training procedure. Our experiments demonstrate that our set-based training approach scales well with the system dimension and naturally handles complex nonlinear dynamics.