論文の概要: Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates

• arxiv url: http://arxiv.org/abs/2405.14058v1
• Date: Wed, 22 May 2024 23:06:34 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-24 19:44:34.059616
• Title: Formally Verifying Deep Reinforcement Learning Controllers with Lyapunov Barrier Certificates
• Title（参考訳）: Lyapunov Barrier Certificatesを用いたDeep Reinforcement Learning Controllerの形式検証
• Authors: Udayan Mandal, Guy Amir, Haoze Wu, Ieva Daukantas, Fletcher Lee Newell, Umberto J. Ravaioli, Baoluo Meng, Michael Durling, Milan Ganai, Tobey Shim, Guy Katz, Clark Barrett,
• Abstract要約: 離散時間システムのためのNLBベースの証明書をトレーニングし、検証するための新しい手法を提案する。 具体的には,高度に複雑なシステムの検証を簡略化する証明書合成手法を提案する。 DRL制御宇宙船の安全性と生存性を保証するためのケーススタディにより,本手法の利点を実証する。
• 参考スコア（独自算出の注目度）: 2.0611129932396164
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Deep reinforcement learning (DRL) is a powerful machine learning paradigm for generating agents that control autonomous systems. However, the "black box" nature of DRL agents limits their deployment in real-world safety-critical applications. A promising approach for providing strong guarantees on an agent's behavior is to use Neural Lyapunov Barrier (NLB) certificates, which are learned functions over the system whose properties indirectly imply that an agent behaves as desired. However, NLB-based certificates are typically difficult to learn and even more difficult to verify, especially for complex systems. In this work, we present a novel method for training and verifying NLB-based certificates for discrete-time systems. Specifically, we introduce a technique for certificate composition, which simplifies the verification of highly-complex systems by strategically designing a sequence of certificates. When jointly verified with neural network verification engines, these certificates provide a formal guarantee that a DRL agent both achieves its goals and avoids unsafe behavior. Furthermore, we introduce a technique for certificate filtering, which significantly simplifies the process of producing formally verified certificates. We demonstrate the merits of our approach with a case study on providing safety and liveness guarantees for a DRL-controlled spacecraft.
• Abstract（参考訳）: 深層強化学習(DRL)は、自律システムを制御するエージェントを生成するための強力な機械学習パラダイムである。 しかし、DRLエージェントの「ブラックボックス」の性質は、現実世界の安全クリティカルなアプリケーションへの展開を制限する。 エージェントの行動に強い保証を与えるための有望なアプローチは、エージェントが望むように振る舞うことを間接的に暗示するシステム上で学習された関数であるNeural Lyapunov Barrier(NLB)証明書を使用することである。 しかしながら、NLBベースの証明書は一般的に習得が困難であり、特に複雑なシステムでは検証が困難である。 本研究では,離散時間システムのためのNLBベースの証明書をトレーニングし,検証するための新しい手法を提案する。 具体的には,証明書のシーケンスを戦略的に設計することで,複雑度の高いシステムの検証を簡略化する証明書合成手法を提案する。 ニューラルネットワーク検証エンジンと共同で検証する場合、これらの証明書はDRLエージェントがその目標を達成し、安全でない振る舞いを避けることを正式な保証を提供する。 さらに,正式に認証された証明書を生成するプロセスを大幅に単純化する証明書フィルタリング手法を提案する。 DRL制御宇宙船の安全性と生存性を保証するためのケーススタディにより,本手法の利点を実証する。

関連論文リスト

• 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 Verification Framework for Dynamical and Control Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Approximate Model-Based Shielding for Safe Reinforcement Learning [83.55437924143615]
  本稿では,学習したRLポリシーの性能を検証するための,原則的ルックアヘッド遮蔽アルゴリズムを提案する。 我々のアルゴリズムは他の遮蔽手法と異なり、システムの安全性関連力学の事前知識を必要としない。 我々は,国家依存型安全ラベルを持つアタリゲームにおいて,他の安全を意識したアプローチよりも優れた性能を示す。
  論文  参考訳（メタデータ） (2023-07-27T15:19:45Z)
• Value Functions are Control Barrier Functions: Verification of Safe Policies using Control Theory [46.85103495283037]
  本稿では,制御理論から学習値関数への検証手法の適用方法を提案する。 我々は値関数と制御障壁関数の間の関係を確立する原定理を定式化する。 我々の研究は、RLベースの制御システムの汎用的でスケーラブルで検証可能な設計のための公式なフレームワークに向けた重要な一歩である。
  論文  参考訳（メタデータ） (2023-06-06T21:41:31Z)
• COPA: Certifying Robust Policies for Offline Reinforcement Learning against Poisoning Attacks [49.15885037760725]
  本研究は, 中毒発生時におけるオフライン強化学習(RL)の堅牢性を検証することに注力する。 本報告では, 許容可能な毒素トラジェクトリの数を認証する最初の認証フレームワークであるCOPAを提案する。 提案手法のいくつかは理論的に厳密であり,一部はNP-Complete問題であることを示す。
  論文  参考訳（メタデータ） (2022-03-16T05:02:47Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)
• CRFL: Certifiably Robust Federated Learning against Backdoor Attacks [59.61565692464579]
  本稿では,第1の汎用フレームワークであるCertifiably Robust Federated Learning (CRFL) を用いて,バックドアに対する堅牢なFLモデルをトレーニングする。 提案手法は, モデルパラメータのクリッピングと平滑化を利用して大域的モデル平滑化を制御する。
  論文  参考訳（メタデータ） (2021-06-15T16:50:54Z)

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

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