Set-Based Training of Neural Barrier Certificates for Safety Verification of Dynamical Systems
For researchers in formal verification of dynamical systems, this work reduces the iterative training-verification loop to a single step, improving efficiency.
This paper proposes a set-based training method for neural barrier certificates that integrates verification into training via a set-based loss function, enabling a single training procedure to formally prove safety. Experiments show the approach scales well with system dimension and handles complex nonlinear dynamics.
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.