lucid/CITATION.cff at main · TendTo/lucid · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
# This CITATION.cff file was generated with cffinit.
# Visit https://bit.ly/cffinit to generate yours today!

cff-version: 1.2.0
title: Lucid
message: >-
  If you use this software, please cite it using the
  metadata from this file.
type: software
authors:
  - given-names: Ernesto
    family-names: Casablanca
    email: e.casablanca2@newcastle.ac.uk
    name-particle: Ernesto
    affiliation: Newcastle Univeristy
    orcid: "https://orcid.org/0009-0009-3741-1624"
  - given-names: Oliver
    family-names: Schön
    email: o.schoen2@newcastle.ac.uk
    affiliation: Newcastle University
    orcid: "https://orcid.org/0000-0002-0214-6455"
  - given-names: Paolo
    family-names: Zuliani
    email: zuliani@di.uniroma1.it
    affiliation: Universita di Roma "La Sapienza"
    orcid: "https://orcid.org/0000-0001-6033-5919"
  - given-names: Sadegh
    family-names: Soudjani
    email: sadegh@mpi-sws.org
    affiliation: Max Planck Institute for Software Systems
    orcid: "https://orcid.org/0000-0003-1922-6678"
identifiers:
  - type: url
    value: "https://arxiv.org/abs/2512.11750"
    description: arXiv
repository-code: "https://github.com/TendTo/lucid"
url: "https://tendto.github.io/lucid/"
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.
keywords:
  - Control Systems
  - Machine Learning
license: CC-BY-4.0
commit: 93b77e9fa9ca1443b460ff1c0187cdeb0dd22adf
version: 0.0.2
date-released: "2025-12-14"