Neural Network Verification as Piecewise Linear Optimization: Formulations for the Composition of Staircase Functions
We present a technique for neural network verification using mixed-integer programming (MIP) formulations. We derive a \emph{strong formulation} for each neuron in a network using piecewise linear activation functions. Additionally, as in general, these formulations may require an exponential number of inequalities, we also derive a separation procedure that runs in super-linear time in the input dimension. We first introduce and develop our technique on the class of \emph{staircase} functions, which generalizes the ReLU, binarized, and quantized activation functions. We then use results for staircase activation functions to obtain a separation method for general piecewise linear activation functions. Empirically, using our strong formulation and separation technique, we can reduce the computational time in exact verification settings based on MIP and improve the false negative rate for inexact verifiers relying on the relaxation of the MIP formulation.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Convex Bounds on the Softmax Function with Applications to Robustness Verification
The softmax function is a ubiquitous component at the output of neural networks and increasingly in intermediate layers as well. This paper provides convex lower bounds and concave upper bounds on the softmax function, w…
Optimization Over Trained Neural Networks: Taking a Relaxing Walk
Besides training, mathematical optimization is also used in deep learning to model and solve formulations over trained neural networks for purposes such as verification, compression, and optimization with learned constra…
Error Bounds for Compositions of Piecewise Affine Approximations
Nonlinear expressions are often approximated by piecewise affine (PWA) functions to simplify analysis or reduce computational costs. To reduce computational complexity, multivariate functions can be represented as compos…
Deep Neural Networks and Finite Elements of Any Order on Arbitrary Dimensions
In this study, we establish that deep neural networks employing ReLU and ReLU$^2$ activation functions can effectively represent Lagrange finite element functions of any order on various simplicial meshes in arbitrary di…
Verification of Geometric Robustness of Neural Networks via Piecewise Linear Approximation and Lipschitz Optimisation
We address the problem of verifying neural networks against geometric transformations of the input image, including rotation, scaling, shearing, and translation. The proposed method computes provably sound piecewise line…