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

• URL: http://arxiv.org/abs/2512.11750v1
• Date: Fri, 12 Dec 2025 17:46:50 GMT
• Title: LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems
• Abstract summary: Traditional formal verification tools fall short when faced with systems that embed both opaque black-box AI components and complex dynamics.<n>We introduce LUCID, a verification engine for certifying safety of black-box embedding dynamical systems.<n> LUCID is the first known tool capable of establishing quantified safety guarantees for such systems.
• Score: 0.8574682463936006
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• The Cognitive Circuit Breaker: A Systems Engineering Framework for Intrinsic AI Reliability [0.0]
  Large Language Models (LLMs) are increasingly deployed in mission-critical software systems.<n>We propose the Cognitive Circuit Breaker, a novel systems engineering framework that provides intrinsic reliability monitoring with minimal latency overhead.<n>We demonstrate statistically significant detection of cognitive dissonance, highlight architecture-dependent Out-of-Distribution (OOD) generalization, and show that this framework adds negligible computational overhead to the active inference pipeline.
  arXiv  Detail & Related papers  (2026-04-15T02:34:37Z)
• BarrierSteer: LLM Safety via Learning Barrier Steering [83.12893815611052]
  BarrierSteer is a novel framework that formalizes safety by embedding learned non-linear safety constraints directly into the model's latent representation space.<n>We show that BarrierSteer substantially reduces adversarial success rates, decreases unsafe generations, and outperforms existing methods.
  arXiv  Detail & Related papers  (2026-02-23T18:19:46Z)
• Safe Reinforcement Learning via Recovery-based Shielding with Gaussian Process Dynamics Models [57.006252510102506]
  Reinforcement learning (RL) is a powerful framework for optimal decision-making and control but often lacks provable guarantees for safety-critical applications.<n>We introduce a novel recovery-based shielding framework that enables safe RL with a provable safety lower bound for unknown and non-linear continuous dynamical systems.
  arXiv  Detail & Related papers  (2026-02-12T22:03:35Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Kernel-Based Learning of Safety Barriers [0.9367224590861915]
  Rapid integration of AI algorithms in safety-critical applications is raising concerns about the ability to meet stringent safety standards.<n>Traditional tools for formal safety verification struggle with the black-box nature of AI-driven systems.<n>We present a data-driven approach for safety verification and synthesis of black-box systems with discrete-time dynamics.
  arXiv  Detail & Related papers  (2026-01-17T10:42:35Z)
• BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems [4.530582224312311]
  We introduce an LLM-based agentic framework for barrier certificate synthesis.<n>The framework uses natural language reasoning to propose, refine, and validate candidate certificates.<n> BarrierBench is a benchmark of 100 dynamical systems spanning linear, nonlinear, discrete-time, and continuous-time settings.
  arXiv  Detail & Related papers  (2025-11-12T14:23:49Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  We develop scalable formal verification algorithms without shifting the problem to unrealistic assumptions. In a pursuit of developing scalable formal verification algorithms without shifting the problem to unrealistic assumptions, we employ the concept of barrier certificates. We show how to solve the resulting program efficiently using sum-of-squares optimization and a Gaussian process envelope.
  arXiv  Detail & Related papers  (2024-03-15T17:32:02Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Log Barriers for Safe Black-box Optimization with Application to Safe Reinforcement Learning [72.97229770329214]
  We introduce a general approach for seeking high dimensional non-linear optimization problems in which maintaining safety during learning is crucial. Our approach called LBSGD is based on applying a logarithmic barrier approximation with a carefully chosen step size. We demonstrate the effectiveness of our approach on minimizing violation in policy tasks in safe reinforcement learning.
  arXiv  Detail & Related papers  (2022-07-21T11:14:47Z)
• Safety Certification for Stochastic Systems via Neural Barrier Functions [3.7491936479803054]
  barrier functions can be used to provide non-trivial certificates of safety for non-linear systems. We parameterize a barrier function as a neural network and show that robust training of neural networks can be successfully employed to find barrier functions. We show that our approach outperforms existing methods in several case studies and often returns certificates of safety that are orders of magnitude larger.
  arXiv  Detail & Related papers  (2022-06-03T09:06:02Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.