Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes

Summary

Following the discussion with the authors, I am increasing my score to weak accept. ---- This paper presents a new branch-and-bound-based verification algorithm for neural networks with ReLU activation. The main idea is to produce additional constraints to the verification problem by identifying small combinations of neuronal states which would not lead to an adversarial input, so that these combinations are not explored again in another part of the branch-and-bound tree. Because smaller sets are always better, the authors develop an algorithm for reducing the number of neurons involved in such combinations. They also leverage multiple branch-and-bound trees explored in breadth-first search as a means of producing constraints involving fewer neurons.

Strengths

The ideas presented by the authors are intuitively reasonable and unsurprisingly effective as a consequence. In fact, they have been studied in other contexts with other names. Most notably, the idea of producing a constraint based on a path of the branch-and-bound tree is commonly known as nogood learning (see [1] for an early use in constraint programming, such as with the concept of a conflict set in page 9; and [2] for the first application to mixed-integer programming). The canonical application has been to identify infeasible nodes, but it is not a big stretch to apply the same idea for when the objective function is likely suboptimal (positive objective function when what we need is a negative value). Moreover, the idea of exploring multiple branch-and-bound trees in parallel is not far from solver restarts [3], which have been widely used in constraint programming and subsequently adopted in mixed-integer programming as well. All in all, this is a paper that speaks for itself because the right ideas were used and better numbers were obtained. Issues come next. [1] https://ftp.cs.ucla.edu/pub/stat_ser/r77-II-reprint.pdf [2] https://www.cs.cmu.edu/~sandholm/nogoodsForMip.techReport06.pdf [3] http://www.cs.cornell.edu/selman/papers/pdf/98.aaai.boost.pdf

Weaknesses

One problematic omission in this paper is that nowhere it is said that MIP solvers also use branch-and-bound. Otherwise, it sounds as if MIP solvers are some sort of black box magic that tries to solve problems in some inefficient way. There is also some broad generalizations such as "MIP solver may not return any cuts before timeout" (149): Which solver? When? Under which conditions? All that a generic MIP solver needs to generate a Gomory cut is the solution of the LP relaxation and the corresponding tableau. The fact that branches are defined in terms of neuron outputs is also problematic because there is an overlap between the two resulting subproblems when x=0. The effectiveness of branch-and-bound comes from partitioning the feasible set, and moreover from slicing off the parts of the LP relaxation that are not feasible according to the MIP formulation (such as when z=0 is one subproblem, z=1 is another subproblem, and 0<z<1 gets thrown away). Because your implementation is extending someone else's work, I believe that this might be a mismatch between the code and what the paper describes. Since the z variables are nevertheless a way to parameterize the LP problems to be solved along the way, there would be no problem in defining the constraints directly in terms of z instead of x. In fact, this is exactly what you do when you finally formalize the cut that you are using. When it gets to Proposition 3.1, the statement is unnecessarily complex: why define a diagonal matrix only to multiply it by a vector of ones immediately after? In terms of notation, it doesn't make sense to have output variables indexing which neurons should be removed. Instead, you could use only the corresponding indices. Hence, Z = {1, 3} instead of Z = {x_1, x_3}. Moreover, this is a commonly known cutting plane in MIP, perhaps first introduced in 1972 by [4] and at this point widely known and applied in the MIP community. It would have been better to use the conventional notation $\sum_{i \in Z^+} z_i - \sum_{i \in Z^-} z_i \leq |Z^+| - 1$ directly in the paper rather than using it in the appendix and keeping a less readable version in the paper. [4] https://epubs.siam.org/doi/10.1137/0123007 Algorithm 1 relies on a threshold, but values or experiments to find the right one are not mentioned anywhere. The paper also talks very briefly about prior work, to the point that it sounds as if specialized cutting planes for MIP problems involving neural networks were never proposed before. However, your reference 1 (Anderson et al.) does exactly that. The same is true about [5-6], and a broader perspective about this area can be found in Section 4 of the survey [7]. [5] https://arxiv.org/abs/1810.03370 [6] https://arxiv.org/abs/2102.04373 [7] https://arxiv.org/abs/2305.00241 Other major comments about the writing follow below. A) The "The NN Verification Problem" paragraph in Section 2 is not very precise because it confuses values with variables and do not properly qualify functions when values are dependent on inputs. What follows is a possible correction to that. In line 84, replace "scalar values" with "scalar variables". In line 85, add "the values of" after "for". In line 86, replace ", when they depend on a specific x" with "for a given input x". In line 87, add to "that limit [the post-activation values of] individual neurons". B) The text talks about an example in which you no longer want to see both neurons 1 and 3 inactive at the same time, but the example in Figure 1 shows neuron 3 active. Other minor comments about writing follow below. 10-11: "cutting planes constraints": this is not an adequate expression (all constraints define a plane); use either cutting planes, valid inequalities, constraints, or cuts. 21-22: First sentence is a strong statement with no reference provided and never discussed again. 32: "statuses" -> states (again in 53) 67: "discussed" -> discuss (not past tense) 98: "> 0" -> < 0? 98: "pro[p]erty" 125: "status" -> state 139: remove "BIC" 149: "and [the] MIP solver" 162: "positive regime": active regime? 163: "in [the] LP formulation" Authors repeated twice in reference 11. References 13 and 14 are the same. Use {CDCL} instead of CDCL in reference 28 and {SAT} instead of SAT in reference 30 to keep the casing in the output, since otherwise what you get is cdcl and sat.

Questions

1) In light of the comments about nogood learning and restarts, can the authors please reframe their contribution in the paper in terms of the existing related work? 2) Can you please qualify your discussion about MIP solvers by being more precise in what they can and cannot do? 3) Are you branching on the output of the neurons (x) , or on the state of the neurons (z)? 4) Can you simplify Proposition 3.1? 5) Can you please describe what thresholds were used for Algorithm 1, and how they were obtained? 6) Can you please rectify the discussion about cutting planes for neural networks by acknowledging prior work on this? 7) Can you please comment on incorporating the major and minor corrections to writing? 8) In lines 145-146, what do you mean by "[49] solved these cuts using GPU-accelerated bound propagation"? What is the concept of solving a cut? Do you mean generating the cut? Do you mean solving the LP relaxation after the cuts are included?

Rating

6

Confidence

5

Soundness

3

Presentation

2

Contribution

3

Limitations

The authors were very upfront about limitations to their work.

Summary

The paper presents BICCOS: a method to derive cutting planes for use within a state-of-the-art neural network verification framework based on branch and bound (BaB). Given verified (UNSAT) subproblems, BICCOS tries to find a subset of the employed branching choices that led to the verification result, and applies a cutting plane that prunes this subtree from the rest of the BaB procedure. Engineering improvements (going over multiple BaB tree and branching choices in parallel as a pre-processing step) are also presented. The experimental results suggest moderate improvements upon the state-of-the-art over the considered benchmarks.

Strengths

The idea behind BICCOS is fairly simple, yet relatively novel in the context of neural network verification. Given the additional overhead linked to the "strengthening" procedure (recomputing bounds after removing branching decisions), which is required for the overall algorithm, one may think that the overall approach may not pay off. The experiments show that it does, although somewhat marginally, I would believe.

Weaknesses

**Presentation.** The paper feels quite rushed, and the quality of the presentation definitely needs to improve to meet the NeurIPS bar. The figures are fairly small (especially Figure 2) and fairly hard to read on paper. I would suggest that the authors remove the shadows too, which make things harder. The Tables are also fairly hard to read on paper. The text still has some typos (e.g., "BICwhere" in line 139). The example from Figure 1 does not correspond to the text in lines 160-166 (x_3 >= 0 vs x <= 0) or to Figure 2a. In lines 308-310 the text suggests that the comprehensive BICCOS configuration performs the best in all cases: this is not what appears from Table 3. **Feasibility.** This is linked to the presentation but it's important enough to stand as a separate point. Page 4 repeatedly speaks of infeasibility in a context where I think it's technically incorrect. I think that the fact that a subproblem lower bound is positive does not imply infeasibility: it could very well be that both its lower and upper bounds are positive (with UB > LB), simply suggesting that the minimum for that subproblem (but of course not necessarily for the original problem) is positive. This means that the counter-example search is infeasible, but not the variable assignment (the series of branching decisions). In order to prove infeasibility of the subproblem, one would need to either show that the local UB is smaller than the subproblem LB, or show that the subproblem LB would go to infinity in the limit for iterations (that is, the underlying dual problem is unbounded). All the arguments being made still apply even for feasible yet verified subproblems: the goal is simply to exclude BaB subregions which we know already will lead to positive lower bounds (hence pruning the tree). But this terminology should be adapted to avoid any confusions. **Results.** While the fact that the proposed approach works is interesting (see *strengths* above), I do not think the presented experimental results are particularly impressive. Most of the improvements over GCP-CROWN (or Beta-CROWN, when GCP-CROWN can't be applied because of scalability issues) are fairly small. Furthermore, more granularity in the results would be needed (see questions). While this should not be a problem for acceptance on its own, I think it is when combined with the presentation issues above. -------- **Post-discussion.** I am increasing my score to 6 following the discussion with the authors. I encourage them to acknowledge the shortcomings of the proposed approach in the next version, and to improve the presentation as discussed.

Questions

1) It is repeatedly claimed that the procedure is specific to NN verification, but I think such an approach would apply more generally to any BaB procedure (finding subsets of branching decisions that led to a positive verification result and using that as cutting plane), or at least on any BaB procedure for MILPs. Could you please elaborate on this? 2) As commonly done in previous work (for instance, Beta-CROWN), plots showing the number of verified properties within a given runtime are needed to fully assess the trade-offs associated to the proposed approach. For instance, how much does it slow verification down on easier properties? 3) It seems to me that Table 2 reports the best configuration across those in Table 3, for each BICCOS row. Could the authors clarify this?

Rating

6

Confidence

5

Soundness

2

Presentation

1

Contribution

2

Limitations

Limitations are appropriately addressed in the conclusions.

Summary

The paper extends GCP-CROWN, an existing toolkit for the verification of neural networks which is based on GPU-accelerated bound propagation combined with a branch-and-bound (BaB) approach. The strength of the existing algorithm is its ability to incorporate cutting planes into the bound propagation process. GCP-CROWN uses cutting planes generated by a Mixed Integer Linear Programming (MILP) solver which is run in parallel to the bound propagation, however, MILP solvers generally do not scale to large problems and only generate generic, problem-independent cutting planes. The authors propose a new approach to generate cutting planes called BICCOS which works by exploiting information from verified branches in the BaB tree. Once a branch is verified, the idea is to remove a number of constraints from the branch in an attempt to obtain a subset of constraints that is sufficient for obtaining a "verified" result. If successful, a cut which is valid for all other branches in the BaB tree can be generated based on these constraints. The generation of cuts is run during the normal verification process, but the authors propose adding a presolve step that initially generates multiple shallow BaB trees in an attempt to create a pool of cuts before starting the standard BaB phase from GCP-CROWN. The experimental evaluation shows that BICCOS scales well, is able to generate cuts for problems that the MILP solver employed in GCP-CROWN can't scale to, and outperforms many competing tools.

Strengths

- Neural Network Verification is a relevant research topic - A cut generation method that scales to larger networks as well as cuts that are problem-specific and less generic than those generated by a MILP solver are useful contributions. - The method outperforms most other toolkits in the experimental evaluation

Weaknesses

- The work is somewhat incremental compared to GCP-CROWN - When comparing the performance of GCP-CROWN and BICCOS (base) in Table 3, this seems to indicate that the newly introduced cuts are weaker than the MILP cuts. Including presolve (BICCOS(with multi-tree)) improves performance compared to GCP-CROWN in only some instances. It's good to have a cut generation method which scales to larger networks, but the method would be a lot stronger if the BICCOS cuts alone outperformed the generic MILP cuts. - A comparison with existing cuts, such as the ones from [1], is missing. In the related work section the authors only state that Venus (which implements the cuts from [1]) delivers weaker empirical results than their approach. However, the contribution of this paper are the new cuts and comparing the BICCOS cuts in a GPU-enabled bound propagation framework to the cuts by Botoeva et al. implemented in a MILP-based verifier (which can't make use of GPU acceleration) is not fair since it is well-known in the literature that bound propagation frameworks outperform MILP verifiers. To assess whether the BICCOS cuts are more effective than the cuts in [1] they should be implemented in the same general framework. Without this comparison it is hard to judge the contribution of this work. - Appendix A2: This part of the appendix is either very unclear or has a lot of typos. There are a lot of expressions like $\sum_{i \in \mathcal{Z}^+} z_i + \sum_{j \in \mathcal{Z}^-} (1 - z_i)$. Do the authors mean to write $\sum_{i \in \mathcal{Z}^+} \left ( z_i + \sum_{j \in \mathcal{Z}^-} (1 - z_i) \right )$? If so, the extra set of brackets should be added. If the authors actually do mean to write $\sum_{i \in \mathcal{Z}^+} \left ( z_i \right ) + \sum_{j \in \mathcal{Z}^-} (1 - z_i)$ then the $z_i$ in the second sum makes no sense, should this be $z_j$ then? This unclarity/mistake appears in the two equations between line 516 and 517 (which aren't labeled so I can't refer to them), in line 518, in the first equation between line 518 and line 519 and the second equation between line 518 and 519 (these also aren't labeled so I can't refer to them directly). ### Minor points - Line 10-11: cutting planes constraints --> cutting **plane** constraints - Line 60: proposed --> **propose** - Line 67: discussed --> **discuss** - Line 98: The paper states "If $f^* > 0$, it is unclear whether the property might hold" --> Shouldn't this be "If $f^* < 0$" (i.e. the inequality being flipped?) - Line 98: proerty --> pro**p**erty - Line 109: Remove "the" (sentence should be "most existing NN verifiers use cheaper methods such as (...)") - Line 139: Remove **BIC** at the beginning of the line - Line 143: they --> **the authors** - Figure 2a): these subproblems already includes the constraint --> these subproblems already **include** the constraint - Line 194: along --> **alone** - Line 198-199: using as fewer variables as possible --> using as **few** variables as possible - Line 202: we performs a re-verification step, where it recomputes the lower bound --> we **perform** a re-verification step **which** recomputes the lower bound - Line 208: we propose --> **W**e propose - Table 3: For MNIST, CNN-A-Adv the "Ver%" for BICCOS (with MIP cuts) is $0.71$. Is this a typo, what is the correct number? - Appendix A.2: The authors derive two equations by "taking a negation of this equation". I find this part a bit unclear, do they mean that if the equation holds then this is equivalent to one of the two new equations holding? Or do both of the two new equations need to hold? - Line 547-549 in Appendix A4: The authors write "on the CIFAR CNN-B-Adv model, BICCOS with multi-tree search explores $2.54 \times 10^3$ branches, significantly lower than the $1.57 \times 10^3$ branches explored by the base BICCOS version." However, as far as my understanding goes, $2.54 \times 10^3$ is not a **smaller** but a **larger** number than $1.57 \times 10^3$ so the sentence here makes no sense. I tried to double-check this but the same numbers are reported in the table below (I assume that "BICCOS with multi-tree search" in the text is the same as "BICCOS (with Presolve)" in the table). Could the authors clarify what their point is here? ### References [1] Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A. & Misener, R. (2020) Efficient Verification of ReLU-Based Neural Networks via Dependency Analysis. In: Proceedings of the AAAI Conference on Artificial Intelligence. 3 April 2020 pp. 3291–3299. doi:10.1609/aaai.v34i04.5729.

Questions

- Table 3: Why does BICCOS with multi-tree perform worse than BICCOS (base) for CNN-A-Adv-4, do the authors have an explanation for this? - Why is BICCOS run with a shorter timeout compared to other algorithms? Also why is MN-BaB run with a 600s timeout and then $\beta$-CROWN, GCP-CROWN and BICCOS are run with a 200s timeout in Table 2, but then in Table 3 the footnote seems to suggest that BICCOS is run with a 200s timeout while $\beta$-CROWN and GCP-CROWN use a longer timeout? This seems inconsistent. The experiments would be more informative if all algorithms were run with the same time budget as is usual practice e.g. in VNNComp. - In Table 1/2 does BICCOS use cuts from a MILP solver (if the solver scales to the problem) or only the newly introduced cuts? - Table 3: For CNN-A-Mix-4 the BICCOS-MIP approach has a verified accuracy of 56.5% but BICCOS-all has 56%. What is the authors' intuition here regarding why adding the multi-tree approach worsens performance, do they think this is an issue/can be avoided? - Line 302-310: Could the authors clarify what each variant of the algorithm includes here? The text makes it sound a bit like the authors start from BICCOS (base) and then gradually add other components, but does BICCOS (with multi-tree) also include MIP cuts? If so, the performance drop from 52 to 51.5% on e.g. CIFAR CNN-B-Adv would be surprising, any explanations?

Rating

4

Confidence

4

Soundness

3

Presentation

2

Contribution

2

Limitations

Limitations are sufficiently addressed.

Summary

This work proposes a new approach to produce cutting planes in the context of branch-and-bound-based solvers for neural network verification. Whenever an infeasible subproblem is encountered in branch-and-bound, this method generates a cut from the conflicting assignment that led to the infeasible subproblem (initially redundant w.r.t. the remainder of the tree), and attempts to strengthen this cut by heuristically dropping some of the assignments and rechecking for infeasibility via the lower bound. This is further enhanced by using several parallel shallow trees to produce stronger cuts. This method is implemented on top of the $\alpha,\beta$-CROWN framework and provides meaningful computational improvements compared to various baselines on a set of benchmarks.

Strengths

This paper provides a solid contribution to the area of neural network verification methods. It builds on top of cut-based branch-and-bound verification solvers by presenting a method to quickly infer cuts, which appear to be novel and computationally useful. In particular, they nicely leverage the fact that there are fast methods to produce bounds in NN verification, allowing us to quickly recheck cut validity. This makes for a clean and simple method, which has the advantage of not being too complicated to integrate with an existing cut-based BaB verification solver. Both the set of benchmarks and baselines are reasonably extensive, and we can observe improvements in verifiability that are sufficient for a meaningful computational contribution, especially in the CIFAR instances in both VNN-COMP and SDP-FO, without much additional cost in computational time. The paper is overall clearly written and the figures and algorithms are helpful.

Weaknesses

In some of the benchmarks, the computational results may be somewhat incremental, but overall they are positive. There is potential room for improvement in parts of the methods (see Questions section below); in particular, it is not clear if the authors have explored variations of their constraint strengthening approach. In general, I do not see major weaknesses in this paper, though minor concerns are expanded on below.

Questions

General comments: 1. I see that your variable-to-drop selection heuristic is based on their improvements to the lower bound in the tree. While this seems reasonable as a fast heuristic since you already have all the data, these improvements are not independent from each other since they are constrained over previous assignments, and thus there is some bias depending on the depth (i.e. if the assignments were done in a different order in the tree, you'd select different variables, but the constraint is the same). This makes me wonder if there is a better heuristic. Have you considered other approaches? 2. It seems that you try to continue strengthening the cuts based on a fixed drop percentage. I am curious if you have tried something more like a binary search approach over the verification bound? You can also add some sort of tolerance on the bound to stop searching when you are close enough to zero. 3. In Algorithm 1, lines 12-13, you add the cut, and then try to strengthen it again. It sounds like you could just add the best cut here, instead of adding all cuts throughout strengthening, since the best cut dominates the other ones. 4. I appreciate the explanation of the differences between this method and [7] and DPLL/CDCL in the Related Work section, as both of these were in my mind as I was reading the paper. However, I'd like to comment that the reasoning for CDCL makes it sounds like it is impossible in practice to use learned clauses from CDCL as cuts; rather, I believe this is more of a challenging engineering task than not being practically viable. Much like branch-and-bound has been customized for NN verification in a more effective way than generic MIP solvers, I do not see a reason why one would not be able to customize ideas from CDCL for your cut generation procedure. The learned conflicts can be naturally translated to the type of cuts you have in Sec. 3.1 of this paper (except already stronger) and then further strengthened in the same way. Given that CDCL is a tried-and-true method to produce good conflicts, I suspect that this might lead to better cuts and may be interesting future work that would already fit very well with what you have so far. 5. I would have liked to see some data to better understand the cuts generated. In particular, what is the fraction of infeasible nodes from which you were able to produce a (non-redundant) cut, and what was the total number of cuts? What was the average number of assignments that you were able to drop? This sort of data would reveal more information on the overhead of these cuts and how easy or hard it is to find them. I wonder if some cut selection procedure would make sense here, but I do not know if you have many or few cuts. Comments on text: 6. In the MIP section, it would be useful to mention that MIP is also based on branch-and-bound, and modify the last sentence to include why a custom branch-and-bound is more effective than MIP branch-and-bound in practice (e.g. because MIP is based on solving LPs which can be expensive, etc.). 7. In Sec 3.1., I suggest preparing the reader to the fact that the cuts from Sec. 3.1 are redundant w.r.t. the tree until strengthened, instead of waiting until Sec. 3.2 to mention that. This is a question one would naturally have while reading Sec. 3.1, and it would make the reading easier if they already know the answer to that question. 8. Figure 2 is a bit too small to read especially when printed out. If possible, please make it larger. 9. Can you include in the text that your bound computation when strengthening a cut includes the global set of cuts? I see it in Algorithm 1, but I didn't see it in the text. 10. Could you include exactly how the trees differ from each other in the multi-tree approach? The text mentions that they explore a different set of branching decisions, but not how. 11. Could you expand on which methods/baselines use GPUs, and how they are used? This is important for a proper comparison. 12. Typos: Remove "BIC" in line 139, capitalize "we" in line 208, "instances" and double period in caption of Table 4.

Rating

7

Confidence

4

Soundness

4

Presentation

4

Contribution

3

Limitations

The Limitations section is reasonable, covering cases where this approach does not work well.

Thank you for your response

I thank the authors for their response. I appreciate the willingness to improve the presentation of their work in a future version, and thank the authors for the clarification on their use of feasibility. Unfortunately, I am still leaning towards rejection, as I still believe the experimental improvements to be somewhat marginal, and I still think that, presentation-wise, the submission feels a bit rushed. I understand that it is common practice in VNN-COMP to tune and engineer a framework to a given setting, but in my own view the goal of a paper is slightly different. The shortcomings of the presented approach should have featured more prominently, along with a comprehensive explanation as to why something would not pay off in a given setup. Instead, the submission appears to be seeking to sweep the shortcomings of the full configuration under the rug. For instance, line 309 even states "The comprehensive BICCOS configuration, incorporating all optimizations, achieves the highest verified accuracies across models.", which is either incorrect or misleading. Related to this, I think the paper should have included a more prominent description of the overhead of the framework on easier properties. I appreciate the inclusion of Figure 2 in the response, albeit I think it is incomplete and would have read better in a log scale over time (as it is, the overhead on slow properties is hard to quantify as a share of runtime). An updated Figure 2, also featuring other baselines such as GCP-CROWN, which is expected to perform much better than Beta-CROWN on harder properties, should definitely appear in the next version of the work.

Follow up comments

I appreciate the effort of the authors with my questions. Here is a brief follow up on each point. I would appreciate a brief rebuttal on those. - Q1: This is exactly what most of the scholarship on mathematical optimization does: it tailors these general-purpose techniques to a particular problem at hand; yours is no different. By acknowledging that your contribution fits in this broader theme and adapts tried and proven methods (or rediscovers them, which is fair to say since we can assume you were not aware of those), you are doing less "marketing" and better scholarship. In my opinion, that would make your paper considerably better. - Q2: This is helpful for perspective. Please include those in the paper itself. - __Q3: This is wrong. Effective branch-and-bound works by defining disjunctions. Not only overlaps are ineffective, but in your case they lead to an algorithm that would never terminate (if you were really branching on $x$ that way, rather than on $z$ as you probably are). By branching on $x \leq 0$ and $x \geq 0$, the second subproblem is identical to the original problem (since $x \geq 0$ if $x$ is the output of a ReLU).__ - Q4: Perfect! - Q5: Please add a note in the main paper linking to that. - Q6: Your comments about [5] and [6] do not cover cutting planes at all. Not worth including those references if you are not going to explain the cutting planes in those papers. - Q7: Good. - Q8: This is great. Please add some of this to the main paper.