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

TL;DR

This work targets safe control of discrete-time systems by synthesizing neural network barrier functions with formal guarantees. It introduces a discrete-time NN vector barrier function that preserves convexity, enabling a convex formulation and tunable expressivity. To provide termination guarantees in the verification-aided learning loop, the paper embeds a CEGIS-inspired fine-tuning routine based on analytic center cutting-plane methods that updates only the last linear layer, with provable finite-step convergence. Empirical results on a double integrator and a 6D quadrotor demonstrate improved success rates and reduced runtimes across multiple NN verifiers, highlighting practical scalability and reliability for safety-critical NN controllers.

Abstract

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.

Figures (6)

• Figure 1: The verification-aided learning framework with our proposed fine-tuning method (highlighted in blue).
• Figure 2: Illustration of the fine-tuning method. After training the NN barrier function (left), we fine-tune the last linear layer through a counterexample-guided inductive synthesis framework (right) which enjoys termination guarantees.
• Figure 3: The $0$-level sets of the vector barrier function using linear functions (left) and scalar barrier function using a quadratic function (right) for safety certification of the system considered in Example \ref{['example:linear']} are plotted. The lower-left, encircled regions given by $\{x \mid B(x) \leq 0\}$ separate the trajectories starting from the initial set from the unsafe set.
• Figure 4: As shown on the left figure, proposing a candidate solution (blue dot) at the center of the localization set is guaranteed to remove a large portion of the search space (shaded area) after verification, while selecting the candidate in an uncontrolled manner (see the right figure) may lead to minimal search space improvement.
• Figure 5: The $0$-levelset of $B_0(x)$ (dotted line) separates the trajectory of the double integrator system under a NN controller from the unsafe regions. The gray arrows denote the dynamics of the closed-loop system.

Theorems & Definitions (8)

• Theorem 1: Scalar barrier function
• proof
• Lemma 1
• proof
• Theorem 2
• Example 1
• Theorem 3
• proof