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

要約

深層強化学習 (DRL) には多くの成功例がありますが、安全性が重要なシナリオでこれらの高度な手法を通じて学習したポリシーの大規模な展開は、正式な保証がないために妨げられています。
変分マルコフ決定プロセス (VAE-MDP) は、任意の RL ポリシーから正式に検証可能なコントローラーを抽出するための信頼できるフレームワークを提供する離散潜在空間モデルです。
関連する保証は、パフォーマンスや安全性の特性の満足度などの関連する実用的な側面に対処しますが、VAE アプローチには、主に抽象化と表現の保証がないため、いくつかの学習上の欠陥 (事後崩壊、遅い学習速度、不十分なダイナミクス推定) があります。
潜在的な最適化をサポートします。
Wasserstein auto-encoded MDP (WAE-MDP) を導入します。これは、元のポリシーを実行するエージェントの動作と抽出されたポリシーとの間の最適なトランスポートのペナルティ付きフォームを最小化することによって、これらの問題を修正する潜在空間モデルです。
保証が適用されます。
私たちのアプローチは、抽出されたポリシーを学習しながら二重シミュレーションの保証をもたらし、抽象化と表現モデルの品質の具体的な最適化を可能にします。
私たちの実験では、ポリシーを最大 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, Google