論文の概要: LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems

• arxiv url: http://arxiv.org/abs/2512.11750v1
• Date: Fri, 12 Dec 2025 17:46:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-15 15:48:11.861251
• Title: LUCID: Learning-Enabled Uncertainty-Aware Certification of Stochastic Dynamical Systems
• Title（参考訳）: LUCID:確率力学系の学習可能不確かさを意識した認証
• Authors: Ernesto Casablanca, Oliver Schön, Paolo Zuliani, Sadegh Soudjani,
• Abstract要約: 従来の形式的検証ツールは、不透明なブラックボックスAIコンポーネントと複雑なダイナミクスの両方を組み込んだシステムに直面したときに不足する。 我々は,ブラックボックス埋め込み動的システムの安全性を証明するための検証エンジンであるLUCIDを紹介する。 LUCIDは、このようなシステムの安全性を定量化する最初のツールである。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: AI対応システムの安全性を確保することは、特に自動運転やヘルスケアといった高度な分野において、ますます重要になっている。 従来の形式的検証ツールは、不透明でブラックボックスのAIコンポーネントと複雑な確率力学の両方を組み込むシステムに直面したときに不足する。 これらの課題に対処するために、ランダム状態遷移の有限データセットからブラックボックス確率力学系の安全性を証明するための検証エンジンであるLUCID(Learning- capable Uncertainty-aware Certification of stochastIc Dynamical systems)を導入する。 そのため、LUCIDは、そのようなシステムに対する定量化された安全保証を確立できる最初のツールである。 モジュラーアーキテクチャと広範なドキュメントのおかげで、LUCIDは容易に拡張できるように設計されている。 LUCIDは、制御バリア証明書に根ざしたデータ駆動方式を採用し、システム移行データから直接学習し、正式な安全保証を保証する。 条件付き平均埋め込みを用いて、再現カーネルヒルベルト空間(RKHS)にデータを埋め込む。 LUCIDにおける重要な革新は、半無限の非凸最適化問題をトラクタブル線形プログラムに再構成するために有限フーリエカーネル拡張を使用することである。 その結果,高速フーリエ変換を利用して緩和された問題を効率的に生成し,安全性を検証するためのスケーラブルかつ分散的に堅牢なフレームワークを提供する。 したがって、LUCIDは堅牢で効率的な検証フレームワークを提供し、安全の正式な保証を提供しながら、現代のブラックボックスシステムの複雑さを処理できる。 これらのユニークな機能は、挑戦的なベンチマークで示されています。

関連論文リスト

• BarrierBench : Evaluating Large Language Models for Safety Verification in Dynamical Systems [4.530582224312311]
  バリア証明書合成のための LLM ベースのエージェントフレームワークを提案する。 このフレームワークは自然言語推論を使用して、候補証明書を提案し、洗練し、検証する。 BarrierBenchは、線形、非線形、離散時間、連続時間設定にまたがる100の動的システムのベンチマークである。
  論文  参考訳（メタデータ） (2025-11-12T14:23:49Z)
• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。 問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。 本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
  論文  参考訳（メタデータ） (2024-03-15T17:32:02Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。 次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。 これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
  論文  参考訳（メタデータ） (2022-08-23T05:02:09Z)
• Log Barriers for Safe Black-box Optimization with Application to Safe Reinforcement Learning [72.97229770329214]
  本稿では,学習時の安全性維持が不可欠である高次元非線形最適化問題に対する一般的なアプローチを提案する。 LBSGDと呼ばれるアプローチは、慎重に選択されたステップサイズで対数障壁近似を適用することに基づいている。 安全強化学習における政策課題の違反を最小限に抑えるためのアプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2022-07-21T11:14:47Z)
• Safety Certification for Stochastic Systems via Neural Barrier Functions [3.7491936479803054]
  バリア関数は、非線形システムに対する非自明な安全性証明を提供するために使用できる。 ニューラルネットワークとしてバリア関数をパラメータ化することにより、ニューラルネットワークの堅牢なトレーニングを成功させてバリア関数を見つけることができることを示す。 提案手法は,いくつかのケーススタディにおいて既存の手法よりも優れており,桁違いに大きい安全証明書を返却することが多い。
  論文  参考訳（メタデータ） (2022-06-03T09:06:02Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。