Algorithms for Verifying Deep Neural Networks

Neural networks [15] have been widely used in many applications, such as image classification and understanding [17], language processing [24], and control of autonomous systems [26]. These networks represent functions that map inputs to outputs through a sequence of layers. At each layer, the input to that layer undergoes an affine transformation followed by a simple nonlinear transformation before being passed to the next layer. These nonlinear transformations are often called activation functions, and a common example is the rectified linear unit (ReLU), which transforms the input by setting any negative values to zero. Although the computation involved in a neural network is quite simple, these networks can represent complex nonlinear functions by appropriately choosing the matrices that define the affine transformations.