ReachNN: Reachability Analysis of Neural-Network Controlled Systems
ReachNN: Reachability Analysis of Neural-Network Controlled Systems
复制标题
DOI：
10.1145/3358228
复制
发表时间：
2019-10-01
影响因子：
2
通讯作者：
Zhu, Qi
中科院分区：
文献类型：
--
作者：
Huang, Chao;Fan, Jiameng;Zhu, Qi
在动态系统中应用神经网络作为控制器已显示出巨大的潜力。然而，验证包含神经网络控制器的此类控制系统的安全性至关重要且极具挑战性。先前用于验证神经网络控制系统的方法仅限于少数特定的激活函数。在这项工作中，我们提出了一种基于伯恩斯坦多项式的新的可达性分析方法，该方法能够验证具有更通用形式激活函数的神经网络控制系统，即只要它们能确保神经网络是利普希茨连续的。具体而言，我们考虑针对一小部分输入用伯恩斯坦多项式对前馈神经网络进行抽象。为了量化抽象所引入的误差，我们基于伯恩斯坦多项式理论提供了理论误差界估计，并且基于前向可达性分析的紧密利普希茨常数估计方法提供了更实用的基于采样的误差界估计。与先前的方法相比，我们的方法适用于更广泛的神经网络，包括包含多种类型激活函数的异构神经网络。在各种基准测试上的实验结果表明了我们方法的有效性。
Applying neural networks as controllers in dynamical systems has shown great promises. However, it is critical yet challenging to verify the safety of such control systems with neural-network controllers in the loop. Previous methods for verifying neural network controlled systems are limited to a few specific activation functions. In this work, we propose a new reachability analysis approach based on Bernstein polynomials that can verify neural-network controlled systems with a more general form of activation functions, i.e., as long as they ensure that the neural networks are Lipschitz continuous. Specifically, we consider abstracting feedforward neural networks with Bernstein polynomials for a small subset of inputs. To quantify the error introduced by abstraction, we provide both theoretical error bound estimation based on the theory of Bernstein polynomials and more practical sampling based error bound estimation, following a tight Lipschitz constant estimation approach based on forward reachability analysis. Compared with previous methods, our approach addresses a much broader set of neural networks, including heterogeneous neural networks that contain multiple types of activation functions. Experiment results on a variety of benchmarks show the effectiveness of our approach.