# Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Jul 2020.

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

- [Neural Termination Analysis](https://mlsanity.com/paper/2102.03824/) (2021)
- [Infinite Time Horizon Safety of Bayesian Neural Networks](https://mlsanity.com/paper/2111.03165/) (2021)
- [Safe Reach Set Computation via Neural Barrier Certificates](https://mlsanity.com/paper/2404.18813/) (2024)

## Abstract (arXiv)

We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The approach is underpinned by an inductive framework: this is structured as a sequential loop between a learner, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate's validity or generates counter-examples to further guide the learner. We compare the approach against state-of-the-art techniques, over polynomial and non-polynomial dynamical models: the outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine (up to five orders less), whilst needing a far smaller data set (up to three orders less) for the learning part. Beyond improvements over the state of the art, we further challenge the new approach on a hybrid dynamical model and on larger-dimensional models, and showcase the numerical robustness of our algorithms and codebase.