論文の概要: Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties
- arxiv url: http://arxiv.org/abs/2405.04015v1
- Date: Tue, 7 May 2024 05:23:56 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-08 15:18:57.107637
- Title: Certified Policy Verification and Synthesis for MDPs under Distributional Reach-avoidance Properties
- Title（参考訳）: 分散リーチ回避特性下におけるMDPの認証政策検証と合成
- Authors: S. Akshay, Krishnendu Chatterjee, Tobias Meggendorfer, Đorđe Žikelić,
- Abstract要約: 我々は,分散リーチ回避仕様の下でのMDPにおける認証済みポリシー検証と合成の問題点を考察する。
我々のゴールは、所定のポリシーの証明書を合成するか、証明書と共にポリシーを合成し、不正な配布を避けながらターゲットの分布に到達できることを証明することである。
- 参考スコア（独自算出の注目度）: 8.302192554732208
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Markov Decision Processes (MDPs) are a classical model for decision making in the presence of uncertainty. Often they are viewed as state transformers with planning objectives defined with respect to paths over MDP states. An increasingly popular alternative is to view them as distribution transformers, giving rise to a sequence of probability distributions over MDP states. For instance, reachability and safety properties in modeling robot swarms or chemical reaction networks are naturally defined in terms of probability distributions over states. Verifying such distributional properties is known to be hard and often beyond the reach of classical state-based verification techniques. In this work, we consider the problems of certified policy (i.e. controller) verification and synthesis in MDPs under distributional reach-avoidance specifications. By certified we mean that, along with a policy, we also aim to synthesize a (checkable) certificate ensuring that the MDP indeed satisfies the property. Thus, given the target set of distributions and an unsafe set of distributions over MDP states, our goal is to either synthesize a certificate for a given policy or synthesize a policy along with a certificate, proving that the target distribution can be reached while avoiding unsafe distributions. To solve this problem, we introduce the novel notion of distributional reach-avoid certificates and present automated procedures for (1) synthesizing a certificate for a given policy, and (2) synthesizing a policy together with the certificate, both providing formal guarantees on certificate correctness. Our experimental evaluation demonstrates the ability of our method to solve several non-trivial examples, including a multi-agent robot-swarm model, to synthesize certified policies and to certify existing policies.
- Abstract（参考訳）: マルコフ決定プロセス(MDP)は、不確実性の存在下での意思決定の古典的なモデルである。
多くの場合、それらはMDP状態を越える経路に関して定義された計画目標を持つ状態変換器と見なされる。
人気が高まっている別の選択肢は、これらを分布変換器と見なすことで、MDP状態上の確率分布の列を生じさせることである。
例えば、ロボット群や化学反応ネットワークの到達性と安全性は、状態上の確率分布の観点から自然に定義される。
このような分布特性の検証は困難であることが知られており、しばしば古典的状態に基づく検証技術の範囲を超えている。
本研究では,分散リーチ回避仕様の下でのMDPにおける認証ポリシ(すなわちコントローラ)の検証と合成の問題点について考察する。
認証により、政策とともに、MDPが実際にその財産を満足することを保証する(確認可能な)証明書の合成も目指している。
したがって、MDP状態上の分布のターゲットセットと安全でない分布の集合を考えると、我々のゴールは、所定のポリシーの証明書を合成するか、または証明書と共にポリシーを合成し、不正な分布を回避しつつ目標分布に到達できることを証明することである。
そこで本研究では,(1)所定のポリシの証明書を合成するための自動手順と,(2)証明の正確性に関する公式な保証を提供するとともに,その証明書とともにポリシーを合成する手法を提案する。
実験により,本手法は,マルチエージェントロボット・ショームモデルを含むいくつかの非自明な事例を解決し,認証ポリシーを合成し,既存のポリシーを認証する能力を示す。
関連論文リスト
- Conformal Off-Policy Prediction for Multi-Agent Systems [6.32674891108819]
マルチエージェントシステムに関わるOPP問題を解くための最初の共形予測手法であるMA-COPPを紹介する。
MA-COPPの重要な貢献は、エージェント軌道の出力空間の列挙や徹底的な探索を避けることである。
我々は,PetttingZooライブラリとF1TENTH自律走行環境のマルチエージェントシステムにおけるMA-COPPの有効性を評価する。
論文 参考訳（メタデータ） (2024-03-25T15:37:43Z) - Off-Policy Evaluation in Markov Decision Processes under Weak
Distributional Overlap [5.0401589279256065]
本稿では,マルコフ決定過程(MDP)における非政治的評価の課題を再検討する。
本稿では,この環境での良好な性能を期待できる2重頑健性(TDR)推定器のクラスを紹介する。
論文 参考訳（メタデータ） (2024-02-13T03:55:56Z) - Conformal Policy Learning for Sensorimotor Control Under Distribution
Shifts [61.929388479847525]
本稿では,センサコントローラの観測値の分布変化を検知・応答する問題に焦点をあてる。
鍵となる考え方は、整合量子を入力として取ることができるスイッチングポリシーの設計である。
本稿では, 基本方針を異なる特性で切り替えるために, 共形量子関数を用いてこのようなポリシーを設計する方法を示す。
論文 参考訳（メタデータ） (2023-11-02T17:59:30Z) - Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently
Distilled RL Policies with Many-sided Guarantees [0.0]
変分マルコフ決定過程(VAE-MDPs)は、任意のRLポリシーから検証可能なコントローラを蒸留するための信頼性の高いフレームワークを提供する離散潜在空間モデルである。
本稿では, 原政策を実行するエージェントの挙動と蒸留政策との最適輸送のペナル化形式を最小化することにより, これらの問題を解決する潜在空間モデルであるWasserstein Auto-encoded MDP(WAE-MDP)を紹介する。
実験の結果, 蒸留法が10倍高速であるのに加えて, 潜水モデルの品質も良好であることが示唆された。
論文 参考訳（メタデータ） (2023-03-22T13:41:42Z) - Policy Dispersion in Non-Markovian Environment [53.05904889617441]
本稿では,非マルコフ環境下での国家行動ペアの歴史から,多様な政策の学習を試みる。
まず、ポリシー埋め込みを学習するために、トランスフォーマーベースの手法を採用する。
次に,政策埋め込みを積み重ねて分散行列を構築し,多様な政策の集合を誘導する。
論文 参考訳（メタデータ） (2023-02-28T11:58:39Z) - Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal
Abstractions [59.605246463200736]
雑音分布の明示的な表現に依存しない新しい制御器合成法を提案する。
まず、連続制御系を有限状態モデルに抽象化し、離散状態間の確率的遷移によってノイズを捕捉する。
我々は最先端の検証技術を用いてマルコフ決定プロセスの間隔を保証し、これらの保証が元の制御システムに受け継がれるコントローラを演算する。
論文 参考訳（メタデータ） (2023-01-04T10:40:30Z) - Distillation of RL Policies with Formal Guarantees via Variational
Abstraction of Markov Decision Processes (Technical Report) [0.0]
我々は、強化学習(RL)を通して学んだ政策の文脈で、政策の単純化と検証の課題を考える。
未知の環境と学習された離散潜在モデルの間に新しい双シミュレーション境界を導出する。
本稿では、現状のRLを用いて得られたポリシーを用いて、ほぼ正しいバイシミュレーション保証を持つ離散潜在モデルを生成する変分オートエンコーダを効率的に訓練する方法を示す。
論文 参考訳（メタデータ） (2021-12-17T17:57:32Z) - Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian
Noise [59.47042225257565]
雑音分布の明示的な表現に依存しない新しい計画法を提案する。
まず、連続系を離散状態モデルに抽象化し、状態間の確率的遷移によってノイズを捕捉する。
いわゆる区間マルコフ決定過程(iMDP)の遷移確率区間におけるこれらの境界を捉える。
論文 参考訳（メタデータ） (2021-10-25T06:18:55Z) - SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
パラメータ化マルチエージェントシステム(MAS)の検証について検討する。
特に、与えられた状態公式として特徴づけられる不要な状態が、所定のMASで到達可能かどうかについて検討する。
論文 参考訳（メタデータ） (2020-08-11T15:24:05Z) - Implicit Distributional Reinforcement Learning [61.166030238490634]
2つのディープジェネレータネットワーク(DGN)上に構築された暗黙の分布型アクター批判(IDAC)
半単純アクター (SIA) は、フレキシブルなポリシー分布を利用する。
我々は,代表的OpenAI Gym環境において,IDACが最先端のアルゴリズムより優れていることを観察する。
論文 参考訳（メタデータ） (2020-07-13T02:52:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。