Many approaches for verifying input-output properties of neural networks have been proposed recently. However, existing algorithms do not scale well to large networks. Recent work in the field of model compression studied binarized neural networks (BNNs), whose parameters and activations are binary. BNNs tend to exhibit a slight decrease in performance compared to their full-precision counterparts, but they can be easier to verify. This paper proposes a simple mixed integer programming formulation for BNN verification that leverages network structure. We demonstrate our approach by verifying properties of BNNs trained on the MNIST dataset and an aircraft collision avoidance controller. We compare the runtime of our approach against state-of-the-art verification algorithms for full-precision neural networks. The results suggest that the difficulty of training BNNs might be worth the reduction in runtime achieved by our verification algorithm.
and
Stanford University
Neural networks have been shown to be susceptible to adversarial attacks [Papernot et al., 2016] often leading to drastically different outputs when slightly perturbing their input which can be costly or dangerous. Multiple approaches to evaluate the robustness of networks to adversarial attacks have been developed. Many of these only provide statistical assessments and focus on evaluating the network on a large but finite collection of points in the input space. However, given that the input space is, in principle, infinite in cardinality, it is not viable to assess the output for all the points in the input space.
Recently, new approaches have emerged as an alternative to formally certify the input-output properties of neural networks [Liu et al., 2021]. Properties are often specified in the form of a statement that if the input belongs to a set X , then the output is in a set Y . In the context of control, this formulation can be used to verify that the network satisfies safety constraints; in the classification setting, this formulation can be used to certify that points near a training sample are assigned the same label as that sample.
Verification algorithms are typically designed to be sound, which means that they will only conclude a property holds if the property truly holds [Katz et al., 2017; Katz et al., 2019]. With the aim to improve efficiency, some approaches sacrifice completeness, meaning that even if a property holds, the algorithm might fail to identify it. Incomplete algorithms often rely on over-approximation, allowing them to scale to problems involving larger networks, high dimensional input spaces, or high dimensional output spaces.
Even when restricting the class of networks to those with Rectified Linear Unit (ReLU) activation functions (or even a more general piecewise-linear function) the problem has been shown to be NP-hard [Katz et al., 2017]. The hardness of the verification problem has motivated many different approaches [Liu et al., 2021], including reachability, optimization and search algorithms. Even incomplete algorithms struggle to verify properties of networks with sizes commonly encountered in contemporary applications. In principle, simpler models should be easier to verify and binarized neural networks (BNNs) [Hubara et al., 2016] are simpler than traditional full precision neural networks. Their parameters are binary and their activations are binary.
Binarization is an extreme quantization scheme that can significantly reduce memory and computation requirements. However, binarization introduces non-differentiable and even non-continuous blocks to the computational graph of a network, which complicates the optimization used to train the network. However, recent work motivated by their applicability in highly constrained environments such as edge devices has enabled them to achieve performance comparable to traditional full precision networks [Hubara et al., 2016].
The reduced memory requirement and simplified computation resulting from this representation has a drawback: binarized neural networks are harder to train. A major challenge is back propagating the gradient of the weights through sign functions. There are workarounds [Simons and Lee, 2019] such as using straight-through estimators (STE) [Hubara et al., 2016].
This paper presents an approach to verify properties of BNNs that leverages their structure. The verification problem is formulated as a mixed integer programming (MIP) problem that encodes the input set X by constraining variables associated with the input layer of the network and the output set Y by constraining variables associated to the output layer of the network. In our approach, we leverage the binary nature of both the parameters and the activations of the network.
Experimentally, we show that our approach can verify properties of BNNs. Section 4 demonstrates the capabilities of our approach by formally assessing the adversarial robustness of BNNs trained on the MNIST [LeCun and Cortes, 2010] dataset and properties of a collision avoidance system [Katz et al., 2017]. We compare the runtime of our approach to that of the state-of-the-art implementation of a full precision network verification algorithm for the equivalent full precision networks. Our proposed approach reduces significantly verification runtime. 2
Consider F a feedforward neural network with n layers with input x 2 Dx Rk0 and output y 2 Dy Rkn . Here, y = F (x) corresponds to evaluating the network on input x and obtaining output y, k0 is the dimensionality of x, and kn is the dimensionality of y. We assume that all inputs and outputs are flattened to vectors. Each layer in F is a function fi : Rki 1 ! Rki , where ki is the dimensionality of the hidden variable zi in layer i. Accordingly, z0 = x and zn = y. The network can be represented by
F = fn fn fn 1 f1 and
zi = fi(zi 1) = i (Wizi 1 + bi) where Wi 2 Rki ki 1 is the weight matrix, bi 2 Rki is the bias vector, and i : Rki ! Rki is the activation function.
Let zi;j be the value of the jth node in the ith layer, wi;j 2 R1 ki 1 be the jth row of Wi, and wi;j;k be the kth entry in wi;j . Given that activation functions are usually componentwise vector functions we have that zi;j = i;j (wi;j zi 1) =
X wi;j;kzi 1;k k
! = i;j (z^i;j ) (1) (2) (3) (4) where z^i := Wizi 1. We dropped the bias terms in this analysis for compactness and without loss of generality.
A binarized neural network is a network involving binary weights and activations [Hubara et al., 2016]. The goal of network binarizaion is to represent the floating-point weights W and the activations zi;j for a given layer using 1 bit. The parameters are represented by: where BW and Bz are binarized weights and binarized activations, with scaling factors and used for batch normalization. The sign function is often used to compute QW and
The above representation enables an easy implementation of batch normalization while keeping most parameters and operations binary.
In this context, the arithmetic operations needed for a forward pass of a layer zb in a binarized network F b can be computed as:
Some BNN architectures call for binarized inputs as well. Our verification approach does not require binarized inputs, but this requirement is easy to incorporate by representing floating or fixed point inputs as a combination of binary inputs, either by quantizing or directly using their binary representation.
Section 3 derives how each type of block can be encoded with linear constraints, enabling the formulation of a mixedinteger programming problem for verification purposes. The last layer of a network can be used in different ways, often using a softmax or an argmax operator. In either case, we can encode desired properties at the output of the layer before such functions, at the so called logits.
The verification problem consists of checking whether inputoutput relationships of a function hold [Liu et al., 2021]. A subset of the input space X Dx and a subset of the output space Y Dy are defined. In its most general form, solving the verification problem requires certifying whether the following holds: In general, the input and output sets could have any geometry but are often constrained by the verification algorithm. Our approach restricts the class of X and Y to closed polytopes, corresponding to the intersection of half-spaces. These regions can be encoded as a conjunction of linear constraints, which is required for our mixed integer programming formulation.
Applications Given that neural networks provide the stateof-the-art performance for many tasks, such as perception and control [Katz et al., 2017] tasks, studying their robustness has attracted significant attention [Papernot et al., 2016]. In the context of image classification, a network F assigns a value to each of the possible labels in its training set and the maximum value arg maxi yi is often used to impute the label of an input x. Consider an input x0 with label i 2 f1; : : : ; lng. It would be desirable that yi > yk for all j 6= i , which can be encoded with the following sets:
n X = x 2 Dx : kx
x0kp Y = fy 2 Dy : yi > yj 8j 6= i g ; o ; (13) (14) where is the radius of the allowable perturbation in the input. If p = 1 or p = 1, we have linear constraints. Encoding the output set Y is not possible with a single linear program given that the maximum operator requires a disjunction of half-spaces. With our MIP formulation, the set can be encoded directly.
There are plenty of approaches to verifying properties of neural networks [Liu et al., 2021]. Some methods approach verification as an optimization problem, which is an idea that we will use here. Many methods that only work for piecewise linear functions implement a search strategy over the activation state of the nodes in the network. Some apply Satisfiability Modulo Theory (SMT) by iteratively searching for assignments that satisfy all given constraints while treating the non-linear constraints lazily. One such method is the Reluplex algorithm [Katz et al., 2017; Katz et al., 2019], which can be used to verify properties of binarized neural networks. However, without significant modification, it would not exploit the specific characteristics of BNNs.
There are a few approaches designed specifically for verifying properties of BNNs. Some approaches rely on SAT solvers by reducing the verification problem to a Boolean satisfiability problem [Narodytska et al., 2018; Narodytska et al., 2020] which limits their applicability exclusively to fully binarized networks (networks with exclusively binary parameters and activations). Recently, a SAT solver based approach that is able to handle BNN constraints to speedup the verification process was introduced [Jia and Rinard, 2020a].
Another approach that can be applied to networks with both binary and full precision parameters and piece-wise linear activations functions was recently introduced [Amir et al., 2021] and is an SMT-based technique that extends the Reluplex algorithm [Katz et al., 2019] and includes various optimizations specifically designed to leverage BNNs.
Our approach relies on a simple mixed integer linear programming formulation, allowing us to handle both fully and partially binarized neural networks. A similar approach has been demonstrated to work well for DNNs [Tjeng et al., 2019] and MIP has been also used for reachability analysis [Lomuscio and Maganti, 2017]. Our main contribution is to apply MIP to the verification of BNNs. 3
Binarized neural networks are composed of piecewise-linear layers that may be fully connected, convolutional, or averagepooling that may have piecewise-linear activation functions, such as ReLU, max and sign. Other commonly used elements such as batch normalization, shortcut connections, and dropout can be also characterized as affine transformations at evaluation time.
In order to address the verification problem in Section 2.3, we encode each of the components of the network as a set of linear constraints and then apply existing MIP technology to solve it. We encode the input and the linear equations that describe the forward-pass of the network. We then encode YC , the complement of the output set Y, and search for a feasible assignment. Any feasible assignment corresponds to a counterexample of the desired property. If no feasible assignment is found, then we can conclude that the network maps all the points in X to Y, which certifies the property.
Below we present the formulation of each block as a set of linear constraints.
Input and Output Sets. The verification problem consists of determining whether all the elements in an input set X map to an output set Y. In order to formulate that problem as a MIP, then X must be expressible as a conjunction of linear constraints. Additionally, given that the MIP solver will search for a feasible assignment, we need to formulate YC as another polyhedron given that Therefore, the input set and the complement of the output set have to be encoded as linear constraints on their corresponding variables.
Linear. z^i = Qizi 1 where Qi 2 f 1; 1gki+1 ki z^i;j = qjT zi 1 j = 1; : : : ; ki+1 (18) ReLU. zi = ReLU(z^i) = max(0; z^i) and given that l z^i u and 2 f0; 1g, we can encode the block as: Sign. zi = sign(z^i) l(1
) zi z^i zi 0 z^i z^i zi zi
u 2 f0; 1g
0 =) zi = 1 z^i < 0 =) zi = 0 (15) (16) (17) (19) (20) (21) (22) (23) (24) 2 f0; 1g (31) Additionally, given the structure of the linear block that precedes the sign block and the fact that the variables only take values in f 1; 1g, we can always easily compute l ki and u ki.
Batch Normalization. The batch normalization blocks have the output of linear blocks as their input.
zi = ki yi ki ki + k where y = (y1; : : : ; ynk+1 ) and k; k; k ki 2 R, assuming ki > 0. which can be rewritten as
ki zi = ki yi ki ki + ki ki i = 1; : : : ; nk+1 (33) which is a linear constraint.
Max. y = max(x1; x2; : : : ; xm) and li xi ui can be formulated as a set of linear constraints in the following way: y xi + (1 i)(umax; i li) xi y m X i = 1 i=1 i = 1; : : : ; m i = 1; : : : ; m i 2 f0; 1g (37)
In practice, BNNs are implemented by repeated compositions of the blocks described above. In the case of BNNs, the usual order of the linear layer and batch normalization are exchanged as suggested by [Hubara et al., 2016] but the MIP formulation is equivalent.
Using the above formulations, we proceded to encode the verification problem by parsing a BNN to construct the constraints that represent its forward pass and the corresponding input and output set constraints. We then call a mixed integer program solver and search for a feasible solution. If a feasible solution is found, then it certifies that the property does not hold and it serves as a counter example. If the search for a feasible solution terminates, given the completeness of the procedure, we certify that the property holds.
We implemented a tool that parses networks and produces their corresponding encoding for the solver. In the following section, we present the experiments we used to evaluate our approach and compare it to traditional DNN verification tools. 4
To demonstrate our approach, we performed a series of experiments. We then compared the performance of our approach to that of other publicly available verification algorithms. However, given the fact that our algorithm is specifically designed for BNNs, we decided to compare its performance to the performance of verification algorithms for (26) (27) (28) (29) (30) (32) (34) (35) (36)
DNNs. Even though the networks are not identical, we opted for this comparison to motivate the use of BNNs for tasks where DNNs are normally favored given that we expect BNN verification to be significantly faster. 4.1
We trained DNNs and BNNs on the MNIST dataset [LeCun and Cortes, 2010]. We did not tune hyper-parameters, and we used a very simple training setup. The test set accuracy of the DNN was 98:2% and the BNN 95:6%. We thresholded all the grayscale values to black and white, which is equivalent to adding a binarization block at the input of the network.
We verified robustness properties using the input and output sets defined in equations 13 and 14 by allowing a maximum perturbation of around known input points using the p = 1 norm. We set a time limit of 120 seconds for each property and report our results in Table 1. timeout
0.1 0.3 We used a networks and property introduced by Katz et al. [2017]. We trained a BNN version of the ACAS controller and tested a subset of Property 10 that only requires running one query. We sliced the state space by setting the time until loss of vertical separation = 5 and the previous advisory as clear-of-conflict. We fixed the speed of ownship and speed of intruder values to simplify the property. For the BNN, we used 8-bits to represent each input and added a layer at the input to decrease the dimensionality to that of the original ACAS network. Quantizing the input can significantly alter the behavior of the controller, our goal was simply to assess the speedup of verification. We also trained versions of the network with full precision inputs but neither satisfied the property. We report our results in Table 2. 5
Our results indicate that our simple MIP approach for verifying properties of BNNs performs significantly faster than other methods for DNNs. Training BNNs is challenging but full precision 8 bit 2174.43 1203.44 1634.25 time (s) result violated holds holds the reduction in verification cost should be considered and incentivize their use for safety-critical applications that require verification of certain properties.
In our MNIST experiments we were able to verify the robustness of networks with about a 10 reduction in verification time.
Our ACAS experiments show that our approach is able to verify BNNs that implement controllers in about 20 reduced time. BNNs appear to be particularly well suited as controllers for safety critical systems.
Our proposed approach encodes BNN as mixed integer linear programs and is able to verify properties of binarized neural networks and partially binarized neural networks. Our experiments indicate that this approach is about an order of magnitude faster than verifying properties of comparable full precision neural networks.
The ease with which we can verify BNNs should increase their use for safety critical applications. BNNs are harder to train, but the difficulty might be worth the cost given how much faster verification becomes along with the efficient hardware implementations that they enable. The use of BNNs has some drawbacks and requires considerations such as how to handle non-binary inputs. Quantizing the inputs allows us to preserve the binary architecture but decreases the applicability of BNNs because some applications might have continuous input domains that would be better modeled with floating point numbers. However, it appears that even verified networks with floating point parameters are potentially unsafe [Jia and Rinard, 2020b].
We used a general purpose mixed integer programming solver. A potential area of future research would be to design a MIP solver that exploits some of the BNN specific characteristics of the problems to further decrease verification time. Another potential direction would be to train ternary BNNs in order to explore the impact of sparsification on runtime, given that he equations that encode ternary BNNs require fewer variables