Venue: ICLR 2022 Conference

Reviews:

final_score: rating: 3: reject, not good enough
review_content: summary_of_the_paper: The paper proposes a new machine learning model TT-DCNN as an
alternative to Binarized Neural Networks (BNNs). The paper claims that
the new machine learning model simplifies and improves
interpretability of the SAT encodings.

main_review: In my opinion, the paper's premises are not correct. As far as I can
understand, BNNs were developed to target issues like power
consumption and ease of circuit-level integration, and not the
difficulties with propositional encodings or the sizes of such
encodings, or even issues interpretability, of the models or their
encodings.

Furthermore, I cannot understand why interpretability of a SAT
encoding is a concern. The SAT encoding is simply a representation
that is used to reason about the original machine learning model.
SAT encodings are important because they enable efficient reasoning in
some settings, but not because of issues with interpretability.
Furthermore, any information resulting from reasoning about the
original machine learning model on such a representation can be
related with the original model.

To obtain a SAT encoding the paper makes several critical decisions.
One is to consider features to take boolean values. Another one is to
assume a very restricted representation, one where at most nine
features can be considered. From what I can understand, raising
significantly the number of features used in the representation would
make the encoding impossibly large.

In my opinion the paper is not well written. For example, 2D-CNNs are
briefly described in a paragraph containing no references. The
explanation is not easy to follow. This applies to section 2, but also
to section 3. For example, I was unable to understand how one goes
from equation (1) to an intermediate equation claiming that one can
generate both CNF and DNF representations. I was unable to make sense
of the subsequent example, and I have some experience with logical
encodings.

Also, the integration of different blocks is unclear. I can understand
how this might be done in the case of an intermediate CNF
representation. However, I was unable to understand how this might be
done for a DNF intermediate representation. If this was easy to do,
then satisfiability for CNNs should be easy to decide, and that cannot
be the case. I could be missing something here, but the writeup does
not help. 

summary_of_the_review: The paper proposes to learn a new machine learning model, one that
simplifies the propositional encoding, and subsequent reasoning with a
SAT solver. The work could be of importance, but the current writeup
does not help to convey the key ideas. In its present form, I cannot
recommend acceptance of this paper.
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: 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. 
main_review: Strengths: 
- the idea of using a truth table to distill (or approximate) real-valued feature vector is novel and very interesting
- TT-DCNN provides certain interpretability and supports manual post-processing
- the robustness of TT-DCNN can be verified using SAT solvers

Weaknesses and actionable feedback:
- 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. 
- 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. 
- 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. 
- TT-DCNN seems to be a new architecture, and some discussion regarding training would be necessary.

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.
review_title: null

final_score: rating: 3: reject, not good enough
review_content: 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).
main_review: **Strength**
This work has proposed a method to improve the scalability of SAT solvers to deep networks to aid robustness verification. 

**Weakness**
* 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.
* 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*. 
* 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. 

**citations**

[1] Subham Sekhar Sahoo, Subhashini Venugopalan, Li Li, Rishabh Singh, and Patrick Riley. Scaling Symbolic Methods
using Gradients for Neural Model Explanation. International Conference on Learning Representations, 2021.
https://arxiv.org/abs/2006.16322
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.

**citations**

[1] Subham Sekhar Sahoo, Subhashini Venugopalan, Li Li, Rishabh Singh, and Patrick Riley. Scaling Symbolic Methods
using Gradients for Neural Model Explanation. International Conference on Learning Representations, 2021.
https://arxiv.org/abs/2006.16322
review_title: null

final_score: rating: 5: marginally below the acceptance threshold
review_content: 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.  
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.
main_review: Explainability and formal verification of deep neural networks are vibrant research venues.
Instead 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.

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

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

Minors:
The definition of patch function is unclear to me.
"We have P (1) = k and P (s + 1) = P (s) if and only if the kernel size of the layer is 1."
What if the kernel size isn't 1?

"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)."
I would then avoid mentioning these concepts.

"To the best of our knowledge, this is the first time that the exact knowledge of a real-valued DCNN is formally extracted."
Isn't this true for BNNs compiled to propositional formulas too?

summary_of_the_review: - The paper addresses a very relevant problem in AI
- Developing deep architectures that are verifiable and interpretable by construction is a sensible idea in my opinion
- The presentation of the proposed architecture could be improved by adding figures and more examples
- Adding some definitions would benefit a large audience of non-experts in verification
- The trade-off between interpretability and predictive performance is not well characterized
- The claim that the model is more interpretable should be substantiated with experiments comparing TT-DCNs with other XAI methods
review_title: null

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