Kernel-Based Learning of Safety Barriers

TL;DR

This work addresses safety verification for black-box autonomous systems with unknown discrete-time stochastic dynamics by learning control barrier certificates (CBCs) directly from trajectory data. It introduces a distributionally robust, kernel-based framework using conditional mean embeddings to encode the system's conditional behavior in an RKHS and constructs an RKHS ambiguity set to guard against out-of-distribution dynamics. A central novelty is the Fourier barrier approach, which casts the typically semi-infinite, hard optimization problem into a tractable linear program via finite Fourier feature expansion and FFT-based computations, enabling scalable safety verification and extension to temporal-logic specifications through automata and Streett supermartingales. The method is validated on complex safety specifications and a neural-network controlled overtaking scenario, demonstrating meaningful probabilistic safety guarantees with controllable conservatism and highlighting the practical impact for safety-critical AI systems.

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.

Figures (9)

• Figure 1: Examples of safety-critical embodied AI systems in the transport sector.
• Figure 2: Sequence of steps to generate a Fourier barrier certificate.
• Figure 3: Abstraction of a 1-dimensional Gaussian spectral measure of the SQExp kernel for $M=3$.
• Figure 4: Components of the spectral basis expansion used for the barrier in Section \ref{['sec:benchmark_complexspec']} with a maximum frequency of $f_{\text{max}}=2$. Note that Fourier barriers are thus composed of a superposition of standing waves yielding a Fourier series expansion.
• Figure 5: Robustified CBCs and level sets at ${B(x)=1}$ (in red) and $\eta$ (in blue) computed for the benchmark in Section \ref{['sec:benchmark_complexspec']}, robustified with $\varepsilon\bar{B}\sigma_f={0.007}$ and with (a) $M=35$ wavenumbers or (b) $M={99}$ wavenumbers.

Theorems & Definitions (24)

• Definition 1: Markov decision process (MDP)
• Example 1
• Definition 2: Control barrier certificate (CBC)
• Proposition 1: Finite-horizon safety
• Remark 1: Infinite-horizon safety
• Definition 3: Mean embedding (ME)
• Definition 4: Conditional mean embedding (CME)
• Proposition 2: Empirical CME
• theorem 1
• theorem 2