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. As a result, various methods have beenput forth to address this issue by providing formal safety guarantees. Two mainapproaches include shielding and verification. While shielding ensures the safebehavior of the policy by employing an external online component (i.e., a``shield'') that overruns potentially dangerous actions, this approach has asignificant computational cost as the shield must be invoked at runtime tovalidate every decision. On the other hand, verification is an offline processthat can identify policies that are unsafe, prior to their deployment, yet,without providing alternative actions when such a policy is deemed unsafe. Inthis work, we present verification-guided shielding -- a novel approach thatbridges the DRL reliability gap by integrating these two methods. Our approachcombines both formal and probabilistic verification tools to partition theinput domain into safe and unsafe regions. In addition, we employ clusteringand symbolic representation procedures that compress the unsafe regions into acompact representation. This, in turn, allows to temporarily activate theshield solely in (potentially) unsafe regions, in an efficient manner. Ournovel approach allows to significantly reduce runtime overhead while stillpreserving formal safety guarantees. We extensively evaluate our approach ontwo benchmarks from the robotic navigation domain, as well as provide anin-depth analysis of its scalability and completeness.