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