Verification-Guided Shielding for Deep Reinforcement Learning

TL;DR

The paper tackles the safety guarantees gap in DRL by proposing verification-guided shielding, which partitions the input space into provably-safe and potentially unsafe regions using both probabilistic and formal verification. Safe regions run the original policy without shielding, while unsafe regions trigger a shield to enforce the safety specification, substantially reducing runtime overhead compared to always-on shielding. The approach combines domain splitting via $\epsilon$-ProVe, formal verification with Marabou, clustering of unsafe regions, and symbolic encoding to enable efficient online checks and shield activation, with empirical validation on Particle World and Mapless Navigation. The offline verification cost is high but amortized, while online performance shows significant overhead reductions, maintaining formal safety across the input domain. This work advances reliable DRL deployment in safety-critical domains and points to future directions in tighter region descriptions and training-time integration.

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.

Figures (4)

• Figure 1: A shielding architecture scheme for a DRL agent AlBloEh18.
• Figure 2: The environments analyzed in our evaluation: Particle World (left) and Mapless Navigation (right). The plot displays the number of episodes on the x-axis and the corresponding success rate on the y-axis.
• Figure 3: An overview of verification-guided shielding. In step (1) we employ $\epsilon$-ProVe to split the input domain into approximated safe (green) and unsafe regions; (2a) these can be further validated with a formal verification tool, (2b) which complements the set of approximated unsafe regions with the ones formally found as such. (3) To reduce the cardinality of this set we employ a clustering algorithm and (4) further simplify the encoded results by using symbolic representation.
• Figure 4: A toy DNN.

Theorems & Definitions (1)

• Definition 1: The DNN-Verification Problem