論文の概要: Formal Verification of Neural Certificates Done Dynamically
- arxiv url: http://arxiv.org/abs/2507.11987v1
- Date: Wed, 16 Jul 2025 07:37:23 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-17 19:00:11.280339
- Title: Formal Verification of Neural Certificates Done Dynamically
- Title（参考訳）: 動的に行うニューラルネットワーク証明書の形式的検証
- Authors: Thomas A. Henzinger, Konstantin Kueffner, Emily Yu,
- Abstract要約: 本稿では,リアルタイム検証を統合した軽量なランタイム監視フレームワークを提案する。
提案手法は,安全性違反や不正証明書を最小限のオーバーヘッドでタイムリーに検出することを可能にする。
- 参考スコア（独自算出の注目度）: 7.146556437126553
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Neural certificates have emerged as a powerful tool in cyber-physical systems control, providing witnesses of correctness. These certificates, such as barrier functions, often learned alongside control policies, once verified, serve as mathematical proofs of system safety. However, traditional formal verification of their defining conditions typically faces scalability challenges due to exhaustive state-space exploration. To address this challenge, we propose a lightweight runtime monitoring framework that integrates real-time verification and does not require access to the underlying control policy. Our monitor observes the system during deployment and performs on-the-fly verification of the certificate over a lookahead region to ensure safety within a finite prediction horizon. We instantiate this framework for ReLU-based control barrier functions and demonstrate its practical effectiveness in a case study. Our approach enables timely detection of safety violations and incorrect certificates with minimal overhead, providing an effective but lightweight alternative to the static verification of the certificates.
- Abstract（参考訳）: ニューラル証明書は、サイバー物理システム制御の強力なツールとして登場し、正しさの証人を提供している。
これらの証明書、例えばバリア関数は、しばしば制御ポリシーと共に学習され、一度検証されると、システムの安全性の数学的証明として機能する。
しかし、その定義条件の従来の形式的検証は通常、徹底的な状態空間探索によるスケーラビリティの課題に直面している。
この課題に対処するために、リアルタイム検証を統合し、基盤となる制御ポリシーへのアクセスを必要としない軽量なランタイム監視フレームワークを提案する。
監視装置は, 配置中のシステムを監視し, 有限の予測地平線内での安全性を確保するために, ルックアヘッド領域上で認証をオンザフライで検証する。
本稿では、このフレームワークをReLUベースの制御バリア関数にインスタンス化し、その実効性を事例研究で示す。
提案手法では,安全性違反や不正証明書を最小限のオーバーヘッドでタイムリーに検出することが可能で,証明書の静的検証に代わる,効果的かつ軽量な代替手段を提供する。
関連論文リスト
- Verification of Visual Controllers via Compositional Geometric Transformations [49.81690518952909]
到達可能な集合の外部近似を生成できる知覚ベースのコントローラのための新しい検証フレームワークを提案する。
提案手法の音質を理論的に保証し,ベンチマーク制御環境における有効性を示す。
論文 参考訳（メタデータ） (2025-07-06T20:22:58Z) - Learning Verifiable Control Policies Using Relaxed Verification [49.81690518952909]
本研究は,実行中にプロパティを評価可能なポリシを目標として,トレーニングを通じて検証を実施することを提案する。
アプローチは、微分可能な到達可能性分析を使用して、新しいコンポーネントを損失関数に組み込むことである。
論文 参考訳（メタデータ） (2025-04-23T16:54:35Z) - Formal Verification of Permission Voucher [1.4732811715354452]
Permission Voucher Protocolは、分散環境におけるセキュアで認証されたアクセス制御のために設計されたシステムである。
この分析では、重要なセキュリティ特性を評価するために、象徴的検証のための最先端のツールであるTamarin Proverを使用している。
結果は、メッセージの改ざん、偽装、リプレイなどの一般的な攻撃に対するプロトコルの堅牢性を確認する。
論文 参考訳（メタデータ） (2024-12-18T14:11:50Z) - Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates [2.0611129932396164]
離散時間システムのためのNLBベースの証明書をトレーニングし、検証するための新しい手法を提案する。
具体的には,高度に複雑なシステムの検証を簡略化する証明書合成手法を提案する。
DRL制御宇宙船の安全性と生存性を保証するためのケーススタディにより,本手法の利点を実証する。
論文 参考訳（メタデータ） (2024-05-22T23:06:34Z) - Transfer of Safety Controllers Through Learning Deep Inverse Dynamics Model [4.7962647777554634]
制御障壁証明書は、制御システムの安全性を正式に保証する上で有効であることが証明されている。
制御障壁証明書の設計は、時間がかかり、計算に費用がかかる作業である。
本稿では,制御器の正当性を保証する妥当性条件を提案する。
論文 参考訳（メタデータ） (2024-05-22T15:28:43Z) - Safe Online Dynamics Learning with Initially Unknown Models and
Infeasible Safety Certificates [45.72598064481916]
本稿では、制御バリア関数(CBF)2次コーンプログラムに基づく、堅牢な安全証明書を備えた学習ベースの設定について考察する。
制御バリア関数証明書が実現可能ならば,その安全性を確保するため,本手法では,データ収集と制御バリア関数制約の実現可能性の回復のために,システムダイナミクスを探索する。
論文 参考訳（メタデータ） (2023-11-03T14:23:57Z) - A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳（メタデータ） (2023-09-12T09:37:26Z) - Value Functions are Control Barrier Functions: Verification of Safe
Policies using Control Theory [46.85103495283037]
本稿では,制御理論から学習値関数への検証手法の適用方法を提案する。
我々は値関数と制御障壁関数の間の関係を確立する原定理を定式化する。
我々の研究は、RLベースの制御システムの汎用的でスケーラブルで検証可能な設計のための公式なフレームワークに向けた重要な一歩である。
論文 参考訳（メタデータ） (2023-06-06T21:41:31Z) - FI-ODE: Certifiably Robust Forward Invariance in Neural ODEs [34.762005448725226]
本稿では,ニューラルネットワークのフォワード不変性をトレーニングし,確実に証明するための一般的なフレームワークを提案する。
このフレームワークを、堅牢な継続的制御において認証された安全性を提供するために適用します。
さらに,画像分類における逆方向の堅牢性を証明するために,このフレームワークの汎用性について検討する。
論文 参考訳（メタデータ） (2022-10-30T20:30:19Z) - Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
CBFをベースとした安全クリティカルコントローラのモデル不確実性を考慮した再構成を提案する。
次に、結果の安全制御器のポイントワイズ実現可能性条件を示す。
これらの条件を利用して、イベントトリガーによるオンラインデータ収集戦略を考案する。
論文 参考訳（メタデータ） (2022-08-23T05:02:09Z) - Joint Differentiable Optimization and Verification for Certified
Reinforcement Learning [91.93635157885055]
安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。
本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
論文 参考訳（メタデータ） (2022-01-28T16:53:56Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。