Improving Branching in Neural Network Verification with Bound Implication Graph

We greatly appreciate the reviewer for recognizing the strengths of our work. We answer your questions about the limitations of our work, details about the new benchmark, and applicability to other verifiers. We also provide new experiments comparing our method to prior work which also used case-analysis-based approaches to find neuron implications. We hope the reviewer can reevaluate our paper based on the new evidence provided.

The paper only considers certifying adversarial robustness on perception networks.

Our method largely relied on state-of-the-art BaB-based verification frameworks such as [2,3,4,5,6], and is limited by the capability of existing verifiers, which focuses on branch-and-bound (BaB) for ReLU networks only. We want to point out that this is a limitation of the majority of verification papers. For other non-linear activations and non-perception networks (such as Transformers), one very recent workshop paper [1] (still unpublished) considered BaB. Our method can be extended to the generalized BaB in [1], by changing the right-hand-side constraint in Eq. (5) and (6) to a non-zero splitting point. We will work towards this direction in our future work.

The general idea of removing sub-problems during case-analysis-based search has been considered in Planet.

We acknowledge that prior work such as Planet (2017) considered case analysis in the same spirit. We revised our paper and discussed this reference in the relevant part in Section 5. We want to emphasize that our main contribution is a new optimization-based formulation that is more powerful and less restrictive to find bound implications. In our revised paper, we added a more recent baseline, Venus2 (2021) [7,8], which also finds dependencies among neurons but with a much weaker and simpler method compared to ours.

We highlighted the new results below (more details added to Section 4). Following [7,8], here we divide the implications into inter-layer (implicated and implicant from different layers) and intra-layer (from the same layer) ones. We outperform the baselines by finding 7x - 180x more implications. So although some existing work also considered similar analysis, ours is significantly stronger.

The technical contribution of this paper is rather incremental

Besides the strong empirical improvements (7x - 170x improvement) shown above, our paper also makes a few unique technical contributions:

1. Our first theoretical contribution is the formulation of finding implications constraints as a generic optimization problem. The optimization formulation did not exist in prior work, and is a stronger formulation than previous work, enabling finding implications between any two neurons (prior work [7,8] was restricted to neurons in the same layer or consecutive layers).

2. Our second theoretical contribution is a fast way of solving these optimization problems, by reusing bound equations that were readily available during the solving process without recomputation. None of the existing work shows that the bound equations (for free) can be used to find neuron implications and improve verification.

3. Our method also works significantly better on convolutional networks due to its technical advantage. The technique in [7,8] considers implications using weak intermediate layer bounds of one convolutional layer only, and very few implications can be found because the convolutional layer weights are sparse and uncorrelated (zero reported in Table 1) . In contrast, our optimization-based formulation found hundreds of implications.

4. In addition, we also demonstrated multiple subproblem-specific bound implication graphs can be built to further enhance its effectiveness.

The technical contribution of this paper is specific to CROWN. Are the techniques described in the paper applicable beyond ab-CROWN, such as in NNV and Marabou?

Our algorithm to find the bound implication is independent of ab-CROWN, as it only takes linear bound equations and then returns the implication graph. The graph can potentially be used in many BaB-based verifiers, including Marabou, Mn-BaB, VeriNet, and Oval. Some of these verifiers also have similar linear bounds so we can obtain them without additional cost, and for the verifiers that do not use these linear bounds, a single pass of CROWN bound propagation (very fast) is sufficient to get these bounds to enable the benefits of bound implications in these verifiers. The only exception is NNV, where it is unclear to us whether BaB over ReLU neurons was used. We will provide our implementation in a separate module, independent of ab-CROWN so it may potentially be used in other verifiers.

What is the actual perturbation bounds and perturbation dimensions on the VeriHard benchmark sets?

Thanks for pointing this out. We include the perturbation bounds and dimensions on the VeriHard benchmark sets in an anonymous Google sheet so you can take a look. We will publish our dataset once our paper is accepted.

References:

[1] Shi, Zhouxing, et al. "Formal Verification for Neural Networks with General Nonlinearities via Branch-and-Bound." 2nd Workshop on Formal Verification of Machine Learning (WFVML 2023). 2023.

[2] Katz, Guy, et al. "The marabou framework for verification and analysis of deep neural networks." Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31. Springer International Publishing, 2019.

[3] Wang, Shiqi, et al. "Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification." Advances in Neural Information Processing Systems 34 (2021): 29909-29921.

[4] Ferrari, Claudio, et al. "Complete verification via multi-neuron relaxation guided branch-and-bound." arXiv preprint arXiv:2205.00263 (2022).

[5] Zhang, Huan, et al. "General cutting planes for bound-propagation-based neural network verification." Advances in Neural Information Processing Systems 35 (2022): 1656-1670.

[6] Xu, Kaidi, et al. "Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers." arXiv preprint arXiv:2011.13824 (2020).

[7] Kouvaros, Panagiotis, and Alessio Lomuscio. "Towards Scalable Complete Verification of Relu Neural Networks via Dependency-based Branching." IJCAI. 2021.

[8] Botoeva, Elena, et al. "Efficient verification of relu-based neural networks via dependency analysis." Proceedings of the AAAI Conference on Artificial Intelligence. Vol. 34. No. 04. 2020.

We have also addressed each individual weakness you pointed out:

a. While the experimental results from [1] clearly show that implication constraints help with verification times, the paper says "they were handled as constraints to a black-box MIP solver without validating their usefulness".

We removed this confusing sentence. Our new characterization of [1,2] is provided throughout the paper, particularly in Sections 1 and 5.

b. Bound implication graphs were previously constructed in [2], where they were precisely used to reduce the total number of branches. The paper however presents the implication graph as a novel aspect of the paper and does not reference [2].

We removed this claim throughout the paper, cited [2], and rewrote the relevant paragraphs in section 3. Our new formulation to find neuron implications is an important theoretical contribution, and we outperformed [2] by finding 7x - 170x more implications. This is not an incremental contribution.

c. While the procedures computing the implication constraints in [1] are GPU-friendly the paper claims the opposite.

Although [1,2] did not use a GPU implementation, we acknowledge that [1,2] can potentially be applied to any verifiers and we removed relevant claims in our paper.

d. The paper does not clarify with the introduction of the implication constraints that they were first introduced in [1].

We rewrote the introduction and cited [1,2] at the beginning.

We thank the reviewer again for discussing the details in relevant papers [1,2], and we hope all your concerns are now addressed. We hope the new representation of our paper has made it clear that [1,2] is important prior work in this field. Please let us know if you have any further concerns, thank you.

References:

[1] E. Botoeva, et al. Efficient Verification of ReLU-based Neural Networks via Dependency Analysis. AAAI 2020.

[2] P. Kouvaros, A. Lomuscio. Towards Scalable Complete Verification of ReLU Neural Networks via Dependency-based Branching. IJCAI 21.

The implication constraint identification procedures are not compared with the ones from [1]. It is not clear that they perform better.

We added comparisons in both experiments (Section 4) and in theoretical perspectives (Section 5).

Experimental comparison to [1,2]: We added experiments in Section 4 to compare to [1, 2] and showed that we could find significantly more neuron implications. We evaluate our method on a few networks used in [1,2], and we use the official code of Venus2. To allow a fair comparison, here we do not use any particular BaB solver and consider the implications found in the initial verification problem. The results are presented in Table 1 in our revised paper and also highlighted below. We outperform the baselines by finding 7x - 180x more implications. The difference is especially significant in convolutional networks - the zero results from Venus2 are not errors (see our contribution 4 above).

Theoretical comparison to [1,2]: Compared to [1,2], our formulation is significantly stronger, for the following reasons:

1. For inter-layer dependency, [1,2] can only consider the case where a neuron in one layer is set to be inactive (0), and propagation the bound to the layers following it. In Lemma 3 of [2], cases 3 and 4 are empty, indicating that they cannot find any implications when one neuron is set to be active. Our methods can be used to find all four kinds of implications.

2. Furthermore, our method can find implicated neurons before the implicant neuron. For example, by setting a neuron in layer 3 to be active or inactive, we may imply that a neuron in layer 1 or 2 (before layer 3) is active or inactive. This is impossible in [1, 2].

3. For intra-layer dependency, our methods use bound equations that are propagated to the input layer, which utilizes tighter bounds on the input layer rather than the relatively looser intermediate layer bounds in [1,2]. Our formulation is also optimization-based, allowing us to find the strongest implications under this formulation. As a result, we found significantly more intra-layer neuron dependencies (Table 1).

4. Furthermore, the method in [1,2] does not work well for convolutional networks, because the equivalent weight matrices are sparse, so the pair of neurons under investigation may have no correlation at all (Table 1 where Venus2 reports 0). Our method uses the bound equations at the input x, which is often dense (as large as the receptive field of the entire network, rather than one layer) and can capture neuron correlations better.

We thank the reviewer for giving detailed technical explanation for your mentioned work [1,2]. We have significantly revised our paper based on your suggestions, and correctly cited and discussed [1,2] throughout the paper; major changes were marked in blue. We now discuss [1,2] early in our paper in the introduction, do not claim the implication graph as part of our contribution in Section 3, and remove imprecise sentences in Section 5. We also added a detailed experimental comparison to [1,2] to show our strong improvements.

The main novelty of our paper is not about constructing the graph, but a new formulation that is more powerful and less restrictive to find bound implications. Compared to [1,2], we have both theoretical advantage and strong experimental evidence with 7x - 170x more bound implications found (Table 1 in our revised paper). We respectfully disagree this is a “small delta” or incremental contribution. We hope the reviewer can reevaluate our paper based on new discussions and experiments about [1,2], where we have made it clear that [1,2] are important prior work in this field.

The main novelty of the paper is the computation of the implication constraints using bound equations (which are computed using previously established methods) instead of concrete bounds.

We thank the reviewer for recognizing that part of our contribution was to use bound equations to solve bound implications. However, this is only a small part, and our method includes multiple novel contributions that were never discussed or demonstrated:

1. Our first theoretical contribution is the formulation of finding implications constraints as a generic optimization problem. The optimization formulation did not exist in prior work, and is a stronger formulation than previous work, enabling finding implications between any two neurons. We discuss the theoretical advantage of our work in Section 5 and also in this response (a few paragraphs below).

2. Our second theoretical contribution is a fast way of solving these optimization problems, by reusing bound equations that were readily available during the solving process without recomputation. None of the existing work shows that the bound equations can be used to find neuron implications. In addition, as you mentioned, these bound equations are “previously established” and have been widely used in many verifiers, and here our novel usage of these equations in a new setting shows potential wide applications of our approach in many verifiers.

3. Empirically, we demonstrated that our new method of finding implications is significantly better than [1,2]. In our added experiments, we used the same networks as evaluated in [1,2], and we reported 7x - 170x more inter-layer and intra-layer implications (see details below).

4. Our method also works significantly better on convolutional networks due to its technical advantage. The technique in [1,2] considers implications using intermediate layer bounds of one convolutional layer only, and very few implications can be found because the convolutional layer weights are sparse and uncorrelated (zero reported in Table 1). In contrast, our optimization-based formulation found hundreds of implications.

Presentation of Theorem 3.2 can be improved. An illustration of Theorem 3.2 could help communicate the underlying intuition.

We have split Theorem 3.2 into a Theroem and a Corollary, as suggested. Here “linear bounds to not have an intersection with C” means that the implicant lower constraint Eq. (6) is too far away from $x_0$, and it is outside of the box C centered at $x_0$. We have revised the presentation of the theorem accordingly. In addition, we’ve added a figure (Fig. 2) to showcase the cases in the Corollary, as you suggested.

The scaling of the y-axis in Figure 2 is unclear making it hard to interpret. I would consider a linear scale instead.

Thanks for pointing this out. We revised our figures to have a linear y-axis scale in our revision.

I believe it should be "(inputs <= 0)" for the "inactive" case in Section 1 paragraph 3. Other typos.

Thanks for your nice catch! We have fixed these typos in our revision.

Thanks for your valuable comments and constructive feedback. We added comparisons to GCP-CROWN as you suggested, and also improved the clarity of theorems. We carefully addressed your comments below, and we hope the reviewer can reevaluate our paper based on these new results.

a direct comparison or even better combination with GCP would be essential

Thanks for pointing this out. We carefully reviewed the GCP-CROWN paper you mentioned and we also integrated BIG into GCP-CROWN. However, we want to emphasize that GCP-CROWN heavily relies on a MIP solver to find cutting planes, which cannot be applied to large models (e.g. CIFAR100, TinyImageNet models) due to its high computational cost. Thus, in many settings of our paper, GCP-CROWN cannot bring improvements, yet our method still can.

We evaluate the total number of branches (less is better) on several benchmarks below. GCP-CROWN+BIGs could further reduce the number of branches compared with GCP-CROWN only. Note that GCP-CROWN cannot scale to CIFAR100 and TinyImageNet, yet our bound implications can still bring improvements. We added these results to Appendix G.

Did you investigate the interaction of these bound implications with the general cutting planes from GCP (also based on beta-CROWN)?

That’s a very interesting question. We exported the cutting planes from GCP-CROWN and compared them to our implications on the same set of instances. We report the average number of implications found by us, the average number of cutting planes in GCP-CROWN, and the overlaps. Here overlap means that GCP-CROWN finds a constraint mentioning the same pair of two neurons as we found as implicated and implicant neurons.

As we can see, the overlaps only take a minority of the overall implications we found with our method. This is expected because GCP-CROWN uses a MIP solver to generate cutting planes, which is unaware of the underlying neural network architecture and uses generic methods (such as Gomory cuts) to find implications among variables. We added these results to Appendix G.

Significance of improvements on established benchmarks

Thanks for mentioning the issue. We believe that minor improvements on established benchmarks are largely due to the benchmark design. These benchmarks were proposed when neural network verifiers were relatively weak. Nowadays a majority of SDP-FO[1] and ERAN[2] benchmarks have been largely solved, while a small portion of unsolved instances with unknown (potentially very high) difficulty. The improvement in the verification framework cannot be fully reflected by considering these instances with unknown difficulty. Our new VeriHard benchmark contains difficult examples that existing verifiers can guarantee to solve with a long timeout (so the difficulty is known, similar to the classic oval20 benchmark used in many papers). The progress of neural network verifiers can be reflected better in this new benchmark.

[1] Dathathri, Sumanth, et al. "Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming." Advances in Neural Information Processing Systems 33 (2020): 5318-5331.

[2] Singh, Gagandeep, et al. "Fast and effective robustness certification." Advances in neural information processing systems 31 (2018).

Thanks for recognizing the importance of our work and for strongly supporting our paper! Following your suggestions, we’ve added discussions of bottlenecks to the paper and also considered using BIG to discover hard adversarial examples.

More discussions on the bottleneck of the proposed method would further strengthen the paper.

Thanks for your suggestion. We’ve added a discussion to our paper (Section H) on the bottleneck as suggested. Our proposed method is highly relied on BaB-based verification framework so it has some common issues: 1) Our derived implications follow the large body of papers for verifying ReLU networks [1,2,3,4] and need further extensions to other non-piecewise linear activation functions. 2) We cannot support the verification of very large neuron networks, such as Transformer with billions of parameters. We will keep investigating the possibility of applying our implication concept into the verification of more general models in the future.

Could you comment on how would the BIG can be used to discover hard adversarial examples or train the model to be robust against those examples?

This is a very interesting direction. In our work, we did not use our implication graph (BIG) to discover adversarial examples during branch-and-bound, but there exist some papers focusing on finding adversarial examples through branch-and-bound procedure [5]. Our method can be applied on top of these BaB-based methods to reduce the research space when finding adversarial examples, and this could be an interesting future work.

[1] Katz, Guy, et al. "The marabou framework for verification and analysis of deep neural networks." Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I 31. Springer International Publishing, 2019.

[2] Wang, Shiqi, et al. "Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification." Advances in Neural Information Processing Systems 34 (2021): 29909-29921.

[3] Ferrari, Claudio, et al. "Complete verification via multi-neuron relaxation guided branch-and-bound." arXiv preprint arXiv:2205.00263 (2022).

[4] Zhang, Huan, et al. "General cutting planes for bound-propagation-based neural network verification." Advances in Neural Information Processing Systems 35 (2022): 1656-1670.

[5] Zhang, Huan, et al. "A branch and bound framework for stronger adversarial attacks of relu networks." International Conference on Machine Learning. PMLR, 2022.