Verification-Guided Shielding for Deep Reinforcement Learning

要約

近年、深層強化学習 (DRL) が現実世界のタスクを解決するための効果的なアプローチとして台頭してきました。
ただし、成功にもかかわらず、DRL ベースのポリシーは信頼性が低いため、安全性が重要なドメインへの導入が制限されます。
その結果、正式な安全保証を提供することでこの問題に対処するためのさまざまな方法が提案されています。
2 つの主なアプローチには、シールドと検証が含まれます。
シールドは、潜在的に危険なアクションをオーバーランする外部オンライン コンポーネント (つまり、「シールド」) を使用することでポリシーの安全な動作を保証しますが、すべての決定を検証するために実行時にシールドを呼び出す必要があるため、このアプローチには多大な計算コストがかかります。
。
一方、検証はオフライン プロセスであり、安全でないポリシーを展開前に特定できますが、そのようなポリシーが安全でないとみなされた場合に代替アクションを提供する必要はありません。
この研究では、検証ガイド付きシールド、つまりこれら 2 つの方法を統合することで DRL の信頼性のギャップを埋める新しいアプローチを紹介します。
私たちのアプローチは、形式的検証ツールと確率的検証ツールの両方を組み合わせて、入力ドメインを安全な領域と安全でない領域に分割します。
さらに、クラスタリングと、安全でない領域をコンパクトな表現に圧縮するシンボリック表現手順を採用します。
これにより、効率的な方法で、(潜在的に) 危険な領域のみでシールドを一時的にアクティブにすることができます。
私たちの新しいアプローチにより、正式な安全保証を維持しながら、実行時のオーバーヘッドを大幅に削減できます。
私たちはロボット ナビゲーション ドメインの 2 つのベンチマークでアプローチを広範囲に評価し、そのスケーラビリティと完全性についての詳細な分析を提供します。

要約(オリジナル)

In recent years, Deep Reinforcement Learning (DRL) has emerged as an effective approach to solving real-world tasks. However, despite their successes, DRL-based policies suffer from poor reliability, which limits their deployment in safety-critical domains. As a result, various methods have been put forth to address this issue by providing formal safety guarantees. Two main approaches include shielding and verification. While shielding ensures the safe behavior of the policy by employing an external online component (i.e., a “shield”) that overruns potentially dangerous actions, this approach has a significant computational cost as the shield must be invoked at runtime to validate every decision. On the other hand, verification is an offline process that can identify policies that are unsafe, prior to their deployment, yet, without providing alternative actions when such a policy is deemed unsafe. In this work, we present verification-guided shielding — a novel approach that bridges the DRL reliability gap by integrating these two methods. Our approach combines both formal and probabilistic verification tools to partition the input domain into safe and unsafe regions. In addition, we employ clustering and symbolic representation procedures that compress the unsafe regions into a compact representation. This, in turn, allows to temporarily activate the shield solely in (potentially) unsafe regions, in an efficient manner. Our novel approach allows to significantly reduce runtime overhead while still preserving formal safety guarantees. We extensively evaluate our approach on two benchmarks from the robotic navigation domain, as well as provide an in-depth analysis of its scalability and completeness.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google