Venue: ICLR 2022 Conference

Reviews:

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: The paper introduces a complete verification procedure that 1) encodes PRIMA constraints as a Lagrangian function, which admits GPU-based algorithm; 2) uses the values of the Lagrange parameter to guide the branching (ACS); and 3) regularizes the branching score with the estimated cost for a split.
main_review: In general I like the directions that this paper is taking to push the state-of-the-art of neural network verification. The contributions are novel to my knowledge. The encoding of the verification problem using Lagrange multipliers looks sound. The two ideas on branching heuristics are also interesting. After reading the previous sections, I expect the experimental evaluation to demonstrate two points: 
1) the GPU-based dual algorithm is better than an (almost equivalent) MILP-encoding;
2) ACS and CAB are competitive with SOTA branching heuristics. 

The experiment on ResNets suggest does seem to show that CAB is beneficial for both BABSR and ACS.  However, I'm not fully convinced of the efficacy of the rest of the proposed techniques. My concerns and questions are listed below:
1. In Table 1, why does MB-BAB use different branching heuristics for different networks? Maybe show the numbers of BABSR+CAB and ACS+CAB in two different columns? 
2. Table 1 suggests that ERAN (PRIMA + MILP-encoding) solves the most instances overall, while being slower on only 1 network. To draw the conclusion that Gurobi (with 16 cpus) is less scalable than a GPU-based procedure on the verification problem (which is the motivation of the proposed encoding of the verification problem), more experiments are needed than a single perturbation bound and a single network.
3. In Table 2, why is "DeepPoly only" instead of "PRIMA only" (or kReLU only) used as a filter for easy verification problem.
4. What are the number of ReLUs in the ResNet architecture and in the ConvBig/Small networks? I saw the concrete architectures in the Appendix but since the motivation for excluding ERAN from Table 2 is the claim that MILP-encoding is less scalable than the GPU-based approach on larger models, the architecture information (or at least the number of ReLUs) seems to be relevant enough to be put in the main paper.
5. There are more recent branching heuristics than BABSR as mentioned in the related work. It would strengthen the paper to use one of those (e.g., FSB) as the baseline.

Overall, while I find the proposed techniques promising, a more thorough evaluation is needed to show their benefits.

Minor comments:
- Typo: page 5: Enforcing split constraitns
- Figures 5, 6 are compressed in a way that favors the proposed techniques. Maybe present it with the same width and height?
summary_of_the_review: Promising verification procedure, but a more thorough evaluation is needed.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: This paper presents a branch-and-bound algorithm for neural network verification that uses a dualized variant of an existing approach for generating multi-neuron relaxations. Computational results are presented showcasing the quality of the verification bounds, and the scalability of the method.
main_review: The paper is clearly written, with a clean, linear presentation of the method and its derivation. The "novelty" of the work is somewhat incremental, but the new methods show their efficacy, and the paper is a worthy contribution to the literature.

* I wish that the authors spent more time describing the work of Muller et al that they build on for the multi-neuron constraint generation. Consider adding a brief discussion.
* p2: To what extent is your framework "applicable" to network with Sigmoid and Tanh activations? If it involves approximating the nonlinear activations, is it still sound and exact?
* p2: I think you need to add a "sound" to "A method is called complete if..."?
* p3: "we derive linear upper and lower bounds of the form z^i >= Az^(i-1) + c for each...". This seems like it's only lower bounds?
* p6: Is "noisy proxies" the right choice of words?
* p8: Is there a fundamental reason beta-Crown and Oval don't support ResNet, or is it simply a matter of implementation? What about ERAN?
* The authors mention a "GPU-based dual optimizer" in the abstract and introduction, but there is no explicit mention of GPU compatibility of the method in the body of the paper. Can the authors clarify?
summary_of_the_review: The paper presents its new idea cleanly, and the improvements appear substantial enough for publication.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: The paper puts forward a method for the formal verification of ReLU-based
neural networks. The method incorporates  previously developed multi-neuron
relaxation and split constraints in a bound propagation algorithm which is used
in a branch-and-bound procedure. Experimental results are reported that compare
the procedure with related methods on a number of  MNIST and CIFAR10 models.
Ablation studies are also carried out on ResNet6-A and ResNet6-B.
main_review: The method proposed  comprises (i) the integration of  multi-neuron relaxation
constraints  into a  bound propagation algorithm; (ii) the integration of ReLU
split constraints in said algorithm; (iii) the active constraint score and
cost-adjusted branching heuristics. Part (i) was previously developed and used
in a bound propagation-based tool (Eran). Part (ii) was previously developed
and used in a similar framework to the one in present paper (Wang et al.,
2021).  Therefore the novel contribution of the paper are the branching
heuristics.  These are however straightforward thereby (in my view) not
meriting an ICLR publication from a technical point of view.

Concerning the empirical evaluation, the paper carries out extensive ablation
studies whereby the effectiveness of the different constrains and heuristics
used is shown. It is definitely nice to see that these work in the context of
branch-and-bound. The comparison with related work is in my view weak however.
First, out of the four networks used, the present method marginally wins only
in two them in terms of average runtime and marginally wins only in one of them
in terms of verified accuracy. Whilst the authors claim that the efficacy of
their method is better observed in bigger networks, they do not include
comparisons with related tools on bigger networks. I think that the inclusion
of these in future revisions of the paper would significantly strengthen the
evaluation section.

Overall the paper is very well written; it was a joy to read. Some minor
comments:

- I did not find clear how the number of floating-point operations in the
  computation of the bounds is calculated in the cost-adjusted branching
  heuristic. In particular, how does this vary with different splits?

- Page 2. greater 0 -> greater than 0.
kkk
summary_of_the_review: Whilst the paper introduces some novel branching heuristics for the complete
verification of ReLU neural networks via branch-and-bound, the overall
contribution lacks in my opinion the sufficient novelty to merit an ICLR
publication. I think that  the authors should include additional empirical
comparisons with related tools on bigger networks and consider submitting a
tool paper in a top venue.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: The paper presents a novel framework for neural network verification by combining two popular paradigms in literature: tight multi-neuron relaxations [1][2] and branch-and-bound [3][4][5]. The benefit of such a framework is combing the best of both paradigms by improving the bounding method (multi-neuron relaxations) in a Branch-and-Bound framework resulting in scalability and completeness. Additionally, the authors also present a branching heuristic that can leverage their multi-neuron setup and propose a computation cost-adjusted branching to obtain decreased runtimes. They validate their hypothesis by comparing it to state-of-the-art verification tools and verifying established convolution network benchmarks for MNIST & CIFAR-10. They also present ablation studies for various features on two larger ResNet architectures showing how each system component contributes to improved results. 

main_review: Strengths:

- Previously multi-neuron relaxations have shown to be instrumental in going beyond smaller networks [1][2]. Combining this in branch-and-bound framework is a novel idea that could potentially lead to interesting future work.
- Branching decisions are important in a BaB setting [5], the authors present interesting proposals (ACS + CAB) for both effective and efficient branching. Previous branching heuristics make branching decisions on expected bound improvements. Since MN-BaB operates on multi-neuron relaxations, branching heuristic ACS is presented that factors the improvements by multi-neuron relaxations into consideration.  CAB (cost-adjusted branching) postulates that runtime is a key factor in branching decisions for complete verifiers, hence proposing to do the branching decision as a function of expected bound improvement per cost instead of just expected bound improvement.
- The ablation studies show each system component is beneficial (Figure 3, 4, 5) and contributes to the overall improvements (Figure 6).

Weakness
- Experimental evaluation of the framework seems non-exhaustive and missing comparisons to important baselines (see more details below), making it hard to place MN-BaB (this paper) alongside the literature. 

Reg. experimental evaluation:

Table 1: The authors claim that three out of the four networks are well-solved by previous methods and are less relevant, while for the fourth one, they perform the best. I have a few reservations:

- For the first three rows, it seems like MN-BaB isn’t the most effective and efficient method and for the fourth row the margin seems too small to claim “outperformance” -- hence more evaluation or analysis might be needed to better understand the behaviour. 
- A possible remedy to this: Seems like there’s some promise in larger networks. Previous works have also considered ConvSuper [6], networks larger than ConvBig. Did the authors try to evaluate these benchmarks? What were the results?
- Another remedy for better understanding: Previous works [1][2][6][7][10][11][12] have all considered a larger set of benchmarks including more kinds of conv networks + FFNNs. I already mentioned conv networks above but the method presented seems to work for feed-forward networks (FFNNs) too but no evaluation is presented. Maybe because of space constraints and/or the argument that ERAN can already do very well. But it would be a good idea to have the results in the paper (or appendix) for a more holistic picture. While Beta-CROWN might not work for MLPs but comparisons to other baselines (including other variants of CROWN) would be useful.  
- Reg. branching for MN-BaB: It’s unclear why three out of the four rows use BaBSR branching and the last one uses ACS. Was only the best performing branching heuristic reported? Since ACS is stated as one of the main contributions of the paper too, it would be good to see a breakdown of ACS vs. BaBSR for at least all these four benchmarks otherwise the MN-BaB results are not generated from a consistent set of options.
- Fixes needed (at minimum, the difficulty of fix in brackets):
            * ACS+CAB reporting for all benchmarks. (easy fix)
            * One larger conv network eval to claim “outperformance”. (medium fix)
- Fixes needed (ideally)
            * A couple of FFNNs evaluation for comparison with ERAN/OVAL. (larger change, can reuse numbers from PRIMA paper) 


Table 2: The authors claim that their methods work on more challenging less regularized networks. This section is important and interesting and highlights how each component of the system contributes to the final results. My primary concern is that this experiment is in isolation and not placed well with the rest of the related works:
- For ResNet-6-A and ResNet-6-B: Was ERAN run since it can handle ResNets? What were the results? I agree OVAL does not support residual architectures. But other variants of CROWN that do support ResNet architectures and have a public implementation of the same [7][8][9], could have been evaluated (with alpha-beta-CROWN being the current best option). 
- I raise this issue because the paper seems to claim “26% more samples while being around 30% faster” in multiple places but this seems to be on only one network (ResNet-6-A) against only one (weak) baseline for current SOTA (BaBSR). Comparing multiple benchmarks to a few relevant tools (at least one) would be a rigorous way to compute the performance improvements esp. since Table 1 is not shedding a lot of light.
- Fixes needed (at minimum, the difficulty of fix in brackets):
           * Report ERAN and a CROWN-variant (alpha-beta-CROWN is open-source, all options here [7][8][9]) in the table (medium change).
           * Fix the improvement claims to be relative to SOTA (best tool), averaged over all networks instead of just one. (easy change)

A suggestion regarding clarity: Section 2.3 briefly mentions two cases of unstable & stable ReLUs and different convex relaxations. This could be elaborated on some more, particularly on how it is incorporated and affects future decision choices. 

Minor comments: Page 5: Enforcing split constraitns → Enforcing split constraints

Finally out of personal curiosity, it seems like the Beta-CROWN results in Table 1. were directly pulled from the paper [10]. Could the authors point me to the table/graph they referred to? Asking as I couldn’t find it myself. 


- [1] PRIMA: Precise and General Neural Network Certification via Multi-Neuron Convex Relaxations. Müller et. al.
- [2] Beyond the Single Neuron Convex Barrier for Neural Network Certification. Singh et. al.
- [3] Branch and Bound for Piecewise Linear Neural Network Verification. Bunel et. al. 
- [4] Scaling the Conve Barrier with Active Sets. De Palma et. al. 
- [5] Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition. De Palma et.al.
- [6] An Abstract Domain for Certifying Neural Networks. Singh et.al. 
- [7] alpha-beta-CROWN: https://github.com/huanzhang12/alpha-beta-CROWN 
- [8] auto_LiRPA: https://github.com/KaidiXu/auto_LiRPA 
- [9] CROWN-IBP: https://github.com/huanzhang12/CROWN-IBP
- [10] Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification. Wang et.al.
- [11] Automatic perturbation analysis for scalable certified robustness and beyond. Xu et.al.
- [12] Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. Xu et.al.

summary_of_the_review: In conclusion, I feel the paper presents an interesting idea but needs a more thorough evaluation and comparisons to related works to justify the claims made. Hence,  the current submission is marginally below the acceptance threshold for ICLR.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: This paper deals with complete verification of neural network, based on a branch and bound framework.

It is essentially a combination of two recent papers:
- Beta-crown[1], which optimizes with first order methods the bounds obtained by LIRPA type bounds. Additional constraints on the network activations (such as the ones resulting from branching) are included through lagrange multipliers and optimized over.
- Prima[2], which derives linear constraints to impose on the activation of the network to obtain tighter relaxations. These constraints comes from the fact that you can obtain a tighter convex hull by relaxing a group of neurons together, rather than relaxing each neuron independently. In the Prima paper, the constraints are simply encoded into an off-the-shelf LP solver.

The main contribution of this paper comes from adding the linear constraints that comes from the Prima relaxation (using Lagrange multiplier) to the problem optimized by Beta-crown.

In addition to that, the paper also propose new branching heuristics:
- Active Constraint Score Branching, which uses the lagrangian variables associated with the constraints of the multi-neuron relaxation to prioritize branching.
- Cost Adjusted Branching, which aim to correct the score of the branching heuristic based on the expected computational cost induced by each possible branching choice.

Experiments are ran on MNIST and CIFAR10

[1] Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Verification
[2] PRIMA: Precise and General Neural Network Certification via Multi-Neuron Convex Relaxations
main_review: # Strengths of the paper:
The paper is easy to follow, and provide clear attributions of the ideas it is based on, citing the relevant works. The approach suggested makes sense and the authors have indicated that they will release the code to reproduce their results.
The empirical results that are included are useful to assess how much methods like beta crown can be extended to tighter relaxations.

# Clarification needed
## Q1: Clarification about Cost Adjusted Branching
The description of CAB is that it "scales the expected bound improvement with the inverse of the cost expected for the split".
There is no description about how "the expected bound improvement" is computed. If this the score given by a method like "Active Constraint Score Branching" or BABSR, I think it's inaccurate to call it like this.
There should be a clarification as to why different branching decisions have "considerable differences in computational cost". Is it simply because branching a "late" layer requires to recompute less intermediate bounds? This is unclear because nowhere is described what exactly you compute at each level (you could decide to tighten intermediate bounds based on the new branching constraints, even if they appear before the branching constraint)

## Q2: Experimental evaluation not supporting the claim
The last contribution listed is that the authors "improve on the state-of-the-art in terms of certified accuracy by as much as 26% while being 30% faster". This numbers come from the experiments that are listed in Table 2, but this is only a comparison to different ablated version of the authors method. I understand that beta-crown would be equivalent to (BaBSR, no MNC) but this is still missing a comparison to other methods that use tighter relaxation than single neuron relaxation. Even if beta-crown and OVAL do not support residual connections, why not train a larger CNN if the issues of the models of table 1 is that the network are too easy?
Similarly, the only baseline used for Branching method proposed is BaBSR, while something like Filtered Smart Branching (FSB) could have been tested (the authors mention that method in their related works)

When compared against strong baselines (Table 1), the improvements of the method proposed are significantly lower.

In addition, is there a reason why for Table 1, the branching is BaBSR+CAB for all but one of the networks, rather than ACS + CAB, given than ACS is one of the paper's contribution?

There is also the additional problems of comparing different branch and bound verifiers on only two numbers. With branch and bound verifiers, It is always possible to obtain higher verified accuracy if you are willing to trade off time (just do more branching steps). Comparing two methods based on only the verified accuracy and the time it took means that there is only a partial view and the result might depend on some settings with regards to termination. Why not follow the usual method of drawing cactus plots as is common in complete verification paper?

# Small questions:
- SQ1: Why is the verification attempt on MNIST in Table 1 given for eps=0.120? I am familiar with seeing verification for eps=0.1 or eps=0.3. Is there a motivation for departing from standard benchmarks?

summary_of_the_review: This paper combines existing techniques to improve the performance of complete verifiers. The contributions to the bounding process (incorporating the additional constraints with Lagrange multipliers) are relatively minor. The improvements to the branching procedure are interesting but should be clarified further.
It is however disappointing that the empirical evaluation has several weaknesses, mainly due to the lack of comparing to strong baselines.
review_title: null

Meta-review: The authors improve upon existing algorithms for complete neural network verification by combining recent advances in bounding algorithms (better bounding algorithms under branching constraints and relaxations involving multiple neurons) and developing novel branching heuristics. They show the efficacy of their method on a number of rigorous experiments, outperforming SOTA solvers for neural network verification on several benchmark datasets.

All reviewers agree that the paper makes valuable contributions and minor concerns were addressed adequately during the rebuttal phase. Hence I recommend that the paper be accepted.
Decision: Accept (Poster)