Abstract
In recent years, Deep Reinforcement Learning (DRL) has emerged as aneffective approach to solving real-world tasks. However, despite theirsuccesses, DRL-based policies suffer from poor reliability, which limits theirdeployment in safety-critical domains. Various methods have been put forth toaddress this issue by providing formal safety guarantees. Two main approachesinclude shielding and verification. While shielding ensures the safe behaviorof the policy by employing an external online component (i.e., a ``shield'')that overrides potentially dangerous actions, this approach has a significantcomputational cost as the shield must be invoked at runtime to validate everydecision. On the other hand, verification is an offline process that canidentify policies that are unsafe, prior to their deployment, yet, withoutproviding alternative actions when such a policy is deemed unsafe. In thiswork, we present verification-guided shielding -- a novel approach that bridgesthe DRL reliability gap by integrating these two methods. Our approach combinesboth formal and probabilistic verification tools to partition the input domaininto safe and unsafe regions. In addition, we employ clustering and symbolicrepresentation procedures that compress the unsafe regions into a compactrepresentation. This, in turn, allows to temporarily activate the shield solelyin (potentially) unsafe regions, in an efficient manner. Our novel approachallows to significantly reduce runtime overhead while still preserving formalsafety guarantees. We extensively evaluate our approach on two benchmarks fromthe robotic navigation domain, as well as provide an in-depth analysis of itsscalability and completeness.