Title: IN SEARCH FOR A SAT-FRIENDLY BINARIZED NEU-RAL NETWORK ARCHITECTURE

Abstract: Analyzing the behavior of neural networks is one of the most pressing challenges in deep learning. Binarized Neural Networks are an important class of networks that allow equivalent representation in Boolean logic and can be analyzed formally with logic-based reasoning tools like SAT solvers. Such tools can be used to answer existential and probabilistic queries about the network, perform explanation generation, etc. However, the main bottleneck for all methods is their ability to reason about large BNNs efficiently. In this work, we analyze architectural design choices of BNNs and discuss how they affect the performance of logic-based reasoners. We propose changes to the BNN architecture and the training procedure to get a simpler network for SAT solvers without sacrificing accuracy on the primary task. Our experimental results demonstrate that our approach scales to larger deep neural networks compared to existing work for existential and probabilistic queries, leading to significant speed ups on all tested datasets.

1. INTRODUCTION:

Deep neural networks are among the most successful AI technologies making impact in a variety of practical applications ranging from vision to speech recognition and natural language (Goodfellow et al., 2016) . However, many concerns have been raised about the decision making process behind machine learning technology. For instance, can we trust decisions that neural networks make (EU Data Protection Regulation, 2016; Goodman & Flaxman, 2017; NIPS IML Symposium, 2017) ? One way to address this problem is to define properties that we expect the network to satisfy. Verifying whether the network satisfies these properties sheds light on the properties of the function that it represents. Verification guarantees can reassure the user that the network behaves as expected.

There are two main approaches to neural network analysis. The first approach, the certification of neural networks, trains a verified network that satisfies given properties, e.g. a network that is guaranteed to be robust to adversarial perturbations (Wong & Kolter, 2018; Dvijotham et al., 2018; Raghunathan et al., 2018; Mirman et al., 2018) . However, a set of properties must be known in advance, which might not always be possible. Moreover, enforcing a set of properties during the training procedure can significantly affect the accuracy of the network on the primary task. Finally, certification techniques work with relaxation of the original problem and might not be able to certify robust inputs. The second approach, the verification of neural networks, takes a trained network as input and focuses only on the verification task (Katz et al., 2017; Weng et al., 2018; Singh et al., 2019; Xiao et al., 2019) . A number of verification frameworks were proposed over the last few years that can be roughly divided into complete (Katz et al., 2017; 2019; Tjeng et al., 2019) and incomplete methods (Weng et al., 2018; Zhang et al., 2018; Singh et al., 2018) . As the training and verification tasks are separated, a wide set of properties can be checked. However, the scalability of this approach remains an issue, especially for complete methods.

In this work we tackle the scalability problem of the complete verification approach, in the context of an important class of networks, Binarized Neural Networks(BNNs) (Hubara et al., 2016) . A BNN is an extreme case of quantized neural networks where parameters are primarily binary. These networks have a number of important features that are useful in resource constrained environments, like embedded devices or mobile phones (McDanel et al., 2017; Kung et al., 2017) . They are memory efficient as only one bit per weight must be stored and are computationally efficient as all activations are binary, which enables the use of specialized algorithms for fast binary matrix multiplication. More importantly, these networks admit an exact representation in Boolean logic (Narodytska et al., 2018; Cheng et al., 2018) . Such a representation enables us to apply powerful Boolean reasoning tools to the analysis of BNNs. For example, we can perform a rich set of queries, ranging from existential queries (e.g., is there a faulty input to the network?), to counting queries (e.g., how many faulty inputs exist?), using logic-based reasoners (Baluta et al., 2019; Shih et al., 2019) . This paper makes two main contributions.

• First, we analyze how different architectural design choices for BNNs affect the performance of SAT solvers. To identify influential parts of the design, we scrutinize BNNs at three levels of granularity: individual neurons, blocks of layers, and network as a whole.

Our work continues work of (Narodytska et al., 2018; Cheng et al., 2018) where BNNs were analyzed on the network level. For the block and network levels, we only analyse bottlenecks, propose possible research directions, and position existing work on the network level. Our main contribution here is within the network level.

• Second, we exploit our findings to train SAT-friendly BNNs. We propose a modified training procedure that makes the resulting network easier for logic-based verification tools, like SAT solvers, to reason about. Modifications to training are crucially performed so that the accuracy of the network is unaffected. Overall, our approach (a) preserves the separation between training and verification, by not committing to a certain property during training and (b) boosts the performance of logic-based verification. We implemented the proposed methods and demonstrated significant performance gains over previous work (Narodytska et al., 2018; Khalil et al., 2019; Baluta et al., 2019) . We get more than 10x-20x improvements on tested benchmarks for both verification and quantitative queries, e.g., finding the probability that a perturbation yields an adversarial example.

2. BACKGROUND:

Boolean satisfiability (SAT). We assume notation and definitions standard in Boolean Satisfiability (SAT), i.e. the decision problem for propositional logic (Biere et al., 2009) . SAT formulas are defined over a set of Boolean variables {x 1 , . . . , x n }. A literal l i is a variable x i ('positive' polarity) or its complement xi ('negative' polarity). Cardinality constraints over Boolean variable are constraints of the form

n i=0 l i ≥ k, where l i ∈ {x i , xi }.

In this work we employ reified cardinality constraints: x ⇔ n i=0 l i ≥ k. We use the full sequential counters encoding (Sinz, 2005b) to model this constraint in SAT (see Appendix A for details of the encoding). However, other encodings can be used. We also work with (approximate) solutions counting solvers, e.g. ApproxMC3.

See details on such methods in Appendix as well A.

Binarized neural networks:

We summarise standard BNN structure (Hubara et al., 2016) . A BNN consists of blocks of layers, each mapping binary vectors to binary vectors. We define a block (referred to as BLOCK) as a function mapping an input to an output, i.e., BLOCK i : {-1, 1} ni → {-1, 1} ni+1 , i = 1, . . . , d -1, where d -1 is the number of hidden layers. The last block, denoted OUTPUT, has a slightly different structure: OUTPUT : {-1, 1} n d → R p , where p is the number of outputs of the network. Each BLOCK takes an input vector x and applies three transformations: a linear transformation (LIN), batch normalization (BN) and binarization (BIN)1 . Table 1 shows transformations of internal and output blocks in detail.

Structure of ith internal block, BLOCKi:

: {-1, 1} n i → {-1, 1} n i+1 on input x i ∈ {-1, 1} n i LIN y = A i x i + b i , where A i ∈ {-1, 1} n i+1 ×n i and y, b i ∈ R n i+1 BN zj = α i j y j -µ i j σ i j + γ i j , where α i , γ i , µ i , σ i , z ∈ R n i+1 BIN x i+1 = sign(z), where x i+1 ∈ {-1, 1} n i+1

Structure of the output block, OUTPUT : 

{-1, 1} n d → R p on input x d ∈ {-1, 1} n d LIN o = Cx d + q, where C ∈ {-1, 1} p×n d and q ∈ R p

3. LOGIC-BASED ANALYSIS OF BNNS:

An important property of BNNs is that they allow exact encoding into SAT: for each BNN there exists a SAT formula such that solutions of the formula are exactly the set of all valid input/output pairs of the BNN (Narodytska et al., 2018; Cheng et al., 2018) . Such translation opens many possibilities for logic-based analysis of BNNs. In this section, we describe several such methods. We highlight that reasoning tools available for BNNs are more diverse and powerful compared to frameworks available for the analysis of conventional networks, which focus mostly on verification and certification of NNs. Since logic-based analysis of BNNs exploits their logical representation, we start by revisiting how to obtain such a representation before discussing logic-based BNN analysis tools.

3.1. SAT ENCODING OF BNNS:

We consider how to generate a logical encoding of a BNN (Narodytska et al., 2018) . Consider a single block BLOCK i , which applies three transformations to the input vector. The first step is a linear (affine) transformation (LIN) of the input vector. The linear transformation can be based on a fully connected layer or a convolutional layer. The linear transformation is followed by a scaling which is performed with a batch normalization operation (BN) (Ioffe & Szegedy, 2015a) . Finally, a binarization is performed using the sign function to obtain a binary output vector (BIN). We will use the following running example to demonstrate the encoding.

Example 3.1. Consider a block with three inputs and two outputs. We define transformation parameters as follows:

LIN : A = [1, -1, 1; -1, -1, 1], b = [0, 0] BN : α = [0.1, 0.1], µ = [1, -1], σ = [1, 1], γ = [0.1, 0.2]

We encode these transformations as a system of logical constraints. We introduce a vector of binary variables x i ∈ {-1, 1} ni to encode inputs and x i+1 ∈ {-1, 1} ni+1 to encode outputs of BLOCK i . Since transformations are applied sequentially, we can encode the block as their composition:

z j = α i j σ i j ( ni t=1 a i j,t x i t + b i j -µ i j ) + γ i j , j = 1 . . . n i+1

(1)

EQUATION

where a i j,t and b i j are parameters of LIN, α i j , σ i j , µ i j and γ i j are parameters of BN. To obtain a SAT encoding, we need to eliminate binary variables as a SAT formula is defined over Boolean variables. We introduce Boolean variables x t ∈ {0, 1}, t = 1, . . . , n i and relate them to the corresponding binary variables x t : x t = 2x t -1, t = 1, . . . , n i . We get that if x t = 0 then x t = -1, otherwise x t = 1. We can now rewrite the last expression as

x i+1 j = sign α i j σ i j ( ni t=1 a i j,t 2x i t - ni t=1 a i j,t + b i j -µ i j ) + γ i j , j = 1 . . . n i+1 .

We denote C j = (-ni t=1 a i j,t + b i j -µ i j ), as these are just constants. We get

EQUATION

Example 3.2. Consider how the encoding works on Example 3.1. We introduce three binary variables to encode inputs x 0 i , i = 0, 1, 2, and two binary variables to encode outputs x 1 0 and x 1 1 . Inputs and outputs are connected as follows:

x 1 0 = sign(0.1(x 0 0 -x 0 1 + x 0 2 -1) + 0.1 ≥ 0); x 1 1 = sign(0.1(-x 0 0 -x 0 1 + x 0 2 + 1) + 0.2 ≥ 0). Next we perform variable replacement as explained above using the relation x t = 2x t -1. Note that α 0 1 and α 0 2 are both positive so we get:

x 1 0 ⇔ (0.1(2x 0 0 -1 -(2x 0 1 -1) + 2x 0 2 -1 -1) + 0.1 ≥ 0) ⇔ (x 0 0 -x 0 1 + x 0 2 ≥ 1/2), x 1 1 ⇔ (0.1(-(2x 0 0 -1) -(2x 0 1 -1) + 2x 0 2 -1 + 1) + 0.2 ≥ 0) ⇔ (-x 0 0 -x 0 1 + x 0 2 ≥ -4/2).

The final step is to encode reified cardinality constraints using Boolean variables instead of binary (integer) variables in Equation 3. We recall the following tautology for a Boolean variable x t + xt = 1, where xt is a negation of x t . As all coefficients a i jt ∈ {-1, 1}, Equation 3 contains linear constraints with unary coefficients (see the last transformation in Example 3.2). We denote N j = |{a i jt < 0, t = 1, . . . , n i+1 }| the number of negative coefficients in the jth row and assume

EQUATION

where

l i t = x i t if a i jt > 0 xi t if a i jt < 0 and h j = -γ i j σ i j /(2α i j ) -C j /2 -N j if α i j > 0 -γ i j σ i j /(2α i j ) -C j /2 -N j if α i j < 0.

We recall that a constraint of type Equation 4 is a reified cardinality constraint that can be translated into Boolean formulae (Narodytska et al., 2018) . We present details of such translation in Appendix A. We refer to a SAT encoding of BLOCK as BINBLOCK i (x i , x i+1 ). Similarly, we can encode the OUTPUT block that we show in details below as our method needs to make modifications to the original encoding (see Appendix B.1). We refer to encoding of OUTPUT as BINOUTPUT. We can now represent the entire network as a Boolean formula: BINBNN(x, o)

≡ d-1 i=1 BINBLOCK i (x i , x i+1 ) ∧ BINOUTPUT(x d , o), where BINBLOCK i (x i , x i+1 ) encodes the ith block BLOCK i with input x i and output x i+1 , i ∈ [0, d -1], BINOUTPUT(x d , o

) is a Boolean encoding of the last layer.

3.2. BNN'S REASONERS:

We consider three types of reasoners designed for BNNs. The first type includes property checkers that can handle existential queries, e.g. 'is there an input of the network that violates a given property?'. The second type deals with probabilistic queries, e.g. 'what is an approximate probability that a valid input will violate a given property?'. Finally, the most powerful reasoner answers a large set of queries, like generating explanations, finding exact probabilities of property violations, etc.

Property checkers. Property checking of BNNs using a SAT-based approach was proposed in (Narodytska et al., 2018; Cheng et al., 2018) . Given a precondition prec on the inputs x and a property prop on the outputs o, we check if the following statement is valid:

prec(x) ∧ BINBNN(x, o) ⇒ prop(o).

To decide if there exists a counterexample to this property, we look for a model of: prec(x) ∧ BINBNN(x, o) ∧ ¬prop(o). An example of property checking is to check for the existence of adversarial perturbations. In this case, prec defines an -ball of valid perturbations and prop states that the classification should not change under small perturbations. An optimization version of this problem was considered in (Khalil et al., 2019) using ILP rather than SAT solvers to reason about BNNs.

Quantitative reasoners. In many practical applications, it is not sufficient to check for the existence of a counterexample to a given property. We would like to know precise or approximate probability of the undesired behavior. (Baluta et al., 2019) , proposes a framework to answer such probabilistic queries using approximate model counting tools. The main technical challenge is to perform efficient approximate solution counting of a SAT formula that contains a BINBNN as a subformula. Consider the property verification formula above. By approximately counting solutions, we obtain an estimate of the probability of a valid input leading to a property violation with a controllable and bounded error2 . Baluta et al. (2019) identified three applications of this framework in the security domain: robustness, trojan attacks, and fairness. Narodytska et al. (2019) investigated how a similar type of quantitative reasoning can be used to assess the quality of ML explanations.

Knowledge compilation engines. The compilation of BNNs is an interesting research direction that aims to compile a BINBNN into a tractable structure, a logic graph-based representation of the formula (Shih et al., 2019; Choi et al., 2019) that supports a wide range of queries about the original BNN, including exact solution counting for probabilistic queries or generating logical explanations for network decisions. Interestingly, BNNs often admit succinct representations as the networks contain redundancies that can be eliminated by compilation. For example, (Choi et al., 2019) reports large reduction in the representation size on some benchmarks.

As can be seen from this overview, the success of these applications depends on the ability to reason efficiently about the underlying formula in the corresponding logical reasoner, e.g., a SAT solver, an approximate model counting method, or a knowledge compilation engine. On the one hand, BNNs are potentially easier to reason about compared to full-precision networks3 . On the other hand, SAT is a hard combinatorial problem. Hence, developing efficient decision procedures require exploiting the special structure of BNNs.

4. ANALYSIS OF BNN'S FROM THE SAT STANDPOINT:

In this section we analyze the properties of the formula BINBNN from the perspective of a solver developer. We discuss how these properties affect solver performance both positively and negatively. We highlight parts of the BNN architecture that can be exploited to speed up logical reasoners. To structure our analysis, we consider BNN's at three levels of granularity that naturally correspond to sub-formulas of BINBNN. (Narodytska et al., 2018; Cheng et al., 2018; Khalil et al., 2019) discussed and exploited properties of BNNs on the highest level of granularity, but we believe that there are more opportunities to take advantage of the structure if we look at all levels systematically.

Neuron level:

We start with the level of an individual neuron. Recall that the value of a neuron is determined by Equation 4. Let us examine it in more detail. We note that A is a dense matrix by design as all entries must be 1 or -1. At the same time, the number of literals in Equation 4 is equal to the width of A for fully-connected layers or the filter size for convolutional layers. Therefore, the high density of A leads to a large number of variables in the cardinality constraint of Equation 4. To make things worse, depending on the encoding, the number of auxiliary variables to encode Equation 4 depends on n i and h j , e.g., the number of auxiliary variables introduced is O(n i h j ) for the sequential counters encoding, leading to large SAT representations. Hence, dense matrices lead to large encodings. Next, consider the logical structure of Equation 4. Note that we have an equivalence relation between the value of the neuron and the cardinality constraint. A key component of a SAT solver is the inference procedure, that at each point of the search infers values of unassigned variables. Suppose Equation 4 produces the following constraint x 1 1 ⇔ (x 0 0 + x0 1 + x 0 2 ≥ 2). Moreover, suppose x 1 0 and x 0 2 have not been fixed yet and x 0 0 = 1. Note that any setting of variables x 0 1 , x 0 2 can be extended to a valid assignment in this constraint. Hence, no inference is possible. In contrast, assume we only had cardinality constraints, i.e. x0 0 + x0 1 + x 0 2 ≥ 2, then we can infer that x 0 1 = 0 and x 0 2 = 1 at this point. As the vast majority of constraints in the encoding contain the equivalence relation, this hinders the inference algorithm's ability to find implied variables, making the solver dive deep before a conflict occurs.

Block level Next we go up one level of granularity and focus on the encoding of BLOCK. We note that a block is encoded by a set of constraints over the same variables. We count over these variables therefore multiple times. This observation hints at an opportunity to identify shared computations and exploit them to get more succinct encodings. For example, if we have two constraints (x 0 0 -x 0 1 + x 0 2 ≥ 2) and (-x 0 0 -x 0 1 + x 0 2 ≥ -2) then we encode the partial sum -x 0 1 + x 0 2 for both constraints and this can be shared. Our ability to share computations depends on the patterns in which 1 and -1 appear in the matrix A as these coefficients control whether variables appear positively or negatively in each constraint. As A is a full matrix and no patterns are enforced on occurrences of 1 and -1 between rows the amount of sharing is rather small for the standard BNN architecture.

Network level Finally, we consider the entire BNN as a chain of blocks. As each block is encoded individually, BINBNN is a conjunction of BINBLOCK formulas that are loosely connected via variables x i , i = 1, . . . , d -1. As discussed above, x i variables are a small fraction of the total number of variables. Two factors affect solver performance. First, the block-wise structure of the BINBNN formula suggests that formula decomposition can be exploited by the solver. Second, the BINBNN formula effectively simulates the network function for all possible inputs. Additional constraints on inputs/outputs of the network, e.g., in the verification problem in Section 3.2, are the main source of inconsistencies. Therefore, conflict-driven learning, which is the core of all SAT solvers, should perform directed search, starting from either the last or the first blocks of the formula moving toward the first (last) blocks as search progresses rather than jumping unguided between layers. Such guidance might help to discover conflicts faster.

5. TOWARD SAT-FRIENDLY BNNS:

We discuss how alternative architectural design choices for BNNs can be used to take advantage of the identified properties to reason faster. We observe that, assuming a fixed network architecture, our design options are limited. We therefore make an important assumption that we can change the architecture of the BNN and have access to the training procedure. While this is a strong assumption, we believe that BNN designers will be willing to incorporate changes into the training procedure as long as they do not cause accuracy loss. As before, we structure our solutions and observations using different levels of granularity.

Neuron level As discussed above, there are two properties of Equation 4 that need to be addressed. First issue is that A is a dense matrix by design of BNNs. To deal with this issue, we propose using a ternary quantization procedure instead of a binary quantization to learn sparse matrices for linear transformations. We recall that BNN is trained using two matrices: a full-precision matrix W i that is updated during the gradient decent and a binarized matrix A i , connected as follows A i = sign(W i ). A i is used on the forward path and during inference. The modification we make is a simple twosided ternary quantization of A i during training:

EQUATION

)

where T is a parameter. In principle, T can be a learnable parameter (Zhu et al., 2017) . However, in (Darabi et al., 2018) , it was observed that weights of W are naturally grouped around points -1, 1 and 0 during training. Therefore, we use a fixed threshold T , obtained from the distribution of weights of a trained vanilla BNN. Allowing zero weights in A requires some modifications in the original encoding of the last layer that we discuss in Appendix B.1. Consider how ternary quantization helps to reduce the encoding in our example.

Example 5.1. Consider Example 3.1. We recall that the first row of A is [1, -1, 1] and the corresponding reified cardinality constraint is

x 1 0 ⇔ (x 0 0 -x 0 1 + x 0 2 ≥ 1/2), (see Example 3.2)

. Now we assume that after using ternary quantization the first row of A is [1, 0, 0]. Then the last reified cardinality constraint is simplified to x 1 0 ⇔ (x 0 0 ≥ 1), which is mush simpler constraint.

Interestingly, our approach resembles the lottery ticket hypothesis training framework introduced by Frankle & Carbin (2019) . The main conceptual difference is that pruning and training are tightly coupled in our case as ternary quantization of weights is performed during every forward path.

In Frankle & Carbin (2019) , training and pruning are two separate phases4 .

The second issue at this level is that SAT solver inference is weak due to equivalence relations in Equation 4. Here we take the stabilization approach proposed in (Xiao et al., 2019) and adjust it to work for BNNs. The idea is to perform bounds propagation of the input bounds through the network to estimate lower and upper bounds of each neuron in the network. We denote z j an input of the sign function of a neuron x i+1 j , x i+1 j = sign(z j ) (Equation 1 defines z j ). If sign(ub(z j )) = sign(lb(z j )) then the sign operator is stable in the sense that we know the value of x i+1 j , e.g. if both bounds are positive then x i+1 j = 1, otherwise -1. For stable neurons, we can remove the equivalence relation and fix x i+1 j simplifying the encoding (see Appendix C for more details on bounds propagation and an example).

Estimates of lower and upper bounds must be binarized as the bounds computation goes across BLOCKs. To mimic the computation flow on the bounds computation path, we apply hard tanh before the sign operator: lb(x i+1 j ) = sign(HARDTANH(lb(z j ))) and ub(x i+1 j ) = sign(HARDTANH(ub(z j ))). We must also take into account that parameters of the BN layer are learned in a different way. Namely, µ i j and σ i j are computed from the batch of samples, while other parameters are learned via gradient descent (Ioffe & Szegedy, 2015b ). When we compute bounds, we pass them through the BN layer, but we should exclude these fake inputs from the computation of µ i j and σ i j . Finally, to achieve the effect of stabilization during training, for each neuron, we encourage ub(z j )) and lb(z j ) to take the same sign by adding an extra term to the loss function that approximates sign(ub(z j )) sign(lb(z j )) as -tanh(1 + ub(z j )lb(z j )) (Xiao et al., 2019) .

Block level We recall that the main issue we identified is that it is not obvious how to take advantage of shared partial computations in constraints of a block. One solution could be to enforce a pattern of zero and non-zero coefficients for each matrix A. A recent and successful example of this is a butterfly matrix (Dao et al., 2019b; a) . This is a structured matrix with a predefined sparsity pattern. The original matrix is replaced with a composition of highly sparse matrices of a rigid structure that provides a very good approximation of the original matrix (Dao et al., 2019a) . This new matrix can potentially be used to create a natural decomposition of our block constraints. However, it is a matter of future research if butterfly matrices can be used alongside quantization. Another solution that we can use is a different binary quantization, e.g. -1/0 or 0/1, for each row of the matrix instead of ternary quantization. This will ensure that variables either occur in the negative/positive polarity or are absent in each constraint. Keeping the same polarity per constraint may foster shared computations. However, the distribution of zeroes is also important here to get a good level of sharing. Hence, we believe that using predefined patterns might be more promising.

Network level Recall that we found two avenues for optimizing encoding at the network level: formula decomposition and directed search. In (Narodytska et al., 2018; Cheng et al., 2018) , decomposability of BINBNN was exploited in limited forms there the authors independently proposed using CEGAR-like search to reason about property verification. (Khalil et al., 2019) took advantage of both decomposition and directed search by proceeding from the last to the first layer for a similar problem. However, while all these ideas appear to be helpful, there is no solver designed to incorporate such techniques. On the other hand, a number of verification frameworks exploit similar domain properties for bounded model checking (Bradley, 2011; Gurfinkel et al., 2015) . So, it would be interesting to see if these solvers can be adapted for property verification of ML models.

6. EXPERIMENTS:

We focus on the improvements we proposed for the neuron level of granularity. We use three datasets from (Narodytska et al., 2018; Baluta et al., 2019; Khalil et al., 2019) . For each, we experiment with two tasks. First, we check if there is an untargeted adversarial attack (Goodfellow et al., 2015) . Second, we compute an approximate number of adversarial examples for a given image. We used 4 hidden layers and one output layer. The input of the network is an image of size 28 × 28. The network has the following dimensions for all layers: [784, 500, 300, 200, 100, 10] . This gives 623K parameters, which is 3 to 10 times bigger than the networks in (Narodytska et al., 2018; Baluta et al., 2019) . We used a full-precision trained network to seed weights before binarized training (Alizadeh et al., 2019) . As the first layer inputs are reals, we used an additional BN + sign layer after the Published as a conference paper at ICLR 2020 input layer to binarize inputs (see Appendix D.1). We used the PySAT tool (Ignatiev et al., 2018) to encode logical constraints to SAT and Glucose as a SAT solver (Audemard & Simon, 2018) .

Untargeted adversarial attacks. In this task, we look for a perturbation x of the given input x where |x -x | ≤ . We used five values of epsilon, ∈ {1, 3, 5, 10, 15, 20}5 . We train three groups of networks. First, we trained vanilla BNNs. Then we trained two types of BNNs using our ideas from the neuron level.We trained BNNs with the ternary quantization method ('Sparse'). We used the value of T = 0.03 for MNISTBG and FASHION and T = 0.04 for MNIST using 60%-80% quantile depending on the dataset and the accuracy of the resulting network. Finally, we trained BNNs with stabilization of neurons ('Sparse+Stable'). We seeded initial weights of 'Sparse+Stable' network with weights of the trained 'Sparse' network as such a setup up gave better accuracy. In addition, we investigate the effect of a popular L1 regularizer on ternary quantization during the training ('Sparse+L1') and it stabilization version ('Sparse+L1+Stable').

Table 2 summarizes test accuracy results and the number of non-zero parameters per network for all trained networks and datasets. From Table 2 , we can see that we can significantly reduce the number of parameters using ternary quantization during the training ('Sparse'). Interestingly, we do not lose test accuracy compared to the vanilla BNNs in all cases. If we consider the effect of L1 regulazation then we see that the number of parameters reduces even further but the accuracy drops a bit as well: the more we reduce the number of non-zero parameters the more we lose in terms of the accuracy. Using additional stabilization can also hurt the accuracy a bit for both 'Sparse' and 'Sparse+L1' networks. However, on average, we get about 40% of signs stabilized.

Figure 1 shows the performance of a SAT solver on three datasets. Results are averaged over 100 benchmarks. The average size of the encoding for all datasets and = 5 are shown in Table 4 . Note that the size of the encoding is 50x smaller compared to millions of variables and classes reported in Narodytska et al. (2018) for MNIST and MNISTBG for a much smaller network and the same . Another interesting observation is that stabilization helps a lot to reduce the size of the encoding. If the PySAT tool takes more than 10G of memory to generate a SAT encoding then we terminate the generation process. If a solver time/memory outs on more than 70% of benchmarks we do not plot these results. Therefore, we do not have a plot for vanilla BNNs in these datasets as we either had a timeout or (mostly) memory out exceptions. Each plot shows the average time to solve the untargeted adversarial attack problem for each value of . In addition, Figure 3 shows the number of solved problems for each value within the timeout (100 sec) by the SAT solver. As can be seen from these plots, in all except one case, at least 95% of benchmarks were solved within the 100 sec timeout

The plots show that ternary quantization greatly improves performance on three datasets as we were not even able to solve any benchmarks for the vanilla case. Using the 'L1' regularizer slightly improves performance in two datasets and helps a lot on MNIST. Finally, the stabilization of signs method consistently improves performance of a SAT solver across datasets for both 'Sparse' and 'Sparse+L1' networks, e.g. we get from 3x to 6x speedup due to stabilization.

Figure 2 shows the number of successful attacks as it is an interesting measure to understand properties of a network. Each plot shows the ratio of successful adversarial attacks for each value of . Naturally, this ration plateaus at 1 as the value of perturbation grows. The results are mixed here. In some cases, using 'L1' does not significantly change the vulnerability of the network compare to 'Sparse' network, e.g. FASHION and MNISTBG, while it does help for MNIST. Interestingly, stabilization of signs can lead to increase in vulnarabilities if we compare a network with and with-out stabilization. Consider for example, MNIST with = 5. Only 13 out of 100 benchmarks were successfully attacked for 'Sparse+L1' while 43 were attacked for 'Sparse+L1+Stable'. Finally, Table 3 shows original (the top row) and perturbed (the bottom row) samples of images from MNISTBG dataset for the following values of = 3, 5, 15, 20 (from left to right). As can be seen from these sample, if = 3 then original and perturbed images are identical. For = 20 (last column), perturbations are visible.

Likelihood of adversarial examples. Next we estimate the probability of a perturbation to be an adversarial example. We reproduce a setup from (Baluta et al., 2019) where an approximate model counting, ApproxMC3, was used to perform such estimate. The main goal of this experiment is to demonstrate that our approach allows approximate model counting techniques to scale to larger networks. We focus on robustness as above, so SAT formulas check for existence of untargeted adversarial attacks. Hence, each solution corresponds to an adversarial attack. We perform model counting on binarized inputs (see Appendix D.1) with a timeout of 600 sec. We use default parameters of ApproxMC3. Table 4 summarizes results. We report the mean value of the solution count estimate divided by the total number of solutions (P(adv)) and the percentage of benchmarks solved by ApproxMC3 out of all benchmarks that we know are susceptible to adversarial perturbation (#solved). On average, we can solve 80% of benchmarks within the timeout. This contrasts with results reported in (Baluta et al., 2019) , where it took 24 hours to perform approximate model counting for a BNN with about 50K parameters and a large fraction of benchmarks were not solved. Table 4 shows that the probability of adversarial attack is small for two out of three datasets. Another observation is sparsification and stabilization do not significantly change the probability of an input to be adversarial. Table 4 : The average size of the SAT encoding in terms of the number of variables (#vars) and clauses (#cls), the probability of perturbation to be an adversarial attack(P(adv)) and the number of solved benchmarks out all of benchmarks that can be attacked for = 5.

A ILP solver performance. For completeness of the evaluation, we report results of an ILP solver on the same benchmarks for the untargeted adversarial attacks. The second experiment (to estimate the probability of a perturbation to be an adversarial example) is not currently possible for ILP formulations as we are not aware of an efficient approximate model counting solver for ILPs. We used the CPLEX solver with default configuration. Figure 4 shows results. As before Figure 4 shows the performance of a ILP solver on the untargeted adversarial example task for each value of . Results are averaged over 100 benchmarks. We observe similar patterns as for ILP solvers: sparsification and stabilization are mostly helpful for all datasets as we cannot solve most of the benchmarks if we do not apply these techniques. As can be seen from the graph, the ILP solver exhibits a bell shape in two datasets, MNIST and FASHION: if is small or large then the instance is easier to solve. values in the middle are the hardest to solve for an ILP solver. We have not observed this bell shape for SAT solvers. Overall, if we compare performance of SAT and ILP solvers, the SAT solver is more efficient and solves more benchmarks (see Figure 5 for the number of solved benchmarks in Appendix D.2). In summary, our results show that a significant speed up can be obtained if we design an architecture of BNNs and its training procedure taking into account potential bottlenecks of SAT solvers. We achieved 10-20x speed up in verification and in probabilistic queries compared to state of the art results in (Narodytska et al., 2018; Baluta et al., 2019) .

7. CONCLUSIONS:

In this work, we analyze architectural design choices of BNNs and discuss how they affect the performance of logic-based reasoners, focusing on the individual neuron and block levels. We demonstrated how to train BNNs so that the resulting network is easier to verify for logic-based engines, like SAT solver or approximate model counting solvers.

A BACKGROUND. ADDITIONAL DETAILS.

Model counting. The problem of model counting is to calculate the number satisfying assignments or models of a given SAT formula. This problem is complete for the complexity class #P (Valiant, 1979) , which contains the entire polynomial hierarchy. Despite the high complexity, a number of tools for model counting have been developed (Sang et al., 2005; Thurley, 2006; Muise et al., 2012; Lagniez & Marquis, 2017) , which were shown to work well on certain benchmarks arising in practice. However, for many applications, obtaining exact counts is not necessary and a good approximation often suffices, especially when it leads to better scalability. These requirements have led to the emergence of approximate counting approaches (Ermon et al., 2013; Chakraborty et al., 2013; Soos & Meel, 2019) which employ universal hash functions along with specialized SAT solvers (Soos et al., 2009) for balancing accuracy and scalability. The most successful approximate counters provide Probabilistically Approximately Correct (PAC)-style guarantees (Valiant, 1984) on accuracy, while scaling to formulas with thousands of variables in practice. In our experiments, we use a state-of-the-art tool called ApproxMC3 (Soos & Meel, 2019) which has been shown to scale much better than other exact and approximate counters. A key advantage of ApproxMC3 is that it supports projected model counting, i.e. counting over a subset of the variables in the given formula, which is essential for our purposes as we count over variables that represent inputs of the network.

Sequential counters encoding. We recall the definition of sequential counters encoding from (Sinz, 2005a; b) that are used to encode cardinality constraints. Consider a cardinality constraint: m i=1 l i ≥ k, where l i ∈ {0, 1} is a Boolean variable, x i , or its negation, xi , and k is a constant. Then the sequential counter encoding, can be written as the following Boolean formula using auxiliary Boolean variables r (j,k) :

EQUATION

where i ∈ {2, . . . , m}. Essentially, this encoding computes the cumulative sums k i=1 l i and the computation is performed in unary, i.e., the Boolean variable r (j,k) is true iff j i=1 l i ≥ k. In particular, r (m,k) encodes whether m i=1 l i is greater than or equal to k.

B PROPOSITION ENCODING OF BNNS. B.1 ENCODING OF THE OUTPUT LAYER AND ITS ADJUSTMENT FOR TERNARY:



QUANTIZATION:

We recall that the OUTPUT block is just a linear transformation: o = Cx d-1 + q. Example B.1. We continue Example 3.1. Suppose our single block is followed by an output block with two inputs and two outputs. We define transformation parameters as follows.

LIN : C = [1, -1; -1, -1], q = [0.5, -0.1] (7) Hence, we can write the following system of linear constraints over {-1, 1} variables.

o 0 = x 1 0 -x 1 1 + 0.5, o 1 = -x 1 0 -x 1 1 -0.1.

As before, we perform variable replacement to obtain constraints over Boolean variables only.

o 0 = 2x 1 0 -1 -(2x 1 1 -1) + 0.5, o 1 = -(2x 1 0 -1) -(2x 1 1 -1) -0.1. After rearrangements, we get o 0 = 2x 1 0 -2x 1 1 + 0.5, o 1 = -2x 1 0 -2x 1 1 + 1.9.

Usually, we are not interested in absolute values of o. Rather, we need to know the index of the maximum element of o, which corresponds to the top prediction in the classification task. Hence, we need to encode the ordering relation over variables o. To do so, we use an additional set of Boolean variables d ij , i = 1, . . . , p, j = i + 1, . . . , p. Applying variable replacements and rearranging terms, we get:

d ij ⇔ p t=1 c it 2x d t - p t=1 c it + q i ≥ p t=1 c jt 2x d t - p t=1 c jt + q j (8) we denote R ij = ( p t=1 c it -q i - p t=1

c jt + q j ), so we get (9)

EQUATION

Finally, we note that c it , c jt ∈ {-1, 1} are applied to the same variable x d t . Hence, depending on the sign of these coefficients, the difference |c it -c jt | is either 0 or 2. So we can rewrite: ⇔(2x 1 0 -2x 1 1 + 2x 1 0 + 2x 1 1 ≥ 1.9 -0.5) ⇔(x 1 0 -x 1 1 + x 1 0 + x 1 1 ≥ 1.4/2) ⇔x 1 0 ≥ 1.4/4 )

EQUATION

The final observation is that if C is a sparse matrix then we lose the property that the difference c| it -c jt | is either 0 or 2 as c it , c jt ∈ {-1, 0, 1}. Hence, the last division by two (Equation 13) is not possible. However, we take advantage of the fact that coefficients are small, |c it -c jt | ≤ 2. So, we can duplicate variables to model non-unary coefficients, for example. Example B.3. Suppose, we get the following matrix C due to ternary quantization:

LIN : C = [1, 0; -1, -1], q = [0.5, -0.1] (14)

Then we have the following ordering constraint:

d 0,1 ⇔o 0 ≥ o 1 ⇔(2x 1 0 -1 + 0.5 ≥ -2x 1 0 + 1 -2x 1 1 + 1 -0.1) ⇔(x 1 0 + x 1 0 + x 1 1 ≥ 2.4/2) ⇔2x 1 0 + x 1 1 ≥ 2.4/2 )

We can introduce an extra variable x 1 0 and replace 2x 1 0 + x 1 1 with x 1 0 + x 1 0 + x 1 1 and an equality constraint x 1 0 = x 1 0 .

C BOUNDS PROPAGATION:

Let us split BLOCK computation into two parts that correspond to LIN and BN layers: y j = ni t=1 a i j,t x i t + b i j and z j = α i j σ i j (y j -µ i j ) + γ i j to demonstrate computations of lower and upper bounds on y j (z j are computed similarly). We get that lb(y j ) = Example C.1. Consider our example for BLOCK and the second neuron computation:

x 1 1 = sign(0.1(-x 0 0 -x 0 1 + x 0 2 + 1) + 0.2 ≥ 0). Suppose we derive that for all possible samples, ub(x 0 0 ) = ub(x 0 1 ) = -1. In this case, we have lb(x 0 0 ) = lb(x 0 1 ) = -1 as all activations are in {-1, 1}. We can compute bounds on the all variables y and z. lb(y 1 ) = lb(-x 0 0 -x 0 1 + x 0 2 ) = 1 + 1 -1 = 1, ub(y 1 ) = ub(-x 0 0 -x 0 1 + x 0 2 ) = 1 + 1 + 1 = 3, lb(z 1 ) = 0.1 × lb(y 1 + 1) + 0.2 = 0.4, ub(z 1 ) = 0.1 × ub(y 1 + 1) + 0.2 = 0.6. So, we get that sign(lb(z 1 )) = sign(ub(z 1 )), so we know that x 1 1 = 1 and we can use this information to reduce the encodings.

D EXPERIMENTAL EVALUATION.:



D.1 BINARIZATION OF INPUTS.:

As we discussed in Section 6, we introduce an additional block before the first internal layer that mimics binarization of inputs. This layer constraints BN and sign operators only (hard tanh is used during the training). Consider how this layer works.

Published as a conference paper at ICLR 2020 If min t ≥ 0 then we know that x 0 t = 1. If max j < 0 then we know that x 0 t = 0. In other cases, x 0 t ∈ {0, 1}. Consider the reverse transformation. If x 0 j = 0 is a solution of a problem produced by the SAT solver then we can map back to x t = min t . Similarly, if x 0 t = 1 then x t = max t . As each transformation in Equation 17-Equation 18 is performed on a single input, we can build a valid input from a solution over Boolean variables. 

x 0 t ⇔

:

In the training phase, there is an additional hard tanh layer after batch normalization, but it is redundant in the inference phase.

The error bounds depend on the parameters of the model counting algorithm.

For example, dealing with high-precision floating-point arithmetic requires specialized tools.

We thank an anonymous reviewer for pointing out the connection to(Frankle & Carbin, 2019)

We are able to use large values of compared toNarodytska et al. (2018), where ≤ 5.

Figures and Tables:

Figure 1: Performance of a SAT solver on the untargeted adversarial attack task.

Figure 2: The percentage of successful adversarial attacks.

Figure 3: The number of solved benchmarks.

Figure 4: Performance of an ILP solver on the untargeted adversarial attack task.

Coming back to our Example B.1, as we have two variables, we introduce one Boolean variable d 01 to signal the top prediction: d 0,1 ⇔o 0 ≥ o 1

EXPERIMENTAL EVALUATION USING ILP SOLVERS. MISSING FIGURE.

Figure5shows the number of solved problems for each value within the timeout.

Figure 5: The number of solved benchmarks.

Structure of internal and output blocks, which, stacked together, form a BNN.

Table content: <table/>

The test accuracy (%) and the number of non-zero parameters (#prms) of the trained networks.

Table content: <table/>

The original (the top row) and successfully perturbed (the bottom row) images for MNISTBG for = 3, 5, 15, 20.

Table content: <table><tr><td>BNNs</td><td/><td>MNIST</td><td/><td/><td>FASHION</td><td/><td/><td>MNISTBG</td><td/></tr><tr><td/><td>#vars/#cls</td><td>P(adv)</td><td>#solved</td><td>#vars/#cls</td><td>P(adv)</td><td>#solved</td><td>#vars/#cls</td><td>P(adv)</td><td>#solved</td></tr><tr><td>Sparse</td><td>63K/224K</td><td>0.04</td><td>71%</td><td>34K/116K</td><td>0.04</td><td>87%</td><td>24K/80K</td><td>0.17</td><td>95%</td></tr><tr><td>Sparse+Stable</td><td>42K/146K</td><td>0.05</td><td>70%</td><td>19K/58K</td><td>0.06</td><td>89%</td><td>12K/36K</td><td>0.16</td><td>93%</td></tr><tr><td>Sparse+L1</td><td>8K/20K</td><td>0.07</td><td>100%</td><td>34K/115K</td><td>0.07</td><td>87%</td><td>17K/53K</td><td>0.17</td><td>98%</td></tr><tr><td>Sparse+Stable+L1</td><td>11K/33K</td><td>0.05</td><td>95%</td><td>12K/33K</td><td>0.06</td><td>98%</td><td>10K/28K</td><td>0.16</td><td>94%</td></tr></table>

sign α t σ t (x t + b t -µ t ) + γ t , x t ∈ [x t -, x t + ].First, we consider two extreme values of the expression that is an input of sign w.r.t. . Suppose α t ≥ 0 (α t < 0 is analogous).

Table content: <table><tr><td>max t =</td><td>α t σ t</td><td colspan="2">(x t + + b t -µ t ) + γ t ,</td><td>(17)</td></tr><tr><td>min t =</td><td colspan="2">α t σ t</td><td>(x t -+ b t -µ t ) + γ t</td><td>(18)</td></tr></table>

Peer review (iclr2020):
This paper approaches the problem of using logic-based reasoning tools to analyze binary neural networks. They propose general changes to BNN architectures at the neuron level so as to adapt them for more efficient usage by such tools. Their main contributions are a new design choice utilizing ternary, rather than binary, quantization, and additional variables to propagate through the network containing upper and lower bounds for each layer output. They also suggest further promising directions to adapt BNNs at the block and network level. Their experiments show that the proposed changes do not significantly alter test accuracy from a standard trained baseline model while dramatically reducing the number of model parameters. Consequently, they are able to demonstrate that SAT solvers can find adversarial examples much more quickly with their new architectural alterations. Overall, this paper presents a novel contribution with an idea for more efficient BNNs and experimentally verifies the success of their proposed changes. However, there is a concern regarding the experimental setup. A large part of the motivation for this task arises from the field of verification regarding adversarial examples. While binarized neural networks are not my area of expertise, I am familiar with a number of verification papers on full neural networks. As such, I find the datasets used, accuracies reported, and model size a bit peculiar. In ‘Scaling provable adversarial defenses’ (Wong ’18), the authors were able to verify models with a couple million parameters on both MNIST and CIFAR. In my understanding, the primary advantage of BNNs is their efficiency in having only binary weights. If this is the case, I see no reason why the experimental setup would have such a small model. Additionally, it is generally well-known that MNIST and its variants are not a particularly hard datasets to classify. Many different architectures can easily achieve 98 or 99 percent test accuracy. A quick literature search found ‘A review of Binarized Neural Networks’ (Simons ’19), which reports better numbers on MNIST and decent results on CIFAR-10 (and in fact, even ImageNet). Their experimental evidence crucially relies on the conclusion that their techniques allow for faster SAT solver computation *while* maintaining comparable test accuracy. As such, it is my opinion that to be a strong paper, they must show this property holds for larger networks and more significant datasets. Additionally, a comment for the authors to consider: I would suggest switching some of the supplementary materials with the main content. The exposition on BNNs is quite dense and detailed. Some of these details could be moved to the appendix and replaced with more experimental graphs and images. This would provide some breaks in the text so as to provide ease of reading.