Wasserstein Auto-encoded MDPs: Formal Verification of Efficiently Distilled RL Policies with Many-sided Guarantees

要約

タイトル：Wasserstein Auto-encoded MDPs：多角的な保証で効率的に蒸留されたRLポリシーの形式的な検証

要約：
– DRLは成功例が多いものの、安全性に関するシナリオで学習されたポリシーを展開することはフォーマルな保証の欠如によって妨げられている。
– VAE-MDPは、任意のRLポリシーから形式的に検証可能なコントローラを蒸留する信頼性のあるフレームワークを提供する離散潜在空間モデルであるが、VAEアプローチはいくつかの学習的な欠陥を持っている。
– この問題を解決するために、WAE-MDPを提案している。このモデルは、元のポリシーを実行するエージェントの振る舞いと蒸留されたポリシーの最適輸送の罰則化された形式の最小化を最小化することで、最適輸送の欠点を解決し、精度を高める。
– 我々のアプローチは、蒸留されたポリシーを学習している間にbisimulation保証を提供し、抽象化および表現モデルの品質を具体的に最適化することができる。
– 実験結果から、蒸留ポリシーは最大10倍高速に蒸留でき、潜在モデルの品質が改善されることが示されている。
– さらに、潜在空間での単純な故障時間検証アルゴリズムについての実験結果が提示される。このアプローチによって、簡単な検証技術が可能になり、適用範囲が広がることが示されている。

要約(オリジナル)

Although deep reinforcement learning (DRL) has many success stories, the large-scale deployment of policies learned through these advanced techniques in safety-critical scenarios is hindered by their lack of formal guarantees. Variational Markov Decision Processes (VAE-MDPs) are discrete latent space models that provide a reliable framework for distilling formally verifiable controllers from any RL policy. While the related guarantees address relevant practical aspects such as the satisfaction of performance and safety properties, the VAE approach suffers from several learning flaws (posterior collapse, slow learning speed, poor dynamics estimates), primarily due to the absence of abstraction and representation guarantees to support latent optimization. We introduce the Wasserstein auto-encoded MDP (WAE-MDP), a latent space model that fixes those issues by minimizing a penalized form of the optimal transport between the behaviors of the agent executing the original policy and the distilled policy, for which the formal guarantees apply. Our approach yields bisimulation guarantees while learning the distilled policy, allowing concrete optimization of the abstraction and representation model quality. Our experiments show that, besides distilling policies up to 10 times faster, the latent model quality is indeed better in general. Moreover, we present experiments from a simple time-to-failure verification algorithm on the latent space. The fact that our approach enables such simple verification techniques highlights its applicability.

arxiv情報

提供元, 利用サービス

arxiv.jp, OpenAI