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

TL;DR

This paper introduces a set-based training method for neural barrier certificates that integrates verification into training, enabling scalable safety verification of complex dynamical systems.

Contribution

It proposes a novel set-based loss function that soundly encodes barrier certificate properties, unifying training and verification into a single process.

Findings

Scales well with system dimension

Handles complex nonlinear dynamics effectively

Eliminates iterative training and verification

Abstract

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.