Venue: NeurIPS 2021 Conference

Reviews:

final_score: rating: 6: Marginally above the acceptance threshold
review_content: summary: The paper deals with efficiently incorporating CROWN into the branch-and-bound framework for complete verification. The authors propose to relax the split constraints using Lagrangian relaxation, and show how this can be done within the bound propagation framework. They also jointly optimise the intermediate bounds to tighter verification.

The technical contribution is fairly simple.

The method gives good improvements over existing complete verification methods. Authors have done a very good experimental evaluation, on different datasets and compared with many baselines.

The writing is good overall. Sections 2 and 3 are very well written. I have some comments which I have added in the main review.

The related work section and conclusion section need some work.

main_review: The paper proposes a new method for neural network verification (mainly complete verification), which gives state-of-the-art results on a wide range of datasets. The authors propose a technique to deal with neuron split constraints while using CROWN within branch-and-bound.  

The key idea is to use Lagrangian relaxation to relax the split constraints. This is done in a way such that linear bound propagation can still be used. The idea is fairly simple, and the method section is well written. The authors also jointly optimize the intermediate bounds. 

This technique is very useful for the verification community. CROWN has been a state-of-the-art incomplete verifier but has not had much success in complete verification. This technique allows the use of efficient CROWN style algorithms to speed up complete verification.

I have a few comments:
1. Introduction
- I don't see why the authors have not added the details about using Lagrangian relaxation to relax the split constraints in L46-48? It would help better understand what alpha and beta are in L48.

2. Section 3
- The layer constraints seem to be missing from Eq 2.
- L186-188 are good. This intuition can be brought forward to the introduction too. It takes 4 pages before anything about the actual method is brought. Giving detail about the Lagrangian function in the introduction would help better capture the interest of the reader.

3. Experimental Results
- In section 4.1, are all these methods run on the same machine (GPU and CPU)?
- The colours in Fig.1 are quite confusing. It takes many minutes to understand the figure, maybe remove some baselines to avoid confusion.

4. Related Work
- L334 discussion about [35] is factually incorrect. They do not relax a layer of neurons. They give a relaxation for composition of linear+ReLU. Please be careful when writing related work.
- L336 I don't think you are breaking the convex barrier since you are still using the planet relaxation. From your definition, all bab methods will break the barrier. I don't think that is the point that the convex barrier paper is trying to make.
- The main comparing baselines seem to be [9, 10 and 42]. So discuss these more thoroughly. The description about [9] is not clear.

6. Conclusion
- No future work is mentioned.
- No limitations mentioned.
- No broader impact discussed.
Please add these


====================================

***Updates after rebuttal***

I would like to thank the authors for answering the questions. I hope that the authors will indeed add the limitations in the main paper. My initial questions were sufficiently answered by the authors.
However, some points raised by other reviewers are valid. I also believe that the technical delta over alpha-crown is incremental.
The experimental results are good and I am still voting for acceptance.

limitations_and_societal_impact: The paper does not discuss limitations or societal impact. A potential negative societal impact is that since verification exposes potential flaws in networks, it can be misused too.
review_title: null

final_score: rating: 7: Good paper, accept
review_content: summary: The paper develops a bound propagation method for neural network verification.
Differently from related work, the method adds support for ReLU split constraints 
thereby offering a more efficient way (than linear programming) to bound a
verification problem under the constraints.

main_review: Bound propagation methods were shown particularly effective in both incomplete
and complete verification, where in the latter case they are commonly used to
derive strong MILP formulations of the verification problem in question.
However, in the case of customised BaB methods for neural network verification,
where the verification sub-problems resulting from branching on the ReLU nodes
need to be bounded, propagation methods cannot handle the ReLU constraints
introduced from branching. I believe that the paper makes a significant
contribution towards overcoming this shortcoming, thus contributing to improved
scalability in complete verification.  Indeed, the extensive experimental
results speak for themselves of the attractiveness of the approach.

The paper is very well written and easy to follow. Some typos that I found: 

Line 108: u \leq \upsilon \leq l -> l \leq \upsilon \leq u ?
Line 135: intersection -> union ?


limitations_and_societal_impact: The authors adequately addressed the limitations of their work. There is no discussion on potential negative societal impact of their work.
review_title: null

final_score: rating: 7: Good paper, accept
review_content: summary: The authors propose an augmentation to CROWN that leverages weak duality to enable neuron-split constraints. This approach is amenable to GPU acceleration and can theoretically attain (or even surpass) the bounds produced by the costlier LP based incomplete verification methods. 
main_review: Originality: 
At its heart, this approach is a small tweak to well-established techniques that introduces a new set of optimization variables (the beta variables) than can then be optimized in a similar fashion to the alpha's (i.e. in the Fast-and-complete paper). The notation is heavy, but the idea itself is quite simple. Similarly, the proofs are only minor modifications to existing results. The related work is clearly and fairly compared against, and it the exact contributions of this work are clearly delineated. 

Clarity:
The paper is clearly written and easy to follow (for CROWN-style papers, which are notoriously heavy in their notation). The lengthy derivations are conveniently pushed to the appendices and only the relevant details are kept in the main paper. In some of the experiments, it is not 

Quality: 
The experimentation section is very thorough and extremely convincing. The approach presented by the authors is the new state-of-the-art for both complete and incomplete neural network verification on a standard set of benchmark networks and properties. I have very little to complain about here: while the tweak to CROWN is fairly minor, the resulting method wins in both the verification% and time against the extensive set of benchmarks considered. Certainly it would be interesting to also consider cases outside of the VNN suite of metrics, such as i) ablating against a lack of GPU to demonstrate how much GPU acceleration helps here, ii) considering different domains outside of image classification or the standard benchmark models, iii) considering different threat models; but the lack of these results does not detract from the paper. From a theoretical standpoint, the comparisons to the dual form and arguments that Beta-CROWN can attain the same LP bounds with the same intermediate layer bounds (and improve when the intermediate layer bounds are adaptive), is a nice addition to the paper and increases the strength of this submission. 

Significance: 
The problem of verifying neural networks against adversarial inputs is very important, and this work extends SOTA in that domain. Bound propagation methods, or complete verification techniques, however, still do not show the promise of being able to provide meaningful guarantees against large SOTA image classifiers (such as Resnet50, etc). While this work certainly is better than existing works, I'm hesitant to highly praise a line of work that seems unlikely to ever be applicable to real-world networks, or even the standard threat-models for the small networks. Chipping away at faster and tighter bounds on small networks and small threat models seems like a great way to get papers published, but I require more convincing that this line of work has the potential to be applicable to the networks or threat models used in practice. 

Overall: 
This paper clearly explains an approach that modifies existing techniques to extend the state of the art for a problem that is important and receives significant attention within the community. I am dubious of this approach for long-term success or impact, but for the stated problem, this is the best solution we have right now and I'd like to see this paper accepted. 

Some typos: 
line 108 and 506: inequalities should be flipped to show $l <= v <= u$ 

limitations_and_societal_impact: The limitations of this approach were not addressed, nor were the societal impacts. For methods guaranteeing safety of neural networks, the societal impacts are mostly beneficial and can be read in many other papers. It would be nice to see the authors address the potential limitations of this work.
review_title: null

final_score: rating: 6: Marginally above the acceptance threshold
review_content: summary: The paper presents Beta-CROWN, a novel algorithm to compute bounds on the output of neural network activations.
Beta-CROWN is designed to be employed within recent branch-and-bound frameworks [6, 10], resulting in an effective complete (or incomplete, when returning early) verification algorithm.

The authors build on the bounding algorithm presented in [43] ("alpha-CROWN"), which (with fixed intermediate bounds) is an effective solver for the popular triangle LP relaxation (Planet [14]) of ReLU neural networks.
The main contributions of the paper are the following:
- differently from alpha-CROWN, beta-CROWN can represent the effect that a ReLU split at the i-th layer has on the activations preceding it, leading to tighter bounds within branch and bound;
- when jointly optimizing over intermediate bounds and output bounds, beta-CROWN shares fewer parameters between the various sub-problems, resulting in tighter final bounds.
main_review: **Strengths:**
Alpha-CROWN [43] has shown the potential of optimized propagation-based methods within branch and bound for neural network verification, resulting in very fast complete verification on easier verification properties.
Beta-CROWN successfully addresses the main weakness of alpha-CROWN (lack of split constraint support), enhancing performance on the harder properties and improving upon the considered baselines.

**Concerns:**
While the empirical results look good, I believe the presentation of the paper is rather confusing. Beta-CROWN is an incremental improvement over alpha-CROWN, the main difference being the addition of split constraints in the formulation (see equation (32) for a dual perspective).
While this is not a problem per se, the connection seems to be systematically understated in the paper: for instance, alpha-CROWN should be properly described in section 2, whereas the presentation in section 3 rarely mentions alpha-CROWN [43] and does not cite it when introducing the optimization over the alpha variables (lines 197-200). As made clearer in the Appendix, the results in section 3.2 follow from results in alpha-CROWN with only minor modifications to include split constraints (yet this discussion is absent in the main paper).
Furthermore, from a quick reading, it would appear like beta-CROWN is the first GPU-accelerated dual bounding algorithm (excluding LP solvers) that can incorporate split-constraints (lines 136,137,149), however they were naturally incorporated by some previous methods such as [5, 9, 12] (as mentioned by the authors in Appendix B.2).

I feel like ablation studies are missing: the importance of the joint optimization of intermediate bounds is often stressed. However, how much improvement is due to the split constraints, and how much to the joint optimization? What would be the performance if tight intermediate bounds were computed only once, before any branching? In addition, it would be great if the authors could investigate the performance of the algorithm if the alpha variables from alpha-CROWN are not optimized over.  

The authors could perhaps tone down the claims on the relative performance of Beta-CROWN to other GPU-based verifiers (lines 59-60). For instance, Beta-CROWN on average does not appear to be "2 to 7" times faster than [10] (and [9]) on the Wide and Deep networks of Table 1. Moreover, the relative improvement over [10] further decreases when part of its contributions (the FSB branching strategy) are not integrated within Beta-CROWN.

Finally, the incomplete verification results (verified accuracy) in the main paper should include more branch-and-bound-based incomplete verifiers such as alpha-CROWN [43] (and the experiments on [9] presented in the Appendix), which may be stronger baselines than the ones considered.
limitations_and_societal_impact: I could not find any detailed description of the limitations of the paper. While most of the limitations are shared with many works in the area of neural network verification, the authors could point out to the fact that proposed method only deals with ReLU activations, or state the assumptions on the input-output specifications of the networks to be verified (for instance, convexity of the input set).
review_title: null

Meta-review: The paper was well-received. The main idea is fairly simple, but the problem is important and the writing and empirical evaluation are solid. Based on the reviewers' advice, I am recommending acceptance. Please make sure to add to the final version the new results and the text on limitations and societal impact that you described in your author response. 
Decision: Accept (Poster)