We present a novel approach to efficiently compute tight non-convex enclosures of the image through neural networks with ReLU, sigmoid, or hyperbolic tangent activation functions. In particular, we abstract the input-output relation of each neuron by a polynomial approximation, which is evaluated in a set-based manner using polynomial zonotopes. While our approach can also can be beneficial for open-loop neural network verification, our main application is reachability analysis of neural network controlled systems, where polynomial zonotopes are able to capture the non-convexity caused by the neural network as well as the system dynamics. This results in a superior performance compared to other methods, as we demonstrate on various benchmarks.

翻译：我们提出了一种新颖方法，能够高效计算具有 ReLU、Sigmoid 或双曲正切激活函数的神经网络的图像紧致非凸包络。具体而言，我们通过多项式逼近抽象每个神经元的输入-输出关系，并利用多项式 zonotope 以集合形式对其进行求值。尽管我们的方法同样有利于开环神经网络验证，但其主要应用场景为神经网络控制系统的可达性分析——多项式 zonotope 能够同时捕获由神经网络与系统动力学导致的非凸特性。我们在多种基准测试中证明，与其他方法相比，该方法展现了更优的性能。