TRUTH TABLE DEEP CONVOLUTIONAL NEURAL NETWORK, A NEW SAT-ENCODABLE ARCHITECTURE - APPLICATION TO COMPLETE ROBUSTNESS
Year: 2021

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 TTDCNNs 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.

heading: 1 INTRODUCTION
text: 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 in a variety of applications, several concerns have emerged: lack of robustness emphasized by a lack of explainability, difficulty of integrating human knowledge in postprocessing and impossibility to formally verify their behavior due to their large complexity. Under these circumstances and especially when these systems are 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 a patent on the DNNs’ portability on a platform
incorporating a component dedicated to formal verification (Driscoll, 2020). Also, the European Union’s general data protection regulation includes a 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., 2018) which are not yet scalable to real-valued DNNs. Some recent publications (Jia & Rinard (2020);Narodytska et al. (2019b); Narodytska et al. (2018)) approach the problem of complete verification from the well-known boolean SATisfiability (SAT) (Biere et al., 2009) point of view where Binary Neural Networks (BNNs, Hubara 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 a vast range of question such as how many adversarial attacks exist for a given DNN, image and noise level (Narodytska et al., 2019a). Besides, this approach is faster than SMT or MIP robustness verification method (Jia & Rinard, 2020). 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. Finally, only few studies (Ignatiev et al. (2019a) ; Ignatiev et al. (2019b)) investigated the relationship between formal DNNs’ verification and XAI.
Our contributions. In 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 a truth table to allow weights and certain intermediate values to be real. To the best of our knowledge, this is the first method to encode a real-valued DCNN into SAT. For the first time, we can extract all the logic classification rules from a subfamily of DCNNs which allows a 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. (2) TT-DCNNs offer two main valuable conversion properties over BNNs. (2-a: Post-tuning) The first one allows us to integrate human knowledge in the 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 a filtering approach, which increases the verifiable accuracy without decreasing the natural accuracy (cf. Appendix A.1). (2-b: Tractability) The second property is the possibility to compute all possible model inputs/outputs prior to deployment in production. In an 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.1). TT-DCNNs offer a good tradeoff between the state-of-the-art of BNN/SAT method (Jia & Rinard, 2020) and of real-valued DNN/MILP complete robustness verification methods (Xiao et al. (2018); Tjeng et al. (2017)). This is expected as our network is both real-weighted and SAT-convertible. 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 CIFAR10 when compared to BNN/SAT method while decreasing the verification time by a factor of 9 for MNIST and 150 for CIFAR10 high noise when compared to DNN/MILP methods. Finally, our SAT formulas are 5 and 9 times more compact in term of number of clauses for high noise MNIST and CIFAR10 respectively compared to the BNN/SAT method.
Outline. Section 2 introduces the notations and the related work. Section 3 presents our new TT-DCNN model and its two main properties. Section 4 details the complete robustness verification set-up and reports the evaluation results. Finally, we conclude this work in Section 5.

heading: 2 BACKGROUND & RELATED WORK
text: 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 a boolean expression in a Conjunctive Normal Form (CNF) or in a Disjunctive Normal Form (DNF). They are both defined over a set of boolean variables (x1, · · · , xn). A literal li is defined as a variable xi or its complement xi. A CNF is a conjunction of a set of clauses: Φ = (c1 ∧ · · · ∧ cm), where each clause cj is a disjunction of some literals cj = lj1∨· · ·∨ljr. A DNF is a disjunction of a set of clauses: Φ = (c1∨· · ·∨cm), where each clause cj is a conjunction of some literals cj = lj1 ∧ · · · ∧ ljr. A pseudo-boolean constraint is a
constraint of the form: N∑ p=1 aplp ◦ b, where ap ∈ Z, b ∈ Z and ◦ ∈ {≤,=,≥}, which can be mapped to a SAT formula (Roussel & Manquinho, 2009). However, the output SAT formula contains a tremendous number of clauses and literals compared to the number of variables in the pseudo-boolean constraint making it very hard to understand (cf. example in Appendix A.2). A boolean function has the form {0, 1}n → {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 a function Φf , which, for a given filter f , takes n = k2c inputs at position (i, j) with k the kernel size and c the number of input channels. The outputs can be written y(i,j)f = Φf (x (i,j) 1 , · · · , x (i,j) n ). 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 k needs to be replaced by a patch function P (s) (also referred to as the size of a 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 sth layer at position (i, j). 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 a DNN into a SAT formula is limited to BNNs (Narodytska et al. (2018); Cheng et al. (2018)) and involves recomposing a block formed of a 2D-CNN layer, a batch normalization layer and a step function into an inequality in order to apply the pseudo-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 to the number of variables in the pseudo-boolean constraint (cf. example Appendix A.2). This prevents both the interpretability and the tractability of those SAT/BNNs formulas. Hence, our goal is to find a real-valued DCNN with good performance and coincidentally convertible to SAT with fully interpretive inference.
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 et al. (2018)). PI-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 to obtain the equivalent conjectures. Using truth tables in machine learning has been documented for hardware optimisation (Soga & Nakahara (2020), Wang et 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.

heading: 3 TRUTH TABLE DEEP CONVOLUTION NEURAL NETWORK (TT-DCNN)
text: 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 Sf 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 a 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 Sf for all filters, we no 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 1. We will initially analyse a 2D-CNN layer with a single filter (Section 3.1). 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.

heading: 3.1 SAT ENCODING OF A ONE-LAYER 2D-CNN
text: 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.
One filter. The main idea is to 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 Section 2, we have as output y(i,j)binary,f , for the filter f :
y (i,j) binary,f = Bin(y (i,j) f ) = Bin(Φf (x (i,j) 1 , · · · , x(i,j)n )) (1)
with Bin being the Heaviside step function, defined as Bin(x) = 12 + sgn(x) 2 . If xj ∈ {0, 1}, we can establish the truth table of the 2D-CNN’s filter f by trying all the possible inputs, for a total of 2n operations. In this paper, we will limit ourselves to n ≤ 9. Hence, in 29 = 512 operations, we can trivially generate our truth table. Then, we can convert the truth table into a simplified SAT formula and by doing so we can rewrite Equation 1 as:
y (i,j) binary,f = SAT DNF f (x (i,j) 1 , · · · , x(i,j)n ) = SAT CNF f (x (i,j) 1 , · · · , x(i,j)n )
with SATDNFf (resp. SAT CNF f ) being the formal expression of the filter in the DNF form (resp. CNF form). It is noteworthy that unlike previous works, our approach is not limited to binary weights but allows for arbitrary weights within the 2D-CNN.
Example. We consider a 2D-CNN with one filter and a kernel size of 2, with the weights: W1 =[ 10 −1 3 −5 ] . As c = 1, we have X = [ x0 x1 x2 x3 ] and the sixteen possible entries are: [ 0 0 0 0 ] ,
1Link video: https://youtu.be/loGlpVcy0AI
[ 0 0 0 1 ] , [ 0 0 1 0 ] , [ 0 0 1 1 ] , · · · , [ 1 1 0 1 ] , [ 1 1 1 1 ] . For each input, we calculate the corresponding output:
y = [0,−5, 3,−2,−1,−5, 3,−2, 10, 5, 13, 8, 9, 4, 12, 7]. After binarization with the Heaviside step function, we have ybinary = [0, 0, 1, 0, 0, 0, 1, 0, 1, 1, 1, 1, 1, 1, 1, 1]. Therefore, after simplification, we have SATDNF1 = (x2 ∧ x3) ∨ x0 and SAT CNF 1 = (x2 ∨ x0) ∧ (x3 ∨ x0).
Multiple filters. For multiple filters, the above described method is simply repeated for each individual filter, thus yielding one expression per filter.
Multiple channels. As convolutional networks generally take several channels as input (3 for RGB images or 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 = 9. 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 a factor of g. We have in that case n = k2c/g. Thus, in the above example, by using 16 groups, the number of inputs to our truth tables becomes 3216 ×2 2 = 8.
Limits. At this point of the model development and despite the real-valued weights, we observe sub-optimal performances due to 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 8 of Appendix A.9.2 for detailed results.

heading: 3.2 SAT ENCODING OF A TWO-LAYERS 2D-CNN: ONE BLOCK OF TT-DCNN
text: 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 a second layer as long as we do not increase the patch size. This can be simply achieved by adding a layer with kernel size 1. Note that the intermediate values from the first layer do not need to be binary anymore. From a 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 a so-called amplification parameter which corresponds to the ratio between the number of filters of the first layer and the number of filters of the second layer (value often set at 8). Each layer is followed by a batch normalisation and a non-linear activation function: ReLU for the first layer and Heaviside step function for the second one.

heading: 3.3 THE TT-DCNN ARCHITECTURE
text: Having defined one block of 2D-CNN in the previous section, we may now examine how this block is integrated into the TT-DCNN. The overall architecture is presented in Appendix A.3.1
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 a three steps first-layer or pre-processing procedure: (i) Quantitation of inputs (Jia & Rinard, 2020); (ii) Batch normalization (Narodytska et 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-boolean constraint as detailed in Section 2
as long as the weights are integers 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.

heading: 3.4 INTERPRETATION OF OUR TT-DCNN MODEL AND TWO IMPORTANT PROPERTIES
text: Interpretation. To illustrate the ease of interpretability of our conversion method, we now offer an interpretation of the SAT formula of the filter with weight matrix W1 defined in the example of Section 3.1: SATDNF1 = (x3 ∧ x2)∨ x0. First of all, we can observe that the expression is now independent of the value of x1. Then, because the formula is a DNF, we observe that there are two conditions to activate the feature. We
can define the set of masks S1 = {M1,M2} with M1 = [ N N 1 0 ] and M2 = [ 1 N N N ] , corresponding to the clause x2 ∧ x3 and x0 respectively, with N denoting Null. We can 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 can be either a 0 or a 1) and that only the 0 and 1 positions should exactly match the 0 and 1 positions of the transformed binary input in order to activate the feature. A formal definition of the operator ≡ is given in Appendix A.4. The features for filter 1 are therefore indicator functions in the case of our model.
More generally, from the SATDNFf expression we can establish Sf , the set of masks for filter f . Then, the value V at position (i, j), for filter f is:
V (f, i, j) = { 1 if ∃M ∈ Sf such that P (L, i, j) ≡M 0 otherwise
In our example with f = 1, the feature V (1, i, j) would be activated if P (L, i, j) ≡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 Sf . The existence and the analysis of Sf creates a strong link between XAI and formal verification. To the best of our knowledge, this is 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 Sf for a specific purpose. We will see in the next section how we can build a heuristic to 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 4 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.

heading: 3.5 EXPERIMENTS
text: Results. Our aim is to provide a fully interpretable SAT-convertible model with high natural accuracy. Table 6 compares the performance of a given real-valued DCNN with its corresponding TT-DCNN and BNN (cf. results and architectures in Appendix A.9.1). As expected, this TT-DCNN gives better natural accuracy than BNN (+1.37% for MNIST, +0.57% for CIFAR10) but inferior than the original DCNN (-0.14% for MNIST, -12.05% 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.
Limits and further works. Our results look promising for further scaling up, by adding a block layer or/and increasing the truth table dimension (for n ≥ 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 Sf . For instance, before using the MNIST dataset, we could force training filters with relevant geometrical shapes (arc of circle, circle, line etc.). Ideally, it 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 et al. (2019b); 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 be solved by classic SAT solvers and exact model counting. In doing so, we improve the previous state-of-the-art of SAT complete neural network robustness verification for high and low noise levels.

heading: 4 APPLICATION TO COMPLETE ROBUSTNESS VERIFICATION
text: 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 Sf 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 use the first property to address a very general problem: adding domain knowledge into a 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, we 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 art models.

heading: 4.1 POST-TUNING: CHARACTERIZING AND FILTERING OVERFITTING MASKS
text: General. One may envision the set Sf as a bag full of masks. Upon training, this set is fixed such that it 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
the mask M2 = [
1 N N N
] is too general and decide to remove it from the set S1. By doing so, we modify the
activation of filter 1 by integrating human knowledge in post-tuning.
Characterizing overfitting masks. A mask is considered as an overfitting mask if the ratio of the number of Null values over the total number of variables in the mask is below a certain threshold (cf Appendix A.6). 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 can 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 as 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 CIFAR10: from 22.79% to 23.08%, without affecting the natural accuracy: from 31.18% to 31.13%. The results are shown in Table 1.

heading: 4.2 TRACTABILITY: ENCODING THE ADVERSARIAL SETUP INTO SAT
text: General. Another feature of the TT-DCNN’s architecture is that one can calculate all the possible inputs/outputs of the 2D-CNN block before using the model in production.
Encoding pixel noise. Let us consider some noise (e.g. norm-bounded by l∞) 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 to 1 or from 1 to 0) and hence we consider them "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 4 entries, there are 34 = 81 input possibilities for the block level in
an adversial/production setting due to noise: [ 0 0 0 0 ] , [ 0 0 0 1 ] , [ 0 0 0 U ] , · · · , [ U U U U ] . More generally, as
the maximum number of variables for the SAT entry was set to n = 9 in this paper, there are therefore a maximum of 39 = 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. In order to encode noise propagation through blocks, we encode in SAT the input/output relationship y(i,j)f = SAT CNF f (x (i,j) 1 , · · · , x (i,j) n ) for all (i, j) and f . For example, for
the filter 1 SATDNF1 = (x2 ∧ x3) ∨ x0, the entry [ 0 1 0 U ] gives x3 = U as output. The latter result depends
on U , whereas the input [ 0 U 0 0 ] 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 ri,j = yi − yj > 0 as a reified cardinality constraint which denotes whether the score of class i is higher than the score of class j. Being able to 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-the-art models. Looking at MNIST high noise for instance, our SAT equation yields on average 4K clauses and 1K variables (Table 1). This is a 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 CIFAR10 noise (Table 1). 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.

heading: 4.3 EXPERIMENTS
text: Untargeted attack. Table 1 presents gathered results for natural accuracy, verifiable accuracy for l∞-norm bounded input perturbations, verification time and the average number of clauses and variables in the SAT formulas on MNIST and CIFAR10. We compare our work with the state-of-the-art of exact verification for BNNs (Jia & Rinard, 2020) and for real-valued networks (Xiao et al. (2018); Tjeng et al. (2017)). We present model architectures details and experimental settings in Appendix A.3.1 and A.6. Table 1 shows that our model after filtering masks considered to be overfitting is more robust. Moreover, our verifiable accuracy is always superior to that of the BNN and even superior to that of the real value based model in the CIFAR10 high noise case. We also show that, with a general SAT solver (here MiniCard (Liffiton & Maglalang, 2012)), we reach a resolution time competitive with BNNs and much lower than the real-valued model. The latter
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-art. Extended comparison are given in Appendix A.7.
Likelihood of adversarial examples. The objective of this experiment is to demonstrate that our approach, thanks to 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 is 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 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.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.

heading: 5 CONCLUSION
text: 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-processing the model. It exhibits competitive performance given low and high noise with state-of-the-art complete verification methods on MNIST and CIFAR10. 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 a suitable response to the rising demand for functional formal verification.

heading: 6 REPRODUCIBILITY
text: The project code reproducibility for can be found at this URL address2

heading: A APPENDIX

heading: A.1 COMPLETE VERIFICATION & ROBUSTNESS.
text: Property verification of SAT-convertible DNNs has been presented in (Narodytska et al., 2018) as follows: given a precondition prec on the inputs x, a property prop on the outputs o and a SAT relations given by a DNN between inputs/outputs denoted as DNN(x, o), we check whether the following statement is valid: prec(x) ∧ DNN(x, o) =⇒ prop(o). In order to seek a counterexample to this property, we look for a satisfying assignment of prec(x) ∧DNN(x, o) ∧ prop(o). An application example of property verification is to check for the existence of adversarial perturbation in a trained DNN. In this case, prec defines an -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.

heading: A.2 EXAMPLES OF PSEUDO-BOOLEAN CONSTRAINT ENCODING.
text: The first row of Table 2 presents one inequality example containing 3 natural variables (x1, x2, x3). The corresponding output SAT encoding are given for 5 different published methods: (Abío et al. (2011), Hölldobler et al. (2012) , Eén & Sörensson (2006), Manthey et al. (2014)).
We can 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 li and the inequality variables xi, or between the coefficient of the inequality and the clauses.

heading: A.3 MODEL DESCRIPTION

heading: A.3.1 OVERALL ARCHITECTURE
text: In this study, we considered the two architectures shown in Table 3. All the paddings are set to 0.

heading: A.3.2 FIRST LAYER
text: Like in (Jia & Rinard, 2020), before applying the batch normalisation and the step function, we quantize the inputs as xq = bxq c · s where x is the real-valued input, x
q is the quantized input to be fed into the TT-DCNN and s is the quantization step size which can be set to s = 1/255 to emulate 8-bit fixed-point values, or 2 for adversarial training with a l∞ disturbance limit of .

heading: A.3.3 LAST LAYER
text: 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 to a large increase in the size of the SAT formulas.
Natural features. We may also increase the amount of information held by the vector of features V by accepting natural values. Coming back to our previous example, we can see the output y = [0,−5, 3,−2, 1,−4, 4,−1, 10, 5, 13, 8, 11, 6, 14, 9] as y = −5 × [0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + 3 × [0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + · · · + 9 × [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1]. Therefore, each of these coefficients can have an associated SAT expression of its own.
For the sake of natural accuracy performance, as in (Evans et al., 2021), it is advisable to 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 a final linear layer then a batch normalisation, we encoded the last layer for the label i as follow:
yi = |V |∑ k=1 wk,iVk + bi
and
yBNi = BatchNorm(yi) = γ · yi − E(yi)√ V ar[yi] + + β
yBNi = BatchNorm(yi) =
∑|V | k=1 γwk,iVk + γbi − E(yi)√
V ar[x] + + β
with = 1e− 5 and · denotes element-wise multiplication.
yBNi = |V |∑ k=1 w̃k,iVk + b̃i
with
w̃k,i = b γwk,i√
V ar[yi] + c
b̃i = γbi − E(yi)√ V ar[yi] + + β
To facilitate the SAT conversion, we also restrict the variance statistics and the scale parameter γ in BatchNorm() of the last layer to be scalars computed on the whole feature map rather than per-channel statistics. Before rounding, we multiply w̃k,i and b̃i by 100 in order to keep some details contained in the floating points.

heading: A.4 OPERATOR
text: We note as · the operator standing for the product term by term between two matrices. A mask (for example
M1 = [ N N 1 0 ] ) can be decomposed into two masks: M (0) and M (1). M (0) is 0 where M takes the value
Null, 1 everywhere else (ie as M (0)1 = [ 0 0 1 1 ] ). M (1) is 1 where M takes the value 1, 0 everywhere else
(ie as M (1)1 = [ 0 0 1 0 ] ).
Now let us note I the input matrices of the 2D-CNN and M̃ the matrix given by M̃ = I ·M (0). Then, we say that M matches I if and only if: ∀(i, j) M̃ [i, j] = M (1)[i, j].

heading: A.5 DETAILS OF TT-DCNN ENCODING

heading: A.5.1 FIRST LAYER
text: Published as in Narodytska et al. (2019b), we note xq the quantified pixel variable, and xb the bit variable after the first preprocessing layer, we have xb = sign(ασ (xq − µ) + γ) = sign(xinter)with α, σ, µ, γ 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: xmaxinter = α σ (xq + − µ) + γ) and xmininter = α σ (xq − − µ) + γ)
If xmininter ≥ 0 then we know that xb = 1. If xmaxinter < 0 then we know that xb = 0. Otherwise, xb ∈ {0, 1}, therefore it’s a literal for the SAT encoding. We can consider the reverse transformation. If xb = 0 (i.e. for xb = 1) is a solution of a problem produced by the SAT solver then we can map back to xattack = x− (i.e. for xattack = x+ ).

heading: A.5.2 LAST LAYER
text: Let V be the feature vector before the last linear layer, and U the set of indices of V that are unknown due to noise propagation and K those that are known. We have, for the class attack a higher than class target t:
|V |∑ k=1 wk,aVk > |V |∑ l=1 wl,tVl
We can divide the set [1 · · ·n] into U and K∑ k∈K wk,aVk + ∑ k∈U wk,aVk > ∑ l∈K wl,tVk + ∑ l∈U wl,tVl
We group together the set known and∑ k∈U (wk,t − wk,a)Vk < ∑ l∈K (wl,a − wl,t)Vl
We note c = ∑ l∈K(wl,a − wl,t)Vl, then c is a integer number. We have∑
k∈U
(wk,t − wk,a)Vk ≤ c− 1
We note G = GCD(abs(wk,t − wk,a)∀k ∈ U), then we have:
∑ k∈U (wk,t − wk,a) G Vk ≤ c− 1 G
As c−1G need to be an integer, we have:
∑ k∈U (wk,t − wk,a) G Vk ≤ b c− 1 G c
This inequality is encoded with the project (Ignatiev et al., 2018).

heading: A.6 EXPERIMENTAL DETAILS
text: 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 address3. Our work station is constituted of a 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 Jia & 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 a 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 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 α 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 α are between 0.6 to 3.0 with a step of 0.4. Note that α is a global parameter shared by all neurons. We do not use any data 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.
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× 2 + 0.01 for training on the MNIST dataset, and 0.064 ≈ 16.3/255 for CIFAR10, which are chosen to be slightly greater than twice the largest perturbation bound we consider for each dataset. Except for CIFAR10 for wich we double the trainig noise, the training noise level is equal to the testing noise level. The CBD loss is applied on MNIST high noise only and ν is set to be 5e− 4, 0 otherwise. We apply a weight decay of 1e− 7 on the binarized mask weight of BinMask. We use the encoding proposed in (Abío et al., 2011). In Table 1, we use model Big except for the high noise model with CIFAR10. For the post tunning parameters, we use a 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 a probability p = 0.01 for CIFAR10 low noise and we double it for high noise.

heading: A.7 COMPARISON WITH SAT METHOD FOR EXACT SAME ARCHITECTURE AND EXACT SAME TRAINING CONDITIONS
text: 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 CIFAR10 high noise as we trained it for a noise of 16/255. Results can be found in Table 4. We can observe that our model always outperforms the BNN model in term of verifiable accuracy.
3https://github.com/iclr2022anonymous/Truth-Table-Deep-Convolutional-Neural-Network

heading: A.8 MODEL COUNTING
text: Exact model counting. Given a CNF formula Φ, 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 a trained DNN. In this case, prec defines an -ball of valid perturbations and prop states that the classification should change under small perturbations. And the problem is given to a model counting solver (instead of a 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 inequality: by encoding such that the class i is greater than all others. Then, we start the MaxSAT solver on this formula: it gives us how many entries lead to an 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 5. 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.

heading: A.9 ABLATION STUDY

heading: A.9.1 NATURAL ACCURACY
text: 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 real-valued model. TT-DCNN has a final layer with
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 6. We observe that for MNIST and CIFAR10, TT-DCNN outperforms BNN and is inferior to the real-valued model. We also observe that as n increases, TT-DCNN tends to the real-valued model performances. We use n = 27 as it seems reasonable to compute 227 operations to get the SAT formula of a filter.

heading: A.9.2 STUDY ON INFLUENCE OF AMPLIFICATION LAYER
text: We tested three models: a model without amplification (one block is one layer), a model with minimal amplification (one block is two layers - with amplification factor 1) and a model with standard amplification (model presented in Appendix A.3.1). Results are presented in Table 8. We respect the training conditions proposed in Appendix A.6.
We can observe that the amplification layer is always profitable for the natural accuracy.

heading: A.9.3 OTHERS
text: For the study, we tested the first 1K 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 report the number of timeout as they are all 0. The results were computed on an other computer than those of Table 1. We took the measures for different:
• Size of the model. We use the two models presented above. • Dataset. We use MNIST and CIFAR10 • 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 an important impact on the verification accuracy and the time computation.We can observe that most of the time the filtering leads to a better verifiable accuracy and sometimes to a better natural accuracy.

Review summaries:
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. 

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).

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.   To 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 performance.