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.

翻译：确保人工智能赋能系统的安全性，尤其是在自动驾驶和医疗等高风险领域，已变得日益关键。面对同时包含不透明的黑盒人工智能组件和复杂随机动态的系统，传统的形式化验证工具显得力不从心。为应对这些挑战，我们提出了LUCID（随机动态系统的学习驱动不确定性感知认证），这是一种用于从有限随机状态转移数据集中认证黑盒随机动态系统安全性的验证引擎。因此，LUCID是首个已知能够为此类系统建立量化安全保证的工具。得益于其模块化架构和详尽的文档，LUCID被设计为易于扩展。LUCID采用基于控制屏障证书的数据驱动方法，该方法直接从系统转移数据中学习，以确保形式化的安全保证。我们利用条件均值嵌入将数据嵌入到再生核希尔伯特空间（RKHS）中，并在其中构建一个RKHS模糊集，该集合可通过膨胀来增强结果对分布外行为的鲁棒性。LUCID的一个关键创新在于其使用有限傅里叶核展开，将半无限非凸优化问题重新表述为一个可处理的线性规划问题。由此产生的谱屏障使我们能够利用快速傅里叶变换高效生成松弛问题，从而提供了一个可扩展且分布鲁棒的安全验证框架。因此，LUCID提供了一个鲁棒且高效的验证框架，能够处理现代黑盒系统的复杂性，同时提供形式化的安全保证。这些独特能力在具有挑战性的基准测试中得到了验证。