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

We thank the reviewer for the constructive comments and valuable questions. We hope the reviewer can reevaluate our paper based on our response below:

• Q1: Reframe the contribution in the paper in terms of the existing related work about nogood learning and restarts.

  Thank you for your valuable input, which allows us to view our research from a broader perspective. Other NN verification papers, such as beta-CROWN, have utilized branch-and-bound techniques specifically tailored to NN verification. While branch-and-bound is a general technique, its adaptation to the unique challenges and requirements of NN verification is what distinguishes our work. We will make sure to cite these works appropriately and discuss their relevance to our context.

• Q2: Discussion about MIP solvers more precisely.

  Thank you for your comments highlighting the need for a more detailed discussion regarding MIP solvers. We will clarify in our revision that MIP solvers, including CPLEX which we primarily used, employ branch-and-bound algorithms as a fundamental part of their operation. We found that in many of these large-scale benchmarks, the MIP solver fails to solve the initial (root) LP relaxation for the verification problem within the timeout threshold, so branch-and-bound has never started, and also no effective cuts can be generated. For instance, in the cifar100 benchmark with networks size between 5.4-31.6 M and tiny-imagnet with a network size of 14.4 M, CPLEX was unable to generate any cuts within 200 seconds (timeout threshold for this benchmark). These examples will illustrate the limitations more concretely and contextualize the generic statements we previously made, which we will add this discussion to our revised paper.

• Q3: Clarification of branching on the output of $x$ or $z$.

  By definition (line 100) of $z$, $z=0$ is equivalent to $x \leq 0$, and $z=1$ is equivalent to $x \geq 0$. This is encoded in Appendix A1, Equation 12 and 13: By inserting z=0 (z=1), x is restricted to the respective non-negative (non-positive) domain. Therefore, branching over $x \leq 0$ vs $x \geq 0$ is equivalent to branching over $z=0$ vs $z=1$. Note that technically we cannot use strict inequality like $x > 0$ or $x < 0$, so the $x=0$ case is needed in both branches. The equvalence of the two formulations has been used in prior work such as GCP-CROWN.

• Q4: simplify Proposition 3.1

  We will remove the diagonal matrix and simplify the notation. Additionally, we acknowledge that this cutting plane is a commonly known concept in MIP, first introduced in 1972 by [4]. Here is the revised cut expression:

  $\sum_{i \in \mathcal{Z}^{+}} z_i - \sum_{i \in \mathcal{Z}^{-}} z_i \leq |\mathcal{Z}^{+}| - 1$

• Q5: Thresholds used for Algorithm 1 and how do we obtain it

  The specific threshold value and its justification were detailed in Section A.3.1. The threshold, drop_percentage=50% was determined based on preliminary experiments during code development and empirical observations. We conducted multiple trials to assess the impact of different threshold values on the performance and effectiveness of the algorithm. Through these experiments, we observed that a 50% threshold provided a balanced trade-off between pruning weak constraints and maintaining a robust constraint set. We will ensure it is included in future revisions for clarity.

• Q6: Discussion about cutting planes for neural networks by acknowledging prior work on references

  We acknowledge that our discussion on prior work was brief, and we appreciate the opportunity to rectify this by acknowledging significant contributions in this area.

  1. We will cite and acknowledge Prior Works:

     • Anderson et al. propose cutting planes specifically designed for neural networks by leveraging convex-hull constraints.
     • [5] explores empirical bounds on the linear regions of deep rectifier networks, contributing to the understanding of the behavior and optimization of neural networks.
     • [6] discusses partition-based formulations for optimizing ReLU neural networks, providing a framework for mixed-integer optimization in this context.
     • [7] Section 4.2.4 offers a comprehensive overview of cutting planes and related techniques applied to neural networks, situating our work within a broader context.

  2. Our work differs from Anderson et al. [1] in several key aspects:

     • Cutting Plane Design: While Anderson et al. focus on selecting the most violated constraints among an exponential number of convex-hull constraints in one layer, our constraint can involve neurons from any layer, and our constraint can be easily found in infeasible subproblems during BaB.
     • Computational Expense: Anderson et al. propose a linear-time method for constraint selection, which can still be computationally intensive for large-scale problems. In their experiments, they use neural networks within 2000 ReLUs, in contrast, we can scale to any network that beta-CROWN works, such as CIFAR100-ResNet-large, a network with 15.2M parameters and 286820 ReLU neurons.

• Q7: Comment on Corrections to Writing

  Thank you for your detailed feedback on the writing. We appreciate the opportunity to improve the clarity and precision of our paper. We will carefully review and revise the specified sections to incorporate these corrections.

• Q8: What does "solve these cuts" mean?

  To clarify, we don’t mean to generate the cut, the term "solving cuts" was intended to describe the process of incorporating generated cuts—as additional constraints—into the linear programming (LP) problem. This process involves re-solving the LP relaxation with these new constraints to tighten the bounds of the problem.

  In our revision, we will replace the phrase "solved these cuts" with "solving the LP relaxation with cuts included, which should more accurately reflect the process.

Thank you for your insightful comments and suggestions regarding Q3 and Q6. I've considered them and would like to share the following points:

For Q3, we agree that it would be beneficial to discuss branching more directly in the main paper. We will add a clarification on how this is done with the triangle relaxation in the appendix, with a brief mention in the main text to direct readers there.

Regarding Q6, we didn't go into depth in our initial response due to word limitations. However, here's the official version we are going to add to the related work section:

[5] investigates the use of parity constraints as a cutting plane method in MILP for ReLU neural networks. These constraints are instrumental in defining a convex hull of feasible assignments, thereby improving the accuracy of approximating the number of linear regions and enhancing the network's expressiveness. While parity constraints (XOR cuts) significantly improve MILP performance by separating assignments with specific properties, they can also increase computational complexity due to their potential exponential growth with the number of variables. It is noteworthy that the XOR constraint used in [5] to construct the convex hull is similar to ours. However, their cut is constructed by solving the primal problem using the MILP solver, whereas ours is derived from infeasible domains in the inexpensive BaB.

[6] delves into the use of cutting planes derived from convex hull constraints to optimize trained ReLU neural networks within MILP. These cutting planes serve as tightening constraints, effectively excluding infeasible solutions and improving solution quality. A notable feature of the proposed method is its linear-time approach to selecting the most violated constraints, which enhances optimization efficiency. By integrating these cutting planes into a partition-based formulation, the method achieves a balance between model size and tightness during optimization. However, the generation and integration of these cuts can be computationally expensive, and not all MILP solvers may support cut generation, potentially limiting their applicability in some scenarios.

Please let us know if there are any further adjustments or if you'd like to discuss this in more detail.

We thank the reviewer for the constructive comments and valuable questions. We want to clarify a few key misunderstandings about feasibility and results. We hope the reviewer can reevaluate our paper based on our response below:

• For Weakness

  • Presentation.

    For presentation, we will fix typos and adjust format according to the reviewer's feedback and revise the text to accurately reflect the results shown in Table 3, clarifying that the comprehensive BICCOS configuration does not perform best in all cases.

  • Explanation of feasibility.

    We realize the potential for confusion. Our formulation is in line with your last statement: We are only interested in the regions that may potentially contain adversarial examples, i.e. there exist inputs $x$ such that $f(x) <= 0$. Therefore, if the lower bound does become positive, the existence of adversarial examples in this subdomain can be excluded (infeasible). Generally, in neural network verification, the safety property (non-existance of adversarial examples) is negated and posed as a satisfyability problem. Tools then report SAT if adversarial examples exist and UNSAT if the safety property holds. This implies that the input $x$ is restricted not only to the given input area, but also to those $x$ where $f(x) <= 0$. If no adversarial example exist, no $x$ with $f(x) <= 0$ exists, so the assignment becomes infeasible. Often, this constraint is only used indirectly: First, a lower bound of $f(x)$ is computed. Then, if it is positive, this implies that the underlying assignment is in fact infeasible, as the constraint $f(x) <= 0$ would always be violated. There is also work [1,2] on directly incorporating this constraint into the optimization process. While the implicit conversion from “lower bound > 0” to “infeasible” is common in the neural network verification community, we recognize the need to make this step explicit. We will rewrite the respective sentences accordingly to avoid confusion, but we want to emphasize that the our existing theoretical results are sound and not affected by these changes.

    [1] Kotha, S., Brix, C., Kolter, J. Z., Dvijotham, K., & Zhang, H. (2023). Provably bounding neural network preimages. Neurips 2023.

    [2] Pengfei Yang, Renjue Li, Jianlin Li, Cheng-Chao Huang, Jingyi Wang, Jun Sun, Bai Xue, and Lijun Zhang. Improving neural network verification through spurious region guided refinement. Tools and Algorithms for the Construction and Analysis of Systems, 2021b.

• Q1. Can BICCOS be applied to any BaB procedure?

  BICCOS is specialized to the branch-and-bound procedure of most SOTA neural network verification tools. While neural network verification constitutes a sub-problem of the more general MILP problem set, the respective tools have been tuned to its specific kind of problems.

  Specifically, the ReLU activation functions in neural networks are difficult for regular MILP solvers to handle, as they require extensive branching to cover all possible combinations of assignments. Neural network verification tools have developed specialized techniques to deal with those non-linear activation functions by overapproximating them and - crucially - improving this overapproximation iteratively using GPU-acceleration.

  However, by tuning the neural network verification tools toward this specific subset of tasks, they have become non-ideal (or impossible) to apply to regular general verification problems. Therefore, BICCOS cannot be directly applied to generic MIP problems not relavent to non-neural network verification.

• Q2. How much does BICCOS slow down the verification on easier properties?

  Thank you for pointing out the need for plots to demonstrate the trade-offs of our approach, in response to your query, Fig.2 in the pdf file illustrates the number of verified properties within various runtime thresholds. This visualization helps to clarify the performance trade-offs associated with our approach. As indicated in the figure, the slowdown experienced with our method is relatively minor for simpler properties, which are often verified before the implementation of cuts. For more complex instances, however, the benefits of our approach become more evident, with a notable improvement in time efficiency for verification. This trend suggests that while our method introduces a slight delay in simpler cases, it significantly enhances performance on more challenging properties, providing a net gain in efficiency across a diverse set of scenarios. We believe that this balanced approach is beneficial for practical applications where varying levels of difficulty are encountered.

• Q3 Does Table 2 report the best configuration?

  Thank you for your observation. Table 2 indeed reports the best configuration for each BICCOS row as identified among those listed in Table 3. This approach ensures that the reported settings are optimal for each benchmark. For instance, large models perform best with MTS, while small models benefit from MIP cuts, etc., on each dataset. This methodology is consistent with common practices in the field. E.g. in the VNN-COMP, teams often fine-tune their tools for each benchmark set. Crucially, we note that we did not explore a large set of hyperparameters, and using all BICCOS features (MILP cuts, constraint strengthening, multi-tree search) is best for all but 2 benchmarks, where it is outperformed by the tuned version (multi-tree search disabled to avoid its overhead) by only 0.5 percentage points.

We thank you again for the valuable comemnts and we hope our weaknesses (especially on infeasibility) has been addressed. We hope you can reevaluate our paper based on our response. Thank you.

We thank the reviewer for the constructive comments and valuable questions. We hope the reviewer can reevaluate our paper based on our response below:

• For Weakness.

  • W1. The work is somewhat incremental compared to GCP-CROWN

    GCP-CROWN and our work make orthogonal contributions. GCP-CROWN does not provide an efficient way to find cuts as we do. GCP-CROWN primarily focuses on solving cuts provided to it without engaging in the cut-finding process. We just use GCP-CROWN as a solver to do bound propagation with constraints. On the other hand, our work introduces an efficient algorithm specifically designed to find these cuts. This distinction highlights a significant contribution of our method: the ability to identify and generate cuts, not just solve them. By developing an algorithm that efficiently finds cuts, we add a valuable tool to the existing framework, enhancing the overall effectiveness of neural network verification.

  • W2. Performance Comparison of MILP cuts and BICCOS.

    We agree that MILP solver cuts are inherently powerful due to the solver's comprehensive approach from a lot of previous works [1] during the past decades. However, a critical limitation of MILP solver cuts is their scalability. As the network size increases, i.e., above 4M parameters, the complexity and computational resources required for MILP solvers to generate cuts even initialize the model become prohibitively high. In our experiment, we found MILP could not scale to large networks like cifar100 (5.4-31.6 M) and tiny-imagenet (14.4 M). This limits their practical applicability to larger neural networks.Our BICCOS method, while producing slightly weaker cuts compared to MILP, offers significant advantages in terms of scalability.

    [1] Wolsey, L. A., & Nemhauser, G. L. (2014). Integer and combinatorial optimization. John Wiley & Sons.

  • W3. Comparison with Venus2

    Fig. 1 in the PDF file shows a comparison with Venus2. We emphasize on making a fair comparison on the strengths of cuts. Since Venus2 uses an MILP solver to process its cuts, in these experiments we do not use the efficient GCP-CROWN solver. Instead, we also use an MILP solver to handle the BICCOS cuts we found. This ensures that the speedup we achieve is not coming from the GPU-accelerated GCP-CROWN solver. Since our cut generation relies on the process with BaB, we first run BICCOS to get the cuts, and then import the cuts into the MILP solver.

    We note that Venus uses branching over ReLU activations to create multiple strengthened MILP problems. On the other hand, we only create one single MILP and do not perform additional branching. Therefore, our MILP formulation is weaker. The fact that we can outperform Venus2 anyway underlines the strength of the generated cuts by BICCOS.

  • W4. Appendix A2 function typo.

    A We apologize for the confusion caused by the typo. We intended to write $\sum_{i \in \mathcal{Z}^{+}} z_i + \sum_{i \in \mathcal{Z}^{-}} (1 - z_i) \leq |\mathcal{Z}^+| + |\mathcal{Z}^-| - 1$

• For minor issues

  • Typos. Thank you for the detailed review, we will fix the typos. The correct number is 71, not 0.71.

  • Explanation in Appendix A.2. When we refer to "taking a negation of this equation," we mean that if the original equation holds, it leads us to the two new conditions. However, given the context and the bounds on $z$, only the first equation needs to hold.

  • Explanation in Appendix A4. The sentence was meant to highlight the efficiency of the multi-tree search despite exploring a larger number of branches because the multi-tree search domains are also counted in the total number of branches. The multi-tree search method inherently examines multiple trees, thereby increasing the number of branches explored. These domains represent different subproblems that are explored simultaneously. Although this increases the branch count, the exploration within each domain is optimized, leading to faster convergence and overall reduced computation time. We will correct the text to reflect this explanation accurately. Thank you for your careful review and for helping us improve the clarity of our paper.

• For questions

  • Q1. Why does BICCOS with multi-tree perform worse than BICCOS (base) for CNN-A-Adv-4?

    For the CNN-A-Adv-4 dataset, BICCOS with multi-tree search performs worse than BICCOS (base) primarily due to the additional time cost associated with the multi-tree search approach. This dataset contains 200 instances, and each instance has 10 predicted classifications, requiring us to validate 9 properties so in the worst case we have to perform a multi-tree search for each property.

  • Q2. Timeout difference in comparisons

    We apologize for the confusion. The MN-BaB results were copied from the VNN-COMP 2022 report. We did not reproduce those ourselves, though we use the same hardware for our experiments as they did. In table 3, BICCOS, beta-CROWN and GCP-CROWN all have a timeout of 200s. We will update the table caption accordingly. The increased timeout for MN-BaB may increase the percentage of verified instances. However, we can still outperform it.

  • Q3. Question in Table 1 & 2.

    In Table 1/2,BICCOS uses cuts from BICCOS base + multi-tree search + MIP cuts from CPLEX

  • Q4. Question in Table 3.

    In table 3, the performance degradation by multi-tree search is caused by the associated computational overhead.

  • Q5. Clarification what each variant of the BICCOS uses

    • Biccos base: only contains the cut inference during regular bab,
    • BICCOS (with multi-tree): includes BICCOS base but not MIP cuts,
    • BICCOS (all): includes base multi-tree and MIP cuts.

Thank you very much to the authors for the clarification of the points that I raised and for answering my questions. I appreciate the thorough response regarding concerns W1/W2 and the explanations regarding what the main contributions are from your side. The additional comparisons as a response to W3 are very useful, thank you for this. I think it would be helpful if this was included in the appendix of the paper.

We thank you very much for your constructive feedback and for correctly recognizing our key contributions. We appreciate your support and very helpful feedback. We provided additional experiments as requested and clarified the key questions below:

• Q1: Do You Consider Other Drop Heuristics?

  We acknowledge that while our current approach, based on improvements to the lower bound in the tree, is efficient given the available data, it does introduce dependency biases due to the constrained nature of previous assignments. There might exist better heuristics that can be explored in future work, but our work is the first of this kind and we want to start with a simple and effective heuristic.

  We have considered and tested a random drop heuristic and KFSB score heuristic as alternatives. Our benchmark results across SDP and oval22 indicated no significant improvement in performance compared to beta-CROWN, please refer to the following table. These results suggest two heuristics do not provide a robust alternative in this context.

  Dataset	Beta CROWN	Random Drop	KFSB Score	Influence Score
  cifar_cnn_a_adv	44.50%	44.50%	44.50%	47%
  cifar_cnn_a_mix	41.50%	41.50%	41.50%	45.5%
  cifar_cnn_b_adv	46.50%	46.50%	46.50%	49%

• Q2: Exploring Binary Search Approaches for Cut Strengthening

  It’s correct that our current method employs a fixed drop percentage. We did not investigate a binary-search-based approach, as this would increase the number of verification queries. Instead, we recursively tighten (line 205) the cut further should the first query succeed. If it fails, re-introducing constraints would reduce the benefit of BICCOS, while increasing the associated overhead. However, we do acknowledge that this could be tuned further in future research. We did explore dropping only 30% of the constraints at a time, with no immediate benefit. This demonstrates that we are not sensitive to this hyperparameter.

• Q3: Optimizing Cut Addition in Algorithm 1 by Selecting Only the Best Cut

  We agree the strengthened cuts make the previous cuts obsolete. We will replace lines 12 and 13 of the algorithm with

  recursively_strengthened_cuts = constraint_strengthening(f, C_{new}, C_{cut}, drop_percentage)
  if strengthening_was_successfull:
      C_{cut} <- C_{cut} \cup recursively_strengthened_cuts
  else:
      C_{cut} <- C_{cut} \cup strengthened_cuts
  

  Intuitively, if the next rounds of constraint strengthening produce a better cut, we use these better cuts rather than the currently inferred cuts.

• Q4: Integrating CDCL Learned Clauses as Cuts for Enhanced Cut Generation

  We agree that CDCL can be used to generate cuts even though this will be a challenging engineering task. This is an interesting future work and we will rephrase our paper accordingly. Our current approach focuses on generating cuts and then strengthening them, which has proven to be both easy to implement and effective. While CDCL could enhance the initial cut generation, it does not inherently provide a mechanism to strengthen these cuts using the solver, a novel step in our paper that is crucial for performance.

• Q5: Data Analysis on Cut Generation Efficiency and Feasibility in Neural Network Verification

  We evaluated the UNSAT nodes and calculated the percentage that resulted in the generation of cuts. The table below provides a detailed breakdown:

  Dataset	Avg. # Cuts Generated	Avg. UNSAT Nodes	Fraction of Cuts/UNSAT Nodes
  cifar_cnn_a_adv	345.78	763.70	0.4528
  cifar_cnn_a_adv4	86.33	2165.11	0.0399
  cifar_cnn_a_mix	121.56	1766.77	0.0688
  cifar_cnn_a_mix4	25.93	807.19	0.0321
  cifar_cnn_b_adv	105.79	808.00	0.1309
  cifar_cnn_b_adv4	106.14	1800.21	0.0590
  mnist_cnn_a_adv	11.24	1351.67	0.0083

  Regarding the number of dropped assignments, this is related to the number of rounds of BaB (Branch and Bound) using our heuristic. Our setting has a drop ratio of 0.5 if the Lagrange factor of the neuron is 0, so the average number of dropped assignments will be less than 50%. This number decreases as BaB goes deeper and the domain becomes more refined.

  Given this data, we agree with your suggestion that a cut selection procedure could be beneficial. We are implementing the new selection algorithm mentioned in Q3 above and will report back.

• Minor Issues

  • Global set of cuts in strengthening: Thank you for noting this omission. We'll add explicit mention in the text that our bound computation during cut strengthening includes the global set of cuts, aligning with Algorithm 1.
  • Introducing cut redundancy earlier: We agree this would improve readability. We'll revise Section 3.1 to briefly mention that the initial cuts are redundant until strengthened, providing context for Section 3.2.
  • Multi-tree approach differences: We'll expand on how the trees differ in the multi-tree approach. Specifically, we'll clarify that in the first round, we select different neurons to start each tree, leading to diverse branching decisions. This will lead to different exploration paths.
  • GPU usage in methods/baselines:
    • CPU: nnenum, Marabou, Venus2.
    • GPU: ERAN, OVAL, VeriNet, MN-BaB, PRIMA.
  • Typos: we will fix typos and adjust the format according to the reviewer's feedback.