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

arXiv: https://arxiv.org/abs/2512.11750 · HTML: https://mlsanity.com/paper/2512.11750/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 18 of its 37 references that are in the map.
- First posted on arXiv 12 Dec 2025.

## Builds on (most cited first, 18 of 18)

- [Kernel Mean Embedding of Distributions: A Review and Beyond](https://mlsanity.com/paper/1605.09522/) (2016)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [A Measure-Theoretic Approach to Kernel Conditional Mean Embeddings](https://mlsanity.com/paper/2002.03689/) (2020)
- [Demystifying the Draft EU Artificial Intelligence Act](https://mlsanity.com/paper/2107.03721/) (2021)
- [OmniSafe: An Infrastructure for Accelerating Safe Reinforcement Learning Research](https://mlsanity.com/paper/2305.09304/) (2023)
- [A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems](https://mlsanity.com/paper/2005.02979/) (2020)
- [Optimal Rates for Regularized Conditional Mean Embedding Learning](https://mlsanity.com/paper/2208.01711/) (2022)
- [A Tutorial on the Non-Asymptotic Theory of System Identification](https://mlsanity.com/paper/2309.03873/) (2023)
- [Formal Verification and Control with Conformal Prediction](https://mlsanity.com/paper/2409.00536/) (2024)
- [Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models](https://mlsanity.com/paper/2311.09793/) (2023)
- [Data-driven verification and synthesis of stochastic systems via barrier certificates](https://mlsanity.com/paper/2111.10330/) (2021)
- [Sampling-based Reachability Analysis: A Random Set Theory Approach with Adversarial Sampling](https://mlsanity.com/paper/2008.10180/) (2020)
- [Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings](https://mlsanity.com/paper/2403.10497/) (2024)
- [Formal Policy Synthesis for Continuous-Space Systems via Reinforcement Learning](https://mlsanity.com/paper/2005.01319/) (2020)
- [Bounding Multivariate Trigonometric Polynomials with Applications to Filter Bank Design](https://mlsanity.com/paper/1802.09588/) (2018)
- [Distributionally Robust Control Synthesis for Stochastic Systems with Safety and Reach-Avoid Specifications](https://mlsanity.com/paper/2501.03137/) (2025)
- [TRUST: Stability and Safety Controller Synthesis for Unknown Dynamical Models Using a Single Trajectory](https://mlsanity.com/paper/2503.08081/) (2025)
- [Formal Methods for Autonomous Systems](https://mlsanity.com/paper/2311.01258/) (2023)

## Built on by (most cited first, 2 of 2)

- [Kernel-Based Learning of Safety Barriers](https://mlsanity.com/paper/2601.12002/) (2026)
- [Safety Certification is Classification](https://mlsanity.com/paper/2605.06087/) (2026)

## Abstract (arXiv)

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.