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

Authors: duo  zhou
christopher  brix
grani a hanasusanto
huan  zhang
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-15 20:18:40

Abstract: Recently, cutting-plane methods such as GCP-CROWN have been explored to enhance neural network verifiers and made significant advancements. However, GCP-CROWN currently relies on ${\it generic}$ cutting planes ("cuts") generated from external mixed integer programming (MIP) solvers. Due to the poor scalability of MIP solvers, large neural networks cannot benefit from these cutting planes. In this paper, we exploit the structure of the neural network verification problem to generate efficient and scalable cutting planes ${\it specific}$ to this problem setting. We propose a novel approach, Branch-and-bound Inferred Cuts with COnstraint Strengthening (BICCOS), that leverages the logical relationships of neurons within verified subproblems in the branch-and-bound search tree, and we introduce cuts that preclude these relationships in other subproblems. We develop a mechanism that assigns influence scores to neurons in each path to allow the strengthening of these cuts. Furthermore, we design a multi-tree search technique to identify more cuts, effectively narrowing the search space and accelerating the BaB algorithm. Our results demonstrate that BICCOS can generate hundreds of useful cuts during the branch-and-bound process and consistently increase the number of verifiable instances compared to other state-of-the-art neural network verifiers on a wide range of benchmarks, including large networks that previous cutting plane methods could not scale to.

Main paper: 
 introduction: 
 Formal verification of neural networks (NNs) has emerged as a critical challenge in the field of artificial intelligence. In canonical settings, the verification procedure aims to prove certified bounds on the outputs of a neural network given a specification, such as robustness against adversarial perturbations or adherence to safety constraints. As these networks become increasingly complex and are deployed in sensitive domains, rigorously ensuring their safety and reliability is paramount. Recent research progress in neural network verification has enabled safety or performance guarantees in several mission-critical applications [55, 53, 51, 13, 60, 57] .The branch and bound (BaB) procedure has shown great promise as a verification approach [12, 59, 21] . In particular, the commonly used ReLU activation function exhibits a piecewise linear behavior, and this property makes ReLU networks especially suitable for branch and bound techniques. During the branching process, one ReLU neuron is selected and two subproblems are created. Each subproblem refers to one of the two ReLU states (inactive or active) and the bounds of the neurons' activation value are tightened correspondingly. BaB systematically branches ReLU neurons, creates a search tree of subproblems, and prunes away subproblems whose bounds are tight enough to guarantee the verification specifications. Although our work focuses on studying the canonical ReLU settings, branch-and-bound has also demonstrated its power in non-ReLU cases [48] . Despite its success on many tasks, the efficiency and effectiveness of the branch and bound procedure heavily depends on the number of subproblems that can be pruned.Recent work has explored the use of cutting plane methods in neural network verification. Cutting planes ("cuts") are additional (linear) constraints in the optimization problem for NN verification to tighten the bound without affecting soundness. By introducing carefully chosen cuts, they can significantly tighten the bounds in each subproblem during BaB, leading to more pruned subproblems and faster verification. However, it is quite challenging to generate effective cutting planes for large-scale NN verification problems. For example, GCP-CROWN [61] relied on strong cutting planes generated by a mixed integer programming (MIP) solver, which includes traditional generic cutting planes such as the Gomory cuts [24] , but its effectiveness is limited to only small neural networks. The key to unlocking the full potential of BaB lies in the development of scalable cutting planes that are specific to the NN verification problem and also achieve high effectiveness.In this paper, we propose a novel methodology, Branch-and-bound Inferred Cuts with COnstraint Strengthening (BICCOS), that can produce effective and scalable cutting planes specifically for the NN verification problem. Our approach leverages the information gathered during the branch and bound process to generate cuts on the fly. First, we show that by leveraging any verified subproblems (e.g., a subproblem is verified when neurons A and B are both split to active cases), we can deduce cuts that preclude certain combinations of ReLU states (e.g., neurons A and B cannot be both active). This cut may tighten the bounds for subproblems in other parts of the search tree, even when neurons A and B have not been split yet. Second, to make these cuts effective during the regular BaB process, we show that they can be strengthened by reducing the number of branched neurons in a verified subproblem (e.g., we may conclude that setting neuron B to active is sufficient to verify the problem, drop the dependency on A, and remove one variable from the cut). BICCOS can find and strengthen cuts on the fly during the BaB process, adapting to the specific characteristics of each verification instance. Third, we propose a pre-solving strategy called "multi-tree search" which proactively looks for effective cutting planes in many shallow search trees before the main BaB phase starts. Our main contributions can be summarized as follows:• We first identify the opportunity of extracting effective cutting planes during the branch-and-bound process in NN verification. These cuts are specific to the NN verification setting and scalable to large NNs that previous state-of-the-art cutting plane methods such as GCP-CROWN with MIP-cuts cannot handle. Our cuts can be plugged into existing BaB-based verifiers to enhance their performance.• We discuss several novel methods to strengthen the cuts and also find more effective cuts. Strengthening the cuts is essential for finding effective cuts on the fly during the regular BaB process that can tighten the bounds in remaining domains. Performing multi-tree search allows us to identify additional cuts before the regular BaB process begins.• We conduct empirical comparisons against many verifiers on a wide range of benchmarks and consistently outperform state-of-the-art baselines in VNN-COMP [4, 40, 10] . Notably, we can solve the very large models like those for cifar100 and tinyimagenet benchmarks and outperform all state-of-the-art tools, to which GCP-CROWN with MIP-based cuts cannot scale.(i) j = 0 in LP relaxation ⇔ u (i) j = 0 in Planet Relaxation. (⇒) Assume z (i) j = 0 in LP relaxation. From 10, x(i) j ≤ u (i) j × 0 = 0 =⇒ x(i) j ≤ 0. From 8:x(i) j ≥ 0. Combining the above, we get x(i) j = 0. From 11,x(i) j ≤ x (i) j -l (i) j (1 -0) = x (i) j -l (i) j . Sincex(i) j = 0 and 9, this simplifies to 0 ≤ x(i) j -l (i) j =⇒ 0 ≥ x (i) j ≥ l (i) jThis is consistent with the pre-activation bounds of the neuron. Therefore, fixing z (i) j = 0 in the LP relaxation forces the activation x(i) j to be zero, effectively modeling the neuron as inactive. (⇐) Assume u(i) j = 0 in the Planet relaxation. Set u (i) j = 0. The constraint 15 becomes x(i) j ≤ 0 0-l (i) j (x (i) j -l (i) j ) = 0. From 8 x(i) j ≥ 0.Combining the above, we get x(i) j = 0.Thus, setting u (i) j = 0 in the Planet relaxation also forces x(i) j to zero, mirroring the effect of fixing z Proof: Due to the relationship between the x and z in Lemma A.1, i.e. for any unstable neuron i,(i) j = 0 in the LP relaxation. 2. z (i) j = 1 ⇔ l (i) j = 0.x i ≥ l i = 0 ⇐⇒ z i = 1 and x i ≤ u i = 0 ⇐⇒ z i = 0 ⇐⇒ (1 -z i ) = 1,we have the following equation to represent an UNSAT path:EQUATIONBy taking negation of Eq 16 to exclude this path, we have:EQUATIONEQUATIONNotice that z ∈ [0, 1] |Z| , implies that the sum of z should be bounded by its cardinality, i∈Z+ z i + i∈Z -(1-z i ) ≤ |Z + |+|Z -|,and the binary indicator property, thus we only consider inequality 18:EQUATIONThus, the BaB inferred cut 3 can be used to exclude this UNSAT status. □ 
background: 
 Notations Bold symbols such as x (i) denote vectors; regular symbols like x (i) j indicate scalar components of these vectors.[N ] represents the set {1, . . . , N }, and W (i) :,j is the j-th column of the matrix W (i) . A calligraphic font X denotes a set, and R n represents n-dimensional real number space. The NN Verification Problem An L-layer ReLU-based DNN can be formulated as f : x → x (L) , s.t. {x (i) = W (i) x(i-1) + b (i) , x(i) = σ(x (i) ), x (0) = x; i ∈ [L]}, where σ represents the ReLU activation function, with input x =: x(0) ∈ R d (0)and the neuron network parameters weight matrix W (i) ∈ R d (i) ×d (i-1) and bias vector b (i) ∈ R d (i) for each layer i. This model sequentially processes the input x through each layer by computing linear transformations followed by ReLU activations. The scalar valuesx(i) j and x (i) j represent the post-activation and pre-activation values of the j-th neuron in the i-th layer, respectively. We write f (i) j (x) and f (i) j (x) for x(i) j and x (i) j , respectively, when they depend on a specific x.In practical applications, the input x is confined within a perturbation set X , often defined as an ℓ p norm ball. The verification task involves ensuring a specified output property for any x ∈ X . For instance, it may be required to verify that the logit corresponding to the true label f i (x) is consistently higher than the logit for any other label f j (x), thus ensuring f i (x) -f j (x) > 0, ∀j ̸ = i. By integrating the verification specification as an additional layer with only one output neuron, we define the canonical verification problem as an optimization problem:EQUATIONwhere the optimal value f ⋆ ≥ 0 confirms the verifiable property. We typically use the ℓ ∞ norm to define X := {x : ∥x -x 0 ∥ ∞ ≤ ϵ}, with x 0 as a baseline input. However, extensions to other norms and conditions are also possible [44, 58] . When we compute a lower bound f ⋆ ≤ f ⋆ , we label the problem UNSAT if the property was verified and f ⋆ ≥ 0, i.e. the problem of finding a concrete input that violates the property is unsatisfiable, or in other words infeasible. If f ⋆ < 0, it is unclear whether the property might hold or not. We refer to this as unknown. MIP Formulation and LP Relaxation In the optimization problem (1), a non-negative f ⋆ indicates that the network can be verified. However, due to the non-linearity of ReLU neurons, this problem is non-convex, and ReLU neurons are typically relaxed with linear constraints to obtain a lower bound for f ⋆ . One possible solution is to encode the verification problem using Mixed Integer Programming (MIP), which encodes the entire network architecture, usingx ∈ R d (i) to denote the pre-activation neurons, x ∈ R d (i)to denote post-activation neurons for each layer, and binary ReLU indicator z (i) j ∈ {0, 1} to denote (in)active neuron for each unstable neuron. A lower bound can be computed by letting z (i) j ∈ [0, 1] and therefore relaxing the problem to an LP formulation. There is also an equivalent Planet relaxation [20] . We provide the detailed definition in Appendix A. In practice, this approach is computationally too expensive to be scalable. Branch-and-bound Instead of solving the expensive LP for each neuron, most existing NN verifiers use cheaper methods such as abstract interpretation [49, 23] or bound propagation [16, 62, 54, 59] due to their efficiency and scalability. However, because of those relaxations, the lower bound for f ⋆ might eventually become too weak to prove f ⋆ ≥ 0. To overcome this issue, additional constraints need to be added to the optimization, without sacrificing soundness. The branch-and-bound (BaB) framework, illustrated in Figure 1 , is a powerful approach for neural network verification that many state-of-the-art verifiers are based on [12, 54, 16, 29, 21] . BaB systematically tightens the lower bound of f ⋆ by splitting unstable ReLU neurons into two cases: x j ≥ 0 and x j ≤ 0 (branching step), which defines two subproblems with additional constraints. In each subproblem, neuron x j does not need to be relaxed, leading to a tighter lower bound (bounding step). Note that {x The process repeats on subproblems with negative lower bounds until all unstable neurons are split, or all subproblems are verified. If there are still domains with negative bounds after splitting all unstable neurons, a counter-example can be constructed. General Cutting Planes (GCP) in NN verification A (linear) cutting plane ("cut") is a linear inequality that can be added to a MIP problem, which does not eliminate any feasible integer solutions but will tighten the LP relaxation of this MIP. For more details on cutting plane methods, we refer readers to the literature on integer programming [7, 14] . In the NN verification setting, it may involve variables x (i) (pre-activation), x(i) (post-activation) from any layer i, and z (i) (binary ReLU indicators) from any unstable neuron. Given N cutting planes in matrix form as [61] :(i) j ≤ u (i) j = 0} and {x (i) j ≥ l (i) j = 0}EQUATIONwhere H (i) , G (i) , and Q (i) are the matrix coefficients corresponding to the cutting planes. Based on this formulation, one can introduce arbitrary valid cuts to tighten the relaxation. GCP-CROWN [61] allows us to lower bound (1) with arbitrary linear constraints in (2) using GPU-accelerated bound propagation, without relying on an LP solver.In [61] , the authors propose to find new cutting planes by employing an MIP solver. By encoding (1) as a MIP problem, the MIP solver will identify potentially useful cutting planes. Usually, these cuts would be used by the solver itself to solve the MIP problem. Instead, [61] applied these cuts using GPU-accelerated bound propagation. This approach shows great improvements on many verification problems due to the powerful cuts, but it depends on the ability of the MIP solver to identify relevant cuts. As the networks that are analyzed increase in size, the respective MIP problem increases in complexity, and the MIP solver may not return any cuts before the timeout is reached. In the next chapter, we will describe a novel approach to generate effective and scalable cutting planes.3 Branch-and-bound Inferred Cuts with Constraint Strengthening (BICCOS) 
branch-and-bound inferred cuts: 
 The first key observation in our algorithm is that the UNSAT subproblems in the BaB search tree include valuable information. If the lower bound of a subproblem leads this subproblem to be UNSAT (e.g., subproblems with green ticks in Fig. 1 ), it signifies that restricting the neurons along this path to the respective positive/negative regimes allows us to verify the property. A typical BaB algorithm would stop generating further subproblems at this juncture, and continue with splitting only those nodes that have not yet been verified. Crucially, no information from the verified branch is transferred to the unverified domains. However, sometimes, this information can help a lot.Example. As shown in Fig. 1 , assume that after splitting x 1 ≤ 0 and x 3 ≤ 0, the lower bound of this subproblem is found to be greater than 0, indicating infeasibility. From this infeasibility, we can infer that the neurons x 1 and x 3 cannot simultaneously be in the inactive regime. To represent this relationship, we use the relaxed ReLU indicator variables z 1 , z 3 ∈ [0, 1] in the LP formulation and form the inequality z 1 + z 3 ≥ 1. This inequality ensures that both z 1 and z 3 cannot be 0 simultaneously. If we were to start BaB with a fresh search tree, this constraint has the potential to improve the bounds for all subproblems by tightening the relaxations and excluding infeasible regions.We propose to encode the information gained from a verified subproblem as a new cutting plane. These cutting planes will be valid globally across the entire verification problem and all generated subproblems. We present the general case of this cutting plane below: Proposition 3.1. For a verified, or UNSAT, subproblem in a BaB search tree, let Z + and Z -be the set of neurons restricted to the positive and negative regimes respectively. These restrictions were introduced by the BaB process. Then, the BaB inferred cut can be formulated as:EQUATIONProof deferred to Appendix B.1. The BaB inferred cut (3) will exclude the specific combination of positive and negative neurons that were proven to be infeasible in the respective branches. An example is shown in Fig. 2a .Note that while similar cuts were explored in [9] , they were not derived from UNSAT problems within the BaB process. In our framework, these cuts can theoretically be incorporated as cutting planes in the form of (2) and work using GCP-CROWN. However, a limitation exists: all elements in our cut are ReLU indicator z, although GCP-CROWN applies general cutting planes during the standard BaB process. It was not originally designed to handle branching decisions on ReLU indicator variables z that may have (partially) been fixed already in previous BaB steps. When cuts are added, they remain part of the GCP-CROWN formulation. However, during the BaB process, some z variables may be fixed to 0 or 1 due to branching, effectively turning them into constants This situation poses a challenge because the original GCP-CROWN formulation presented in [61] does not accommodate constraints involving these fixed z variables, potentially leading to incorrect results. To address this issue, we need to extend GCP-CROWN to handle BaB on the ReLU indicators z, ensuring that the constraints and cuts remain valid even when some z variables are fixed during branching.To address this limitation, we propose an extended form of bound propagation for BaB inferred cuts that accommodates splitting on z variables. In the original GCP-CROWN formulation, I (i) represents the set of initially unstable neurons in layer i, for which z cuts were added due to their instability. However, during the branch-and-bound process, some of these neurons may be split, fixing their corresponding z variables to 0 or 1, and thus their z variables no longer exist in the original formulation. While updating all existing cuts by fixing these z variables is possible, it is costly since the cuts for each subproblem must be fixed individually, as the neuron splits in each subproblem is different. Our contribution is to handle these split neurons by adding them to the splitting set Z in the new formulation below, without removing or modifying the existing cuts (all subdomains can still share the same set of cuts). This approach allows us to adjust the original bound propagation in [61, Theorem 3.1] to account for the fixed z variables and their influence on the Lagrange dual problem, without altering the existing cuts. Suppose the splitting set for each layer i isZ +(i) ∪ Z -(i) := Z (i) ⊆ I (i), and the full split set is Z = i∈[L-1] Z (i) . The modifications to the original GCP-CROWN theorem are highlighted in brown in the following theorem. Theorem 3.2. [BaB Inferred Cuts Bound Propagation]. Given any BaB split set Z, optimizable parameters 0 ≤ α(i) j ≤ 1 and β, µ, τ ≥ 0, π (i) j ⋆ is a function of Q (i) :,j : g(α, β, µ, τ ) = -ϵ∥ν (1)⊤ W (1) x 0 ∥ 1 - L i=1 ν (i)⊤ b (i) -β ⊤ d + L-1 i=1 j∈I (i) h (i) j (β)where variables ν (i) are obtained by propagatingν (L) = -1 throughout all i ∈ [L-1]: ν (i) j = ν (i+1)⊤ W (i+1) :,j -β ⊤ (H (i) :,j + G (i) :,j ), j ∈ I +(i) ν (i) j = ν (i+1)⊤ W (i+1) :,j -β ⊤ (H (i) :,j + G (i) :,j ) + µ (i) j , j ∈ Z +(i) , ν (i) j = -β ⊤ H (i) :,j , j ∈ I -(i) , ν (i) j = -β ⊤ H (i) :,j -τ (i) j , j ∈ Z -(i) , ν (i) j = π (i) j ⋆ + α (i) j [ν (i) j ] --β ⊤ H (i) :,j , j ∈ I (i) \ Z (i)Here, νare defined for each initially unstable neuron that has not been split:j ∈ I (i) \ Z (i), and h (i) j (β) is defined for all unstable neurons j ∈ I (i) .[ν(i) j ] + := max(ν (i+1)⊤ W (i+1) :,j -β ⊤ G (i) :,j , 0), [ν (i) j ] -:= min(ν (i+1)⊤ W (i+1) :,j -β ⊤ G (i) :,j , 0) π (i) j ⋆ := max min u (i) j [ν (i) j ] + -β ⊤ Q (i) :,j u (i) j -l (i) j , [ν (i) j ] + , 0 , j ∈ I (i) \ Z (i) h (i) j (β) :=      l (i) j π (i) j ⋆ if l (i) j [ν (i) j ] + ≤ β ⊤ Q (i) :,j ≤ u (i) j [ν (i) j ] + and j ∈ I (i) \ Z (i) , 0 if β ⊤ Q (i) :,j ≥ u (i) j [ν (i) j ] + or j ∈ Z -(i) β ⊤ Q (i) :,j if β ⊤ Q (i) :,j ≤ l (i) j [ν (i) j ] + or j ∈ Z +(i)Proof in Appendix B.2. The brown-highlighted modifications ensure that the bound propagation correctly accounts for the influence of the fixed ReLU indicator z variables-resulting from branching decisions in the BaB process-on each layer's coefficients and biases. Notably, if we remove all cutting planes, this propagation method reduces to β-CROWN [54] . In this context, the new dual variables µ and τ correspond to the dual variable β used for x splits in β-CROWN. To handle splits, we only need to specify the sets Z +(i) and Z -(i) for each layer. By adjusting the dual variables and functions to reflect the fixed states of certain neurons, the extended bound propagation maintains tightness and correctness in the computed bounds.Theorem 3.2 allows us to use the cheap bound propagation method to search the BaB tree quickly to discover UNSAT paths to generate BaB inferred cuts by Proposition 3.1. However, our second key observation is that naively inferred cuts will not be beneficial in a regular BaB search process, illustrated in Fig. 2a , for example, all the subproblems after the split x 1 ≥ 0 (all nodes on the right after the first split) imply z 1 = 1, and thus z 1 + z 3 ≥ 1 always holds. Thus, we have to strengthen these cuts to make them more effective. We propose the Branch-and-bound Inferred Cut with COnstraint Strengthening (BICCOS) to solve this.(a) Based on the UNSAT path {x1 ≤ 0, x3 ≤ 0}, we can infer the cut 3 as -z1 -z3 ≤ -1 ⇒ z1 + z3 ≥ 1. However, none of the other subproblems would violate this constraint anyway, so the bounds do not improve.(b) Starting from the UNSAT path {x1 ≤ 0, x5 ≤ 0, x7 ≥ 0}, {x1 ≤ 0} is not actually needed, as {x5 ≤ 0, x7 ≥ 0} is sufficient to prove that this subproblem is UNSAT. We can infer a new cut z7 -z5 ≥ 1, (c) The root node is split multiple ways. In the sub-tree where the root node is split on x1, we extract the cut z1 + z3 ≥ 1. This cut is then applied to all other sub-trees as well.In the sub-tree with the root node split on x8, inducing another cut z8 ≥ 1 that will be shared across sub-trees. In a known UNSAT subproblem with multiple branched neurons, it is possible that a subset of the branching neurons is sufficient to prove UNSAT, shown in Fig. 2b . By focusing on this subset, we can strengthen the BaB inferred cuts by reducing the number of z variables involved. From an optimization perspective, each cut corresponds to a hyperplane that separates feasible solutions from infeasible ones. Simplifying the cut by involving fewer z variables reduces the dimensionality of the hyperplane, making it more effective at excluding infeasible regions without unnecessarily restricting the feasible space. Thus, we can draw a corollary: Corollary 3.3. Formally, consider the two cuts from Eq. (3):i∈Z + 1 z i - i∈Z - 1 z i ≤ |Z + 1 | -1 (3.1) i∈Z + 2 z i - i∈Z - 2 z i ≤ |Z + 2 | -1 (3.2) If either Z + 1 ⊂ Z + 2 and Z - 1 ⊆ Z - 2 , or Z + 1 ⊆ Z + 2 and Z - 1 ⊂ Z - 2 ,then any assignment {z i } satisfying the cut associated with the smaller split set Z also satisfies the other cut. This implies that the cut with the smaller set is strictly stronger than the one with the larger set.Proof deferred to Appendix B.3. This demonstrates that cuts with fewer variables can be more powerful because they operate in lower-dimensional spaces, allowing the hyperplane to more effectively position itself to exclude infeasible regions. Now, the challenge is determining which unnecessary branches to remove to produce a cut with as few z variables as possible. An important observation from Theorem 3.2 is that the dual variables µ and τ , associated with the fixed ReLU indicators z ∈ Z +(i) and z ∈ Z -(i) respectively, reflect the impact of these fixed activations on the bound. Specifically, a positive dual variable µ > 0 for some z ∈ Z +(i) indicates that the fixed active state of these neurons contributes significantly to tightening the bound. Similarly, a positive τ > 0 for some z ∈ Z -(i) signifies that the fixed inactive neurons are influential in optimizing the bound. However, neurons with zero dual variables (µ = 0 or τ = 0) may not contribute to the current bound optimization. This observation suggests that these neurons might be candidates for removal to simplify the cut. But it's important to note that a zero dual variable does not guarantee that the corresponding neuron has no impact under all circumstances-it only indicates no contribution in the current optimization context. Simply removing all neurons with zero dual variables might overlook their potential influence in other parts of the search space or under different parameter settings. Therefore, the challenge lies in deciding which neurons with zero or negligible dual variables can be safely removed without significantly weakening the cut. This decision requires a careful heuristic that considers not only the current values of the dual variables but also the overall structure of the problem and the potential future impact of these neurons. By intelligently selecting which z variables to exclude, we aim to produce a stronger cut that is both effective in pruning the search space and efficient in computing. To do this, we use a heuristic to determine whether each neuron should be tentatively dropped from the list of constraints. Algorithm 1 shows the constraint strengthening with the neuron elimination heuristic. Neuron Elimination Heuristic for Constraint Strengthening First, we compute a heuristic influence score for each neuron to assess its impact on the verification objective. This score is based on the improvement in the lower bound of f ⋆ before and after introducing the neuron's split in the BaB tree. By recording the computed lower bounds at each node, we can measure how beneficial each constraint is to the verification process. Second, we rank the neurons according to their influence scores and tentatively drop those that contribute least to improving the lower bound. We will retain neurons whose corresponding Lagrange multipliers, µ or τ , are greater than zero. For neurons with µ or τ equal to zero, we remove a certain percentile of neurons with the lowest scores, as indicated by the "drop_percentage" parameter in Algorithm 1. When a neuron is dropped, its split is canceled. Then, we perform a re-verification step using only the reduced subset of constraints. This involves recomputing the lower bound on f ⋆ based solely on the selected constraints. If the verification still succeeds-that is, the lower bound remains non-negative-the reduced set induces a new cutting plane. This new cutting plane is applied to all subproblems within the BaB process after further strengthening. The sentence looks wrong. Do we add them right now? Or after further strenghthenining? Finally, we can iteratively repeat the process of reducing the constraint set, aiming to generate even stronger cuts. The process terminates when the property can no longer be verified with the current subset of constraints. This iterative refinement is designed to focus on the most influential neurons, potentially enhancing the efficiency of the verification. Once the new cuts determined, we merge pairs of cuts if possible (e.g. merging z 1 + z 2 ≥ 0 and z 1 -z 2 ≥ 0 to z 1 ≥ 0).Z new = ∅ 4: for i ∈ [|neuron_influence_scores|] do 5: if Ẑi ∈ T ∪ M ̸ = 0 or neuron_influence_scores i ≥ score_threshold then 6: Z new ← Z new ∪ Ẑi 7: f re-verification ← Solve_Bound(f, C cut ∪ Z new ) 8: if f re-verification ≥ 0 then 9: strengthened_cut ← Infer_Cut(Z new ) 10: C cut ← C cut ∪ {strengthened_cut} 11: C cut ← Constraint_Strengthening(f, f , D, Z new , C cut , drop_percentage) 12: C cut ← Merge_Cuts(C cut ) 13: return C cutMulti-Tree Search Traditionally, the BaB process generates a single search tree. We propose augmenting this approach by performing multiple BaB processes in parallel as a presolving step, with each process exploring a different set of branching decisions. At each branching point, we initialize multiple trees and apply various branching decisions simultaneously. While this initially increases the number of subproblems, the cutting planes generated in one tree are universally valid and can be applied to all other trees. These newly introduced cuts can help prove UNSAT for nodes in other trees, thereby inducing additional cutting planes and amplifying the pruning effect across the entire search space, illustrated in Fig. 2c . Since computational resources must be allocated across multiple trees, we prioritize nodes for further expansion that have the highest lower bound on the optimization objective. This strategy ensures that more promising trees receive more computational resources. After a predefined short timeout, we consolidate our efforts by pruning all but one of the trees and proceed with the standard BaB process augmented with BICCOS on the selected tree. We choose the tree that has been expanded the most frequently, as this indicates that its bounds are closest to verifying the property. BaB Tree Searching Strategy In the standard BaB process (e.g., in β-CROWN), branches operate independently without sharing information, so the order in which they are explored does not affect the overall runtime. For memory access efficiency, there is a slight preference for implementing BaB as a depth-first search (DFS), where constraints are added until unsatisfiability (UNSAT) can be proven [61, 54] . This approach focuses the search on deeper branches before returning to shallower nodes. However, in the context of BICCOS, our objective is to generate strong cutting planes that can prune numerous branches across different subproblems. To maximize the generality of these cutting planes, they need to be derived from UNSAT nodes with as few constraints as possible. While constraint strengthening techniques can simplify the constraints, this process is more straightforward when the original UNSAT node already has a minimal set of constraints. Even if only a few constraints are eliminated, the resulting cutting plane can significantly impact many other subproblems. To facilitate this, we propose performing the BaB algorithm using a breadth-first search (BFS) strategy. By exploring nodes that are closest to the root and have the fewest neuron constraints, we can generate more general and impactful cutting planes earlier in the search process. Algorithm 2 Branch-and-bound Inferred Cuts with Constraint Strengthening (BICCOS).Require: f : model; n: batch size; time out threshold1: D Unknown , f ← Init(f, ∅) 2: D Unknown , C inferred_cuts ← Multi_Tree_Search(f, ∅) 3: while |D Unknown | > 0 and not timed out do 4: (Z 1 , . . . , Z n ) ← Batch_Pick_Out BF S (D Unknown , n) 5: (Z - 1 , Z + 1 , . . . , Z - n , Z + n ) ← Batch_Split(Z 1 , . . . , Z n ) 6: (f Z - 1 , f Z + 1 , . . . , f Z - n , f Z + n ) ← Solve_Bound(f, C inferred_cuts , Z - 1 , Z + 1 , . . . , Z - n , Z + n ) 7: D UNSAT ← Domain_Filter UNSAT ([f Z - 1 , Z - 1 ], [f Z + 1 , Z + 1 ], . . . , [f Z + n , Z + n ]) 8:for all D i ∈ D UNSAT do 9:C inferred_cuts ← Constraint_Strengthening(f, f i , D i , drop_percentage) 10: D Unknown ← D Unknown Domain_Filter Unknown ([f Z - 1 , Z - 1 ], [f Z + 1 , Z + 1 ], . . . , [f Z + n , Z + n ]) 11: return UNSAT if |D Unknown | = 0 else UnknownAlgorithm 2 summarizes our proposed BICCOS algorithm, with the modifications to the standard BaB algorithm highlighted in brown. First (line 2), instead of exploring a single tree, we explore multiple trees in parallel as a presolving step. This process may involve constraint strengthening and utilizes cut inference analogous to the procedures in lines 3-15 of the algorithm. After several iterations, we prune all but one of the trees. From this point forward, only the selected tree is expanded further, following the regular BaB approach. Until all subdomains of this tree have been verified, BICCOS selects batches of unverified subdomains add additional branching decisions, and attempt to prove the verification property. Unlike regular BaB, it then applies constraint strengthening to all identified UNSAT nodes and infers the corresponding cutting planes. These cutting planes are added to all currently unverified subdomains, potentially improving their lower bounds enough to complete the verification process. If BICCOS fails to identify helpful cutting planes, it effectively behaves like the regular BaB algorithm. We have implemented BICCOS in the α,β-CROWN toolbox. Notably, the cuts found by BICCOS are compatible with those from MIP solvers in GCP-CROWN, and all cuts can be combined in cases where MIP cuts are beneficial. 
experiments: 
 We evaluate our verifier, BICCOS, on several popular verification benchmarks from VNN-COMP [4, 40, 10] and on the SDP-FO benchmarks used in multiple studies [15, 54, 41] . In the following discussion, α,β-CROWN refers to the verification tool that implements various verification techniques, while β-CROWN and GCP-CROWN denote specific algorithms implemented within α,β-CROWN.To ensure the comparability of our method's effects and to minimize the influence of hardware and equipment advances, we rerun β-CROWN and GCP-CROWN with MIP cuts for each experiment. The increased timeout for MN-BaB may increase the percentage of verified instances. However, we can still achieve better verified accuracy than all other baselines. Other results are reported from [61] .Additionally, we use the same BaB algorithm as in β-CROWN and employ filtered smart branching (FSB) [16] as the branching heuristic in all experiments. Note that in experiments GCP-CROWN refers to GCP-CROWN solver with MIP cuts. We also conduct ablation studies to identify which components of BICCOS contribute the most, including analyses of verification accuracy & time, number of cuts generated, and number of domains visited. Experimental settings are described in Appendix C.1.We first evaluate BICCOS on many challenging benchmarks with large models, including two VNN-COMP 2024 benchmarks: cifar100-2024 and tinyimagenet-2024; two VNN-COMP 2022 benchmarks: cifar100-tinyimagenet-2022 and oval22. Shown in Table 1 , our proposed method, BICCOS, outperforms most other verifiers on the tested benchmarks, achieving the highest number of verified instances in four benchmark sets. BICCOS consistently outperforms the baseline α, β-CROWN verifier (the β-CROWN and GCP-CROWN (MIP cuts) lines), verifying more instances across almost all benchmark sets. In particular, GCP-CROWN with MIP cuts cannot scale to the larger network architectures in the cifar100 and tinyimagenet benchmarks with network sizes between 14.4 and 31.6 million parameters, due to its reliance on an MIP solver. BICCOS, on the other hand, can infer cutting planes without the need for an MIP solver and noticeably outperforms the baseline on cifar100 and tinyimagenet. Note that the increase in average runtime (e.g., on the cifar100-tinyimagenet-2022 benchmark) is expected. The instances that could not be verified at all previously but can be verified using BICCOS tend to require runtimes that are below the timeout but above the baseline's average runtime.We further evaluated BICCOS, on the challenging SDP-FO benchmarks introduced in previous studies [15, 54] . These benchmarks consist of seven predominantly adversarial trained MNIST and CIFAR models, each containing numerous instances that are difficult for many existing verifiers. Our results, detailed in Table 2 , demonstrate that BICCOS significantly improves verified accuracy across all the tested models when compared to current stateof-the-art verifiers. On both MNIST and CIFAR dataset, BICCOS not only surpasses the performance of methods like β-CROWN and GCP-CROWN on the CNN-A-Adv model but also approaches the empirical robust accuracy upper bound, leaving only a marginal gap. A slight increase in average time in some cases is attributed to the higher number of solved instances. Ablation Studies on BICCOS Components. To evaluate the contributions of individual components of BICCOS, we performed ablation studies summarized in Table 3 . The BICCOS base version with BaB inferred cuts and constraint strengthening already shows competitive performance in many models. Cuts from MIP solvers are compatible with BICCOS and can be added for smaller models that can be handled by MIP solver. Integrating Multi-Tree Search (MTS) significantly boosts performance. On the CIFAR CNN-B-Adv model, verified accuracy rises to 54.5%, outperforming GCP-CROWN with MIP cuts's 49%. We also design an adaptive BICCOS configuration (BICCOS auto), which automatically turns on MTS and/or MIP-based cuts according to neural network and verification problem size and quantity, achieves the highest verified accuracies across models and is used as the default option of the verifier when BICCOS is enabled. A detailed table with the numbers of cuts and domains visited is provided in Appendix C.2. 
related work: 
 Our work is based on the branch and bound framework for neural network verification [12, 17, 59, 28, 54, 16, 37, 21] , which is one of the most popular approaches that lead to state-of-the-art results [4, 10, 40] . Most BaB-based approaches do not consider the correlations among subproblems -for example, in β-CROWN [54] , the order of visiting the nodes in the BaB search tree does not change the verification outcome as the number of leaf nodes will be the same regardless of how the leaves are split. Our work utilizes information on the search tree and can gather more effective cuts when shallower nodes are visited first.Exploring the dependency or correlations among neurons has also been identified as a potential avenue to enhance verification bounds. While several studies have investigated this aspect [2, 16, 42, 50] , their focus has primarily been on improving the bounding step without explicitly utilizing the relationships among ReLUs during the branching process. Venus [9] considers the implications among neurons with constraints similar to our cutting planes. However, their constraints were not discovered using the verified subproblems during BaB or multi-tree search, and cannot be strengthened. On the other hand, cutting plane methods encode dependency among neurons as general constraints [61, 35] , and our work developed a new cutting plane that can be efficiently constructed and strengthened during BaB, the first time in literature.In addition, some NN verifiers are based on the satisfiability modulo theories (SMT) formulations [32, 46, 19, 36] , which may internally use an SAT-solving procedure [8] such as DPLL [22] or CDCL [38] . These procedures may discover conflicts in boolean variable assignments, corresponding to eliminating certain subproblems in BaB. However, they differ from BICCOS in two significant aspects: first, although DPLL or CDCL may discover constraints to prevent some branches with neurons involved in these constraints, they cannot efficiently use these constraints as cutting planes that may tighten the bounds for subproblems never involving these neurons; second, DPLL or CDCL works on the abstract problem where each ReLU is represented as a boolean variable, and cannot take full advantage of the underlying bound propagation solver to strengthen constraints as we did in Alg. 1. Based on our observation in Sec. 3, the constraints discovered during BaB are often unhelpful without strengthening unless in a different search tree, so their effectiveness is limited. However, the learned conflicts can be naturally translated into cuts 3, making this a future work.More related works on SMT, MIP solvers, nogood learning and cutting plane method in VNN [18, 45, 26, 19, 11, 2, 47, 52, 30, 61, 35] are discussed in Section D. 
conclusion: 
 We exploit the structure of the NN verification problem to generate efficient and scalable cutting planes, leveraging neuron relationships within verified subproblems in a branch-and-bound search tree. Our experimental results demonstrate that the proposed BICCOS algorithm achieves very good scalability while outperforming many other tools in the VNN-COMP, and can solve benchmarks that existing methods utilizing cutting planes could not scale to. Limitations are discussed in Appendix E. 
broader impacts: 
 Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?Answer: [Yes]Justification: Societal impacts have been discussed explicitly in Section 7.Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact.• Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?Answer: [NA] Justification: No data or models are released.Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort.12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?Answer: [Yes]Justification: We've cited the sources of the benchmarks we used, such as those from the VNN-COMP.Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided.• If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode.com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset. • For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. • If this information is not available online, the authors are encouraged to reach out to the asset's creators. 
new assets: 
 Question: Are new assets introduced in the paper well documented and is the documentation provided alongside the assets?Answer: [NA] Justification: No new assets are introduced in this paper.Guidelines:• The answer NA means that the paper does not release new assets.• Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc. • The paper should discuss whether and how consent was obtained from people whose asset is used. • At submission time, remember to anonymize your assets (if applicable). You can either create an anonymized URL or include an anonymized zip file. 
crowdsourcing and research with human subjects: 
 Question: For crowdsourcing experiments and research with human subjects, does the paper include the full text of instructions given to participants and screenshots, if applicable, as well as details about compensation (if any)?Answer: [NA]Justification: The paper does not involve crowdsourcing nor research with human subjects.Guidelines:• The answer NA means that the paper does not involve crowdsourcing nor research with human subjects. • Including this information in the supplemental material is fine, but if the main contribution of the paper involves human subjects, then as much detail as possible should be included in the main paper. • According to the NeurIPS Code of Ethics, workers involved in data collection, curation, or other labor should be paid at least the minimum wage in the country of the data collector. 
institutional review board (irb) approvals or equivalent for research with human subjects: 
 Question: Does the paper describe potential risks incurred by study participants, whether such risks were disclosed to the subjects, and whether Institutional Review Board (IRB) approvals (or an equivalent approval/review based on the requirements of your country or institution) were obtained?Answer: [NA]Justification: The paper does not involve crowdsourcing nor research with human subjects.Guidelines:• The answer NA means that the paper does not involve crowdsourcing nor research with human subjects. • Depending on the country in which research is conducted, IRB approval (or equivalent) may be required for any human subjects research. If you obtained IRB approval, you should clearly state this in the paper. 
 
 Appendix: The MIP Formulation The mixed integer programming (MIP) formulation is the root of many NN verification algorithms. Given the ReLU activation function's piecewise linearity, the model requires binary encoding variables, or ReLU indicators z only for unstable neurons. We formulate the optimization problem aiming to minimize the function f (x), subject to a set of constraints that encapsulate the DNN's architecture and the perturbation limits around a given input x, as follows:EQUATIONEQUATIONEQUATIONEQUATIONx(i)EQUATIONEQUATIONx(i) j ≤ uEQUATIONEQUATIONEQUATIONx(i)EQUATIONx(i)EQUATIONHere, the set J (i) comprises all neurons in the layer i, which are further categorized into three distinct classes: 'active' (I +(i) ), 'inactive' (I -(i) ), and 'unstable' (I (i) ); we further let l(i) j = min x∈X f (i) j (x), u (i) j = max x∈X f (i) j (x), ∀j ∈ J (i) , i ∈ [L -1].The MIP approach is initialized with pre-activation bounds l (i) ≤ x (i) ≤ u (i) for each neuron within the feasible set X , across all layers i. These bounds can be calculated recursively through the MIP from the first layer to the final layer. However, MIP problems are generally NP-hard as they involve integer variables.The LP and Planet relaxation By relaxing the binary variables 12 to z(i) j ∈ [0, 1], j ∈ I (i) , i ∈ [L -1],we can get the LP relaxation formulation. By replacing the constraints in 10, 11, 12 withEQUATIONwe can eliminate the z variables and get the well-known Planet relaxation formulation. Both of these two relaxations are solvable in polynomial time to yield lower bounds.Lemma A.1. In the LP relaxation, splitting an unstable ReLU neuron (i, j) based on z(i) j = 0 is equivalent to setting x (i) j ≤ u (i) j =0 in the Planet relaxation with the relaxed variable z ∈ [0, 1] projected out. Correspondingly, splitting based on z(i) j = 1 is equivalent to setting x (i) j ≥ l (i) j = 0.Proof: An unstable neuron (i, j) is one where the pre-activation bounds satisfy l (i) j < 0 < u (i) j . It could be represented as the following system in LP relaxation: 8, 10, 11, 12, and the system in Planet relaxation: 8, 15. We will now analyze the two cases of fixing z (i) j to 0 and 1 in the LP relaxation and show their equivalence to modifying the bounds u (i) j and l (i) j in the Planet relaxation.To derive the bound propagation, first, we assign Lagrange dual variables to each non-trivial constraint in LP relaxation with any BaB split set Z. Next, we analyze how splitting on the ReLU indicator z influences the generation of these dual variables. This analysis helps us determine the impact of the splits on the dual formulation. Then, we formulate the Lagrangian dual as a min-max problem. By applying strong duality and eliminating the inner minimization problem, we can simplify the dual formulation. Finally, this results in a dual formulation that we use to perform bound propagation effectively.Theorem 3.2. Given any BaB split set Z, optimizable parameters 0 ≤ α(i) j ≤ 1 and β, µ, τ ≥ 0, π (i) j ⋆ is a function of Q (i) :,j : g(α, β, µ, τ ) = -ϵ∥ν (1)⊤ W (1) x 0 ∥ 1 - L i=1 ν (i)⊤ b (i) -β ⊤ d + L-1 i=1 j∈I (i) h (i) j (β)where variables ν (i) are obtained by propagating ν (L) = -1 throughout all i ∈ [L-1]:ν (i) j = ν (i+1)⊤ W (i+1) :,j -β ⊤ (H (i) :,j + G (i) :,j ), j ∈ I +(i) ν (i) j = ν (i+1)⊤ W (i+1) :,j -β ⊤ (H (i) :,j + G (i) :,j ) + µ (i) j , j ∈ Z +(i) , ν (i) j = -β ⊤ H (i) :,j , j ∈ I -(i) , ν (i) j = -β ⊤ H (i) :,j -τ (i) j , j ∈ Z -(i) , ν (i) j = π (i) j ⋆ + α (i) j [ν (i) j ] --β ⊤ H (i) :,j , j ∈ I (i) \ Z (i) Here ν(i) j , π (i) j ⋆ and τ (i)j are defined for each unstable and without split neuron j ∈ I (i) \ Z (i) , and h (i) j (β) is defined for all unstable neurons j ∈ I (i) .[ν(i) j ] + := max(ν (i+1)⊤ W (i+1) :,j -β ⊤ G (i) :,j , 0), [ν (i) j ] -:= min(ν (i+1)⊤ W (i+1) :,j -β ⊤ G (i) :,j , 0) π (i) j ⋆ = max min u (i) j [ν (i) j ] + -β ⊤ Q (i) :,j u (i) j -l (i) j , [ν (i) j ] + , 0 , j ∈ I (i) \ Z (i) h (i) j (β) =      l (i) j π (i) j ⋆ if l (i) j [ν (i) j ] + ≤ β ⊤ Q (i) :,j ≤ u (i) j [ν (i) j ] + and j ∈ I (i) \ Z (i) , 0 if β ⊤ Q (i) :,j ≥ u (i) j [ν (i) j ] + or j ∈ Z -(i) β ⊤ Q (i) :,j if β ⊤ Q (i) :,j ≤ l (i) j [ν (i) j ] + or j ∈ Z +(i)Proof: First we write down the primal formulation, and assign the Lagrange multipliers:EQUATIONEQUATIONx(i)EQUATIONL-1 i=1H (i) x (i) + G (i) x(i) + Q (i) z (i) ≤ d ⇒ β ∈ R N + (2)Note that for some constraints, their dual variables are not created because they are trivial to handle in the steps. And from Lemma A.1, some unstable neuron constraints 8, 9, 10, 11 will be eliminated during BaB with split on z, i.e. when z (i) j = 1, the unstable neuron constraints 8 will be reduced tox(i) j = x (i) j ≥ 0 ⇒ µ (i)j ∈ R + , other dual variables for constraints 9, 10, 11 will not be generated, and when z (i) j = 0, only τ (i) j ∈ R + will be generated. Rearrange the equation and swap the min and max (strong duality) gives us:f ⋆ = max ν,µ,τ ,γ,π,β min x, x,z(ν (L) + 1)x (L) -ν (1)⊤ W (1) x(0)+ L-1 i=1 j∈I +(i) ν (i) j + β ⊤ H (i) :,j -ν (i+1)⊤ W (i+1) :,j + β ⊤ G (i) :,j x (i) j + L-1 i=1 j∈Z +(i) ν (i) j + β ⊤ H (i) :,j -ν (i+1)⊤ W (i+1) :,j + β ⊤ G (i) :,j -µ (i) j x (i) j + L-1 i=1 j∈I -(i) ν (i) j + β ⊤ H (i) :,j x (i) j + L-1 i=1 j∈Z -(i) ν (i) j + β ⊤ H (i) :,j + τ (i) j x (i) j + L-1 i=1 j∈I (i) ν (i) j + β ⊤ H (i) :,j + τ (i) j -π (i) j x (i) j + -ν (i)⊤ W (i) :,j -µ (i) j -τ (i) j + γ (i) j + π (i) j + β ⊤ G (i) :,j x(i) j + -u (i) j γ (i) j -l (i) j π (i) j + β ⊤ Q (i) :,j z (i) j - L i=1 ν (i)⊤ b (i) + L-1 i=1 j∈I (i) \Z (i) π (i) j l (i) j -β ⊤ d s.t. x 0 -ϵ ≤ x ≤ x 0 + ϵ; 0 ≤ z (i) j ≤ 1, j ∈ I (i) \ Z (i) z (i) j = 1, j ∈ Z +(i) z (i) j = 0, j ∈ Z -(i) µ ≥ 0; τ ≥ 0; γ ≥ 0; π ≥ 0; β ≥ 0Here W (i+1) :,j denotes the j-th column of W (i+1) . Note that for the term involving j ∈ I +(i) ∪ Z +(i) we have replaced x(i) with x (i) to obtain the above equation. For the term x (i) j , j ∈ I -(i) ∪ Z -(i) it is always 0 so it does not appear. Then solving the inner minimization gives us the dual formulation:EQUATIONEQUATIONEQUATIONEQUATIONEQUATIONEQUATIONEQUATIONwhere h(i) j in the objective 21 is:h (i) j = min z (i) j {π (i) j l (i) j + (-u (i) j γ (i) j -l (i) j π (i) j + β ⊤ Q (i) :,j )z (i) j } (29) =      β ⊤ Q (i) :,j if j ∈ Z +(i) 0 if j ∈ Z -(i) π (i) j l (i) j -ReLU(u (i) j γ (i) j + l (i) j π (i) j -β ⊤ Q (i) :,j ) if j ∈ I (i) \ Z (i) (30)The ReLU(•) term comes from minimizing over z (i) j with the constraint 0 ≤ z (i) j ≤ 1. And when splitting on z ∈ Z (i) , as we discussed above, based on Lemma A.1, there will be no π(i) j , γ (i) jassigned for the constraints. The ∥ • ∥ 1 comes from the dual norm form minimizing over the infinite norm of the input x with the constraint x 0 -ϵ ≤ x ≤ x 0 + ϵ.Thus, the rest of the proof follows from [61, Lemma A.1, Theorem 3.1], which completes the proof of Theorem 3.2.Proof. Let us consider any assignment of the variables {z i } where z i ∈ {0, 1} that satisfies cut 3.1. We aim to show that this assignment also satisfies cut 3.2.Since Z + 1 ⊂ Z + 2 , there exists at least one neuron k such that k ∈ Z + 2 but k / ∈ Z + 1 . Let Z (∆) + = Z + 2 \ Z + 1 denote the additional neurons in the larger cut 3.2. Similarly, define Z (∆) - = Z - 2 \ Z - 1 .In cut 3.2, the left-hand side (LHS) can be expressed as:LHS 3.2 =    i∈Z + 1 z i + i∈Z (∆) + z i    -    i∈Z - 1 z i + i∈Z (∆) - z i   Similarly, the right-hand side (RHS) of cut 3.2 is:RHS 3.2 = |Z + 1 | + |Z (∆) + | -1Subtracting Eq. 3.1 from cut 3.2, we get:LHS 3.2 -   i∈Z + 1 z i - i∈Z - 1 z i   =    i∈Z (∆) + z i - i∈Z (∆) - z i    RHS 3.2 -|Z + 1 | -1 = |Z (∆) + |Therefore, the difference between the LHS and RHS of the two cuts is:   i∈Z (∆) + z i - i∈Z (∆) - z i    ≤ |Z (∆) + |Since each z i ∈ {0, 1}, the maximum value of i∈Z (∆)+ z i is |Z (∆)+ |, and the minimum value of i∈Z (∆) -z i is 0. Thus, the maximum possible value of the LHS difference is|Z (∆)+ |, which equals the RHS difference.i for i ∈ Z (∆) + ∪ Z (∆)-, the inequality:   i∈Z (∆) + z i - i∈Z (∆) - z i    ≤ |Z (∆) + |is always satisfied. This means that satisfying cut 3.1 ensures that cut 3.2 is also satisfied.Conversely, consider an assignment where cut 3.2 is satisfied but cut 3.1 is violated. This can happen if the additional variables in Z (∆) + and Z (∆) -compensate for the violation in the original variables. For instance, setting z i = 1 for all i ∈ Z (∆) + and z i = 0 for all i ∈ Z (∆) -can decrease the LHS of cut 3.2, making it easier to satisfy even if cut 3.1 is not satisfied. Therefore, the feasible region defined by cut 3.1 is a subset of the feasible region defined by cut 3.2, confirming that cut 3.1 is stronger.Our experiments are conducted on a server with an Intel Xeon 8468 Sapphire CPU, one NVIDIA H100 NVL GPU (96 GB GPU memory), and 480 GB CPU memory. Our implementation is based on the open-source α,β-CROWN verifier1 with cutting plane related code added. All experiments use 24 CPU cores and 1 GPU. The MIP cuts are acquired by the cplex [31] solver (version 22.1.0.0).We use the Adam optimizer [33] to solve both α, β, µ, τ . For the SDP-FO benchmarks, we optimize those parameters for 20 iterations with a learning rate of 0.1 for α and 0.02 for β, µ, τ . We decay the learning rates with a factor of 0.98 per iteration. The timeout is 200s per instance. For the VNN-COMP benchmarks, we use the same configuration as α,β-CROWN used in the respective competition and the same timeouts. During constraint strengthening, we set drop_percentage = 50%. We only perform one round of strengthening, with no recursive strengthening attempts. We perform constraint strengthening for the first 40 BaB iterations. For multi-tree search, we perform 5 branching iterations, where we each time pick the current best 50 domains and split them to generate 400 new sub-domains.The ablation studies provide insights into the impact of different components of the BICCOS algorithm on the verification process, focusing on the average number of branches (domains) explored and the number of cuts generated, as shown in Table 4 . A lower number of branches typically indicates a more efficient search process, leading to computational savings and faster verification times.Across the benchmarks, we observe that the BICCOS configurations, particularly BICCOS (auto), often explore fewer branches compared to the baseline β-CROWN and GCP-CROWN methods. For instance, on the CIFAR CNN-A-Adv model, BICCOS (auto) reduces the average number of branches from 63,809.77 (for β-CROWN) and 28,558.70 (for GCP-CROWN) down to 9,902.96. This reduction is attributed to the cutting planes introduced by the BICCOS algorithm, which tighten the relaxations and more effectively prune suboptimal regions of the search space.The multi-tree search (MTS) strategy, which explores multiple branch-and-bound trees in parallel, demonstrates its effectiveness in improving verification efficiency. While MTS may increase the total number of branches explored-since domains from multiple trees are counted-the exploration within each tree is optimized, leading to faster convergence and reduced overall computation time. We also design an adaptive BICCOS configuration (BICCOS (auto)), which automatically enables MTS and/or Mixed Integer Programming (MIP)-based cuts based on the neural network and verification problem size. BICCOS (auto) achieves the highest verified accuracies across models and is used as the default option of the verifier when BICCOS is enabled. However, it is worth noting that on certain benchmarks, such as the CIFAR CNN-A-Mix-4 model, the number of branches explored by different BICCOS configurations does not always decrease compared to the baselines. In some cases, the base BICCOS version explores more branches than β-CROWN. This could be attributed to the models' inherent complexity and the nature of the verification problem, where the benefits of the cutting planes and MTS may be less pronounced.Overall, the analysis of the average number of branches in the ablation studies highlights the effectiveness of the BICCOS algorithm and its components in improving the efficiency of the verification process. The combination of cutting planes, multi-tree search, and other optimizations enables BICCOS to achieve high verified accuracy while often exploring fewer branches compared to baseline methods, ultimately leading to computational savings and faster verification times.To evaluate the performance of the BICCOS cuts in MIP-based solvers, Fig 3 shows comparison with Venus2 [9, 34] . 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.We note that the multi-tree search (MTS) and cut strengthening procedure incur additional overheads compared to the baseline verifiers shown as Fig 4 . The MTS has about 2 -10 seconds overhead in the benchmarks we evaluated, which may increase the verification time of very easy instances that can be sequentially immediately verified in branch and bound. The BICCOS cut strengthening is called during every branch-and-bound iteration, but its accumulative cost is about 3 -20 seconds for hard instances in each benchmark, which run a few hundred branch-and-bound iterations. We note that typically, the performance of the verifier is gauged by the number of verified instances within a fixed timeout threshold, thus when the threshold is too low, the added cutting planes may not have time to show their performance gains due to the lack of sufficient time for the branch-and-bound procedure.We note that such a shortcoming is also shared with other verifiers which require additional steps for bound tightening; for example, the GCP-CROWN verifiers have the extra overhead of a few seconds of calling and retrieving results from the MIP solver, even when the MIP solver is running in parallel with the verifier. The final verified accuracy can justify whether the overhead is worth paying.Furthermore, nogood learning and conflict analysis techniques from constraint programming and SAT solving have been adapted to neural network verification to improve solver efficiency [18, 45, 26, 19 , Figure 3 : Comparison of Venus2 and MILP with BICCOS. For a fair comparison, we do not use GPUaccelerated bound propagation but use a MILP solver (same as in Venus2) to solve the verification problem with our BICCOS cuts. In all 4 benchmarks, MILP with BICCOS cuts is faster than Venus (MILP with their proposed cuts), illustrating the effectiveness. Note that Venus2 can hardly scale to larger models presented in our paper, such as those on cifar100 and tinyimagenet datasets. 11]. These methods record conflicts encountered during the search-known as nogoods-to prevent revisiting the same conflicting states, effectively pruning the search space. While nogood learning can reduce redundant exploration, it typically operates on discrete abstractions of neural networks, representing ReLU activations as boolean variables. This abstraction limits their ability to leverage the properties of neural network activations. In contrast, our approach not only identifies conflicts but also translates them into cutting planes within the continuous relaxation of the verification problem. This allows us to tighten the bounds for unexplored subproblems, enhancing the overall efficiency of the verification process.Mixed Integer Programming (MIP) solvers, such as cplex [31] and gurobi [27] , have also been applied to neural network verification by formulating the problem as a mixed-integer linear program [6] . These solvers inherently utilize branch-and-bound algorithms and incorporate sophisticated cutting plane generation techniques to tighten the feasible region. However, in practice, applying general-purpose MIP solvers to large-scale neural networks presents significant challenges. For instance, in our experiments with benchmarks like CIFAR100 and Tiny-ImageNet-where network sizes range from 5.4 million to over 30 million parameters-cplex was unable to solve the initial LP relaxation within the 200-second timeout threshold. As a result, the branch-and-bound process and cut generation did not commence, underscoring the limitations of using off-the-shelf MIP solvers for large-scale neural network verification tasks.In terms of cutting plane methods, prior work has explored integrating cuts derived from convex hull constraints within MIP formulations of neural networks [2, 47, 52, 30, 61, 35] . For example, [2] propose cutting planes that tighten the relaxation of ReLU constraints in MILP formulations, improving solution quality. While these methods can enhance optimization, they often incur significant computational overhead in generating and integrating cuts and rely heavily on the capabilities of the underlying MIP solver. In contrast, our approach develops new cutting planes that can be efficiently constructed and strengthened during the branch-and-bound process, leveraging the problem's structure to achieve better scalability and performance. For easy instances that can be verified within a few seconds (bottom parts of the figures), the increase of verification time with BICCOS is negligible.Our work bridges the gap between conflict analysis methods like nogood learning and cutting plane techniques by integrating conflict-derived constraints into the continuous relaxation of the verification problem. This integration allows for both effective pruning of the search space and tightening of the problem relaxation, leading to improved verification efficiency. By tailoring our approach to the specifics of neural network verification, we address the limitations observed in general-purpose MIP solvers when applied to large-scale networks, offering a scalable and efficient solution.The approach relies on the piecewise linear nature of ReLU networks (same as most other papers in BaB), and its applicability to other types of neural architectures requires further extension such as those in [48] . Additionally, the effectiveness of the generated cutting planes may vary depending on the specific structure and complexity of the neural network being verified, and there may be cases where the algorithm's performance gains are less pronounced.Question: Does the paper provide open access to the data and code, with sufficient instructions to faithfully reproduce the main experimental results, as described in supplemental material? Answer: [Yes] Justification: BICCOS has been added to the α,β-CROWN toolkit. Guidelines:• The answer NA means that paper does not include experiments requiring code. Guidelines:• The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.• If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics. • The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction).38th Conference on Neural Information Processing Systems (NeurIPS 2024).https://github.com/huanzhang12/alpha-beta-CROWN 


Decision: The submission has received mixed ratings after extensive post-rebuttal discussions. One of the referees recommends rejection based on the weakness of the cuts that are generated by the proposed method, as well as incremental improvements over GCP-CROWN. However, the other referees recommend acceptance, and suggest acknowledging the aforementioned weaknesses in the revised version of the submission. The authors are advised to take into account the detailed reviews as well as the clarifications provided in the rebuttal when preparing the final manuscript.

Reviews: review: paper_summary: paper_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.
strength_weakness: strength_weakness: 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: 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.
limitations: limitations: The Limitations section is reasonable, covering cases where this approach does not work well.
paper_summary: paper_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.
strength_weakness: strength_weakness: - 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: 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?
limitations: limitations: Limitations are sufficiently addressed.
paper_summary: paper_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.
strength_weakness: strength_weakness: **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: 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?
limitations: limitations: Limitations are appropriately addressed in the conclusions.
paper_summary: paper_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.
strength_weakness: strength_weakness: 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: 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?
limitations: limitations: The authors were very upfront about limitations to their work.

Comments: title: Last comment
Feedback on Q3 and Q6: Enhancements and Clarifications
Follow up 2
We greatly appreciate your constructive feedback! Further clarifications on Q3
Discussions on our presentations and results (part 2/2)
Discussions on our presentations and results (part 1/2)
Follow up comments
Thank you for your response
We thank the reviewers again and please let us know if you have any further questions before the discussion is closed
Thank you for the review
comment: This is a good discussion of [6], which in a sense extends Anderson et al (to save you some space). The description of [5] is not correct, but this is a lesser important reference, so don’t worry about it.
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.
I appreciate the explanation regarding Q3. It would indeed be better to talking about branching on $z$ directly in the paper, but I would also recommend adding the comments about how this is done with the triangle relaxation in the appendix - with a brief mention in the paper to them.

Regarding Q6, please make sure to revisit the references to explain them properly.
We greatly appreciate your timely response and found your questions and feebacks very insightful. To follow up on your questions, we want to clarify more, especially on **Q3**.

Q1, Q2, Q5, Q6, Q8: Thank you for your valuable feedback. We will be sure to add/cite/rephrase our paper based on your suggestions here. They greatly helped us to improve our paper.

Q3: We apologize again for the confusion, and we provided a more detailed answer here since there is no character limit any more. In the formulation of many prior papers (for example, beta-CROWN, Wang et al. NeurIPS 2021), $z$ was not explicitly included in the optimization formulation. However, when $x$ is branched to $x \leq 0$ and $x \geq 0$ cases, **the optimization problem is also changed**, essentially equivalent to branching $z$, as detailed below.

For an unstable ReLU neuron, before branching, the ReLU function $y = ReLU(x)$ is relaxed using the "*triangle relaxation*":

$y \geq 0$  
$y \geq x$  
$y \leq \frac{u}{u -l} (x - l)$  

Where $l$ and $u$ are the bounds of ReLU input ("preactivation bounds"). Note that **this formulation is without $z$**, but it is equivalent to the formulation with $z$ but with the relaxed variable $0 \leq z \leq 1$ projected out, forming a linear relaxation of ReLU. (note that our paper used $\hat{x}$, but I used $y$ to make the response easier to read)

After branching, the neuron becomes a linear function in each branch. When $x \geq 0$, this ReLU neuron will be in the active region, and the **triangle relaxation is replaced by $y = x$**; when $x \leq 0$, the **triangle relaxation is replaced by $y = 0$** (following Beta-CROWN). So, the optimization formulation changed after branching on $x$. This is equivalent to branching on $z$: in the formulation where $z$ appears (Appendix A.1), when we set $z = 1$, removing redundant constraints will yield $y = x$; when we set $z = 0$, removing redundant constraints will yield $y = 0$.

So when we say we are branching on $x$, the optimization formulations will change after branching - **it is *not* simply applying the constraints $x \geq 0$ or $x \leq 0$ directly on the triangle relaxation**; that would be incorrect as you pointed out. This branching procedure will be the same as branching $z$. In our paper, our cutting plane actually requires the formulation with $z$ since cuts were added to these variables. We will follow your suggestion to say we branch on $z$ instead of $x$ to make the setting more clear, and also add the above discussion to the appendix to avoid future confusion.

Thank you again for your very constructive feedback. We hope all the questions have been addressed now, and we sincerely hope you can reevaluate our paper based on our response. Feel free to let us know if you have any additional questions for us.
(continued, part 2/2)

> 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.
> description of the overhead of the framework on easier properties

**We will add this paragraph, "Shortcomings and Overhead,"** to the experiment section of our paper:  
We note that the multi-tree search (MTS) and cut strengthening procedure incur additional overheads compared to the baseline verifiers. The MTS has about 2 - 10 seconds overhead in the benchmarks we evaluated, which may increase the verification time of very easy instances that can be sequentially immediately verified in branch and bound. The BICCOS cut strengthening is called during every branch-and-bound iteration, but its cost is *accumulatively* about 3 - 20 seconds for hard instances in each benchmark, which run a few hundred branch-and-bound iterations. We note that typically, the performance of the verifier is gauged by the number of verified instances within a fixed timeout threshold, thus when the threshold is too low, the added cutting planes may not have time to show their performance gains due to the lack of sufficient time for the branch-and-bound procedure. 

We note that such a shortcoming is also shared with other verifiers which require additional steps for bound tightening; for example, the GCP-CROWN verifiers have the extra overhead of a few seconds of calling and retrieving results from the MIP solver, even when the MIP solver is running in parallel with the verifier. The final verified accuracy can justify whether the overhead is worth paying.

> 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

> (the figure) would have read better in a log scale over time 

We have produced these figures with all baselines in log scale locally, but unfortunately we cannot update the figure on the rebuttal PDF anymore and NeurIPS disallows the use of external links. We will be sure to include these in our final revision. To describe these figures verbally, for easy instances (solved within a few seconds), Beta-CROWN is the fastest. GCP-CROWN has the overhead of initializing MIP solver and our method has the overhead of MTS, so they are slower on easy instances; however, on hard instances which distinguish the power of verifiers, BICCOS shows clear benefits (the BICCOS line is bent towards the lower right corner) on all benchmarks. With a log-scale, it is clear to show the overhead on the easy instances and the benefits on hard instances.

Thanks again for your valuable feedback. We want to emphasize that there is no technical or soundness concern in our paper, and the **presentation issues will be fixed in our final version, as we have detailed in our response**, especially on the presentations of the tables/figures and the discussions of the shortcomings and overhead. We sincerely hope you can reevaluate our paper based on our technical contribution, and we hope that these easy-to-fix problems will not become a roadblock to accepting our paper.
We are very grateful for your timely response. Following your constructive advice, we would like to clarify a bit more about the presentation of our paper and the significance of our results.

> the experimental improvements to be somewhat marginal

We want to point out that the room for improvement for many benchmarks is not big—the **verification lower bound is quite comparable to the PGD upper bound**, so a massive improvement cannot be shown if we directly read these numbers. For example, in Table 2, we have MNIST CNN-A-Adv (74.0% vs 76.5%), CIFAR CNN-A-Adv (49% vs 50%), CIFAR CNN-A-Adv-4 (48.5% vs 49.5%), and CIFAR CNN-A-Mix-4 (56.5% vs 57.5%). Although these standardized benchmarks have been widely used in the literature, they have only a few percentage points left for improvement.

In fact, if you look at the gap between the lower and upper bound, we did get a quite pronounced improvement. For example, for MNIST CNN-A-Adv, GCP-CROWN has a **4.5%** gap between lower and upper bound, but we have only **2.5%** gap. That is a ~44% improvement on reducing this gap. Also, in Table 1, on oval21, we completely **close the gap** between lower and upper bound; on cifar10-resnet, the number of unsolved instances (gap) is **reduced from 9 to 6** compared to GCP-CROWN; on cifar100-tinyimagenet, the gap is **reduced from 25 to 18**.

**The verification community has been working hard to close this gap** (see [ref. A] below, Intro section), and in fact, the few instances remaining in each benchmark reported here, are all very challenging ones. For example, in GCP-CROWN paper, which completely solved the oval20 benchmark (their Table 1), only improves the verified instances from 98% to 100% (CIFAR-10 Wide) and 97% to 100% (CIFAR-10 Base). Number-wise, it is just a "marginal" (a few percentage points) improvement similar to the improvements we report, **but it is actually quite a big achievement since no algorithm could solve these remaining hard instances**. Similarly, in [ref. A], which aims to improve the upper bound to close the gap, they also only demonstrated improvements on very few hard instances - **their improvement is less than 0.5%** if evaluated on the entire dataset as we did.

[ref. A] A Branch and Bound Framework for Stronger Adversarial Attacks of ReLU Networks, Zhang et al., ICML 2022

> the submission appears to be seeking to sweep the shortcomings of the full configuration under the rug.

> line 309 even states "The comprehensive BICCOS configuration, incorporating all optimizations, achieves the highest verified accuracies across models."

Following your suggestions, we will rephrase the sentence as "Our results show that the addition of BICCOS cuts is overall beneficial. When a MIP solver is feasible, BICCOS can be combined with the MIP cuts in GCP-CROWN to potentially further improve the verified accuracy of GCP-CROWN, demonstrating the quality and effectiveness of our cuts. When MTS is used, it may further improve the verified accuracy on some benchmarks, but the overhead of MTS may reduce the verified accuracy on some benchmarks."

We will also replace the numbers under the BICCOS column in Table 2 with the numbers with MTS and MIP cuts enabled (if an MIP solver can scale to this setting), even in the case where MTS slows down verification due to overhead. In fact, we have optimized our software further to reduce the overhead of MTS, and the potential overhead has now become smaller. Eventually, we will enable all BICCOS components to be the default in our to-be-released verifier. We will produce a message to users when MTS introduces too much overhead compared to the overall timeout threshold and suggest users turn off this feature.
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.
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.
Thank you for your constructive feedback and for acknowledging our responses. We're glad that the additional comparisons addressing W3 were helpful, and we agree that including them in the appendix would be beneficial. We will make sure to incorporate this in the final version of the paper. We hope these updates might lead you to reconsider your score. Your insights are much appreciated and please let us know if you have any further questions before the discussion is closed

Best Regards,

Anonymous Authors
Thank you for your thoughtful comments and support for the paper. 

We appreciate your insights regarding the binary search method and its potential application in future work. Your feedback on the relationship to existing approaches, especially in the context of NN verification, is constructive. We will ensure that the final version addresses the presentation issues and provides better contextualization concerning MILP, SAT, and other related work. 

We're glad to have your support for acceptance and look forward to refining the paper accordingly.

Best Regards,

Anonymous Authors
Thank you for the response. I have read the reviews and rebuttals and will keep my "Accept" rating. I do agree with other reviewers that this work is more incremental in nature, but I believe that the contribution is still sufficiently significant for acceptance. In my opinion, the ideas in this paper are interesting enough to publish and the presentation issues appropriately raised by other reviewers can be fixed for the final version. While other reviewers bring up topics that I had not considered, I believe the responses are satisfactory.

A couple of minor comments:

* *On binary search:* You can always limit the number of verification queries in your binary search. While I believe it is ok to leave it for future research, I suspect that it would work better than the one proposed in the paper. If you do move forward with future work in this direction (e.g. CDCL + your strengthening), I suggest considering this approach.

* *Relationship to existing methods (based on other reviews):* There is some overlap with known methods from the SAT/MILP literature, but the methodological novelty here is the strengthening in the context of NN verification. During my review I did a quick search over the MILP literature to see if this strengthening approach already existed, because it is actually a rather simple method, and while there are similar approaches, I was surprised to see that it does not exist exactly in the way that is done here. From the SAT/CP literature, DPLL/CDCL/no-good learning is probably the closest one, but it is not quite the same.

   A key here is that in NN verification we have these very fast, GPU-accelerated lower bounds (whereas MILP requires solving LPs). This opens the door to approaches like these which leverage these lower bounds, and it seems effective for verification, even if incrementally. This is also a reason why a custom B&B makes sense for NN verification. More speculatively, another reason why I think this works well is that in verification we focus on proving infeasibility, and in a way instances are expected to be tightly constrained. In particular, extracting cuts from the B&B tree is probably a good idea because ReLU LP relaxations in NN verification are very loose in deeper layers. While this can be naturally translated into other problems in MILP, I am skeptical it would be as effective in typical problems from the Operations Research community. My view of this paper is that it is an early step into incorporating CDCL-like ideas into the custom B&B framework for verification, much like ideas from MILP were incorporated in the past in the form of B&B and cuts, and I believe this is a positive step forward.

Given that all improvements in the rebuttals are made (including the extra analysis that you made for this review, and especially better contextualization w.r.t. MILP, SAT, and other previous work as requested by both myself and iWFh), I support this paper for acceptance.
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.