EVALUATING ROBUSTNESS OF NEURAL NETWORKS WITH MIXED INTEGER PROGRAMMING
Neural networks trained only to optimize for training accuracy can often be fooled by adversarial examples -slightly perturbed inputs misclassified with high confidence. Verification of networks enables us to gauge their vulnerability to such adversarial examples. We formulate verification of piecewise-linear neural networks as a mixed integer program. On a representative task of finding minimum adversarial distortions, our verifier is two to three orders of magnitude quicker than the state-of-the-art. We achieve this computational speedup via tight formulations for non-linearities, as well as a novel presolve algorithm that makes full use of all information available. The computational speedup allows us to verify properties on convolutional and residual networks with over 100,000 ReLUs -several orders of magnitude more than networks previously verified by any complete verifier. In particular, we determine for the first time the exact adversarial accuracy of an MNIST classifier to perturbations with bounded l ∞ norm = 0.1: for this classifier, we find an adversarial example for 4.38% of samples, and a certificate of robustness to norm-bounded perturbations for the remainder. Across all robust training procedures and network architectures considered, and for both the MNIST and CIFAR-10 datasets, we are able to certify more samples than the state-of-the-art and find more adversarial examples than a strong first-order attack.
The authors perform a careful study of mixed integer linear programming approaches for verifying robustness of neural networks to adversarial perturbations. They propose three enhancements to MILP formulations of neural network verification: Asymmetric bounds, restricted domain and progressive bound tightening, which lead to significantly more scalable verification algorithms vis-a-vis prior work. They study the effectiveness of MILP solvers both in terms of verifying robustness (compared to other complete/incomplete verifiers) and generating adversarial attacks (compared to PGD attacks) and show that their approach compares favorable across a number of architectures on MNIST and CIFAR-10. They perform careful ablation studies to validate the importance of the 
Quality: The paper is very well written and organized. The problem is certainly of great interest to the deep learning community, given the difficulty of properly evaluating (and then improving) defenses against adversarial attacks. The experiments are done carefully with convincing ablation studies.
Clarity: The authors explain the relevant concepts carefully and all the experimental results are clearly written and explained.
Originality: The authors propose conceptually simple but practically significant enhancements to MILP formulations of neural network verification. However, the novelty wrt https://arxiv.org/pdf/1711.00455.pdf is not discussed carefully in my view (the  asymmetric bounds were already studied in this paper, as well as a novel branch and bound strategy). The progressive bound tightening is a novel idea as far as I can see - however, the ablation experiments show that this idea is not significant in terms of performance improvement. In terms of experiments, the authors indeed obtain strong results on verified adversarial error rates and generate attacks that PGD is unable to - however, again the results do not outperform latest results (in terms of the  best achievable upper bounds on verified error rates) available well before the ICLR deadline - https://arxiv.org/pdf/1805.12514.pdf . It would be great if the authors addressed these issues in a revised version of the paper.
Significance: The work does establish a strong algorithm for complete verification of neural networks along with several ideas that are critical to obtain strong performance with this approach. 
Question:
1. I am unclear on the "restricted domain" contribution claimed in the paper - is this just exploiting the fact that the inputs to the classifier are normalized to a given range, in addition to being no more than eps away from the nominal input? 
Cons
1. The authors do not compare their approach to that of https://arxiv.org/pdf/1711.00455.pdf , both in terms of conceptual novelty and in terms of experimental results. In particular, it is not clear to me whether the authors' approach remains superior on domains where tight bounds on the neural networks inputs are not available, like the problems studied in the ACAS system in the ReLuPlex paper.
2. The authors' MILP solution approach relies on having access to the state of the art commercial MILP solver Gurobi. While Gurobi is free for academic research use, for large scale neural network verification applications, this does restrict use of the approach (particularly due to limited licenses being available). It would be interesting to see a comparison that uses a freely available MILP solver (like scip.zib.de) to see how critical the approach's scalability depends on the quality of the MILP solver.
3. The authors do not outperform the latest SOA numbers in terms of verified adversarial error rates on MNIST and CIFAR classifers. It would be good to see a comparison on results from https://arxiv.org/pdf/1711.00455.pdf  (I believe the training code and trained networks are available online).