Verification-Guided Shielding for Deep Reinforcement Learning

TL;DR

This paper introduces verification-guided shielding, a novel method that combines formal verification and shielding to improve the safety and efficiency of deep reinforcement learning policies in safety-critical applications.

Contribution

It presents an integrated approach that reduces runtime overhead of shielding while maintaining formal safety guarantees by partitioning input space and compressing unsafe regions.

Findings

Significantly reduces runtime overhead compared to traditional shielding.

Effectively identifies safe and unsafe regions using combined verification methods.

Demonstrates scalability and safety in robotic navigation benchmarks.

Abstract

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. 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 overrides 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.