TRAINING FOR FASTER ADVERSARIAL ROBUSTNESS VERIFICATION VIA INDUCING RELU STABILITY
We explore the concept of co-design in the context of neural network verification. Specifically, we aim to train deep neural networks that not only are robust to adversarial perturbations but also whose robustness can be verified more easily. To this end, we identify two properties of network models -weight sparsity and socalled ReLU stability -that turn out to significantly impact the complexity of the corresponding verification task. We demonstrate that improving weight sparsity alone already enables us to turn computationally intractable verification problems into tractable ones. Then, improving ReLU stability leads to an additional 4-13x speedup in verification times. An important feature of our methodology is its "universality," in the sense that it can be used with a broad range of training procedures and verification approaches.
The paper presents several ways to regularize plain ReLU networks to optimize 3 things
- the adversarial robustness, defined as the fraction of examples for which adversarial perturbation exists
- the provable adversarial robustness, defined as the fraction of examples for which some method can show that there exists no adversarial example within a certain time budget
- the verification speed, i.e. the amount of time it takes some method to verify whether there is an adversarial example or not
 
Overall, the ideas are sound and the analysis is solid. My main concern is the comparison between the authors method and the 'certification' methods, both conceptually and regarding performance.
The authors note that their method falls under 'verification', whereas many competing methods fall under 'certification'. They point to two advantages of verification over certification: (1) the ability to provide true negatives, i.e. prove that an adversarial example exists when it does, and (2) certification requires that 'models must be trained and optimized for a specific certification method'. However, neither argument convinces me regarding the utility of the authors method. 
Regarding (2): The authors method also requires training the network in a specific way (with RS loss), and it is only compatible with verifiers that care about ReLU stability. 
Regarding (1): It is not clear that this would be helpful at all. Is it really that much better if method A has 80% proven robustness and 20% proven non-robustness versus method B that has 80% proven robustness and 20% unknown? One could make the case that method B is actually even better.
So overall, I think one has to compare the authors method and the certification methods head-to-head. And in table 3, where this is done, Dvijotham comes out on top 2 out of 2 times and Wong comes out on top 2 out of 4 times. That does not seem convincing. Also, what about the performance numbers form other papers discussed in section 2?
-------
Other issues:
At first glance, the fact that the paper only deals with (small) plain ReLU networks seems to be a huge downside. While I'm not familiar with the verification / certification literature, from reading the paper, I suspect that all the other verification / certification methods also only deal with that or highly similar architectures. However, I will defer to the other reviewers if this is not the case.
To expand upon my comment above, I think the paper should discuss true adversarial accuracy on top of provable adversarial robustness. Looking at table 1, for instance, for rows 2, 3 and 4, it seems that the verifier used much less than 120 seconds on average. Does that mean the verifier finished for all test examples? And wouldn't that mean that the verifier determined for each test example exactly whether an adversarial example existed or not? In that case, I would write "true adversarial accuracy" instead of "provable adversarial accuracy" as column header. If the verifiers did not finish, I would include in the paper for how many examples the result was "adverarial example exists" and for how many the result was "timeout". I would also include that information in table 3, and I would also include proving / certification times there. 
Based on the paper, I'm not quite sure whether the idea of training with L1 regularization and/or small weight pruning and/or ReLU pruning for the purpose of improving robustness / verifiability was an original idea of this paper. In either case, this should be made clear. Also, the paper seems to use networks with adversarial training, small weight pruning, L1 and ReLU pruning as its baseline in most cases (all figures except table 1). If some of these techniques are original contributions, this might not be an appropriate baseline to use, even if it is a strong baselines.
Why are most experiments presented outside of the "experiments" section? This seems to be bad presentation.
I would include all test set accuracy values instead of writing "its almost as high". Also, in table 3, it appears as if using RS loss DOES in fact reduce test error significantly, at least for CIFAR. Why is that?
While, again, I'm not familiar with the background work on verification / certification, it appears to me from reading this paper that all known verification algorithms perform terribly and are restricted to a narrow range of network architectures. If that is the case, one has to wonder whether that line of research should be encouraged to continue.
--------
Minor issues:
- "our focus will be on the most common architecture for state-of-the-art models: k-layer fully-connected feed-forward DNN classifiers" Citation needed. Otherwise, I would suggest removing this statement.
- "such models can be viewed as a function f(.,W)" - you also need to include the bias in the formula I think
- "convolutional layers can be represented as fully-connected layers". I think what you mean is "convolutional layers can be represented as matrix multiplication"
- could you make the difference between co-design and co-training more clear?
- The paper could include in the appendix a section outlining the verification method of Tjeng