Neural networks have been widely used to solve complex real-world problems.
Due to the complicate, nonlinear, non-convex nature of neural networks, formal
safety guarantees for the output behaviors of neural networks will be crucial
for their applications in safety-critical systems.In this paper, the output
reachable set computation and safety verification problems for a class of
neural networks consisting of Rectified Linear Unit (ReLU) activation functions
are addressed. A layer-by-layer approach is developed to compute output
reachable set. The computation is formulated in the form of a set of
manipulations for a union of polyhedra, which can be efficiently applied with
the aid of polyhedron computation tools. Based on the output reachable set
computation results, the safety verification for a ReLU neural network can be
performed by checking the intersections of unsafe regions and output reachable
set described by a union of polyhedra. A numerical example of a randomly
generated ReLU neural network is provided to show the effectiveness of the
approach developed in this paper.

该论文探讨了一类由 ReLU 激活函数构成的神经网络的输出可达集计算和安全验证问题，并提出了一种逐层计算输出可达集的方法，通过计算输出可达集的结果，可以通过检查不安全区域与由一组多面体描述的输出可达集的交集来执行简单有效的安全验证。