Venue: ICLR 2020 Conference

Reviews:

final_score: rating: 6: Weak Accept
review_content: This paper proposed to use a convex QP relaxed formulation to solve the neural network verification problem, and demonstrated its effectiveness on a few small networks (1-2 hidden layers) on MNIST and Fashion-MNIST datasets.

There are several benefits the proposed methods: they are technically tighter relaxations of ReLU neurons and empirically the authors show they perform well in L2 norm (but not L infinity norm, unfortunately); solving this formulation does not require to know pre-activation bounds of hidden neurons; also the convexity of the QP problem needs to be determined only once for a model, rather than once per example. Although the QP relaxation of ReLU neuron is not new and has been used in Raghunathan et al., 2018b, they solve the problem as a SDP rather than convex QP. SDP is tighter than the convex QP formulation used in this paper, however is much slower.

Issues and Questions:

1. The concept of "bi-direction verification" is not new, since finding an upper bound is basically finding adversarial examples. Many previous papers have been using PGD based attacks to obtain the upper bound. Convex relaxation based verification methods like CROWN can also be used for generating adversarial examples, and it is called "Interval attack", which is demonstrated in [1][2]. Claiming this is the first "bi-direction robustness verification technique" is not accurate.

2. The use of FGSM as an upper bound is inappropriate, as FGSM is known to be a very weak attack. Replacing it with a multi-step PGD attack is necessary. Using a stronger attack will also close the gap between upper and lower bound. Also, compare the upper bound found by PGD with QPRel-LB and update Figure 3(a). If a stronger attack like PGD is used, I think for larger norms CROWN+PGD in Figure 3(c) should be able to verify almost all examples.

3. The models used in Table 1 is trained using a L2 perturbation of epsilon=0.1. This epsilon value is too small for L2 norm. In page 22 (last page of appendix in arxiv version) of [3], you can find the they conduct L2 robustness training but at a much larger epsilon value (eps=1.58). Sine the authors did not use these standard epsilon setting, my concern is that does the proposed method works at larger L2 epsilon?

4. Some experiments on larger and deeper networks are necessary; especially, it is interesting to see how CROWN and the proposed method scale to deeper networks. The presented experiments only include networks with 1 and 2 hidden layers, which is insufficient. A new experiment with number of hidden neurons per layer kept (say 50) and increase the depth from 2 to 10 will be very helpful.

5. The main claim of the paper in Introduction needs to be made clearer, especially the primary strength of the proposed algorithm is in L2 norm, and it does not seem to outperform CROWN in L infinity norm setting.

Further improvements and potential directions:

1. In the proposed method, the authors relaxed ReLU neurons using quadratic programming. This relaxation does not require to computing bounds for the neuron activation values. However, I think it is possible to include neuron activation upper and lower bounds as constraints of the QP problem (adding them as constraints like l <= x <= u in Eq. QPRel). This will make the bounds tighter. The per-neuron lower and upper bounds can be obtained using CROWN efficiently, so there is no too much computation cost.

2. Improving the scalability of QP relaxation is another challenge. CROWN can be implemented efficiently on GPUs [4]. For QP relaxations, this can possibly be done by transforming QP solving into a computation graph that can be executed efficiently on GPUs (this is a potential future work directions and I do not expect the authors to address them during the discussion period).

Overall I am positive with this paper, however before accepting it I think the authors should at least make their claims clearer (the relaxation performs well mainly in L2 norm, and the concept of "bi-directional verification" is also not entirely new), replacing FGSM by a 200-step PGD and compare the upper bound found by PGD with QPRel, and test the proposed algorithm in models trained with a larger epsilon (eps=1.58 to align with previous works, if possible) and deeper models.

[1] Wang, S., Chen, Y., Abdou, A., & Jana, S. (2019). Enhancing Gradient-based Attacks with Symbolic Intervals. arXiv preprint arXiv:1906.02282.
[2] Wang, S., Chen, Y., Abdou, A., & Jana, S. (1811). MixTrain: Scalable Training of Verifiably Robust Neural Networks.
[3] Wong, E., Schmidt, F., Metzen, J. H., & Kolter, J. Z. (2018). Scaling provable adversarial defenses. In Advances in Neural Information Processing Systems (pp. 8400-8409).
[4] https://github.com/huanzhang12/RecurJac-and-CROWN

review_title: Official Blind Review #1

final_score: rating: 8: Accept
review_content: This paper proposes a method to compute the distance to the decision boundary for a given network, where the network is composed of linear layers followed by a RELU activation. The authors provide a lower bound and an upper bound for the distance of a sample from the decision boundary. The lower bound is obtained as the solution to a quadratic program, which in turn is obtained by relaxing the original optimization problem. The relaxation is obtained by decomposing the RELU condition to a set of 3 constraints (eqn 2). The authors also provide conditions under which the quadratic program stays convex.

The paper is clearly written. The method is useful to verify robustness of neural networks. The experiments show the improvement of the proposed method over existing certificates.

While the lower bound is theoretically justified, I did not see any guarantees for the upper bound. I am not referring to a convergence proof here, but simply a guarantee that the value returned by Algorithm 1 is indeed an upper bound. Algorithm 1 does not verify whether the point returned belongs to a different class. It would also be helpful to provide intuition for the iterative procedure to compute the upper bound.

Minor comments:
1) Line 9 is Algorithm 1: x^qp0 should be x^qp (no 0)
2) What is L/N in Table 1? 
review_title: Official Blind Review #3

final_score: rating: 3: Weak Reject
review_content: * Summary:
This paper introduces an encoding of the bounds on Neural Networks based on a (non-convex) quadratic program. The method covers both L_inf and L_2 perturbations, and the optimization problem posed are solved using Gurobi.

The authors formulate the ReLU as a quadratic constraint , and then relax the problem by taking it's Lagrangian dual. This results in the standard properties from taking a lagrangian dual: any choice of dual variables will produce a lower bound.
For an appropriate choice of dual variables, the lagrangian problem is convex and the authors give a way of choosing dual variables that guarantees this convexity such that the bound can be computed.

A method is proposed to find upper bound on the verified region (which can also be understood as just finding an incorrectly classified sample, that should ideally be the closest to the original point), based on iterating the solving of the QP.

Comments:
- Encoding of the ReLU as a quadratic constraint as done in (2) is not novel, as it was done before by Dvijotham et al. (UAI 2019) or Raghunathan et al. (NeurIPS 2018). The Lagrangian relaxation that is then done is to the best of my knowledge different than any one introduced before. 

- The problem solved is also different to most of the literature: rather than verifying robustness for a certain radius, this attempts to find the maximum radius being robust, which provide more information.

- I'm confused at the upper bound finding method. The solution of the QP will not necessarily respect the constraints of forward propagation of the network so if you just consider the variables corresponding to the input, the resulting output may not necessarily a violation. Also, I don't understand the motivation for why repeatedly solving the QP will lead to a good violation on the decision boundary. I know that the paper says that "analytic investigation of this algorithm including a convergence proof remains future work." but at the moment there is not even an intuition for why it might be a good idea. By the second iteration, there is no notion of the reference point around which safety is computed so it's not sure how the closest violation would be found.

- The network tested are extremely small, even by formal verification of neural network standards, which makes it hard to appreciate the impact of the method and makes me question the applicability of the method. Is it because QP are more complex to solve than LPs?
- It is also a little bit problematic to give results as ratio of improvements over the lower bound on radius, when most of the network used are non robust, given that those networks have extremely low verified radius, so the relative difference will look inflated. 

- The reporting of the verification ratio as a function of the perturbation radius is an interesting measure that I think is very benificial to making the point but I think it should be better explained as it took me a long time to get the point. The experiment section in general is quite confuse and hard to parse, having to jump around quite a lot to get what the author meant.

- FGSM is a very very weak baseline for the use that is employed here. By construction, it doesn't look for the smallest violation, is not iterative, and produce perturbations at the limit of the attacked budget.

- The paper takes the opportunity to say that their method is 2000x faster than SDP based method but not that they are 10x to 100x slower than CROWN (outside from the appendix). It's better to report results clearly than only trying to show the good points of the algorithm. The bounds obtained are tighter than those resulting from Crown so it might be a worthwile tradeoff to make.

* Probably worth discussing / comparing to:
Provable Certificates for Adversarial Examples: Fitting a Ball in the Union of Polytopes, Jordan et al. (ICML 2019)

* Typos and minor comments:
- Adjust the label for Figure 2
- "Guarantied" on page 4
- top of page 8 "VerRation"



review_title: Official Blind Review #2

Meta-review: This article is concerned with sensitivity to adversarial perturbations. It studies the computation of the distance to the decision boundary from a given sample in order to obtain robustness certificates, and presents an iterative procedure to this end. This is a very relevant line of investigation. The reviewers found that the approach is different from previous ones (even if related quadratic constraints had been formulated in previous works). However, they expressed concerns with the presentation, missing details or intuition for the upper bounds, and the small size of the networks that are tested. The reviewers also mentioned that the paper could be clearer about the strengths and weaknesses of the proposed algorithm. The responses clarified a number of points from the initial reviews. However, some reviewers found that important aspects were still not addressed satisfactorily, specifically in relation to the justification of the approach to obtain upper bounds (although they acknowledge that the strategy seems at least empirically validated), and reiterated concerns about the scalability of the approach. Overall, this article ranks good, but not good enough. 

Decision: Reject