Reachability analysis is a promising technique to automatically prove or disprove the reliability and safety of AI-empowered software systems that are developed by using Deep Reinforcement Learning (DRL). Existing approaches suffer however from limited scalability and large overestimation as they must over-approximate the complex and almost inexplicable system components, namely deep neural networks (DNNs). In this paper we propose a novel, tight and scalable reachability analysis approach for DRL systems. By training on abstract states, our approach treats the embedded DNNs as black boxes to avoid the over-approximation for neural networks in computing reachable sets. To tackle the state explosion problem inherent to abstraction-based approaches, we devise a novel adjacent interval aggregation algorithm which balances the growth of abstract states and the overestimation caused by the abstraction. We implement a tool, called BBReach, and assess it on an extensive benchmark of control systems to demonstrate its tightness, scalability, and efficiency.

本文提出了一种针对DRL系统的紧密可扩展的可达性分析方法，使用抽象状态处理内嵌的神经网络以避免神经网络的过估计，并设计了一种名为BBReach的工具来评估其紧密性、可扩展性和效率。

BBReach: 深度强化学习系统的紧凑且可扩展的黑盒到达性分析