Differential Safety Testing of Deep RL Agents Enabled by Automata Learning

Learning-enabled controllers (LECs) pose severe challenges to verification. Their decisions often come from deep neural networks that are hard to interpret and verify, and they operate in stochastic and unknown environments with high-dimensional state space. These complexities make analyses of the internals of LECs and manual modeling of the environments extremely challenging. Numerous combinations of automata learning with verification techniques have shown its potential in the analysis of black-box reactive systems. Hence, automata learning may also bring light into the black boxes that are LECs and their runtime environments. A hurdle to the adoption of automata-learning-based verification is that it is often difficult to provide guarantees on the accuracy of learned automata. This is exacerbated in complex, stochastic environments faced by LECs. In this paper, we demonstrate that accuracy guarantees on learned models are not strictly necessary. Through a combination of automata learning, testing, and statistics, we perform testing-based verification with statistical guarantees in the absence of guarantees on the learned automata. We showcase our approach by testing deep reinforcement learning for safety that have been trained to play the computer game Super Mario Bros.