Truth Table Deep Convolutional Neural Network, A New SAT-Encodable Architecture - Application To Complete Robustness
Authors: Adrien Benamira
Thomas Peyrin
Bryan Hooi
Venue: ICLR 2022 Submitted (2022)
Keywords: AI Safety
SAT-encodable Neural Network
Formal Verification
Complete Verification Robustness
Interpretability
Logic Rules
XAI

Abstract: 
With the expanding role of neural networks, the need for formal verification of their behavior, interpretability and human post-processing has become critical in many applications. In 2018, it has been shown that Binary Neural Networks (BNNs) have an equivalent representation in boolean logic and can be formally analyzed using logical reasoning tools such as SAT or MaxSAT solvers. This formulation is powerful as it allows us to address a vast range of questions: existential, probabilistic, explanation generation, etc. However, to date, only BNNs can be transformed into a SAT formula and their strong binary constraints limit their natural accuracy. Moreover, the corresponding SAT conversion method intrinsically leads to formulas with a large number of variables and clauses, impeding interpretability as well as formal verification scalability. In this work, we introduce Truth Table Deep Convolutional Neural Networks (TT-DCNNs), a new family of SAT-encodable models featuring real-valued weights and real intermediate values as well as a highly interpretable conversion method. The TT-DCNN architecture enables for the first time all the logical classification rules to be extracted from a performant neural network which can be then easily interpreted by anyone familiar with the domain. Therefore, this allows integrating human knowledge in post-processing as well as enumerating all possible inputs/outputs prior to deployment in production. We believe our new architecture paves the way between eXplainability AI (XAI) and formal verification. First, we experimentally show that TT-DCNNs offer a better tradeoff between natural accuracy and formal verification than BNNs. Then, in the robustness verification setting, we demonstrate that TT-DCNNs outperform the verifiable accuracy of BNNs with a comparable computation time. Finally, we also drastically decrease the number of clauses and variables, enabling the usage of general SAT solvers and exact model counting solvers. Our developed real-valued network has general applications and we believe that its demonstrated robustness constitutes a suitable response to the rising demand for functional formal verification. 

Under review conference paper at ICLR 2022
TRUTH TABLE DEEP CONVOLUTIONAL NEURAL NETWORK, A NEW SAT-ENCODABLE ARCHITECTURE- - APPLICATION To COMPLETE ROBUSTNESS
Anonymous authors Paper under double-blind review
ABSTRACT
With the expanding role of neural networks, the need for formal verification of their behav- ior, interpretability and human post-processing has become critical in many applications. In 2018, it has been shown that Binary Neural Networks (BNNs) have an equivalent repre- sentation in boolean logic and can be formally analyzed using logical reasoning tools such as SAT or MaxSAT solvers. This formulation powerful as it allows us to address vast range of questions: existential, probabilistic, explanation generation, etc. However, to date, only BNNs can be transformed into a SAT formula and their strong binary constraints limit their natural accuracy. Moreover, the corresponding SAT conversion method intrinsically leads to formulas with a large number of variables and clauses, impeding interpretability well formal verification scalability. In this work, introduce Truth Table Deep Convolutional Neural Networks (TT-DCNNs), a new family of SAT-encodable models featuring real-valued weights and real intermediate values as well highly interpretable conversion method. The TT-DCNN architecture enables for the first time all the logical classification rules be extracted from performant neural network which can be then easily interpreted by anyone familiar with the domain. Therefore, this allows integrating human knowledge in post-processing as well as enumerating all possible inputs/outputs prior to deployment in production. We believe our new architecture paves the way between eXplainability AI (XAI) and formal verification. First, we experimentally show that TT- DCNNs offer better tradeoff between natural accuracy and formal verification than BNNs. Then, in the robustness verification setting, we demonstrate that TT-DCNNS outperform the verifiable accuracy of BNNs with comparable computation time. Finally, we also drastically decrease the number of clauses and variables, enabling the usage of general SAT solvers and exact model counting solvers. Our developed real-valued network has general applications and we believe that its demonstrated robustness constitutes a suitable response to the rising demand for functional formal verification.
1 INTRODUCTION
Deep Neural Network (DNN) systems offer exceptional performance in a variety of difficult domains (Goodfellow et al. 2016) and today these results far outstrip our ability to secure and analyze those DNNs. As DNNs are becoming widely integrated a variety of applications, several concerns have emerged: lack of robustness emphasized by lack of explainability. difficulty of integrating human knowledge in post- processing and impossibility to formally verify their behavior due to their large complexity. Under these circumstances and especially when these systems deployed in applications where safety and security are issues, the formal verification of DNN systems and the field of eXplainable AI (XAI) are under intense research efforts. For example, Tesla has recently filed patent the DNNs portability on platform

---

Under review as conference paper at ICLR 2022
incorporating a component dedicated formal verification (Driscoll 2020). Also, the European Union's s
general data protection regulation includes provision on the explainability of AIs (Regulation 2016).
DNNs formal verification methods are mainly based either on Satisfiability Modulo Theory (SMT) Katz
et al. 2017) or Mixed-Integer Programming (MIP) (Xiao et al. (0118) which are not yet scalable to vallev
DNNs. Some recent publications (Jia Rinard (aroodNa et al. (2019b); Narodytska et al. (2018)
approach the problem of complete verification from the well-known boolean S. SATisiabillity (SAT) (Biere
@ point of view where Binary Neural Networks (BNNs, Hubbar et al. (2016) are first converted
into SAT formulas and then formally verified using SAT or MaxSAT solvers. This pipeline is computationally efficient (Jia & Rinard| 2020), enables security verifications (Baluta et al., 2019) and more generally can answer vast range of question such how many adversarial attacks exist for given DNN, image and noise level (Narodytska et al.] (2019)). Besides, this approach is faster than SMT or MIP robustness verification method (Jia& & Rinard 2020). However, to date, only BNNs can be transformed into SAT formula and their strong binary constraints limit their natural accuracy. Moreover, the corresponding SAT conversion method intrinsically leads to formulas with a large number of variables and clauses, impeding interpretabilitty as well as formal verification scalability. Finally, only few studies (Ignatiev et al. (2019a) Ignatiev et al. (2019)) investigated the relationship between formal DNNs' verification and XAI.
Our contributions. this work, we offer three main contributions. (1) First, we define a new family of real-valued Deep Convolutional Neural Networks (DCNN) that can be encoded into SAT formulas: Truth Table Deep Convolutional Neural Network (TT-DCNN). Our TT-DCNN leverages its model formulation in the form of truth table allow weights and certain intermediate values to be real. To the best of our knowledge, this is the first method to encode real-valued DCNN into SAT. For the first time, we can extract all the logic classification rules from subfamily of DCNNs which allows bridge between XAI and formal verification, while achieving sufficient natural accuracy for practical use. Indeed, the nature of the SAT conversion between TT-DCNN and BNN is intrinsically different: our method relies upon giving one SAT expression per 2D-CNN filter instead of one SAT expression per neuron. This global interpretability method is in sharp contrast with the previous limited BNNs and local DNNs explainability. two main valuable conversion properties over BNNs. (2-a: Post-tuning) The first one allows us to integrate human knowledge in the post-procce post-processing: we can now interpret the model inference with simple concepts, which enables to manually modify the 2D-CNN filter activation towards a desired goal. For example, we decided to focus on reducing overfitting and, to this end, we characterize TT-DCNN logic rules resulting from overfitting and propose filtering approach, which increases the verifiable accuracy without decreasing the natural accuracy (cf. Appendix I.II) (2-b: Tractability) The second property is the possibility to compute all possible model inputs/outputs prior to deployment in production. In adversarial setting, we can assess whether the input noise will propagate to the output. We can therefore disregard filters with no impact on the output. This leads to a lower number of clauses and variables in the SAT formulas compared to BNNs which allows using generic SAT solvers and exact model counting solvers. (3) We apply our model to complete robustness verification (cf. Appendix A TT-DCNNs offer good tradeoff between the state-of-the-an of BNN/SAT method (Jia & Rinard 2020) and of real-valued DNN/MILP complete robustness verification methods (Xiao et al. (0118); TTeng et al. (017)). This is expected as our network is both real-weighted and SATTconvertible. Our TT-DCNN model improves the verifiable accuracy by more than 2.5% for high noise MNIST and by 0.5% for the high noise of CIFARIO when compared to BNN/SAT method while decreasing the verification time by factor of 9 for MNIST and 150 for CIFAR 10 high noise when compared to DNN/MILP methods. Finally, our SAT formulas are 5 and 9 times more compact term of number of clauses for high noise MNIST and CIFARIO respectively compared to the BNN/SAT method.
(2) TT-DCNNs offer
Outline. Section 2 introduces the notations and the related work. Section 3 presents new TT-DENN model and its two main properties. Section I details the complete robustness verification set-up and reports the evaluation results. Finally, we conclude this work in Section 5
2

---

Under review conference paper at ICLR 2022
2 BACKGROUND & RELATED WORK
Boolean SATisfiability (SAT). The boolean SATisfiability problem (SAT) (Biere et al. 2009 is the problem of deciding whether there exists a variable assignment to satisfy a given boolean expression Φ. We can consider boolean expression in a Conjunctive Normal Form (CNF) or in Disjunctive Normal Form (DNF). They are both defined over a set of boolean variables (I1,
In). (",, ... its complement h. A CNF is conjunction of set of clauses: & (ci A-- A Cm), where each clause oj is a disjunction of some literals Cj = 111 Vie- A DNF is disjunction of set of clauses: O = (cr V..-Vem). where each clause Cj is conjunction of some literals Cj 112 A 1yr. A pseudo-boolean constraint is a
A literal 1 is defined as a variable I; or
N constraint of the form: Σ aplp b, where ap E Z, E Z and E (S, =, which can be mapped to a SAT
formula (Roussel & Manguinho 2009). However, the output SAT formula contains a tremendous number of clauses and literals compared to the number of variables in the booulln constraint making it very hard to understand (cf. example in Appendix A..).. A boolcan function has the form {0, 1)" - {0, 1] and its corresponding truth table gives outputs for all possible inputs combinations.
Two-dimensional Convolutional Neural Networks (2D-CNNs). We consider the 2D-CNN as function y which, for a given filter f. takes n = kCc imputs at position (i. with & the kernel size and c the number of input channels. The outputs can be written 5 /مم (x (t.5) .... =. Note that in the binary case, a truth table between inputs and outputs for 2n entries can be easily set up (if n is not too large). If we now consider a multi-layers network with s convolution layers a similar truth table can be constructed, except now the kernel size h needs to be replaced by a patch function P(s) (also referred to as the size of receptive field in the literature). We have P(1)= = k and P(s + 1) = P(s) if and only if the kernel size of the layer is 1. We denote by P(s,ú,)) i,j)). the receptive field after the 5hhh layer at position (i, We denote the vector obtained after the flatten operation and before the final classifier layer as the vector of features V. If there are a total of L layers in the DNN, each element of V is a non-linear function over a patch (P(L), P(L)) on the input.
SAT encoding of neural networks. The sole published method converting DNN into SAT formula is limited to BNNs (Narodytska et al. (2018); et al. (2018) and involves recomposing a block formed of 2D-CNN layer, batch normalization layer and step function into an inequality in order apply the pseudo-booke boolean constraint (Roussel & Manquinho 2009). This approach has been further refined using a different training method and a specific SAT solver resulting in a significantly reduced verification resolution time (Jia & Rinard 2020). Although the proposed inequality rewriting is elegant, the corresponding SAT formula contains a tremendous number of clauses and literals compared the pseudo-booles boolean constraint (cf. example Appendix (.2)). This prevents both the interpretability and the tractability of those SAT/BNNs formulas. Hence, our goal is find real-valued DCNN with good performance and coincidentally convertible to SAT with fully interpretive inference.
the number of variables in
Interpretability by global rule extraction. Machine learning interpretability analysis fall into four main categories: either local (input dependant) or global methods, either exact or non-exact methods. The most famous techniques for local non-exact interpretability are LIME and the ANCHOR explainers (Ribeiro et al.) (2016): Ribeiro al. (2188). Pl-explanations (Shih et al. 2018) and SHAP (Lundberg & Lee 2017 are also popular techniques for local exact method and global non-exact method respectively. The only scalable method for global exact interpretability was proposed in (Granmo et al.) 2019). Our work aims to extend the studies of the latter strategy with the use of truth tables in order obtain the equivalent conjectures. Using truth tables in machine learning has been documented for hardware optimisation (Soga & Nakahara (2020), Wang al. (2019)) and recently in an attempt for global non-exact interpretation of BNNs (Burkhardt et al. 2021). Our work is pioneer in the use of truth table to create a new architecture enabling the extraction of all the global exact logic rules as well as the increase of model robustness for formal verification.
3

---

Under review conference paper at ICLR 2022
3 TRUTH TABLE DEEP CONVOLUTION NEURAL NETWORK (TT-DCNN)
In an attempt to address the currently identified drawbacks of the low interpretability and the high encoding complexity of the SAT formulas of the BNN's transformation process, we designed a new DNN architecture. Our TT-DCNN model is developed first as a DCNN with real-valued weights and some intermediate real values encodable into SAT. Secondly, TT-DCNN is interpretable: each feature can be understood as an indicator function. In fact, the feature associated to the filter f is equal to 1 if there exists a mask M in the set of masks Sy that matches the input patch, 0 otherwise (we will define later what are a mask, a set of masks and the matching operator). We emphasize that our formulation is new paradigm: there is no longer any need for the DNNs in production. Since the knowledge of the TT-DCNN is reduced to the set Sy for all filters, we longer need the model after the training. To the best of our knowledge, this is the first time that the exact knowledge of a real-valued DCNN is formally extracted. Finally, we will show that this formulation gives the user two major degrees of freedom: post-tuning and tractability.
Briefly, our model considers an image with three channels and floating- point inputs, while being composed of only one block of 2D-CNN as defined in Section 3.2 In order to convert the image into binary inputs. we incorporate a preprocessing layer before this block. Finally, we include a final linear layer after the 2D-CNN block to perform classification. For clarity sake, we will present our new TT-DCNN model in a stepwise fashion with increasing complexity using illustrative examples and a companion video D We will initially analyse a 2D-CNN layer with a single filter (Section 3.T). Next, we will define a block of our TT-DCNN architecture (Section 3.2). Finally, Sections 3.3 and 3.4 present the whole architecture of the TT-DCNN and its main properties, respectively.
3.1 SAT ENCODING OF A ONE-LAYER 2D-CNN
For this first building block, we consider as input a binary image with one channel and as a model a trained DCNN with only one layer. We first start to encode one filter.
The main idea is fix the number of possible outputs of the 2D-CNN by fixing the number of its possible inputs, which will allow to test all possible combinations. Following the notations introduced in (G4)
One filter.
Section we have output Dbinary.f- for the filter f:
(t.)) Viinary. Bin(y) (1.5)) = Bin( ( (1-5) ;: 2n (1-5))
with Bin being the Heaviside step function, defined as Bin(x) = + sgn(a) xy E {0. 1). we can 2
establish the truth table of the 2D-CNN's filter f by trying all the possible inpuis, for total of 2" operations. In this paper, we will limit ourselves to n < 9. Hence, in 2 = 512 operations, we can trivially generate our truth table. Then, we can convert the truth table into simplified SAT formula and by doing so we can rewrite Equation as:
(b.d) Vbinary.J SAT (z)
DNF (4:)
(8.5) (i:)) SAT (I(
(111
with SATP DNF (resp. SAT being the formal expression of the filter in the DNF form (resp. CNF form).
It is noteworthy that unlike previous works, approach is not limited to binary weights but allows for arbitrary weights within the 2D-CNN.
Example.
We consider 2D-CNN with one filter and kernel size of 2, with the weights:
W
10
Io æ and the sixteen possible entries are: Is
0 0
As = 1, we have X
3
5
F2
0 0
Link video: hutps:/yoantubebhiipyyygAlll
4

---

Under review conference paper at ICLR 2022
0
0
0
0
0
0
1
1
1
For each input, we calculate the corresponding output:
0
1
0
1
1
1/ [0,
5, 3,
2,
-1,
-0--5- 5,
13, 8, 9, 4, 12, 7/ After binarization with the Heaviside step func- [0, 0, 0,0,0,00,00 0,
20,
5.
tion, have Yhinery
1, 1,1. Therefore, after simplification, have SAT (x2 A T3) V 2o and SAT? (22 V zD) A (कz V mn).
1,
Multiple filters. For multiple filters, the above described method is simply repeated for cach individual filter, thus yielding one expression per filter.
Multiple channels. As convolutional networks generally take several channels as input (3 for RGB images more for intermediate 2D-CNNs) the number of input variables can therefore greatly increase. A 2D-CNN that takes 32 input channels with a kernel size of 2 yields an input of size 128, well above our limit set at n = To overcome this, we gather the channels by groups (Dumoulin Visin 2016). Grouped convolutions divide the input channels into g groups, then apply separate convolutions within each group; this effectively decreases the number of inputs to each individual filter by factor of g. We have in that case n k2 k2e/g. Thus, in the above example, by using 16 groups, the number of inputs to our truth tables becomes 32 x 2 8.
Limits. At this point of the model development and despite the real-valued weights, we observe sub- sub-optimal performances due the group parameters. When we add an extension layer, as detailed in the next subsection, to increase the learning capacity of the DCNN without augmenting the size of the patches seen by the DCNN (Sandler et al. 2018), we experience an improvement of about 5% of natural accuracy. Please refer to Table of Appendix A.9.2 for detailed results.
3.2 SAT ENCODING OF A TWO-LAYERS 2D- ID-CN: ONE BLOCK OF TT-DCNN
Amplification layer. In the previous subsection, we pointed out that only the 2D-CNN input size matters when establishing the 2D-CNN SAT expression. Therefore, we can add second layer as long as we do not increase the patch size. This can be simply achieved by adding layer with kernel size 1. Note that the intermediate values from the first layer do not need be binary anymore. From practical standpoint, using eight filters in layer one and one filter in layer two, drastically improves the learning capacity of the TT-DCNN and therefore the natural accuracy as well. This observation is consistent with other published studies (Sandler et al. 2018). A block is therefore composed of two 2D-CNN layers with so-called amplification parameter which corresponds to the ratio between the number of filters of the first layer and the number of filters the second layer (value often set at 8). Each layer is followed by a batch normalisation and non-linear activation function: ReLU for the first layer and Heaviside step function for the second one.
3.3 THE TT-DCNN ARCHITECTURE
Having defined one block of 2D-CNN in the previous section, we may now examine how this block integrated into the TT-DCNN. The overall architecture is presented in Appendix A.3.I
Preprocessing layer. DCNNs inputs are usually floating points. However, encoding floating points in SAT typically implies high complexity. In order to simplify the verification process and improve the network robustness, we applied three steps first-layer or vrepprcesssin procedure: (i) Quantitation of inputs (Jia & Rinard (220);; (ii) Batch normalization (Narodytska al. 2019b); and (iii) Step Function. Details are presented in Appendix A.3.2
Final layer. TT-DCNN uses a single linear layer as a classifier block. It is straightforward to grasp. even for non-experts and it can be easily encoded into SAT using pseudo- boolenn constraint as detailed in Section
5

---

Under review conference paper at ICLR 2022
long as the weights are inlegers numbers. As shown in (Jia & Rinard 2020), we also incorporate batch normalization after the last layer for improving test accuracy. Please refer to Appendix A.3.3 for more details.
3.4 INTERPRETATION OF OUR TT-DCNN MODEL AND TWO IMPORTANT PROPERTIES
Interpretation. To illustrate the ease of interpretability of our conversion method, we now offer an in- terpretation of the SAT formula of the filter with weight matrix W1 defined in the example of Section 3.1
SAT = (Ig A z V zo. First of all, we can observe that the expression is now independent of the value of I1. Then, because the formula is DNF, we observe that there are two conditions to activate the feature. We
N
N
can define the set of masks S = {M,, M2} with M1 = 0 and M2 = NN
N corresponding to
the clause Z2 A Ty and xy respectively, with N denoting Null. We observe that if one of the two masks "matches" " the patch of the image, the feature corresponding to the patch position (i.j) will be activated. By "matching", an operation denoted as =, we consider that the Null position does not matter (i.e. it be either O or a 1) and that only the 0 and 1 positions should exactly match the 0 and positions of the transformed binary input in order to activate the feature. formal definition of the operator = is given in Appendix A.4 The features for filter are therefore indicator functions in the case of our model.
More generally, from the SAT? expression we can establish Sy, the set of masks for filter f. Then, the value V at position (i, for filter f is:
v(f,i,)) = (
3 Sy such that P(L,i,)) M
otherwise
In our example with f 1, the feature i,,, would be activated if P(L, i, = M1 or P(L, i,j) M2. As V is the feature vector before the last classification layer, the result for each class becomes a weighted sum of these indicator functions. For a particular class, these features add up in a weighted way. This means that these sets either participate in favor of the class (positive weight) or against (negative weight) or are independent (weight equals zero). The knowledge of the TT-DCNN therefore resides in Sy. The existence and the analysis of Sj creates strong link between XAI and formal verification. To the best of our knowledge, this the first time that all these masks are formulated and extracted for real-valued DCNNs. The fact that all the masks can be exhaustively given leads to two main properties of TT-DCNN: post-tuning and tractability.
Two important properties: post-tuning and tractability. After the training, we can modify the set of learned masks S for a specific purpose. We will see in the next section how we can build a heuristic characterize overfitting masks, how we can remove them and therefore increase the overall robustness of our model by hand. Another particularity of this architecture is that we can calculate all the possible inputs/outputs of the 2D-CNN block. The Section describes the application of the latter feature to drastically decrease the SAT complexity and therefore enabling the use of a general SAT-solver and an exact model counting solver.
4
3.5 EXPERIMENTS
Results. Our aim to provide a fully interpretable SAT-convertiblee model with high natural accuracy. Table Taoble/ccomprress the performance of a given real-valued DCNN with its corresponding TT-DCNN and BNN (ef. results and architectures in Appendix A....T. ). As expected, this TT-DCNN gives better natural accuracy than BNN (+1.37% for MNIST, +0.57% for CIFARIO) but inferior than the original DCNN (-0. 14.14% for MNIST. -1..0%% for CIFAR10). By increasing the truth table dimension n to 27, the gap with the BNN performances increases: +1.49% for MNIST, +4.05% for CIFAR10. Those results show that our network achieves sufficient accuracy for practical use. A summary comparison between BNN, DCNN and TT-DCNN is given in Table 7
6

---

Under review conference paper at ICLR 2022
Limits and further works. Our results look promising for further scaling up, by adding block layer or/and increasing the truth table dimension (for n 2 10). We could also attempt using a probability function instead of an indicator function in order to increase interpretability. We could also propose more interpretable sets Sy. For instance, before using the MNIST dataset, we could force training filters with relevant geometrical shapes (arc of circle, circle, line etc.). Ideally, should be possible to give theoretical masks according to the dataset or to the problem.
Conclusion. We have described the TT-DCNN architecture, its encoding and main properties. We then compared our model in the exact verification field as done previously (Narodytska et al. (2018); Narodytska ct al. 2 Jia & Rinard (2020). We will show that the TT-DCNN post-tuning and tractability properties are not just theoretical. The first feature addresses the question of how to inject human feedback into a model. The second leads to SAT formulas that can solved by classic SAT solvers and exact model counting. In doing so, improve the previous state-of-the-ar of SAT complete neural network robustness verification for high and low noise levels.
4 APPLICATION TO COMPLETE ROBUSTNESS VERIFICATION
We previously described the TT-DCNN architecture, its encoding and main properties. We have established that our model gives the user the freedom to modify the set of fully explicit masks S, for all filters f and to pre-compute all possible outputs of the TT-DCNN before proceeding to production. In this section, we show how to the first property to address very general problem: adding domain knowledge into trained TT-DCNN. Namely, we wish to reduce the model overfitting part in order to increase the verifiable accuracy without modifying the natural accuracy. To do so, first propose a characterization of the masks responsible for the overfitting of the TT-DCNN followed by a very simple suppression process. Finally, we will see how the tractability property decreases the final layer encoding size. We validate our approach by testing several performance metrics of our model in comparison with other specific state-of-the the art models.
4.1 POST-TUNING: CHARACTERIZING AND FILTERING OVERFITTING MASKS
General. One may envision the set S as a bag full masks. Upon training, this set is fixed such that can be considered as the TT-DCNN knowledge. Since we have made these masks explicit (see Section 3.4) we may then modify them for a specific purpose. Drawing on the example of Section 3.4 we can consider that
1 N
the mask M₂ activation of filter 1 by integrating human knowledge in post-tuning.
N too general and decide to remove it from the set S1. By doing so, we modify the
N
Characterizing overfitting masks. A mask is considered as overfitting mask if the ratio of the number of Null values over the total number of variables the mask is below a certain threshold (cf Appendix AA.).. Indeed, the less Null values in the mask, the more constraints on the input image there are, which hinders the model to generalize properly. The extreme case of the zero ratio means that the filter is only active if the patch exactly overlaps the mask. Therefore, by changing only one bit, we deactivate that mask.
Deleting overfitting masks. First, we remove the overfitting tagged masks defined above with a given Null ratio. Then, among the remaining masks, we tag additional overfitting masks those having the minimum Null ratio in the formula. Finally, we apply a random Bernoulli process to partially delete tagged masks. This technique increases the verifiable accuracy of the TT-DCNN models trained on CIFARIO from 22.79 12.7% to 23.08%, without affecting the natural accuracy: from 31.18% to 31. 13%. The results are shown in T
7

---

Under review conference paper at ICLR 2022
4.2 TRACTABILITY: ENCODING THE ADVERSARIAL SETUP INTO SAT
General. Another feature of the TI-DCNN's architecture is that one can calculate all the possible in- puts/outputs of the 2D-CNN block before using the model in production.
Encoding pixel noise. Let consider some noise (e.g. norm-bounded by (s)) added to the input image prior binarization. After the preprocessing layer, a binarized pixel may either remain unchanged by the perturbation and so fixed as 0 or 1. or it may flip (from 0 "unknown". further denoted as U. Let us see how this unknown binarized pixel can be integrated in the example of Section 3.4 As there are entries, there are 34 81 input possibilities for the block level in
from 1 to 0) and hence we consider them
0
0
U U
adverssialppooduction setting due to noise:
More generally, UJJ
0
1
0
the maximum number of variables for the SAT entry was set to n = in this paper, there are therefore a maximum of 3 = 19683 input possibilities for our TT-DCNN, Those unknown binarized pixels are therefore the first literals of our SAT equation: they are the gateway to noise propagation.
Noise propagation at the block level. order encode noise propagation through blocks, we encode in SAT the input/output relationship (6.5) = SAT (z)1/)) ,... .nn (t.f)) for all (i.j) and f. For example, for
the filter D
(x22 Iz) V 2o, the entry ( U gives 23 U as output. The latter result depends
0
U 0
on U, whereas the input
gives 0 (whatever U is). Hence, there are two noticeable cases: either
U propagates through the block (case 1), either it does not (case 2). This example of pre-calculation of inputs/outputs illustrates the superior feature of our model allowing to know precisely how the noise will propagate. This comes in sharp contrast with the currently available BNN model where one has to consider that the noise propagates through the layers in both cases.
Encoding the attack at the final layer level. Ultimately, for the final layer, we encode - - y yj > 0 as reified cardinality constraint which denotes whether the score of class i is higher than the score of class j. Being able distinguish between known and unknown elements of the feature V of the image allows us to reduce significantly the size of the SAT formulas when compared to current state-of- state-of-the-art models. Looking at MNIST high noise for instance, our SAT equation yields on average 4K clauses and 1K variables (Table This is substantial improvement over previously published works where (Jia & Rinard 2020) has 21K clauses and 48K variables and where (Narodytska et al., 2019b) reported at least 20K clauses and 8K variables. Similar trends were observed with CIFARIO noise (Table D.
The drastic reduction in the size of SAT formulas renders our model truly amenable to formal verification. Indeed, our SAT verification step is much more tractable for general SAT solvers and exact model counting solvers.
4.3 EXPERIMENTS
Untargeted attack. Table presents gathered results for natural accuracy, verifiable accuracy for I.c- norm bounded input perturbations, verification time and the average number of clauses and variables in the SAT formulas on MNIST and CI. We compare our work with the state-of-the-art of exact verification for BNNs (Tia Rinard 2020) and for real-valued networks (Xiao et al. (2018); Tieng et al. (2017). ). We present model architectures details and experimental settings in Appendix I.3.I and A.6 Table I shows that our model after filtering masks considered to be overfitting is more robust. Moreover, our verifialle accuracy is always superior to that of the BNN and even superior that of the real value based model in the CIFARIO high noise case. We also show that, with a general SAT solver (here MiniCard (Liffiton & Maglalang 2012)). we reach resolution time competitive with BNNs and much lower than the
model. The latter
8

---

Under review conference paper at ICLR 2022
results, as proposed in (Jia & Rinard 2020) is mainly due the fact that it is hard to formally verify floating point errors. Thus, we reached our goals: we developed a new a model that is both highly interpretable and competitive with the state-of-the-an Extended comparison are given in Appendix A..
Table 1: Comparison of TT-DCNN with and without filtering with state-of-the-art regarding complete adversarial robustness verification for high noise bounded by to (results are reported as in the original articles).
Datasel and
Complete Verification Method
Accuracy
Mean time
Timeout
Mels/hhars
Noise Level
(8)
Verifiable
Natural
TI-DCNN (Ours)
94.24%
97.77%
0.2885
1K/0.4K
MNIST
SAT-based
TT-DCNN Filtering (Ours)
94.26%
97.70%
0.3724
1K/0.4K
Jin & Rinard 2020
91.68%
97.46%
0.1115
21K/48K
Flout
Xiao
2018
94.33%
98.68%
5.47
0.05%
Real-value-hased
[jong ct al
2017
95.62%
98. 18%
3.52
MNIST
TT.DCNN (Ours)
79.93%
96.79 %
0.4135
4K/IK
SAT- AxT-based
TT-DCNN Filtering (Ours)
80.36%
96.73 %
0.5722
4K/IK
Jia & Rinard
2020
77.59%
96.36%
0.1179
0
21K/48K
Cesut 0.3
Real-value-based
Xiao
2018
80.68%
97.33%
7.12
1.0%%
[jong et al.
2017
74.21%
86.60%
5,13
CIFARIO
TT-DONN (Ours)
32.72%
40.67%
0.1988
0.7K/O.3K
SAT based
TE Filtering (Ours)
33.04 %
40.62%
0.7782
0
0.7K//.2K
jia Rinard 2020
32.18%
37.75%
0.0236
33K/70K
Éloat 2/255
Real-value-hased
at 2018
45.93%
61.12%
66.08
1866%
CIFARIO
TE-DNN (Ours)
22.79%
31.18%
0. 0.1635
0
1K/0.K
SAT-based
TT-DCNN Filtering (Ours)
23.08%
31.13%
0,3887
1K/0.4K
Jia & Ranard
2020
22.55%
35.00%
0.1781
9K/13K
Ceeat 8/255
Real-value-hased
Xiao et al.
2018
20.27%
40.45%
60.67
2.47%
Likelihood of adversarial examples. The objective of this experiment is to demonstrate that our approach, thanks its tractability property, allows for the first time the use of exact model counting techniques for low and high noise likelihood estimation. As in (Narodytska et al. (2019b) work, we define the probability that a perturbation an adversarial example as the number of input perturbations that leads to an attack divided by the total number of input perturbations. For example, for CIFAR10 10 high noise, the probability of running into an attack is 16.4%, while for low noise it is 10.0%. Complementary results are given in Appendix(A. A..8
Limits and further works. As it is the case with all complete verfication methods, the main limitation of TT-DCNN appears with high noise where observed verifiable and natural accuracies diverge siginificantly and are very far from the computer vision state-of-the art. Further work is required to address this issue. One direction would be to develop a pipeline with exact model counting in order to estimate the prediction distribution of our model at a given noise level.
5 CONCLUSION
We presented a novel architecture of SAT encodable real-valued DCNN based on truth tables. This enables a global and exact interpretability as well as post-procee post-processing the model. It exhibits competitive performance given low and high noise with state-of-the-ar complete verification methods on MNIST and CIFAR1O. In a world where DNNs and DCNNs will be widely embedded, the importance of completly verifying the robustness of neural networks to input perturbations is growing. We believe that the TT-DCNN demonstrated robustness constitutes suitable response the rising demand for functional formal verification.
9

---

Under review conference paper at ICLR 2022
6 REPRODUCIBILITY
The project code reproducibility for can be found at this URL address
REFERENCES
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, and Enric Rodríguez- Rodriguez-Carbonell. Bdds for eseudo-boolese constraints-revisiee In International Conference on Theory and Applications of Satisfiability Testing, pp. 61-75. Springer, 2011.
Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep Meel, and Prateek Saxena. Quantitative verification of neural networks and its security upplications, In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp. 1249-1264, 2019.
Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS press, 2009.
Sophie Burkhardt, Jannis Brugger, Nicolas Wagner, Zahra Ahmadi, Kristian Kersting, and Stefan Kramer. Rule extraction from binary neural networks with convolutional rules for model validation. Frontiers in Artificial Intelligence, 4:90, 2021.
Chih-Hong Cheng, Georg Nührenberg, Chung -Ho Huang, and Harald Ruess. Verification of binarized neural networks via inter-neuron factoring. Working Conference on Verified Software: Theories, Tools, and Experiments, pp. 279-290. Springer, 2018.
Michael Driscoll. System and method for adapting neural network model hardware platform, July 2 2020. US Patent App. 16/728,884.
Vincent Dumoulin and Francesco Visin. A guide to convolution arithmetic for deep learning. arXiv preprint arXiv: 072255, 2016.
Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into sat. Journal on Satisfability. Boolean Modeling and Computation, 2(1-4):1-26. 2006.
Richard Evans, Matko Bošnjak, Lars Buesing, Kevin Ellis, David Pfau, Pushmeet Kohli, and Marek Sergot. Making sense of raw input. Artificial Intelligence, 299:1035211 2021.
lan Goodfellow, Yoshua Bengio, and Aaron Courville. Deep Learning. MIT Press, 2016. http: //ww/ deepleariingookk.rgg org
Olc-Christoffer Granmo, Sondre Glimsdal, Lei Jiao, Morten Goodwin, Christian W Omlin, and Geir Thore Berge. The convolutional tsetlin machine. arXiv preprint arXiv:1905.09688 2019.
Steffen Hölldobler, Norbert Manthey, and Peter Steinke. A compact encoding of pseudo- boouol- constraints into sat. In Annual Conference on Artificial Intelligence, pp. 107-118. Springer, 2012.
Itay Hubara, Matthieu Courbariaux, Daniel Soudry, Ran El- Yaniv, and Yoshua Bengio. Binarized neural networks. Proceedings of the 30th international conference on neural information processing systems, pp. 4114-4122, Citeseer, 2016
Alexey Ignatiev, Antonio Morgado, and Joao Marques- Silva. PySAT: A Python toolkit for prototyping with SAT oracles. In SAT, pp. 428-437, 2018. doi: 10. 10.100779788-3331999444444 URL https
10

---

Under review conference paper at ICLR 2022
Alexey Ignatiev, Nina Narodytska, and Joao Marques- Abduction- explanations for machine learning models. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 33, pp. 1511-1519, 2019a.
Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. On relating explanations and adversarial examples. Advances in Neural Information Processing Systems, 32:15883-15893, 2019b.
Kai Jia and Martin Rinard. Efficient exact verification of binarized neural networks. arXiv preprint arXiv:2005.03597. 2020.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97-117. Springer, 2017.
Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint
arXiv: 6980, 2014.
Mark Liffiton and Jordyn C Maglalang. A cardinality solver: More expressive constraints for free. In International Conference on Theory and Applications of Satisfiability Testing, pp. 485-486.66 Springer, 2012.
Scott M Lundberg and Su-In Lee. A unified approach to interpreting model predictions. In Proceedings of the 31st international conference on neural information processing systems, pp. 4764447777777 2017.
Norbert Manthey, Tobias Philipp, and Peter Steinke. A more compact translation of pseudo-boolean constraints into enf such that generalized are consistency is maintained. In Joint German/Austrian Conference on Artificial Intelligence (Künstliche Intelligenz), pp. 123-134. Springer, 2014.
Nina Narodytska, Shiva Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. Verifying properties of binarized deep neural networks. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 32. 2018.
Nina Narodytska, Aditya Shrotri, Kuldeep S Meel, Alexey Ignatiev, and Joao Marques-Silva. Assessing heuristic machine learning explanations with model counting. In International Conference on Theory and Applications of Satisfibillity Testing, pp. 267-278. Springer, 2019a.
Nina Narodytska, Hongce Zhang, Aarti Gupta, and Toby Walsh. In search for a sat-friendly binarized neural network architecture. In International Conference on Learning Representations, 2019b.
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, al. Pytorch: An imperative style, performefeee deep learning library. Advances neural information processing systems, 32:8026-8033 2019.
General Data Protection Regulation. Regulation eu 2016/679 of the european parliament and of the council 27 april 2016. Official Journal of the European Union. Available at: hupp:/ec. europa. eu/justice/data- protecttoonnefoommfilllerrgaaaae _en_ pdf (accessed 20 September 2017), 2016.
Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. why should i trust you?" explaining the predictions of any classifier. Proceedings of the 22nd ACM SIGKDD international conference on knowledge discovery and data mining, pp. 1135-1144, 2016.
Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. Anchors: High-precision model-agnostic explana-
tions. In Proceedings of the AAAI conference on artificial intelligence, volume 32, 2018.
Olivier Roussel and Vasco Manquinho. Pseudo-boolean and cardinality constraints. In Handbook of satisfiability, pp. 695-733. IOS Press, 2009.
11

---

Under review conference paper at ICLR 2022
Mark Sandler, Andrew Howard, Menglong Zhu, Andrey Zhmoginov, and Liang-Chich Chen. Mobilenetv2: Inverted residuals and linear bottlenecks. In Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 4510-4520, 2018.
Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S Meel. Ganak: A scalable probabilistic exact model counter. In IJCAI, volume 19, pp. 1176, 2019.
Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. arXiv preprint
2018.
Naoto Soga and Hiroki Nakahara. Design method for an lut network-bassee enn with a sparse local convolution. In 2020 International Conference Field- Field-Programmen Programmable Technology (ICFPT), pp. 294-295. IEFE, 2020.
Vincent Tjeng, Kai Xiao, and Russ Tedrake, Evaluating robustness of neural networks with mixed integer programming. arXiv preprint urXiv:1711.07356 2017.
Seinosuke Toda. Pp is as hard as the polynomial-time hierarchy. SIAM Journal Computing, 2065):865-877, 1991.
Erwei Wang, James J Davis, Peter YK Cheung, and George Constantinides. Lutnet: Rethinking inference in fpga soft logic. In 2019 IEEE 27th Annual International Symposium on ffeld-Programmable Custom Computing Machines (FCCM), pp. 26-34. IEEE, 2019.
Kai Y Xiao, Vincent Tjeng, Nur Muhammad Shafiullah, and Aleksander Madry. Training for faster adversarial robustness verification via inducing relu stability. arXiv preprint FrXiv:1809 03000, 2018.
A APPENDIX
A.1 COMPLETE VERIFICATION & ROBUSTNESS.
Property verification of SAT-convertible DNNs has been presented in (Narodytska et al. 2018 as follows: given a precondition prec on the inputs x, property prop on the outputs o and a SAT relations given by a DNN between inputs/outputs denoted as DN N (I, o), we check whether the following statement is valid: prec(x) DNN(Er, o) = prop(o). In order to seek a counterexample to this property, we look for a satisfying assignment of pree(æ) A DNN(x, o) A prop(o). An application example of property verification is check for the existence of adversarial perturbation in trained DNN. In this case, prec defines e-ball of valid perturbations and prop states that the classification should not change under small perturbations. Therefore, we distinguish the traditional "natural accuracy" from the "verified accuracy" the later measuring the fraction of the predictions which remains correct for all adversarial attacks within the perturbation constraints.
A.2 EXAMPLES OF PSEUDO-BOOLER CONSTRAINT ENCODING.
The first row of Table presents one inequality example containing natural variables (I1. 22, m33) The corresponding output SAT encoding given for 5 different published methods: (Abío al. (001)).
Hölldobler et al. (201)) Bén & Sörensson 2006). Manthey et al. (2014).
We see that we systematically end-up with many literals and clauses in the SAT equation. This add complexity to solve the problem. Moreover, there is no straightforward relationship between the SAT formula literals 1; and the inequality variables 2;, between the coefficient of the inequality and the clauses.
12

---

Under review conference paper at ICLR 2022
Table Examples of inequality conversion into SAT formulas according to different methodologies
Inequality convert into
21 2ny + 3zy
Encoding Abio
(4) VLV))A V (
(4) (6 ho] (6 V&L
A(4 v
U1 V (6 Vhu A (1o V (16) A (u V6)
A(12 V (T) (I 44)A
(5V4) (1. V4) (5 VÁJA
Encoding 2 Holldabler et al. (2012
(4) (
(T ( VI.VIA
(5 vl Vhal A ( vi, (G VI
(1o V V. (GT V A (1p V()) (RIA
(4) (G (4) A (ha v4)
Encoding
Eén & Sürensson 2006
(1s (bV 4 v D A T G) & ()) A ( 4 v H4 VEVEA
(5 v V vL
A (,, vh L I vh
A
I
V V VMM
(1 V A A
(ls
V G)
( V
V
(()
Encoding & Sörensson 2006
MGVE vl v vVV
VLVEV V 1)) A (la V l V
4)
IT
l V F) A (vv (
Alle V V () A (6 5
V (
A
G
4)
A (17 4 VIJ
(1 (1, V 4) (4 4, (
(4
4 V 4) A (4 & ( (G
Encoding 5
Manthey et al.
2014
(() A v (1, I 4.)
(4
V 4
A
V
V (T VIJ
(4s V ho)
(1s 44 (1) (I
A.3
MODEL DESCRIPTION
A.3.1
OVERALL ARCHITECTURE
this study, we considered the two architectures shown in Table All the paddings are set to 0.
Table 3: Different studied model architectures details.
Dataset
Name
Layers
Number of Block
Size filters
Kernela
Groups
Strides
Features
Parameters
F1.OP
Patch Size
Model Small
60-48-384-48
1-1-24-24
3-1-2-1
768
15488
(6.6)
Model Big
2
48.48.350 384 48
341-4
1-1-48-8
2-1-2-1
2352
32530
1.77 m
(7.7)
CIFAR
Model Small
Model Dig
2
2
60-48. 184 48
40-48.30 384
3-1-3-1
31111
3.3-48-48
3.3.24.24
2-1-411
3121
2352
1200
1789
32530
0.89
1.87 m
(7.7)
(6.61
A.3.2 FIRST LAYER
Like in (Jia & Rinard 2020), before applying the batch normalisation and the step function, we quantize the
inputs as x = - where the real-valued input, x is the quantized input to be fed into the TT-DCNN and is the quantization step size which can set to s = 1/255 to emulate 8-bit fixed-point values, or for adversarial training with Loo disturbance limit of
A.3.3 LAST LAYER
Last layer. The last linear layer is composed of a linear layer and a batch normalisation. The weights of the linear layer can be natural instead of binary but this leads large increase the size of the SAT formulas.
Natural features. We may also increase the amount of information held by the vector of features by accepting natural values. Coming back to our previous example, we can see the output y = 6, 14,9) as y -5 [0, 0, 0,0,0,0000000,,,00000,000,,, 0, 0, + ... + x 00, 00000000000000000000000000000000 1]. Therefore, each of these coefficients have an associated SAT expression of its own.
[0, -0,3, -2, -.4. 10, 0, 3 x $0000001100000000000000000000000
13

---

Under review conference paper at ICLR 2022
For the sake of natural accuracy performance, as in Evann al. 2021 p, it advisable encode features and weights on 8 bits. Results for features and weights encoded on 8 bits are given in Appendix A.9 However, the results in this paper are given for binary features and weights.
As we trained the TT-DCNN with final linear layer then batch normalisation, we encoded the last layer for the label as follow:
V
3/4
Σ
wk, Vi + b,
and
BN BatchNorm(y))= y Y: E(ys)
y;
+
VV Uul +
Ywk,, V4 + yb, B(y+)
BN y/
BatchNorm(gs)
+
VVal [2) +
with le 5 and denotes element-wise multiplication.
VI
BN
Wk Vs by
with
WWkk
Wkii
VVa ar Wi +
6. 76: EE(+)
/arr [8 +6
To facilitate the SAT conversion, we also restrict the variance statistics and the scale parameter in Batch- Norm() of the last layer to be scalars computed on the whole feature map rather than per-channel statistics. Before rounding, we multiply Wg,s and 6, by 100 in order to keep some details contained the floating points.
A.4 OPERATOR
We note the operator standing for the product term by term between matrices. A mask (for example N
N
M1 =
can be decomposed into two masks: (0)) and M(), M is 0 where M takes the value
I
[o 0
Null, everywhere else (ie ((
1 1 ). M()) is 1 where M takes the value 1, 0 everywhere else
(ie M = 0
Now let note 7 the input matrices of the 2D-CNN and M the matrix given by MM -- Then, we say that M matches if and only if: V(i Mii j] M
14

---

Under review conference paper at ICLR 2022
A.5 DETAILS TT-DCNN ENCODING
A.5.1 FIRST LAYER
Published in Narodytska et al. (2019b), we note Ty the quantified pixel variable, and xy the bit variable
after the first preprocessing layer, we have Tb = sign( [ (2. 14) + + sign(Tinter) ) with a, a, ls, the characteristic of the first batch normalisation. We consider two extreme values of the expression that
is an input of sign w.r.t. We have (for > 0) two extreme point: 2 Lnnter = ( + (1) + 7) and I Finter
(2q - c p)+
If inter 2 0 then we know that 1. If a inter < O then we know that O. Otherwise, {0, 1], therefore it's literal for the SAT encoding. We can consider the reverse transformation. If my (i.e. for Th 1) is solution of problem produced by the SAT solver then we can map back to Tattack (i.e.
for Tattack = x + e).
A.5.2 LAST LAYER
Let be the feature vector before the last linear layer, and 24 the of indices of V that are unknown due noise propagation and K. those that are known. We have, for the class attack higher than class target t:
V
M
Wkoa VR
Wi,VVi
1=1
We can divide the set .l...]] n] into 21 and IC
Σ kEK
Wkia Vi +
Σ
Wk.nVe
Vv >
Σ
Wr, Vx +
Σ
Wi
kEll
leK
IEU
We group together the known and
Σ (wk,t Wk,a Vv
Σ
(wiaa V
kEW
IEK
We note == [w - Vi, then c is a integer number. We have
Σ (wi. Wk,a sc-1
kel
We note G GCD(abs(wgg Wk,a)bk U), then we have:
(wk. wk,a)
C-1
Vx
kEW
As c-1 need to be an integer, we have:
(wkt Wh,a)
Vn S
G
kEW
15

---

Under review conference paper at ICLR 2022
This inequality is encoded with the project (Ignatiev et al. 2018).
A.6 EXPERIMENTAL DETAILS
Experimental environment. The project was implemented with Python and the library PyTorch (Paszke et al. 2019). The project code can be found at this URL address Our work station constituted of GPU Nvidia GeForce GTX 970 with 4043 MiB memory and four Intel core i5-4460 processors clocked at 3.20 GHz.
Training method. We build our training method on the top of & Rinard (2020) project and we refer to their notations for this section. We train the networks using the Adam optimizer (Kingma & Ba 2014) for 90 epochs with minibatch size of 128. The mean and variance statistics of batch normalization layers are recomputed on the whole training set after training finishes.
Learning rate is 0.0005. We use PGD with adaptive gradient cancelling to train robust networks, where the perturbation bound e is increased linearly from 0 to the desired value in the first 50 epochs and the number of PGD iteration steps grows linearly from 0 to 10 in the first 23 epochs.
The parameter a in adaptive gradient cancelling is chosen to maximize the PGD attack success rate evaluated on 40 minibatches of training data sampled at the first epoch. Candidate values of a are between 0.6 to 3.0 with a step of 0.4. Note that augmentation techniques for training. Due to limited computing resource and significant differences between the settings we considered, data in this paper are reported based on one evaluation run.
global parameter shared by all neurons. We do not use any data
Weight initialization. Weights for the final connected layers are initialized from a Gaussian distribution with standard deviation 0.01, and the mask weights in BinMask are enforced to be positive by taking the absolute value during initialization.
Other hyperparameters. The input quantization step s is set to be 0.61 = 0.3 x 2 + 0.01 for training on the MNIST dataset, and 0.064 16.3/255 for CIFARIO, which are chosen to be slightly greater than twice the largest perturbation bound we consider for each dataset. Except for CIFAR1O for wich we double the trainig noise, the training noise level equal to the testing noise level. The CBD loss applied on MNIST high noise only and is set to be 5e 4, O otherwise. We apply a weight decay of Ie 7 on the binarized mask weight BinMask. We use the encoding proposed in (Abío et al. [01T]) In Table [ we use model Big except for the high noise model with CI.AR10. For the post tunning parameters,
use proportion ratio of 0.1 and a probability p = 0.05 for MNIST low noise, we double it for high noise and a proportion ratio of 0.05 and probability p 0.01 for 10 low noise and we double it for high noise.
A.7 COMPARISON WITH SAT METHOD FOR EXACT SAME ARCHITECTURE AND EXACT SAME TRAINING CONDITIONS
As the architectures in (Jia & Rinard 2020) are different from ours, we reproduce the results for BNN with our exact same architecture and the exact same training conditions. We also add an experiment with their model architecture and our training condition for CIFARIO high noise as we trained it for a noise of 16/255. Results can be found in Table We can observe that our model always outperforms the BNN model in term of verifiable accuracy.
16

---

Under review conference paper at ICLR 2022
Table 4: Performance studied models as BNN for equitable comparaison
Datasct and Noise Level
Mean time (S)
Model & Training condition
Accuracy
Timeout
#cls/#vars
Verifiable
Natural
MNIST 0.3
Model Big BNN
49.53%
93.62%
0.010
0
23K/33K
CIFARIO 2/255
Model Big BNN
28.43%
37.66%
0.008
0
32K/46K
Model Small as BNN
20.21%
29.38%
0.005
0
15K/22K
CIFARIO 8/255
Architecture proposed in Jia & Rinard 2020 as BNN with our truining noise conditions
19.86%
31.95%
0.002
0
31K/64K
A.8 MODEL COUNTING
Exact model counting. Given a CNF formula 4. the problem of model counting is to calculate the corresponding number of satisfying assignments # This problem is complete for the complexity class #P (Toda 1991}. A number of tools for exact model counting have been developed and for this study we are using the recent Ganak model counter (Sharma et al. 2019). An application example of model counting is to establish how many adversarial attacks exist for trained DNN. In this case, prec defines e-ball of valid perturbations and prop states that the classification should change under small perturbations. And the problem is given to model counting solver (instead of SAT solver) in the form of CNF.
Exact model counting set up. We encode as condition the input noise and the noise propagation as before. We change the final incquality: by encoding such that the class is greater than all others. Then, we start the MaxSAT solver on this formula: it gives how many entries lead to output if class i. We also add a scenario: we randomly fixed 50% of the first layer literals to a random value (0 or 1). This leads to a partial distribution of prediction instead of an exact distribution prediction. We reports P(adv), the probability to get an adversarial, the number of timout of the exact model counting and finaly, the accuracy given by the argmax of the distribution as prediction. The same is given in the noise scenario. We tested the first 1K samples of the dataset for model with and without filtering
Results. We performed the experiments for MNIST only. Results can be found in Table 3 First, we observe that, for the Small model, the number of solved samples is very high: almost 100% except in 3 cases: when the final linear is not binary (Ter) and when the training noise is not in line with with the testing noise. This contrasts with the results in Narodytska et al. (2019b) where there is only a single configuration with 100% of the instances solved with an approximated model counting. In the case of Small model, the probability to get an adversarial is pretty high. The latter surprisingly increases with the filtering and with the robust training. On the contrary, for the Big model, the probability to get an adversarial is pretty low and the number of time out increases. However, in the noise setting, the number of timeout drastically decreases, but the probability to get an adversarial also increases. We also highlight the very high accuracy if we return the argmax of the output distribution as prediction. We think these observations can lead to interesting further works.
A.9 ABLATION STUDY
1.9.1 NATURAL ACCURACY
We compare the BNNs, TT-DCNN models and the standard real-valued models. We use the two-block Big model, without the amplification blocks for BNN and vellev model. TT-DCNN has final layer with
17

---

Under review conference paper at ICLR 2022
Table 5: Results of TT-DCNN the likelihood adversarial examples set-up for MNIST
Model
Nuise triin
Nuise test
Loss
Amplitication
Final Lincar
Plade
Accuracy Pladv)
Timeout Pladvy
with 50% noise
Plady)
with 50% moise
Accuracy
Raadv
Piadv) with 50% unise
Timeost
Nermal
Frltered
Normal
Filtered
Nornal
Filtered
Nomaa
Filtered
Normal
Fittered
Noemal
Filtered
0.3
Small
Bin
0.119
716
101
0.55
875
0
0.5
Neceaal
Bin
0,00064
0.00162
526
549
432
388
0.0135
0.012
808
862
13
0.1
0.1
0
Nermal
Din
0.2135
0.2194
935
932
0.3787
0.3559
928
930
0
Small
Rin
Rin
0,9265
0.1003
0. 0.1068
0.1085
901
900
0.3019
0.2849
0.28667
0.289
884
865
0.467
0.3439
0.1643
0.3038
Bin
0.1914
0,2060
0,36322
0,3412
Ter
11.0
Bin
Normal
0,022
00229
973
0.05
0.08
978
Rig
0.3
Nermal
Bin
26-10
26-10
802
815
184
174
Nermal
Rin
SF-06
2P-06
802
805
105
0.014
0.017
916
942
31
0.3
Normal
Bin
0J155
864
108
0.4
0.3
Normal
Bin
0.04464
862
125
03
Nermal
Rin
0.005
0.009
867
864
105
94
0012
0,0377
936
923
integer values. We stopped the training at 45 epochs for all three models to prevent overfitting. We also compare TT-DCNN for two values of truth table size n: 9 and 27. The results are given in Table O We observe that for MNIST and CIFARIO, TT-DCNN outperforms BNN and is inferior to the real-valued model. We also observe that increases, TT-DCNN tends to the real-valued model performances. We use 27 as seems reasonable to compute 2 operations to get the SAT formula of filter.
Table 6: Comparison of natural accuracy between TT-DCNN, BNN and DCNN.
Binary based model
Real based model
TT-DCNN Our
TT-DCNN Our (n 27)
BNN
DCNN
(n= 9)
Natural Accuracy on MNIST
96.98%
98.49%
98.35%
98.47% 58.08%
Natural Accuracy on CIFAR10
53.53%
66.16%
54.11% %
Table 7: Comparison of model architectures between TT-DCNN, BNN and DCNN.
BNN
DCNN
TT-DCNN
Type weigths Type Intermediate values
Binary
Floating
Floating
Binary
Flouting
Mixed Floating Binary
Group CNN
Not Grouped
Not Grouped
Grouped
MLP
MLP
Final linear clussification
(Mutti-ayyerPerreppoonn
(Multi-Layer-Pereeproo))
Linear
A.9.2 STUDY ON INFLUENCE OF AMPLIFICATION LAYER
We tested three models: model without amplification (one block is one layer). model with minimal amplification (one block is two layers- with amplification factor 1) and a model with standard amplification (model presented in Appendix I. Results are presented in Table g We respect the training conditions proposed in Appendix A.6
We can observe that the amplification layer is always profitable for the natural accuracy.
18

---

Under review conference paper at ICLR 2022
Table Comparison the natural accuracy of TT-DCNN for three different types of amplification configuration, for CIFARIO and MNIST, in the case of training with noise and without noise.
Dataset
Noise Training
Amplification
Accuracy
Model Small
Model Big
No
59.71%
95.28%
Small Normal
91.66%
95.79%
94.60%
97.53%
MNIST
No
82.63%
92.42%
0.4
Small
85.67%
94.19%
Normal
87.59%
95.77%
No
40.53%
44.33%
Small
42.51%
47.12%
Normal
44.05%
50.27%
CIFARIO
No
22.40%
28.05%
16/255
Small
27.86%
37.29%
Normal
32.19%
47.12%
A.9.3 OTHERS
For the study, tested the first IK samples of the dataset for model small and big with and without filtering. We reported the natural accuracy, the verified accuracy, the total time to compute, the number of clauses and variables. We don't 't report the number of timeout they are all The results were computed on other computer than those of Table I We took the measures for different:
Size of the model. We use the two models presented above.
Dataset. We use MNIST and CIFARIO
Training noise level.
Testing noise level.
Loss coefficient as introduced in Jia & Rinard (2020).
Amplification Layer. Two amplifications possibles described in Appendix A.9.2
Final Layer. Two possibilities: with binary (Bin) or ternary (Ter) weigths.
First, we saw that MNIST and CIFAR10 can be scaled to our two models for low and high noise. Then, we observe that the loss coefficient has little impact on the performances. We can highlight that the training noise level has important impact the verification accuracy and the time computation. We observe that most the time the filtering leads to a better verifiable accuracy and sometimes to a better natural accuracy.
19

---

Under review conference paper at ICLR 2022
Table 9; Results of TT-DCNN in the untargeted attack set-up for CIFARIO
Model
Noise train
Noise test
Less type
Amplification
Final Linear
Natural Accuracy
Venifable Accuracy
Moan time
#clsWvvars
Filtered
8/255
Normal
Small
Bin
Bin
458
456
20
18
0.254
0.266
108501555
972271610
456
(ight)
0.105
0.208
661/258
2/255
2/255
Normal
Bin
463
446
463
300
299 (stoogg)
288
01:45
03:25
0.200
60V/23
584/233
6757269
2,2/255
Normal
Bin
488
431
305
316
0.106
0.217
7302279
676/257
Small
345
245
190
185
0.090
0.239
1349/395
1273/390
Small
8/255
8/255
Normal
Bin
357
357
356
196
231 (Strong)
(light)
0.109
0.213
0.208
2269/509
2176/507
Normal
Bin
368
347
173
186
0.110
0.223
18904494
1519/464
Normal
358
299
178
0.113
0.200
2337/557
203 1/38
0.061
Normal
Bin
329
219
0.092
1342/425
16/255
8/255
Normal
Normal
Bin
Bin
334
344
334
191
194
193
0.093
0.095
0.206
14734161
1339/113
1273H228
16.7/255
Normal
Bin
347
332
201
244
0.998
0.199
1379/051
13004400
8/255
Normal
Small
Bin
539
500
13
10
0.703
0.640
23/73/8874
20183/3545
2/255
8/255
8/255
Normal
Bin
390
133
0.172
40P97730
Big
Small
Bin
294
226
0.193
3595/813
Normal
Bin
366
214
0.205
4606/94
16/255
8/255
0.512
22757/9828
Normal
Bin
348
212
0.175
3625/912
Normal
Bin
327
108
0.174
4661/957
Table 10: Results of TT-DCNN in the untargeted attack set-up for MNIST
Model
Noise tain
Nouse test
Loss type
Amplificaion
Fasll Lineze
Natural Accuracy
Vasifabl Accuracy
Meu time
(6)
Timcrut
#cleidass
Normal
Filioved
Normal
Filizved
Nornal
Hilized
Normal
Fillered
Nocmal
Filteee
0
0.3
Normal
Small
Bia
Bla
936
500
906
226
169
161
0.183
0.239
11268
2771 / 795
32081671
2974833W
0.1
0.1
Necmal
Bia
943
937
548
665
0.073
0.128
456/199
442/195
Small
0.3
0.3
Normal
Normal
Bin
912
906
902
866
674
665
648
637
0.139
0.347
0.207
0.217
665 1405
1405500
1370499
1392 493
Small
$19
670
0.114
977/397
Nermal
Bia
839
676
0..27
1001/425
0.4
0.3
Normal
Bia
830
681
(1.44
12984667
Normal
Bin
836
88
677
680
0.117
0.345
1069 421
1041 419
Normal
Ter
930
641
0.324
4016/1887
0
0.3
Neemal
Bin
974
111
0.716
9879/2637
0.1
0.1
Normal
Bin
976
977
978
944
946 (lw)
947 (low)
0.302
0.496
0.491
11446 461
1137 459
11384459
Dig
0.3
0.3
Normal
Normal
Bin
Din
957
965
964
949
953
771
774
778 (high)
773 (high)
776
0.485
0.463
0.634
0.696
0.634
0
4047/1250
3923 1240
5834/1206
3820 1223
386V1231
Nermal
Bin
951
700
0.435
5165/1039
0.4
0.3
Normal
Normal
Bin
Bia
957
954
931
508
508
781
0.436
0.446
0.590
5017 1062
2816
Normal
Tar
974
723
10.44
20


Reviews:
[{"review_id": "zPuPkw56J4N", "reviewer": "Reviewer_UdYz", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "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": "Explainability and formal verification of deep neural networks are vibrant research venues.\nInstead of focusing on techniques for interpreting/verifying the existing models, this work proposes a novel architecture that admits a more compact symbolic encoding *by construction*, resulting in networks that are more easy to interpret and verify. I think that the idea is sensible.\n\nI think that I got the intuitive idea behind TT-DCNs, but the presentation of the architecture could be largely improved, possibly by adding figures and more examples. The core idea seems simple: reducing the ariety of certain functions, in order to exhaustively enumerate input-output pairs in truth tables. This of course comes at a cost in terms of expressiveness, and the trade-off between interpretability and predictive performance is not very clear. Generating abstractions of logical theories is a venerable field of study and the existing techniques can be applied to other models too. The claim that these architectures are more interpretable (and can be fine-tuned by hand) thanks to their truth tables is not very convincing and should be substantiated with experiments, comparing different XAI approaches. With the current version, I am left wondering if interpretability is a natural by-product of the model's limitation to small truth tables.\n\nThe writing seems tailored towards experts in this area. The reader is assumed to be knowledgeable about formal verification of neural networks. For instance, \"verifiable accuracy\" or \"complete robustness\" are not defined anywhere in the text.\n\nMinors:\nThe definition of patch function is unclear to me.\n\"We have P (1) = k and P (s + 1) = P (s) if and only if the kernel size of the layer is 1.\"\nWhat if the kernel size isn't 1?\n\n\"In fact, the feature associated to the filter f is equal to 1 if there exists a mask M in the set of masks S f that matches the input patch, 0 otherwise (we will define later what are a mask, a set of masks and the matching operator).\"\nI would then avoid mentioning these concepts.\n\n\"To the best of our knowledge, this is the first time that the exact knowledge of a real-valued DCNN is formally extracted.\"\nIsn't this true for BNNs compiled to propositional formulas too?\n", "summary_of_the_paper": "This article proposes a novel convolutional architecture, dubbed Truth Table DCNs (TT-DCNs). Compared to Binary Neural Networks (BNNs), the proposed architecture admits a much more compact propositional logic encoding while improving their accuracy.  \nTo the best of my understanding, the core idea is using real-weighted convolutions and aggregations that are then binarized with step-functions. These convolutions can be fully represented with truth tables, as long as the number of inputs in the filter is low-dimensional.  Furthermore, the authors claim that the proposed architecture is intrinsically more interpretable than BNNs and that it can be post-tuned by integrating human knowledge in the truth tables.  Experiments show that TT-DCNs are more easily verified while retaining practical predictive\nperformance.", "summary_of_the_review": "- The paper addresses a very relevant problem in AI\n- Developing deep architectures that are verifiable and interpretable by construction is a sensible idea in my opinion\n- The presentation of the proposed architecture could be improved by adding figures and more examples\n- Adding some definitions would benefit a large audience of non-experts in verification\n- The trade-off between interpretability and predictive performance is not well characterized\n- The claim that the model is more interpretable should be substantiated with experiments comparing TT-DCNs with other XAI methods", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "cCHX4Q0z95", "reviewer": "Reviewer_wThs", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "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": "**Strength**\nThis work has proposed a method to improve the scalability of SAT solvers to deep networks to aid robustness verification. \n\n**Weakness**\n* The models used in this paper are for very small-sized neural networks trained on simple datasets like MNIST and CIFAR 10. This approach is unlikely to ever scale to large models with millions of parameters trained on datasets like Imagenet. The main reason being *grouping parameters* makes a trade-off between the generalizability of the network and its scalability to SAT solvers.\n* This paper uses *grouping parameters* to keep things scalable. This compromises the overall accuracy of the model but prevents the number of clauses from exploding. Even with this simplification, this method performs marginally better than the real value-based complete verification method for low noise is unable to perform better in high noise cases such as *MNIST epsilon_{test} = 0.3* and *CIFAR 10 epsion_{test} = 8/255*. \n* The statement *The only scalable method for global exact interpretability was proposed in (Granmo et al., 2019)* in sec. 2  is somewhat inaccurate.  [1] is a recent work that addresses the issue of scalability of MIP solvers to Deep Networks in the context of Model Explanation. This work essentially simplifies the formula to be encoded in the MIP solver by using gradient-based methods. The MIP solver then generates explanations by solving for the simplified formulation. This simplified formulation is what allows this method to scale to very deep networks typically feat. millions of parameters. \n\n**citations**\n\n[1] Subham Sekhar Sahoo, Subhashini Venugopalan, Li Li, Rishabh Singh, and Patrick Riley. Scaling Symbolic Methods\nusing Gradients for Neural Model Explanation. International Conference on Learning Representations, 2021.\nhttps://arxiv.org/abs/2006.16322", "summary_of_the_paper": "This paper proposes a new kind of SAT-encodable Neural Network which has real-valued weights and binary activations. Since the activations are binary, this work constructs a truth table to map the inputs of a CNN block to its outputs. This helps to deduce the output of the CNN block as a boolean function of the input variables while allowing intermediate values to be real. This formula also gives a set of masks that identify the conditions for which a given neuron is active. Tuning this set of masks post training helps increase the generalisability of the network - sec 4.1. Furthermore, this causes the encoded formula to be relatively simpler than the other existing methods for verifying BNNs and thus helps in keeping things scalable for the sat solver. The authors have conducted experiments to show that this method achieves a better performance in terms of verifiable accuracy and runtime than the existing methods (Table 1).", "summary_of_the_review": "Working with SAT solvers and Neural Networks is a very challenging task. [1] has already set the bar high and has paved the way for scaling NP-Hard solvers like MIP solvers to very deep neural networks. Unless the authors can achieve a similar feat where their approach scales to much deeper networks (ex. Inception model), I'm leaning towards rejecting this work because I see this work as incremental.\n\n**citations**\n\n[1] Subham Sekhar Sahoo, Subhashini Venugopalan, Li Li, Rishabh Singh, and Patrick Riley. Scaling Symbolic Methods\nusing Gradients for Neural Model Explanation. International Conference on Learning Representations, 2021.\nhttps://arxiv.org/abs/2006.16322", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "UFrJn2jruhN", "reviewer": "Reviewer_garj", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "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": "Strengths: \n- the idea of using a truth table to distill (or approximate) real-valued feature vector is novel and very interesting\n- TT-DCNN provides certain interpretability and supports manual post-processing\n- the robustness of TT-DCNN can be verified using SAT solvers\n\nWeaknesses and actionable feedback:\n- the writing is a bit hard to follow, which is mainly due to frequently referring to the appendices that seem necessary to understand the main content of this paper (e.g., Sec 3.4, V(f,i,j) is not easy to get without carefully looking back and forth). Heavily using appendices in such a way adds extra burden for reviewers and gains unfair advantages. \n- missing important baselines, for instance, the authors are clearly aware of that Narodytska et al. 2019b work is highly related, given it has been cited many times; however, it is a bit surprising to see the evaluation does not use it as a baseline. \n- there are lots of conceptual claims, however, which are not backed up by experimental results. Sometimes the result indicates the opposite.  For instance, \"drastic reduction in the size of SAT formulas renders our model truly amenable to formal verification\". This is not true, since the evaluation shows that the baseline Jia & Rinard (2020) is actually much faster (e.g., 3~30 times faster). For another instance, the authors emphasize \"highly interpretable\" lots of times, however, simply filtering out sparse binary masks seems not sufficient to support that claim, at least some case studies (e.g., what highly interpretable features are actually learned) need to be presented in order to support that claim. \n- TT-DCNN seems to be a new architecture, and some discussion regarding training would be necessary.\n", "summary_of_the_paper": "This paper proposes Truth Table Deep Convolutional Neural Networks (TT-DCNNs), which _distills_ real-valued feature vectors (i.e., small convolutional layers) into truth tables (also called masks), which are represented in boolean formulas using the disjunctive normal form (DNF). These masks indicate certain interpretability, e.g., the set of variables actually contributed to the truth value. Some manual intervention or post processing like removing overfitting masks could help improve model accuracy. The experimental evaluation shows that model accucy on MNIST and CIFAR10 dataset is comparable with or slightly better than other state-of-the-art approaches. ", "summary_of_the_review": "I like the idea presented in this paper and hope it could be backed up in a more systematic and scientific way. Writing issues should be easy to address; it is just the current evaluation is a bit unsatisfactory (i.e., missing a highly relevant and important baseline), thus not very convincing. So I slightly prefer not to accept this paper, at least in its current state. I would be happy to adjust my assessment, if the authors could address my concerns about experimental evaluation during rebuttal.  ", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "FMamCEt_YpC", "reviewer": "Reviewer_RhEH", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "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": "In my opinion, the paper's premises are not correct. As far as I can\nunderstand, BNNs were developed to target issues like power\nconsumption and ease of circuit-level integration, and not the\ndifficulties with propositional encodings or the sizes of such\nencodings, or even issues interpretability, of the models or their\nencodings.\n\nFurthermore, I cannot understand why interpretability of a SAT\nencoding is a concern. The SAT encoding is simply a representation\nthat is used to reason about the original machine learning model.\nSAT encodings are important because they enable efficient reasoning in\nsome settings, but not because of issues with interpretability.\nFurthermore, any information resulting from reasoning about the\noriginal machine learning model on such a representation can be\nrelated with the original model.\n\nTo obtain a SAT encoding the paper makes several critical decisions.\nOne is to consider features to take boolean values. Another one is to\nassume a very restricted representation, one where at most nine\nfeatures can be considered. From what I can understand, raising\nsignificantly the number of features used in the representation would\nmake the encoding impossibly large.\n\nIn my opinion the paper is not well written. For example, 2D-CNNs are\nbriefly described in a paragraph containing no references. The\nexplanation is not easy to follow. This applies to section 2, but also\nto section 3. For example, I was unable to understand how one goes\nfrom equation (1) to an intermediate equation claiming that one can\ngenerate both CNF and DNF representations. I was unable to make sense\nof the subsequent example, and I have some experience with logical\nencodings.\n\nAlso, the integration of different blocks is unclear. I can understand\nhow this might be done in the case of an intermediate CNF\nrepresentation. However, I was unable to understand how this might be\ndone for a DNF intermediate representation. If this was easy to do,\nthen satisfiability for CNNs should be easy to decide, and that cannot\nbe the case. I could be missing something here, but the writeup does\nnot help. \n", "summary_of_the_paper": "The paper proposes a new machine learning model TT-DCNN as an\nalternative to Binarized Neural Networks (BNNs). The paper claims that\nthe new machine learning model simplifies and improves\ninterpretability of the SAT encodings.\n", "summary_of_the_review": "The paper proposes to learn a new machine learning model, one that\nsimplifies the propositional encoding, and subsequent reasoning with a\nSAT solver. The work could be of importance, but the current writeup\ndoes not help to convey the key ideas. In its present form, I cannot\nrecommend acceptance of this paper.\n", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}]

Author rebuttal:

Meta-review: I think there is good research behind this paper, but the presentation issues make it difficult to argue for acceptance. 

On the positive side, the paper has made a clear advance in terms of the ability to do full SAT-based verification of neural networks. However, there are also important issues with the paper that prevent it from being accepted: 
* The paper argues for the value of the new approach for *both* verifiability and interpretability, where interpretability is measured in terms of the ability to make targeted adjustments to the network to change its behavior. These are very different goals, but they are conflated in different parts of the paper, leading to confusion, for example, from reviewer RhEH. 
* The paper only compares against SAT/SMT-based verification, but completely ignores other approaches to verification that are arguably more effective for many problems. In particular, there is an emerging literature on Abstract Interpretation-based verification that is significantly more scalable than SAT-based verification and which this paper ignores.
* The paper's claims sometimes get ahead of the presented evidence, as pointed out by reviewer garj. 

So overall, I think this paper needs another iteration before it is ready for acceptance.
Decision: Reject