Venue: NeurIPS 2022 Conference

Reviews:

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: The paper considers the neural network verification problem where it builds on
bound propagation methods to account for cutting planes generated by MILP
solvers. Experimental results on a number of benchmarks from VNN-COMP 20201
show improved performance over the SoA.
strengths_and_weaknesses: Strengths.

- First work that I am aware of that uses cutting planes from MILP solvers in a
  bound propagation setting.

- It is good to see that this works in practice.

Weaknesses.

- Highly incremental to previous work. The technical novelty is the addition of
  cuts to a previously developed framework, which while is good to see that it
  works, it presents limited originality and overall contribution.

- There is no ablation study that compares GCP-CROWN with cuts and GCP-CROWN
  without cuts. The authors should make precise the contribution of the cuts to
  the overall performance (while there are comparisons with different variants
  of crown, an ablation study on GCP-CROWN would make the actual contribution
  more clear).

- Related work on MILP-based verification which strengthens the MILP
  formulation  with custom cuts is not discussed:  E. Botoeva et al., Efficient
  Verification of ReLU-Based Neural Networks via Dependency Analysis, AAAI
  2020.
questions: Please see comments on Weaknesses.
limitations: These are sufficiently addressed.
review_title: null

final_score: rating: 7: Accept: Technically solid paper, with high impact on at least one sub-area, or moderate-to-high impact on more than one areas, with good-to-excellent evaluation, resources, reproducibility, and no unaddressed ethical considerations.
review_content: summary: These paper improve the general BaB method by integrateing any cutting cut method for formal complete evrifcation of adervarial robustness. This computation allows parallel comptation . they outperfom state of the art againstal several datset, methods, noise level for multilpes models for both verified accuracy and verification time.
strengths_and_weaknesses: Strengths: 

Novelty of the approach: complete verification of DNN specific family 

Important topic 

Sound proof of the Hessian bounds 

Clarity of the paper 

Faster  verification and higher verified accuracy

Weaknesses 

Poor experiments comparison according power resoureces
questions: Can you compare the power ressources used compared to methods DP-FO [12]∗ PRIMA [35] β-CROWN [52] MN-BaB [17] α-CROWN+MIP ? (as you used parralel comptation: what if you did not use paralilsum)?

You did not discuss the limitations of your work

You did not dscuss the comprarsion of different cutting planes.
limitations: cf above
review_title: null

final_score: rating: 6: Weak Accept: Technically solid, moderate-to-high impact paper, with no major concerns with respect to evaluation, resources, reproducibility, ethical considerations.
review_content: summary: The authors extend the popular and effective Beta-CROWN algorithm, a complete verifier that very efficiently operates on the triangle ReLU relaxation in the context of branch and bound, to support general cutting planes. 
The presented algorithm, named GCP-CROWN, relies on cutting planes from off-the-shelf LP solvers, run on a CPU, in parallel to the GPU-based neural network verification procedure. 
GCP-CROWN is shown to outperform state-of-the-art baselines on relevant benchmarks.
strengths_and_weaknesses: While the idea behind GCP-CROWN is simple and somewhat incremental (it is a minor, yet powerful, extension of beta-CROWN), it is undeniably novel in the context of neural network verification. Furthermore, the experimental results clearly indicate that GCP-CROWN outperforms the state of the art on hard verification benchmarks.

My concerns mostly revolve around the sub-par quality of the presentation. Crucially, I believe that the authors should be more upfront with respect to their algorithm's incrementality with respect to beta-CROWN, which is not necessarily a bad thing. However, such incrementality might not be evident to someone outside the sub-field. In other words, the presentation should start from beta-CROWN, and then move on to include the relaxed integer variables, and the cutting planes.
The analysis of the cutting planes, presented in the appendix, is perhaps worth including in the main paper.
Furthermore, it would be nice if the authors could include larger networks in the evaluations: for instance, the cifar2020 benchmark from VNN-COMP-21 includes networks with tens of thousands of activations. I would be curious to see whether cutting planes still pay off with respect to beta-CROWN at that scale.
questions: - I believe MN-BaB, which is closely related to GCP-CROWN, should be more accurately described and presented in the technical part of the paper;

- the authors should explain and argue more on why one has to use these cutting planes in the context of bound propagation rather than lagrangian relaxation or decomposition, where doing so would be easier. It would be nice to see an experimental comparison on that, or theoretical arguments on why bound propagation is to be preferred. From the technical parts of the paper, it would seem like bound propagation methods are the only GPU-friendly alternative to off-the-shelf LP solvers. Many cited works [6, 13, 15] demonstrate otherwise, and that should be more carefully explained.

- Theorem 3.1 shows that GCP-CROWN provides a lower bound to the LP with cutting planes. However, do the optimal values of alpha and beta lead to the optimal primal value? 

- what's the employed branching strategy in the experiments?

- why does GCP-CROWN take more subproblems than beta-CROWN on the deep network of table 1? That's counter-intuitive.
limitations: The authors adequately address the limitations of their work, but should be more upfront with respect to their incremental improvements on beta-CROWN.
review_title: null

Meta-review: metareview: All the reviewers found the work to have promise, but there was concern about the novelty of the work. That said, the experimental results showcased the power of the approach; the authors are advised to put their work in the context of prior work.

Overall, there was a consensus that the paper deserves to be published and hence the recommendation. 
confidence: Certain
Decision: Accept