LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems

TL;DR

LUCID is a novel verification tool that provides safety guarantees for black-box stochastic dynamical systems using data-driven control barrier certificates and kernel methods, scalable to complex real-world systems.

Contribution

LUCID introduces a modular, data-driven verification framework that learns safety certificates directly from transition data, incorporating robustness and scalability for black-box stochastic systems.

Findings

LUCID can certify safety for complex stochastic systems from finite data.

The use of Fourier kernel expansion enables efficient, scalable verification.

LUCID demonstrates effectiveness on challenging benchmark systems.

Abstract

Ensuring the safety of AI-enabled systems, particularly in high-stakes domains such as autonomous driving and healthcare, has become increasingly critical. Traditional formal verification tools fall short when faced with systems that embed both opaque, black-box AI components and complex stochastic dynamics. To address these challenges, we introduce LUCID (Learning-enabled Uncertainty-aware Certification of stochastIc Dynamical systems), a verification engine for certifying safety of black-box stochastic dynamical systems from a finite dataset of random state transitions. As such, LUCID is the first known tool capable of establishing quantified safety guarantees for such systems. Thanks to its modular architecture and extensive documentation, LUCID is designed for easy extensibility. LUCID employs a data-driven methodology rooted in control barrier certificates, which are learned directly from system transition data, to ensure formal safety guarantees. We use conditional mean embeddings to embed data into a reproducing kernel Hilbert space (RKHS), where an RKHS ambiguity set is constructed that can be inflated to robustify the result to out-of-distribution behavior. A key innovation within LUCID is its use of a finite Fourier kernel expansion to reformulate a semi-infinite non-convex optimization problem into a tractable 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. LUCID thus offers a robust and efficient verification framework, able to handle the complexities of modern black-box systems while providing formal guarantees of safety. These unique capabilities are demonstrated on challenging benchmarks.