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

Conference: AAAI 2026 arXiv: 2512.11750 Code: None Area: Autonomous Driving / Formal Verification Keywords: Safety Certification, Stochastic Systems, Control Barrier Certificates, Kernel Methods, Robust Verification

TL;DR¶

This paper proposes LUCID, the first verification engine capable of providing quantified safety guarantees for black-box stochastic dynamical systems. By combining data-driven control barrier certificates, conditional mean embeddings, and finite Fourier kernel expansions, LUCID reformulates a semi-infinite non-convex optimization problem into a tractable linear program.

Background & Motivation¶

Background: AI components (e.g., deep learning controllers) are increasingly embedded in high-stakes systems such as autonomous vehicles and medical devices, making safety assurance critically important. However, traditional formal verification tools face two major challenges: (1) AI components are opaque black boxes; (2) system dynamics are inherently stochastic.

Limitations of Prior Work: Existing verification methods either require precise mathematical models of the system (inapplicable to black-box AI), cannot handle stochasticity (applicable only to deterministic systems), or provide only statistical bounds rather than formal safety guarantees.

Key Challenge: Mathematically rigorous safety guarantees are required for systems that are fundamentally unpredictable (stochastic) and uninterpretable (black-box).

Goal: (1) Learn safety certificates from a finite dataset of state transitions only; (2) provide robustness guarantees against out-of-distribution behavior; (3) maintain computational feasibility.

Key Insight: Leveraging the framework of Control Barrier Certificates (CBCs), but learning them from data via kernel methods rather than assuming a known system model.

Core Idea: Conditional mean embeddings are used to embed data into a Reproducing Kernel Hilbert Space (RKHS), constructing a distributionally robust ambiguity set; finite Fourier kernel expansions then transform the semi-infinite optimization into a linear program.

Method¶

Overall Architecture¶

LUCID takes as input a finite dataset of system state transitions \(\{(x_i, x'_i)\}\), where \(x'_i\) denotes the stochastic successor state from \(x_i\), and outputs a safety certificate proving that the system will not enter an unsafe region with a given probability. The pipeline proceeds as: data embedding → ambiguity set construction → safety-constrained optimization → safety guarantee.

Key Designs¶

Conditional Mean Embeddings:
- Function: Embed the transition probability distributions of the stochastic system into an RKHS.
- Mechanism: For each state \(x\), the distribution of successor states \(P(\cdot|x)\) is embedded as an element \(\mu_{P|x}\) in the RKHS. These embeddings are estimated from data using kernel methods, and an ambiguity set in the RKHS is constructed to cover estimation error and distributional uncertainty.
- Design Motivation: Directly modeling transition probability densities is infeasible in high-dimensional spaces; kernel embeddings provide a nonparametric alternative.
Distributionally Robust Safety Verification:
- Function: Provide safety guarantees against model error and distributional shift.
- Mechanism: The estimation error of kernel embeddings is quantified as an ambiguity ball in the RKHS; safety constraints are required to hold for all plausible true distributions within the ambiguity set. Robustness to out-of-distribution behavior can be increased by enlarging the ambiguity set radius.
- Design Motivation: Transition distributions estimated from finite data inevitably contain errors; distributionally robust optimization ensures that safety guarantees remain valid under these errors.
Finite Fourier Kernel Expansion and Linear Programming:
- Function: Render the optimization problem computationally tractable.
- Mechanism: The verification conditions for control barrier certificates involve semi-infinite constraints (to be satisfied for all states), which are intractable to solve directly. LUCID approximates the kernel function using random Fourier features, relaxing the semi-infinite non-convex problem into a finite-dimensional linear program. The Fast Fourier Transform (FFT) is exploited for efficient generation of the relaxed problem.
- Design Motivation: Computational complexity is a classical bottleneck of kernel methods. Fourier approximation substantially reduces computational cost while preserving theoretical guarantees.

Loss & Training¶

No neural network training is involved. The core procedure is solving a linear program to identify a control barrier certificate satisfying the safety constraints.

Key Experimental Results¶

Main Results¶

Validated on multiple challenging benchmarks.

Benchmark System	Safety Certified	Verification Time	Notes
Simple Dynamical System	Pass	Fast	Low-dimensional validation
High-Dimensional System	Pass	Moderate	Fourier approximation effective
AI Controller System	Pass	Acceptable	Black-box verification successful

Ablation Study¶

Configuration	Result	Notes
Full LUCID	Best	Robust and efficient
Without Distributional Robustness	Safety not guaranteed	Missing error coverage
Exact Kernel (no approximation)	Tighter bounds	But computationally infeasible
Small Dataset	Loose bounds	More data yields tighter bounds

Key Findings¶

LUCID is the first tool to provide formal safety guarantees for black-box stochastic dynamical systems, filling a critical gap in the verification landscape.
The Fourier approximation incurs minimal loss in practice while transforming the problem from intractable to tractable—a key enabler of scalability.
A direct relationship exists between data volume and the tightness of safety guarantees: more data → tighter bounds → greater practical utility.

Highlights & Insights¶

Novelty is the primary highlight—no prior tool could provide formal safety guarantees for black-box stochastic systems; LUCID fills this gap.
The combination of kernel methods and Fourier approximation preserves theoretical rigor while achieving computational feasibility.
The modular design facilitates extension to new system types.

Limitations & Future Work¶

Data requirements may grow prohibitively in extremely high-dimensional state spaces.
The relaxation introduced by Fourier approximation may render safety bounds overly conservative.
Online verification—real-time updating of safety certificates during system operation—is not addressed.
Integration with safe reinforcement learning could provide safety guarantees throughout the training process.

vs. Traditional CBCs: Traditional methods require a known system model; LUCID learns certificates from data.
vs. Statistical Model Checking: SMC provides statistical bounds, whereas LUCID provides formal mathematical guarantees.
vs. Neural Network Verification (e.g., α-β-CROWN): These methods verify the neural network itself; LUCID targets the complete system incorporating AI components.

Rating¶

Novelty: ⭐⭐⭐⭐⭐ First formal safety verification tool for black-box stochastic systems
Experimental Thoroughness: ⭐⭐⭐⭐ Multiple benchmarks validate effectiveness and scalability
Writing Quality: ⭐⭐⭐⭐ High technical depth with clear presentation
Value: ⭐⭐⭐⭐⭐ Foundational contribution to AI safety