Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 7: Good paper, accept
review_content: The authors demonstrate that using a modification of the LiRPA method during the branch-and-bound process for solving the neural network verification problem can lead to significant speed-ups. The experimental results are strong. The authors convincingly show that the their method outperforms the existing state-of-the-art method by Lu & Kumar (2020) on an experimental setup similar to that work. The application of LiRPA to branch-and-bound is straightforward (since any incomplete verifier can be used), as is the use of gradient descent to improve the bound given by LiRPA (a standard technique applied to improve the bounds of certain verifiers). 

Despite the fairly straightforward approach, the strength of the empirical results deserves attention. Overall, a solid contribution to the literature, and proof that research on incomplete verifiers leads to better complete verifiers. 

Some questions/requests:

- The experimental setup details should be provided in the final version. 

- How dependent is the performance of LiRPA on GPUs? For example, if we do a CPU-only comparison between the different methods, would other methods now outperform LiRPA? And if so by how much? What if we use multiple cores? I would understand if a detailed comparison is too computationally intensive, but I would like some sense of this.

---------------------------
Update after author response:
I thank the authors of the paper for significantly improving the prose of the paper, and I agree that the changes make the paper more self-contained and approachable. I have kept my ratings as my score was for primarily for the strong experiment results (and the score was also conditional on the paper being more polished). I am happy to support this paper for acceptance, but I am a little concerned about the degree of changes in the final version versus the initial submission, given the number of concerns the other reviewers had.
review_title: Strong experimental results, straightforward approach

final_score: rating: 5: Marginally below acceptance threshold
review_content: The work proposes a new algorithm that can be used for the complete verification of neural networks (NNs). Unfortunately, the authors do not define the verification problem they study: Based on the second paragraph of the introduction, one is given a neural network (NN) on the input, and the task is to determine whether the NN has a specific formally defined property - but which kind of properties are verified is never explained. Intuitively, one would expect verification to focus on determining whether the NN gives a "correct" output for certain inputs, but that does not really match the general description given in the paper, and I did not find a place where the verification problem is formalized further. Without knowing what "verification" means in the context of this paper, it's difficult to follow the reasoning provided in the paper without having some rough idea of what kind of properties one wishes to verify (for instance, the discussion about using LP bounds assumes that the property that is being verified can be expressed using LP). I believe this issue could have been avoided by formalizing the precise task of verification (the verification problem).

On that note, many parts of the paper seemed rather confusing and hard to follow, either due to inconsistencies or due to language issues. For instance, the sentence "Input domain split is shown effective in verifying the properties with low input dimensions while performs as poorly as incomplete verifiers on higher dimension properties" on page 2 seems to contradict the definitions given for complete and incomplete verification. How can a complete verifier perform "as poorly as incomplete verifiers" if, by the definition given in the paper, complete verifiers must always correctly determine whether the NN has the given "property" or not? (Section 2: "Complete verifiers guarantee to terminate either the property is proved or a violation is located.")

In terms of presentation, the submission contains an incredibly large number of minor language issues (roughly 1 per 2-3 lines on average, ranging from minor article issues to malformed sentences; see also the quote in the previous paragraph), and I strongly encourage authors to fix these as they have a rather disruptive effect when trying to read and understand the paper. A very small number of examples is provided below:
Page 1
-"cause the changes of NN predictions" -> "cause changes of NN predictions"
-"Recently, a framework of Branch and Bound (BaB) (Bunel et al., 2018) is widely used for efficiently verifying NNs" - cannot combine "recently" and "is".
-"adopts Linear Program (LP) bounding procedure" -> "adopts a Linear Program (LP) bounding procedure"
Page 2
-"for construct LPs" -> "for constructing LPs"

The main contribution of the paper is the use of incomplete verifiers for complete verification, and the authors propose an algorithm for doing that using LIRPA bounds. However, I found no proof (or anything resembling a proof) showing that the resulting algorithm is correct, i.e., that it performs complete verification for neural networks. In fact, the problem is not even properly and formally defined in the paper. Hence, regardless of the experimental results, I do not think that the submission is ready for publication at this stage.

Post-Rebuttal Comment:
I thank the authors for responding to my comments. The updated version fixes most of the criticisms raised in the review, and I have raised the score accordingly. My new score is "5", partly because I believe that after performing such a large-scale and comprehensive overhaul of the paper (which was certainly necessary), the paper should go through a full new reviewing process. 
review_title: No Proof of Completeness?

final_score: rating: 5: Marginally below acceptance threshold
review_content: ### Summary
This paper describes a branch-and-bound (BaB) process for neural network verification that uses linear relaxation based perturbation analysis (LiRPA). It gives a way to tighten the bounds obtained via LiRPA. Overall, this results is a complete verification procedure, which is an order of magnitude faster than existing linear programming (LP) procedures.

### Strengths
The biggest strength of the paper is the impressive experimental results in section 5: the method described in the paper is several times faster than previous methods.  

### Concerns 
My main concern is that the paper is very difficult to understand. It seems to require a lot of background knowledge about the problem and the related literature, which is not clearly provided in the paper. I had trouble understanding the problem, the setup, and the proposed algorithm. 

Another concern is that the paper claims that the proposed verifier is complete, but there is no proof of that. It does not seem like that's something too difficult to prove (given that BaB + LP is complete), but it should still be clearly stated. 

Finally, the claim that the proposed framework outperforms previous methods by "at least 10X and up to 50X" is unsupported. Based on the results in section 5, a fairer statement regarding the speed would be "at least 3X and up to 15X" faster.

### Reasons for score
It is very difficult to judge this contribution, as the paper is hard to understand. The two main reasons for the score I give are 1) some of the claims of the paper are unsupported (see above) and 2) I believe this paper will have a much better chance of conveying the idea and making a contribution, if more background knowledge and intuition is provided throughout.

### Suggestions for improvement that have not affected the score I gave to the paper

One way to significantly improve the paper is to introduce more examples. An example consisting of a simple neural network to refer to throughout the explanation of LiRPA and BaB, and also in section 4, would make the paper much easier to read. 

As a reader, I felt I couldn't appreciate the related work section so early in the paper. I encourage you to either move it later in the paper, or even better: introduce more background/examples in the introduction, as well as the notion of completeness, so that the related work is easier to understand.  

Some typos:
* Abstract: "we demonstrate over a magnitude speedup ..." -> "we demonstrate speedup of an order of magnitude ..." 
* First paragraph of section 2: "guarantee to terminate either ..." -> "guarantee to terminate when either ..."
* First paragraph of page 3: "used in state-of-the-art verifier (Lu & Kumar, 2020)" -> "used in the state-of-the-art verifier by Lu & Kumar (2020)".
* Second paragraph of page 3: "Our paper firstly leverage ..." -> "Our paper firstly leverages ..."
* First paragraph of section 3.1: "linear functions in the form of ..." -> "linear functions of the form ..."
* Start of section 4.1.: "As we have introduced ..." -> "As we discussed ..."
* Mid page 5: "greatly limited ..." -> "greatly limits ..."
* Bottom of page 5: "We follow the most challenge experimental setup ..." -> "We follow the most challenging experimental setup ..."
* Mid page 6: "we quickly reaches ..." -> "we quickly reach ..."
* Mid page 6: "with only two hidden node ..." -> "with only two hidden nodes ..."
* Section 4.3: "Benefited from our design ..." -> "Benefitting from our design ..."
* Conclusion: capitalisation of the first sentence

### Post rebuttal 

Thank you to the authors for their detailed response and their effort in improving the presentation of the paper. I was impressed with how much the paper improved in this second version. In particular, I very much appreciate that the introduction starts with a simple one sentence explanation of the problem of neural network verification. This can be further improved if it included (almost) no maths, which can be deferred to the Background section. The figures in the updated paper are very good and a huge improvement of presentation. Finally, the paper now includes two clearly stated theorems, which also make the presentation and contribution much clearer. 

I have increased the score I gave to the paper. Regardless of what the outcome for ICLR will be, I would like to encourage the authors to re-iterate on the presentation to really crystallize the problem, definitions and the suggested approach --- the paper is already so much better than the first version, and even just a little more work can make it even better. 


review_title: Difficult to understand

final_score: rating: 5: Marginally below acceptance threshold
review_content: The paper focuses on verifying simple properties of neural networks on
accelerator hardware.  Instead of using linear programming, Lirpa is
considered as an alternative and minimal amounts of LP is added around
to allow to use the same class of properties. In the considered
examples the approach becomes much faster than the LP approach.

My main problem with the paper, is that is claims a complete
verification procedure without proper proofs. Yes, the new algorithm
is presented and some general discussion of things that are done with
it and how they work is provided. However, to claim complete
verification a general soundness of the procedure should be proved. In
particular I would like a theorem for the correctness of each of the
various components and a combined theorem for the whole procedure.

On the other hand, the experiments show that the approach is fast and
as such makes it more feasible for verification and the paper mostly
reads well.

An interesting alternative to discuss in related work, could be proof
assistants. See for example the work of Bentkamp, Blanchette JAR 2019.
Using proof assistants based on more complex logics, one can verify
properties much more efficiently.  The authors only mention Katz's
work on SMT, but if you consider higher order logic and the logics of
interactive theorem provers, the "NP-hard properties" can be checked
without considering all the cases.

Minor:
Conclusion starts with lowercase "we".

Based on the problems found by the other reviews and having read the rebuttals I have modified my score.
review_title: Verifying simple neural network properties on a GPU

Meta-review: Thank you for your submission to ICLR.  As noted, several of the reviewers had fairly low confidence in evaluating this submission.  However, based upon the reviewers and commenters who were familiar with this line of work, as well as my own evaluation of the paper, I believe it is clearly worth publishing at ICLR.  The proposed method pushes the boundary in methods for exact branch and bound-based verification of neural networks, using clever tricks from existing relaxations.  And while the method is still likely to be relegated to relatively small networks for the time being, pushing forward the state of the art in exact verification is still a worthy goal suitable for publication at ICLR.  I thus think that the paper is quite clearly above the bar, and should be accepted for publication.
Decision: Accept (Poster)