Kernel-Based Learning of Safety Barriers

TL;DR

This paper introduces a scalable, data-driven method for safety verification of black-box systems using kernel-based control barrier certificates, capable of handling complex dynamics and uncertainties.

Contribution

It develops a novel approach combining control barrier certificates with kernel methods and Fourier analysis for efficient, robust safety verification of stochastic black-box systems.

Findings

Effective safety verification on neural network controlled systems.

Scalable linear programming formulation using Fourier transforms.

Robust safety guarantees via RKHS ambiguity sets.

Abstract

The rapid integration of AI algorithms in safety-critical applications such as autonomous driving and healthcare is raising significant concerns about the ability to meet stringent safety standards. Traditional tools for formal safety verification struggle with the black-box nature of AI-driven systems and lack the flexibility needed to scale to the complexity of real-world applications. In this paper, we present a data-driven approach for safety verification and synthesis of black-box systems with discrete-time stochastic dynamics. We employ the concept of control barrier certificates, which can guarantee safety of the system, and learn the certificate directly from a set of system trajectories. We use conditional mean embeddings to embed data from the system into a reproducing kernel Hilbert space (RKHS) and construct an RKHS ambiguity set that can be inflated to robustify the result to out-of-distribution behavior. We provide the theoretical results on how to apply the approach to general classes of temporal logic specifications beyond safety. For the data-driven computation of safety barriers, we leverage a finite Fourier expansion to cast a typically intractable semi-infinite optimization problem as a linear program. The resulting spectral barrier allows us to leverage the fast Fourier transform to generate the relaxed problem efficiently, offering a scalable yet distributionally robust framework for verifying safety. Our work moves beyond restrictive assumptions on system dynamics and uncertainty, as demonstrated on two case studies including a black-box system with a neural network controller.