In Search for a SAT-friendly Binarized Neural Network Architecture
Authors: Nina Narodytska
Hongce Zhang
Aarti Gupta
Toby Walsh
Venue:  (2020)
Keywords: verification
Boolean satisfiability
Binarized Neural Networks

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.


Published as a conference paper at ICLR 2020
IN SEARCH FOR A SAT-FRIENDLY BINARIZED NEU- RAL NETWORK ARCHITECTURE
Nina Narodytska
Hongee Zhang
VMware Research
Princeton University
Palo Alto, USA
Princeton, USA hongcez@princetenn
nha amarodyt.kke @vwware.com com
Aarti Gupta
Toby Walsh
Princeton University
UNSW Sydney, Data61
Princeton, USA aa partig@princetenn
Sydney, Australia tw@cse. www.sse.uss.eee.. wnw.. au
ABSTRACT
Analyzing the behavior of neural networks is one of the most pressing challenges 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 an- swer 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 logie-based rea- soners. We propose changes to the BNN architecture and the training procedure to get a simpler network for SAT solvers without sacrificing accuracy on the pri- mary task. Our experimental results demonstrate that approach scales larger deep neural networks compared to existing work for existential and probabilistic queries, leading significant speed ups on all tested datasets.
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 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 2017 2019 Tjeng et al. 2019) and incomplete methods (Weng et al.) 2018 Zhang et 2018 Singh et al. 2018). As the training and
"This work mostly done during internship at VMware Research.

---

Published as a conference paper at ICLR 2020
verification tasks are separated, 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(BNN) (Hubara et al. 2016). A BNN is an extreme case of quantized neural networks where parameters are primarily binary. These net- works have a number of important features that are useful in resource constrained environments, like embedded devices or mobile phones (McDanel et 2017 Kung 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 representation enables us to apply powerful Boolean reasoning tools to the analysis of BNNs. For example, we can perform 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 perfor- mance of SAT solvers. To identify influential parts of the design, we scrutinize BNNs 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 net- work level. Our main contribution here is within the network level.
Second, we exploit our findings train SAT-friendly BNNs. We propose a modified train- ing procedure that makes the resulting network easier for logic-based verification tools, like SAT solvers, 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. 20188] Khalil et al. 2019| Baluta et al.) 2019). We get more than 10x-20x improve- ments on tested benchmarks for both verification and quantitative queries, e.g., finding the probability that perturbation yields adversarial example.
2 BACKGROUND
Boolean satisfiability (SAT). We assume notation and definitions standard in Boolean Satisfiabil- ity (SAT), i.e. the decision problem for propositional logic (Biere et al., 2009). SAT formulas are defined over a set of Boolean variables (xi...., Xy, A literal 4 is a variable x; ('positive' polarity) or its complement x; ('negative' polarity). Cardinality constraints over Boolean variable are con- straints of the form EL 4 2 k, where 1 E [x;, x.) In this work we employ reified cardinality constraints: x' 21=0 4 2 k. We use the full sequential counters encoding (Sinz (005b) to model this constraint in SAT (see Appendix A details of the encoding). However, other encod- ings 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.c., BLOCK* {-1, 1] + (-1,1)".+1,
1,.... d - 1, where - 1 the number of hidden layers. The last block, denoted OUTPUT, has a slightly different structure: OUTPUT 131 - I where is the number of outputs of the network. Each BLOCK takes an input vector æ and applies three transformations: a linear transformation (LIN), batch normalization (BN) and binarization (BIN)) Table 1 shows transformations of internal and output blocks in detail.
In the training phase, there is an additional hard tanh layer after batch normalization, but is redundant in the inference phase.
2

---

Published as a conference paper at ICLR 2020
Structure of internal block, BLOCK; (-1, 13tt + (-1,1) on input x' E (-1, 13
LIN
A'z' + b' where A' (-1, p x and y. E 12411
aj y + 33. where a', n "',''''' o' 1
BN
BIN
si) where x'tl E (-1,1)
Structure of the output block, OUTPUT (-1,1)" R" input x" E (-1, Cx' + 9, where (-1, and q E R Table 1: Structure of internal and output blocks, which, stacked together, form BNN.
LIN
3 LOGIC-BASED ANALYSIS OF BNNS
An important property BNNs is that they allow exact encoding into SAT: for each BNN there ex- ists 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 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 verification and certifi- cation of NNs. Since logic-based analysis of BNNs exploits their logical representation, we start by revisiting how to obtain such representation before discussing logic-based BNN analysis tools.
3.1 SAT ENCODING OF BNNS
We consider how to generate logical encoding of a BNN (Narodytska et al. 2018). Consider single block BLOCK', which applies three transformations to the inpu vector. The first step is linear (affine) transformation (LIN) of the input vector. The linear transformation can based on fully connected layer convolutional layer. The linear transformation is followed by scaling which is performed with a batch normalization operation (BN) (Toffe Szegedy 2015ap. Finally, binarization is performed using the sign function obtain binary output vector (BIN). We will use the following rumning example to demonstrate the encoding.
Example 3.1. Consider a block with three inputs and two outputs. We define transformation pa- rameters as follows:
LIN
= [1,
[0.0]
BN :
[0.1, [1,- [1,1,, (0.1),7=0011,.2222 E
We encode these transformations as a system of logical constraints. We introduce vector of binary variables z' E (-1, 1) to encode inputs and -i+1 E 1] to encode outputs of BLOCK', Since transformations are applied sequentially, we can encode the block as their composition:
Zj
2 bj p$) + 73
j
10++1
+ 3
sign (zj),
Mi+1s
(2)
where af, and bj are parameters of LIN, a²,, o3. m1 and 7f are parameters of BN. To obtain a SAT encoding, we need to eliminate binary variables as SAT formula is defined over Boolean variables. We introduce Boolean variables x, E (0, = 1...., ., ny and relate them to the corresponding binary variables v;: r 1. We can now rewrite the last expression as
2x, 1, l 1,..., We get that if x, = 0 then -1, otherwise
x5=1
i+1
sign
2x
Σ [=l
1z) + +26 ) , =1 =1... as. + bj
3

---

Published as a conference paper at ICLR 2020
We denote Cj = (- EE 11= jj + +0 2))) as these are just constants. We get
E (jxxi= 2
20j
C
21
if
a
>
++1
1=
of x2
-3/03
20j
C3
if a
<
0
....14111
(3)
Ji 2 0,
if af 0.
Example 3.2. Consider how the encoding works on Example 3.1 We introduce three binary vari-
ables to encode inputs z.., i = 0. 1, and two binary variables to encode outputs 2g and x Inputs and outputs are connected as follows:
zy sign (ig + 1) 1)
sj (0.gn(000(1appppp x + + 0).
Next we perform variable replacement as explained above using the relation Iy that af and al2 are both positive so we get:
2x. 1. Note
0.1 0) 4 (x) X1 + (0.1(-(2x) 1) - (2x - 2x - 1 + 0.2 2 0) + (-x) x + x2 ス 4 4/2).
X + (0.1(2x) 1 (2x - 2x -
x2 2 1/2);
The final step is encode reified cardinality constraints using Boolean variables instead of binary (integer) variables in [quation 3 We recall the following tautology for a Boolean variable x, + x, where x; negation of xx. As all coefficients djs {-1,1), Equation 3 contains linear constraints with unary coefficients (see the last transformation in Example (.2). We denote
N Kaje < 0, I....,,,41.. the number of negative coefficients in the jth row and assume
a + 0.
x + (11
+ 1, 2 hg), if aa and h ( 1 1
x
( if af >0 if af < 0.
-,/22-
where 11
x
if
We recall that constraint of type Equation 4 is reified candinality constraint that can be trans- lated into Boolean formulae (Narodytska et al.] 2018). We present details of such translation in Appendix A We refer to SAT encoding of BLOCK BINBLOCK' (x', x Similarly, we can encode the OUTPUT block that we show in details below as our method needs to make modifications the original encoding (see Appendix [B.T). We refer to encoding of OUTPUT as BINOUTPUT. We can now represent the entire network as a Boolean formula: BINBNN(x,, o) = A BINBL.CCK' (xt, xf+1) A BINOUTPUT(x4" o), where BINBLOCK' (x', x(+1) encodes the ith block BLOCK' with input xf and output x'+1, i [0,d - 1], BINOUTPUT(xe", ,)) is 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 prop- erty?'. The second type deals with probabilistic queries, e.g. 'what is an approximate probability that a valid input will violate given property?'. Finally, the most powerful reasoner answers large set of queries, like generating explanations. finding exact probabilities of property violations, etc.
Property checkers. Property checking of BNNs using SAT-based approach was proposed in (Narodytska et al.) 2018 Cheng et 2018). Given a precondition prec on the inputs and property prop on the outputs we check if the following statement is valid:
prec(x) A BINBNN o) = prop(o).
To decide if there exists counterexample this property, look for model of: prec(x) A BINBNN(x., o) -prop(o).
An example of property checking is to check for the existence of adversarial perturbations. this case, prec defines e-ball of valid perturbations and prop states that the classification should not change under small perturbations. An optimization version of this problem was considered (Khalil et al. 2019) using II.P rather than SAT solvers reason about B NNNs.
4

---

Published as a conference paper at ICLR 2020
Quantitative reasoners. In many practical applications, it is not sufficient to check for the istence 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 framework to answer such probabilistic queries using approximate model counting tools. The main technical challenge is to perform efficient approximate solution counting of SAT formula that contains BINBNN sub- formula. Consider the property verification formula above. By approximately counting solutions, we obtain an estimate of the probability of valid input leading to a property violation with a con- trollable and bounded error Baluta et al. (2019) identified three applications of this framework in the security domain: robustmess, trojan attacks, and fairness. |Narodytska et al. (2019) investigated how 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 BINBNN into a tractable structure, 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) 9 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, c.g., 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 networks On the other hand, SAT is a hard combinatorial problem. Hence, developing efficient decision procedures require exploiting the special structure of NNNs.
ANALYSIS OF BNN'S S FROM THE SAT STANDPOINT
In this section we analyze the properties of the formula BINBNN from the perspective of 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-formula, of BINBNN. (Narodytska al. 2018 Cheng et al. 2018 Khalil 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 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 Enquaaiion 4 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[Equttion 4 To make things worse, depending on the encoding, the number of auxiliary variables to encode Equa- tion 4 depends on n, and lty, e.g., the number of auxiliary variables introduced O(ngh; 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 equiva- lence 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 <> (XB + x + x2 2). More- over, suppose x/ and xy have not been fixed yet and x8 = 1. Note that any setting of variables valid assignment in this constraint. Hence, no inference is possible. In contrast, assume we only had cardinality constraints, i.e. X + x + x2 2 2, then we can infer that this point. As the vast majority of constraints in the encoding contain the
xQ. x2 can be extended
x 0 and xy equivalence relation, this hinders the inference algorithm's 's ability to find implied variables, making the solver dive deep before a conflict occurs.
"The error bounds depend on the parameters of the model counting algorithm. For example, dealing with high-precision floating-poin point arithmetic requires specialized tools.
5

---

Published as a conference paper at ICLR 2020
Block level Next 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 opportunity to identify shared computations and exploit them to get more succinct encodings. For example, if we have two constraints (xß - x + x3 2 2) and (-x8 xf + x3 2 -2) then we encode the partial sum -xf x 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 chain of blocks. As each block is encoded individually, BINBNN is a conjunction of BINBLOCK formulas that are loosely connected via vari- ables x', i == 1.....d d 1. As discussed above, x' variables are small fraction of the total number of variables. Two factors affect solver performance. First, the blick-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 of inconsistencies. Therefore, conflict-drieen learning, which is the core of all SAT solvers, should perform directed search, starting from either the last the first blocks of the formula moving to- ward the first (last) blocks as search progresses rather than jumping unguided between layers. Such guidance might help to discover conflicts faster.
3.2 are the main source
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 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 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 ofEuutioon that need 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 binary quantization to learn sparse matrices for linear transformations. We recall that BNN is trained using two matrices: a prel-ppecision matrix W that is updated during the gradient decent and a binarized matrix A', connected as follows A = sign (W A' is used on the forward path and during inference. The modification we make is simple two- sided ternary quantization of A during training:
sign(w)))) if 1 a'e 0
(5)
otherwise,
where T is parameter. In principle, T can be a learnable parameter (Zhu al. 2017). However, in (Darabi et al.) 2018). it was observed that weights of W are naturally grouped around points -1, and 0 during training. Therefore, we use fixed threshold T, obtained from the distribution of weights of 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.I 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, and the corre- sponding reified cardinality constraint is xb 4> (xf - x + x2 > 1/2), (see Example 3.2). Now we assume that after using ternary quantization the first row of A is [1, 0, 0J. Then the last reified cardinality constraint is simplified to x] <> (x) 2 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 temarr quantization of weights is performed during every forward path. In Frankle& & Carbin 2019), training and pruning are two separate phases [
"We thank an anonymous reviewer for pointing out the connection Frankle & Carbin 2019

---

Published as a conference paper at ICLR 2020
The second issue at this level is that SAT solver inference is weak due 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 imput bounds through the network to estimate lower and upper bounds of each neuron in the network. We denote 2j an input of the sign si)n(z;) [Equation 1 defines 2ÿ). If (1ggmub(z))) = sign(1b((;) then the sign operator is stable in the sense that we know the value of r²) e.g. if both bounds are positive then afjt 1. otherwise -1. For stable neurons, we can remove the equivalence relation and fix 2 20/1 simplifying the encoding (see Appendix C for more details on bounds propagation and an example).
function of a neuron <²tt , ]
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 sign(HARDTANN((((E)))) and ub(aftt)
hard tanh before the sign operator: (b(x)=1) sign HARDDANH((b((;))) learned in a different way. Namely, Ju; and of are computed from the batch of samples, while other parameters are learned via gradient descent (loffe & Szegedy, 2013b). When we compute bounds, we pass them through the BN layer, but we should exclude these fake inputs from the computation of 13 and oj. Finally, to achieve the effect of stabilization during training, for each neuron, we encourage ub(z;)) and (b(zz) to take the same sign by adding an extra term the loss function that approximates (ogn(ubzz)) sign (Ib(z))) as - tanh(1 + (bzz)) (Xiao et al. 2019).
We must also take into account that parameters of the BN layer are
Block level We recall that the main issue we identified is that it is not obvious how to take ad- vantage of shared partial computations in constraints of block. One solution could be enforce a pattern of zero and non-zero coefficients for each matrix A. A recent and successful example of this is butterfly matrix (Dao al. 2019b a). This is 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 very good approximation of the original matrix (Dao al.) 9a). This new matrix can potentially be used to create a natural decomposition of our block constraints. However, it matter of future research if butterfly matrices can be used alongside quantization. Another solution that we can use is different binary quantization, c.g. -1/0 0/1, 1, for each row of the matrix instead of ternary quantization. This will ensure that variables either occur in the neg- ative/positive polarity 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 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 al., 2018 Cheng et al.) 2018), de- composability 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 advan- tage of both decomposition and directed search by proceeding from the last to the first layer for similar problem. However, while all these ideas appear to be helpful, there is no solver designed to incorporate such techniques. On the other hand, number of verification frameworks exploit similar domain properties for bounded model checking (Bradley) 2011] Gurfinkel et al., (015).. So, it would be interesting to see if these solvers can be adapted for property verification of ML models.
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). 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 given image. We used 4 hidden layers and one output layer. The input of the network is an image of size 28 x 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 al.) 2019). We used a full- precision trained network to seed weights before binarized training (Alizadeh al. 2019. As the first layer inputs reals, we used an additional BN + sign layer after the
7

---

Published as a conference paper at ICLR 2020
BNNS
MNIST
FASHION
MNISTBG
1
Upens
4priss
oprms
Vanilla
96.5
623K
82.1
623K
74.3
623K
Sparse
96.4
32K
81.1
37K
78.2
11K
Spurse-Stable
32K
83.2
37K
78.3
K
Sparso-L
96.0
20A
83.7
35K
78.4
36
BpurseLL-SSual
95.2
20A
82.9
37K
80.0
34K
Table 2: The test accuracy (%) and the number of non-zero parameters (#prms) of the trained networks.
input layer binarize inputs (see Appendix D.I
We used the PySAT tool (Ignatiev et al. 2018) to encode logical constraints to SAT and Glucose as SAT solver (Audemard & Simon 2018
Untargeted adversarial attacks. In this task, we look for a perturbation x' of the given input where |r - x'| S 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. trained BNNs with the ternary quantization method ("Sparse"), We used the value of = 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 ("Spaase+Sttable.. ). We seeded initial weights of "Sparse+Stablee" 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+Ll") and it stabilization version (" ("Sparse+LI+Stablee)
Table 2 summarizes test accuracy results and the number of non-zero parameters per network for all trained networks and datasets. From Table [ 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 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 terms of the accuracy. Using additional stabilization can also hurt the accuracy bit for both 'Sparse' and 'Sparse+L1' networks. However, on average, we get about 40% of signs stabilized.
Figure 1 shows the performance of SAT solver three datasets. Results 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. (0018) for MNIST and MNISTBG for a much smaller network and the same Another interesting observation is that stabilization helps lot 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 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 solve the untargeted adversarial attack problem for each value of In addition, Figure 3) shows the number of solved problems for each c 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 we were not even able to solve any benchmarks for the vanilla case. Using the 'L.1' regularizer slightly improves performance in two datasets and helps lot on MNIST. Finally, the stabilization of signs method consistently improves performance of SAT solver across datasets for both 'Sparse' and 'Sparse+L1' networks, e.g. 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 prop- erties of network. Each plot shows the ratio of successful adversarial attacks for each value of Naturally, this ration plateaus at as the value of perturbation e grows. The results are mixed here. In some cases, using 'L.1' does 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-
We are able use large values of compared Narodytska et al. 2018), where S 5.
8

---

Published as a conference paper at ICLR 2020
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+LI+Stable.
Mnist
Fashion
MnlisteG
Spare
Scarre
Sparse Staple
Spana+
Scarnne
Sparone13 +13
Spanne13
Spannell
Sparowel --tatle
Sparmel S--taetee
Everage Erme
Sparnel Staclle
Average
Figure I: Performance of a SAT solver on the untargeted adversarial attack task.
Mnist
Fashion
MniistGG
Ratio succ attacess
Rate of suce attacks
Sparse
Stste
Batto
Sparse Stable
Sparse Stable
Figure 2: The percentage of successful adversarial attacks.
Mnist
Fashion
MnistBG
Sparse
Number of solved Instances
of salved insrance
Spanes
Spamme11
Spame-11- Stablle
Sparse
Sparte
SparseSSthbl Stable Sp
Sparse+ Statle
Sparse+L]
Sparse L11 StaMc
Sponse L1 1toble
Figure 3: The number of solved benchmarks.
Finally, Table 3 shows original (the top row) and perturbed (the bottom row) samples of images from MNISTBG dataset for the following values of e = 3, 5, 15, 20 (from left to right). As can be seen from these sample, if e = 3 then original and perturbed images are identical. For e 20 (last column), perturbations are visible.
Likelihood of adversarial examples. Next 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, 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 [.I] with a timeout of 600 sec. We use default pa- rameters 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 perturba- tion (#solved). On average, we can solve 80% 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 BNN with about 50K parameters and large fraction of benchmarks were not solved. Table 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.

---

Published as a conference paper at ICLR 2020
9
9
Table 3: The original (the top row) and successfully perturbed (the bottom row) images for MNISTBG for
é 3, 5, 15, 20.
BNNs
MINIST Pladv]
FASHION
MNISTBG
Pvars/Clls
#solved
PvarsWelss
Pladv)
Psolivd
Evars/icls
Plady)
Psolved
Sparse Starle
63K/224K
0.04
71%
34K/116K
0.04
87%
24K/80K
0.17
95%
42K/146K
0.05
70%
19K/S8K
0.06
80%
12K/36K
0.16
93%
SparseeL.1
SK/20K
0.07
100%
34K/T15K
0.07
87%
17K/53K
0.
98%
Sparse+Stable-L1
1IK/33K
0.05
95%
12K/33K
0.06
98%
10K/28K
0.16
91%
The average size of the SAT encoding in terms of the number of variables (#vars) and clauses (#tls), the probability of perturbation to be an adversarial attack(P(adv)) and the number of solved benchmarks out all of benchmarks that be attacked for 5.
Table 4:
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
not aware of an efficient approximate model counting solver for ILPs. We used the CPLEX solver with default configuratio. Figure 4 shows results. As before FFiuure 4 shows the performance of ILP solver on the untargeted adversarial example task for each value of e. 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 e small or large then the instance is easier to solve. values in the middle are the hardest to solve for an IIP solver. We have not observed this bell shape for SAT solvers. Overall, if we compare performance of SAT and IIP solvers, the SAT solver is more efficient and solves more benchmarks (see Figure 5 for the number summary, our results show that significant speed
of solved benchmarks in Appendix D.2)
Mnist
Fashion
MnistBG
Sparse
Spars
Sperae
Sparse Stibll
Sparse Stapie
Sparse Staple
Sperweell
Spanse133
Spenaee
Sparoeel1+Saat
Spammel3 Stabbele
Sparaee 1.4 Startle
Averaga
Figure 4: Performance of an II.P solver the untargeted adversarial attack task.
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 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 per- formance of logic-basse based reasoners, focusing the individual neuron and block levels. We demon- strated how to train BNNs so that the resulting network is easier to verify for bagicdbased engines, like SAT solver approximate model counting solvers.
10

---

Published as a conference paper at ICLR 2020
REFERENCES
Milad Alizadeh, Javier Fermandez-Marqués, Nicholas D. Lane, and Yarin Gal. An empirical study of binary neural networks' optimisation. In 7th International Conference on Learning Repre- sentations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL
Gilles Audemard and I Laurent Simon. On the glucose SAT solver. International Journal Artificial Intelligence Tools, 27(1):1-23 2018. doi: 10.1 182//5221821311 8400008... URL. httpss////ooooooo
10.1142/5021821100 8400018
Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S. Meel, and Prateek Saxena. Quantitative verification of neural networks and its security applications. ACM Conference on Computer and Communications Security (CCS 2019), abs/1906. 10395, 2019. URL http://arkiv.or//ass//1966
10395
Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (eds.). Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2009, ISBN 978-1-58603-929-5.
Aaron R. Bradley. Sat-based model checking without unrolling. In Ranjit Jhala and David A. Schmidt (eds.), Verification, Model Checking, and Abstract Interpretation 12th Interna- tional Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings, vol- ume 6538 of Lecture Notes in Computer Science, pp. 70-87. Springer, 2011. doi: 10.1007/ 978-3-642- (424-18275-4)77777 URL http:://doi..og11010000011 3-222 18275-4-7
Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. A scalable approximate model counter. In Christian Schulte (ed.), Principles and Practice of Constraint Programming- 19th Interna- tional Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, volume 8124 of Lecture Notes in Computer Science, pp. 200-216. Springer, 2013.
Chih-Hong Cheng, Georg Nührenberg, Chung- Chang-Hao Huang, and Harald Ruess. Verification of bi- narized neural networks via inter-neuron factoring (short paper). In Ruzica Piskac and Philipp Rümmer (eds.), Verified Software. Theories, Tools, and Experiments 10th International Confer- ence, VSTTE 2018, Oxford. UK, July 18-19, 2018, Revised Selected Papers, volume 1294 of Lec- ture Notes in Computer Science, pp. 279 290. Springer. 2018. doi: 0000007977783000-055555559 16
.16. URL httthhh::://ooooorg TO.
Arthur Choi, Weijia Shi, Andy Shih, and Adnan Darwiche. Compiling neural networks into tractable boolean circuits. 2019.
Tri Dao, Albert Gu, Matthew Eichhorn, Megan Leszczynski, Nimit Sohoni, Amit Blonder, Atri Rudra, and Chris Ré. Butterflies are all you need: A universal building block for structured linear maps. 2019a. URL htw.://www...sstttodd.....od
9/06/ 33bbutterf//l
Tri Dao, Albert Gu, Matthew Eichhorn, Atri Rudra, and Christopher Ré. Learning fast algorithms for linear transforms using butterfly factorizations. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning. ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97, pp. 1517-1527, 2019b.
Sajad Darabi, Mouloud Belbahri, Matthieu Courbariaux, and Vahid Partovi Nia. BNN+: improved binary network training. CoRR,
2018. URL http://arniw.rr/aab//8811.. 1800
Krishnamurthy Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovic, Brendan O'Donoghue, Jonathan Uesato, and Pushmeet Kohli. Training verified learners with learned ver- ifiers. CoRR, 1bs/1805.10265, 2018. URL http://t://arrxvv.orr//// 10////000..1000 10265
Stefano Ermon, Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Taming the curse of dimen- sionality: Discrete integration by hashing and optimization. In Proceedings of the 30th Inter- national Conference on Machine Learning, ICML 2013, Atlanta, GA, USA, 16-21 June 2013, volume 28, pp. 334-342. JMLR.org, 2013.
EU Data Protection Regulation. Regulation (EU) 2016/679 of the European Parliament and of the Council, 2016.
11

---

Published as a conference paper at ICLR 2020
Jonathan Frankle and Michael Carbin. The lottery ticket hypothesis: Finding sparse, trainable neu- ral networks. In 7th Interaational Conference on Learning Representations, ICLR 2019, New Orleans, LA. USA, May 6-9, 2019. OpenReview.net, 2019. URL http://oppnurvvie.ee///mummm
id=rJl-b3ReF7
lan Goodfellow, Yoshua Bengio, and Aaron Courville. Deep Learning. The MIT Press, 2016. ISBN 0262035618, 9780262035613.
lan J Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In ICLR' 15, 2015.
Bryce Goodman and Seth R. Flaxman. European Union regulations on algorithmic pecision-mmaing and a "right to explanation". Al Magazine, 38(3):00-57, 2017.
Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. The seahorn verifica- tion framework. In Daniel Kroening and Corina S. Pasareanu (eds.), Computer Aided Verification 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceed- ings, Part I, volume 9206 of Lecture Notes in Computer Science, pp. 343-361. Springer, 2015. doi: 10.1007/978 1---399-2199---- ,0. URL URL https://doo.or//10.0000//// 3-11788--3311--166-- 2-191----16----22
Itay Hubara, Matthieu Courbariaux, Daniel Soudry, Ran El- and Yoshua Bengio. Binarized Neural Networks. In Advances in Neural Information Processing Systems 29, pp. 4107-4115.
Curran Associates, Inc., 2016. URL http://nnee..iii..ccooooo//t/iaa pdf
Alexey Ignatiev, Antonio Morgado, and Joao Barques-Silva. PySAT: A Python toolkit for prototyp- ing with SAT oracles. In SAT, pp. https://6o.orr//000000/779733333 --0779978--3319-44444-
2018. doi: 10. 10.1007799883331199444444 26. URL
Sergey Ioffe and Christian Szegedy. Batch Normalization: Accelerating Deep Network Train- ing by Reducing Internal Covariate Shift. In ICML' pp. 448-456, 2015a. doi: 10.1007/
513398-014-0173-7..
Sergey loffe and Christian Szegedy. Batch Normalization: Accelerating Deep Network Train- ing by Reducing Internal Covariate Shift. Arxiv, 2015b. ISSN 0717-6163. doi: 10.1007/
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In CAV, pp. 97-117, 2017.
Guy Katz, Derek A. Huang, Duligur lbeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Alcksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. The Marabou framework for verification and analysis of deep neural net- works. In CAV, pp. 443 452, 2019.
Elias B. Khalil, Amrita Gupta, and Bistra Dilkina. Combinatorial attacks on binarized neural networks. In 7th International Conference Learning Representations, ICLR 20/9, New Or- leans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL httppss//oopeeevvvveeeee/oomaaaa SIITEh09FQ
Jaeha Kung, David Zhang, Gooitzen Van der Wal, Sek Chai, and Saibal Mukhopadhyay. Efficient Object Detection Using Embedded Binarized Neural Networks. Journal of Signal Processing Systems, pp. 1-14, 2017.
Jean-Marie Lagniez and Pierre Marquis, An improved decision-dnnf compiler. In IJCAI, pp. 667- 673, 2017.
Bradley McDanel, Surat Teerapitayannon and H. T. Kung. Embedded binarized neural networks. In EWSN, pp. 168-173. Junction Publishing, Canada ACM, 2017.
Matthew Mirman, Timon Gehr, and Martin T. Vechev. Differentiable abstract interpretation for provably robust neural networks. In Jennifer G. Dy and Andreas Krause (eds.), Proceedings of the 35th International Conference on Machine Learning. ICML 2018, Stockholmsmässann. Stockholm, Sweden, July 10-15, 2018, volume 80 of Proceedings of Machine Learning Research, pp. 3575- 88.html
3583. PMLR, 2018. URL
12

---

Published as a conference paper at ICLR 2020
Christian Muise, Sheila A. Mcllraith, J. Christopher Beck, and Eric Hsu. DSHARP: Fast d-DNNF Compilation with sharpSAT. In Canadian Conference on Artificial Intelligenee 2012.
Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. Verifying properties of binarized deep neural networks. In Sheila A. Mcllraith and Kilian Q. Wein- berger (eds.), Proceedings of the Thirty-Second AAA/ Conference on Artificial Intelligence, 18), 2-7, 2018, pp. 6615 6624.6624, AAAI Press, 2018. URL https:/wwww.aii..oooos////// AAAAAAAAATT//aaaae/viii/i//////
Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev, and João Marques-Sin Silla.. Assessing heuristic machine learning explanations with model counting. In Mikolás Janota and Inês Lynce (eds.), Theory and Applications of Satisfiability Testing SAT 2019 22nd Interna- fional Conference, SAT 2019, volume 11628 of Lecture Notes Computer Science, pp. 267-278. Springer, 2019.
NIPS IML Symposium. NIPS interpretable ML symposium, December 2017.
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Semidefinite relaxations for certifying ro- bustness to adversarial examples. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurlPS 2018, 3-8 Decem- ber 2018, Montréal, Canada., pp. 10900-10910, 2018.
Sang, P. Beame, and H. Kautz. Performing bayesian inference by weighted model counting. In Prof. of AAAI, pp. 475-481, 2005.
Andy Shih, Adnan Darwiche, and Arthur Choi. Verifying binarized neural networks by angluin- style learning. Mikolás Janota and Inés Lynce (eds.), Theory and Applications of Satisfiability Testing SAT 2019 22nd International Conference. SAT 2019, volume 1 11628 of Lecture Notes in Computer Science, pp. 354-370. Springer, 2019.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. Fast and effective robustness certification. In NeurlPS, pp. 00825-10833 2018. URL http://papers..mpp (-17778-fftttaaa
(cc/paper/2278- fast- ands--nnd-ffee hetpeeccceeerbuuutttteeetttiiiii
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. Boosting robustness certification of neural networks. In 7th International Conference on Learning Representa- tions, ICLR 2019, New Orleans, LA. USA, May 6-9, 2019. OpenReview.net, 2019. URL
Carsten Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. In CP, volume 3709 of Lecture Notes in Computer Science, pp. 827-831. Springer, 2005a.
Carsten Sinz. Towards an optimal CNF encoding of boolean cardinality constraints. Technical report, University of Tubingen, 2005b.
Mate Soos and Kuldeep S. Meel. Bird: Engineering an efficient enf-xor sat solver and its applica- tions to approximate model counting. In Proceedings of AAAI Conference on Artificial Intelli- gence (AAAI), 2019.
Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers cryptographic prob- lems. In Theory and Applications of Satisfiability Testing SAT 2009, 12th International Confer- ence, SAT 2009, Swansea, UK, June 30 July 3, 2009. Proceedings, pp.
2009.
Mare Thurley. sharpsat counting models with advanced component caching and implicit BCP. In Armin Biere and Carla P. Gomes (eds.), Theory and Applications of Satisfiability Testing SAT 2006, 9th International Conference, Seatlle WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pp. 424 429. Springer, 2006. doi: 10.1007/ 11814948) 38. URL https:://ooooorg/////// 10. 1007/11814948 38
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In ICLR, 2019.
Leslic G. Valiant. The complexity of enumeration and reliability problems. SIAM J. Comput., 8(3); 410-421, 1979. doi: 10. 10.1137/020803. URL https//dhbh.ogg/1.1117700222222
13

---

Published as a conference paper at ICLR 2020
Leslie G Valiant. A theory of the learnable. In Proceedings of the sixteenth annual ACM symposium on Theory of computing, pp. 436-445, ACM, 1984.
Tsui-We Weng, Huan Zhang. Hongge Chen, Zhao Song. Cho-Jui Hsich, Luca Daniel, Duane S. Boning, and Inderjit S. Dhillon. Towards fast computation of certified robustness for relu net- works. In ICML, pp. 5273-5282, 2018.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In Jennifer G. Dy and Andreas Krause (eds.), Proceedings of the 35th Inter- national Conference on Machine Learning, ICML 2018, Stockholmsmmässan, Stockholm, Sweden, July 10-15, 2018, volume 80 of Proceedings of Machine Learning Research, pp. 5283-5292. 18.html
PMLR, 2018. URL http:///pprooeesiingg
Kai Y. Xiao, Vincent Tjeng, Nur Muhammad (Mahi) Shafiullah, and Aleksander Madry. Train- ing for faster adversarial robustness verification via inducing relu stability. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019.
OpenReview.net, 2019, URL http:://pprrreeeeeee////mmmmmm/a
Huan Zhang, Tsui-Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In NewrlPS, pp. 4954, 2018.
Chenzhuo Zhu, Song Han, Huizi Mao, and William J. Dally. Trained ternary quantization. In 5th International Conference on Learning Reprexentations, ICLR 2017, Toulon, France, April 24- 26, 2017, Conference Track Proceedings. OpenReview.net, 2017. URL hhtps://openneiiewwneel forum -id=SI-pAuXil
A BACKGROUND. ADDITIONAL DETAILS.
Model counting. The problem of model counting is to calculate the number satisfying assign- ments or models of given SAT formula. This problem is complete for the complexity class #P [Valiant 1979), which contains the entire polynomial hierarchy. Despite the high complexity,
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 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 ofate-of-the-aa 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 the variables in the given formula, count over variables that represent inputs of the network.
which is essential for our purposes
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 straint: Σ k. where 4; E {0, 1} is a Boolean variable, x,, or its negation, x, and & is a constant. Then the sequential counter encoding, can be written the following Boolean formula using auxiliary Boolean variables T(J,))
(4 + T(I)) (Fas)) jE (,........ .....,,))) k}) A
T(11) + 4 V (1(1111) A ((2) 44Ar(-11-1) Vr(e-15) (2....,k).
(6)
where i E (,,..., m). Essentially, this encoding computes the cumulative sums Σh= 4 and the computation is performed in unary, i.e., the Boolean variable r(j,)) is true iff Ei= 4 2 k. In particular, A(m,A) encodes whether Σ 4 is greater than or equal to k.
14

---

Published as a conference paper at ICLR 2020
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 + +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,, [0.5, -0.1]
Hence, we can write the following system of linear constraints over (-1,1} variables.
Og 20 x + 0.5,
01 = = 20 - + - 0.1.
As before, we perform variable replacement to obtain constraints over Boolean variables only.
On 2x 1 (2x) 1) 0.5, 01 (2x) 1) (2x) 1) 0.1. After rearrangements we get
0g 2x 2x + 0.5,
01 2x - 2x + 1.9.
Usually, we are not interested in absolute values of o. Rather, we need to know the index of the maximum element o, which corresponds the top prediction in the classification task. Hence, need to encode the ordering relation over variables o. To do so, we use an additional set of Boolean variables diy: ........J....................... = I,...,P. Applying variable replacements and rearranging terms, we get:
P Eye
91 91)
dis
2x2
Cat + qi
2x
Σ [=1
(8)
1=1
[=1
t=1
we denote Rij =
9i
Cjt + qj), so we get
(9)
t=1
1=1
Rij
cux
Σ cxX2 2
(10)
2
1=1
Rig 2
Σ 1=1
(Gu cx(xx 2
(11)
Finally, we note that Cit, Cjt E 1) are applied to the same variable o4 Hence, depending on the sign of these coefficients, the difference |ct Cjrl is either 2. So can rewrite:
Rij
dij +
2 x
X 2 x
(12)
2
t=1,ch- =2
1=1, C-r=2
Rij
Σ
Σ
(13)
4
i=1,ca-cf55
Example B.2. Coming back to our Example B.l as we have two variables, we introduce one
Boolean variable doi to signal the top prediction:
do,1 +00 2
(2x) - 2x + 2x + 2x 2 1.9 - 0.5)
* (x]] - + +x +x| 1.4/2)
bxo 2 [1.4/4]) 7
15

---

Published as a conference paper at ICLR 2020
The final observation is that if C is sparse matrix then lose the property that the difference C/ Cjtl either or as Ca, Cjt E f-1,00 0, 1}. Hence, the last division by two (Equation 13) is not possible. However, take advantage of the fact that coefficients are small, |Cu - Cjt 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], [0.5, 001]
(14)
Then we have the following ordering constraint:
do,1 +> 2 01
(2x) - 1+ -2x +1 2x| + -
(x) + x + x 2 2.4/2)
2X + [2.4/21)
We can introduce an extra variable xo6' and replace 2xh + x with x + xb + x} and an equality constraint x]= = x)
C BOUNDS PROPAGATION
Let us split BLOCK computation into two parts that correspond to LIN and BN layers:
E af,aat a bj and 2j -े- (U, - 73 to demonstrate computations of lower and upper bounds on yy (z) are computed similarly). We get that
1b(y))
()(()())) +
Σ
ubx(t) + bb
(15)
t=,,a
t <0
ub(y;)
Σ
ubbx))
+
(b)()(()))) bbj
(16)
t=l,a),
1=,,a,,,0
Example C.I. Consider our example for BLOCK and the second neuron computation:
a ====
Suppose we derive that for all possible samples, ub(x.) 1b(z8) = Ib(xf) = -1 as all activations are in {1, We can compute bounds on the all variables y and
ub(zq) -1 In this case, we have
1b(y1) 1b(- o x 22) 1=1,
ub(y1) ub(-2. x Jf +x]) =1+1+1=3
16(21) = 0.1 x (b(1) +1) = 0.4, ub(21) = 0.1 ub(y) +1)+ 0.6.
So, we get that sign(lb(z)) (l)(((((()))))))( sign(ub(z1)), know that x 1 and we can use this informa- tion to reduce the encodings.
D EXPERIMENTAL EVALUATION.
D. BINARIZATION OF INPUTS.
As we discussed in Section 6 introduce additional block before the first internal layer that mimics binarization of inputs. This layer constraints BN and sign operators only (hard tanh used during the training). Consider how this layer works.
16

---

Published as a conference paper at ICLR 2020
a ( bq Me) + 788
x sign
r E (ot e, 24 6).
First, we consider two extreme values of the expression that is an input of sign w.r.t at 2 (ar < analogous).
Suppose
maz;
(xt + b, 14) n
(17)
dt
min, at (x) c c by - m2) + 7
(18)
min, 2 0 then we know that x² 1. If max, < 0 then we know that x; 0. In other cases, xf E {0, 1). Consider the reverse transformation. If x 0 is solution of a problem produced by the SAT solver then we can map back to 2; = man, Similarly, if xf then 2t = mazz As each transformation in Equation 17 [Equatinn 18lis performed on a single input, we can build valid input from a solution over Boolean variables.
D.2 EXPERIMENTAL EVALUATION USING ILP SOLVERS. MISSING FIGURE.
Figure shows the number of solved problems for each value within the timeout.
Mnist
Fashion
MnistBG
Nurroer of solved Instances
Figure 5: The number of solved benchmarks.
17


Reviews:
[{"review_id": "Syxn9SsnYr", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "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.\nOverall, 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. \nA 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. \nAdditionally, 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.\n", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I carefully checked the derivations and theory."}, "extra_text": {}}, {"review_id": "H1ep15J9OH", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "In this paper, a new design of Binary Neural Network (BNN) is proposed. The purpose of the new design is to make the network easier to analyze using the existing Boolean satisfiability (SAT) solvers. An easier analysis is preferable since the SAT solver can be used to infer existing fragility in the network, e.g., adversarial attacks. Empirically, the proposed design of BNN is shown to outperform traditional BNNs by a large margin in terms of detecting adversarial attacks. \n\nOverall, this paper seems to provide a solid contribution to the design of robust BNNs. I like how the authors tried to address various aspects of the networks for easy analysis of SAT solver, i.e., neuron, block, and network-levels even though they only focused on changing the architecture in neuron-level perspective. The experimental results seem to show benefits without any compromise in performance. \n\n", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I did not assess the derivations or theory.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I made a quick assessment of this paper."}, "extra_text": {}}, {"review_id": "BkgsCUn0qS", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper deals with the scalability of Binarized Neural Networks (BNNs) and their representation in Boolean logic. This encoding enables SAT solvers to reason about the underlying variables and query existential or counting clauses. The main contribution of this paper is the analysis of the architectural design choices of the BNN and modifications of the training procedure in order to improve the efficiency of SAT solvers. The modifications are simple but effective and the authors show consistent improvement on different benchmarks without the SAT solver timing out.\n\nOverall, I am leaning towards accepting this paper due to the improved empirical results compared to the baselines the authors build on. However, it does not seem that there is much novelty in the BNN architecture per se, but rather in the training procedure. The modifications are simple but effective. The paper seems to be well-written and easy to follow also from a reader not familiar with the literature in this area.\n\nI would be interested to have an answer to the following concerns:\n\n- It was not totally clear for me what is are the changes that the paper proposes in the block level and network level and if these modifications are present in their experiments.\n- Did you evaluate your method on other image classification datasets, such as CIFAR-10/-100?\n- The thresholding used to sparsify the matrix A^i and seeding the initialization (correct me if I am wrong) when retraining the BNN seems to be really similar to the Lottery Ticket Hypothesis [1]. It would be interesting to evaluate the sensitivity of your proposed method towards the initialization.\n\n[1] Jonathan Frankle, Michael Carbin. The Lottery Ticket Hypothesis: Finding Sparse, Trainable Neural Networks. In ICLR, 2019", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper studies how the architecture and training procedure of binarized neural networks can be changed in order to make it easier for SAT solvers to verify certain properties of them.

All of the reviewers were positive about the paper, and their questions were addressed to their satisfaction, so all reviewers are in favor of accepting the paper. I therefore recommend acceptance.
Decision: Accept (Poster)