Hybrid MILP to efficiently and accuratly  solve hard DNN verification instances

Authors: Yuke Liao, Blaise Genest, Kuldeep S. Meel, Aryaman Shaan
Primary area: alignment, fairness, safety, privacy, and societal considerations
Keywords: Safety; Neural Netowrks; Verification; robustness; MILP

Abstract:
Deep neural networks have demonstrated remarkable capabilities, achieving human-like or even superior performance across a wide range of tasks. However, their robustness is often compromised by their susceptibility to input perturbations. This vulnerability has catalyzed the verification community to develop various methodologies, each presenting a unique balance between completeness and computational efficiency. $\alpha,\beta$-CROWN has won the last 4 VNNcomp(etitions), as the DNN verifier with the best 
trade-off between accuracy vs computational time. VNNcomp however is focusing on relatively easy verification instances (network, inputs (images)), with few {\em unstable nodes}. In this paper, we consider harder verification instances. On such instances, $\alpha,\beta$-CROWN displays a large gap ($20-58$%) between instances that can be verified, and instances with an explicit attack. Enabling much larger time-outs for $\alpha,\beta$-CROWN only improves verification rate by few percents, leaving a large gap of undecided instances while already taking a considerable amount of time. Resorting to other techniques, such as complete verifiers, does not fare better even with very large time-outs: They would theoretically be able to close the gap, but with an untractable runtime on all but small {\em hard} instances.

In this paper, we propose a novel Utility function that selects few neurons to be encoded with accurate but costly integer variables in a {\em partial MILP} problem. The novelty resides in the use of 
the solution of {\em one} (efficient LP) solver to accurately compute a selection $\varepsilon$-optimal for a given input. 
Compared with previous attempts, we can reduce the number of integer variables by around 4 times while maintaining the same level of accuracy. Implemented in {\em Hybrid MILP}, calling first $\alpha,\beta$-Crown with a short time-out to solve easier instances, and then partial MILP for those for which $\alpha,\beta$-Crown fails, produces a very accurate yet efficient verifier, reducing tremendously the number of undecided instances ($8-15\%$), while keeping a reasonable runtime ($46s-417s$ on average per instance).

Decision: reject
Reviewer scores: 5, 5, 6

Reviews and discussion:
<thread>
creation date:
1730029377103

thread_type:
official_review

<thread_object>
creator: reviewer_zhoq

<content>
summary:
This work proposed Hybrid MILP, a neural network verifier which first uses the optimisation based ab-CROWN to solve easy instances before invoking a MILP solver to solve the remaining hard instances. They key to Hybrid MILP is to only encode a subset of unstable neurons using binary variables (i.e., to 'open' them). This subset is chosen based on an upper bound on the individual neurons utility in such an encoding. The resulting method demonstrates strong performance on hard verification instances on small DNNs.

strengths:
* Novel utility function based on the primal pre-activation values of neurons instead of just their bounds.
* Empirically high effectiveness across a range of neural networks
* Extensive background and discussion of (some) related work.

weaknesses:
* Lack of ablation studies confirming the importance of the proposed utility function and partial encoding (see below).
* Key parameters of the experimental setup for the main experiment in Table 4 are not discussed, e.g., how was K chosen, how were intermediate bounds computed, how was 'z' chosen for the utility function computation, were different sets used for robustness against different alternative classes
* Lack of theoretical and empirical, comparison (or even mention) of the closely related work on branching heuristics (e.g. Bunel et al, De Palma et al., Ferrari et al. and Henriksen et al.) , similarly trying to estimate the importance of encoding neurons exactly in BaB.
* Lack of comparison to the optimizer's relaxation strategy at equal runtime, i.e., the importance of partial encodings in the first place.
* Applicability only to very small DNNs, which previous work (Ferrari et al.) found to be more easily solvable by LP/MILP based verifiers like ERAN, which were not compared to.
* Overclaims regarding the novelty of Proposition 1, which was discussed in similar form in Singh et al Equation 2 and Salman et al. Theorem 4.2.
* Poor copywriting and large number of typos, including in and the abstract formulas (e.g. Line 174 (half sentence missing), Line 292 (UB - UB -> UB - LB), first expression in Line 359 (three closing but only one opening bracket))

**Minor Comments**
* BaB-based methods such as ab-CROWN and MN-BaB are complete, but the opposite is implied in several places.
* Completeness is binary and can not be traded of with efficiency, but precision (at a given timeout) can.

**References**  
* Ferrari et al. "Complete verification via multi-neuron relaxation guided branch-and-bound."
* Salman, et al. "A convex relaxation barrier to tight robustness verification of neural networks."
* Singh et al. "An abstract domain for certifying neural networks."
* Bunel et al. "Branch and bound for piecewise linear neural network verification."
* De Palma et al. "Improved branch and bound for neural network verification via lagrangian decomposition."
* Henriksen et al. "DEEPSPLIT: An Efficient Splitting Method for Neural Network Verification via Indirect Effect Analysis."

questions:
1) Can you include experiments using a full-MILP encoding and different partial MILP encodings using other utility functions after ab-CROWN to better assess the contribution of the novel utility function vs. the combination of ab-CROWN with (any) MILP based strategy?
2) How does your partial MILP encoding compare to a full MILP encoding (of unstable ReLUs) in terms of the achieved upper bounds over time? This is particularly interesting, as a popular approach to solving MILP problems is exactly to relax binary variables (automatically and based on the solvers strategies).
3) How is the solve time in Table 3 affected by the choice of neurons? And how do the results change if no exact MILP bounds but only LP bounds are available for Layer 2?
4) Can you discuss the experimental details as per the weaknesses?
5) Can you include a formulation of the inductive definition of the utility function?
6) Can you include experiments on larger networks to investigate the limitations of the proposed method?

**Conclusion**  
The work is a promising new direction for solving hard verification instances on small Networks. However, comparison to key related work is missing and experimental validation is too granular to assess the effectiveness of the novel components proposed in this work (see weaknesses). In addition, the limitations of this work with regards to applicability to larger and perhaps more relevant networks are not investigated. Overall, I believe this work does thus not meet the bar for acceptance at ICLR but I am more than happy to reconsider this assessment should my concerns be addressed.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730642273873

thread_type:
official_review

<thread_object>
creator: reviewer_zyjy

<content>
summary:
This paper introduces Hybrid MILP, a method designed to efficiently solve complex verification problems in deep neural networks (DNNs), particularly those involving ReLU-based architectures. The paper addresses the limitations of the current state-of-the-art verifier, α, β-CROWN, which performs well on relatively simple instances but struggles with more challenging ones. The authors propose a hybrid approach that initially applies α, β-CROWN with a short time-out to quickly address easier instances. For instances that remain undecided, Hybrid MILP selectively applies a partial MILP (Mixed Integer Linear Programming) that combines integer variables with linear relaxations for a subset of neurons, reducing the number of integer variables by approximately four times compared to prior methods. This approach effectively narrows the undecided instance rate and is experimentally validated to be both accurate and efficient. Results on benchmark datasets, including MNIST and CIFAR, demonstrate Hybrid MILP’s effectiveness in reducing undecided cases by up to 43%, with a manageable runtime.

strengths:
-  Hybrid MILP innovatively combines MILP and linear relaxation techniques to handle challenging verification tasks effectively.
- Experimental results highlight substantial improvements in both verification accuracy and runtime efficiency.

weaknesses:
- No complexity analysis of the proposed method.

- Limited to ReLU activation functions.

questions:
- Could the proposed method extend to MaxPool nonlinear layer? If can, how is the performance of Hybrid MILP compared to $\alpha,\beta$-CROWN?
- MILP is complete but time-consuming. I am curious about the complexity of the hybrid MILP and why it is more efficient than other baseline?
</content>
</thread_object>

</thread>
<thread>
creation date:
1730697883659

thread_type:
official_review

<thread_object>
creator: reviewer_bdus

<content>
summary:
The authors propose a new algorithm for verifying neural networks against local robustness properties. This method takes a hybrid approach, combining an existing “Branch and Bound” verifier ($\alpha,\beta$-CROWN) with MILP-based verifiers. The authors show that this hybrid approach effectively reduces the number of undecided verification instances for non-robustly trained networks, where verification is known to be hard.

strengths:
- Apart from a few typos, the paper is clearly written. 
- The proposed approach effectively reduces undecided verification instances for non-robustly trained networks within a reasonable time limit.

weaknesses:
**Motivation of the work**

Q1. This work focuses on networks that are challenging to verify because they are not robustly trained. Typically, standard-trained networks have low verified accuracy and are vulnerable to attacks. Given that these networks lack robustness, why should we even attempt to verify such difficult cases? For example, in recent papers on certified training [1], networks trained on MNIST and CIFAR-10 show verified accuracies higher than the upper bound in Table 1. Therefore, no sound verifier can achieve verified accuracy beyond what is reported in [1] on these networks. Additionally, even for ReLU networks robustness verification is known to be NP-hard, meaning that in the worst case, complete verification will require exponential time with respect to the number of unsettled ReLU nodes (assuming $ P \neq NP $). So in theory there will always be these hard instances and this was the reason behind certifiable training that makes verification easier.

[1] “Certified Training: Small Boxes are All You Need”, ICLR, 2023.

**Missing related works**

(Lines 296 - 298) The use of two lower bounds (commonly known as the triangle relaxation) within an LP formulation is not new and has been applied in prior works [1] and more recently in [2].


**Technical Contributions:**

The main technical contributions of this work are not entirely clear to me. 

- Q1: Proposition 1 appears to be a well-known result and is used in existing works [1, 2]. The authors should cite the relevant papers.

- Q2: The authors do not provide sufficient detail on the hybrid-MILP algorithm. Authors should include a pseudo-code outlining the key steps of the proposed algorithm.

-  Q3: The high-level idea behind the utility function described in Section 4 closely resembles branching heuristics, such as BaBSR (cited by the authors), in terms of evaluating the importance of an unsettled neuron with respect to a specific verification property. The authors should clarify how their approach differs from existing branching heuristics.


[1] “Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks”, ATVA, 2017.\
[2] “Input-Relational Verification of Deep Neural Networks”, PLDI, 2024.

**Missing Experiments with current SOTA verifiers**
 
$\alpha,\beta$-CROWN is no longer the SOTA verifier for local robustness. The authors should consider providing comparisons with GCP-CROWN and if possible with MN-BaB (on all networks table 4).

**Missing details in the experimental setup**

Q1. The authors should provide the config files (example - https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/complete_verifier/exp_configs/beta_crown/cifar_resnet_2b.yaml) they are using for comparing with $\alpha,\beta$-CROWN including the following details 
- Branching heuristic 
- Batch size 
- Cuts are applied or not (as done in GCP-CROWN)

**UAP/Hyperproperties/Relational property verification:**

Is the proposed approach applicable to verifying robustness against UAP or more general hyperproperties? It appears that prior works [1,2,3] take a similar approach, combining abstract interpretation or bounding techniques with a MILP formulation that is easy to optimize. 

[1] “Towards Robustness Certification Against Universal Perturbations”, ICLR, 2023. \
[2] “Input-Relational Verification of Deep Neural Networks”, PLDI, 2024. \
[3] “Relational DNN Verification With Cross Executional Bound Refinement”, ICML, 2024.



**Typos and Minor comments**

- Line 77 - Missing citation
- Line 174 - incomplete sentence 
- Line 233 - “Box abstraction” - Interval or Box domain is a well-known abstract domain used in traditional program analysis and not introduced by the cited paper. The cited paper introduced DeepPoly a type of symbolic interval domain or restricted polyhedra domain. 
- Line 310 - Typo `nappears`

questions:
Refer to the Weaknesses section
</content>
</thread_object>

</thread>
<thread>
creation date:
1732295516130

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
new version of the PDF

comment:
Dear Reviewers,

Thanks again for your very constructive reviews.
The discussion phase is ending soon. We would like to have your feedback on our revised paper:
We have produced a new pdf file including all of what was discussed, answering all of your concerns, with blue highlights of the major changes.


-Introduction : we rewrote Proposition 1 statement to make the novelty clearer.
We also explained the novelty of our Utility function (it is the first function to rank nodes using a call to a (LP) solver, which makes it particularly efficient, as shown in Table 3).


Section 3 introduce the triangular abstraction first (well known), then later state Proposition 1 (new), with a note that the statement is new up to our knowedlge (in particular, we cannot find it in the referred papers [A,B,C,D]).

[A] “Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks”, ATVA, 2017.

[B] “Input-Relational Verification of Deep Neural Networks”, PLDI, 2024.

[C] Singh et al. "An abstract domain for certifying neural networks" Equation 2.

[D] Salman, et al. "A convex relaxation barrier to tight robustness verification of neural networks. 2019". Theorem 4.2


Section 4: we rewrote Section 4 entirely, stating the key novelty (the fact that we use a (single) call to LP solver in order to rank nodes, which is novel as far as we know, and makes the choice much more accurate than previous attempts), as well as provide a clearer and shorter definition of the Utility function.

Appendix A: has all the necessary parameters for both pMILP and alpha beta CROWN, plus a note on GCP-Crown.

Appendix B: provides the pseudo code and the complexity analysis. 
We also added a comparison with other papers using to improve verification accuracy:
 >Selectively encoding unsettled ReLU nodes with binary variables, and

 >Bound tightening of intermediate layer neurons (as shown in Figure 3 [A]) 

explaining why our approach is more efficient.

In particular, it scales to larger networks than previous attempts using MILP calls.

Appendix C: We added the ablation studies with graphs, showing the efficiency of each features of pMILP.

Appendix D: We kept the comparison with verifiers other than abCROWN.

Appendix E: We added the average and Max time per MILP calls.

Best,
</content>
</thread_object>

</thread>
<thread>
creation date:
1732703660003

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Latest version of the PDF

comment:
To all reviewers:
Thanks again for the constructive direction to explore. 

We commited the latest version of our PDF, with a large rewrite around Proposition 1, and conceptual comparison between Utility and other heurstics, including Bab heuristics, and rework of graphs.

In particular, in page 16, we added an experiment using BaB heuristic (SR and FSB) to choose ReLU nodes to open.
This does not work that well, because the objective to find nodes to branch on, and the objective to open a ReLU node for MILP are not exactly aligned. But the result is interesting nevertheless.

That being said, we believe that novel techniques we are following to open MILP nodes could be potentially adapted to rank nodes to branch on for BaB.

**EDIT:** actually, even without any adaptation, it looks like our Utility function already outperforms FSB / SR  when used as ranking in alpha,beta CROWN (pure BaB) (see post/table above), although its objective is *not* optimized for BaB branching.
</content>
</thread_object>

</thread>
<thread>
creation date:
1733210885425

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Latest experiment and interesting results for BaB / alpha,beta CROWN 2/2

comment:
We use DNN 5x100, image 59. We consider nodes in layer 3, that is, exactly the same setting as Figure 2, 5 and 6 as well as Table 6 and 7.

However, we use alpha,beta CROWN to compute the bounds, and compare FSB with Utility to rank BaB nodes to branch on. We checked that FSB is slightly better than SR using alpha,beta CROWN, although both are very close.

We precomputed the best possible achievable bounds using full MILP for this layer to set the verification goal: we set the goal to verify as these bounds. The verification is obviously not achievable, but then we can  check how close to the bound the different heuristics get for a fixed time-out:
TO means time out, and -X.XX is the latest bound achieved (closer to 0 means closer to verification). We write in bold the best result for each case.

 We fixed the time out at 30s, 300s for both FSB and Utility. In order to get verification, we also relaxed the objectives with bound +0.2, .. +0.5 till verified.

| Node, Objective ...  | ... TO = 30s ... | ... TO = 300s ... |
| --- | --- | --- | 
| Node0,  |  FSB:  TO, -1.0819  | FSB:  TO, -1.0819  |
| UB < -0.05643  |  Utility: TO, **-1.0492** |  Utility: TO, **-1.0492** |  
| Node0,  |    |   FSB:  TO, -0.6819|
| UB < 0.343562  |   | Utility: TO, **-0.6492** | 
| Node0,  |    |   FSB:  verified in 253s|
| UB < 0.443562  |  |    Utility: verified in **172s**|
| --- | --- | --- | 
| Node1,  |  FSB: TO, -0.5927  | FSB: TO, -0.5927   |
| UB < 0.08124   |  Utility: TO, **-0.5726**       | Utility: TO, **-0.5726**  |  
| Node1,  |    |  FSB: TO, -0.3092  |
| UB < 0.28124   |  |  **Utility: verified in 92s**  |  
| --- | --- | --- | 
| Node 2,  |  FSB: TO, **-0.9094**  |   FSB: TO, -0.9094 |
| UB < -0.0964   |  Utility: TO, -1.2575 |  Utility: TO, **-0.7785**  |  
| Node 2,  |    | FSB: TO, -0.5094   |
| UB < 0.3036   | | **Utility: verified, 66s** |   
| --- | --- | --- | 
| Node 3,  |  FSB: TO, -0.7312| FSB: TO, -0.7312   |
| UB < 0.10694   |  Utility: TO, **-0.6926**     | Utility: TO, **-0.6926**  |  
| Node 3,  |  | FSB: TO, -0.0.4271  | 
| UB < 0.40694   |      | **Utility: verified, 112s**  |   
| --- | --- | --- |
| Node 4,  |  FSB: TO, -0.6979  | FSB: TO, -0.6979   |
| UB <  0.22181  |  Utility: TO, **-0.6735**  |  Utility: TO, **-0.6735**  |  
| Node 4,  |   | FSB: TO, -0.4611   | 
| UB <  0.42181  |   |  **Utility: verified, 233s**  |   
| --- | --- | --- | 
| Node 5,  |  FSB: TO, -0.6474  |  FSB: TO, -0.6474  | 
| UB <  0.59545  |  Utility: TO, **-0.6345** |  Utility: TO, **-0.6345**  |   
| Node 5,  |   |  FSB: verified, 156s  | 
| UB <  0.89545  |   |  Utility: verified, **111s**  |   
| --- | --- | --- | 
| Node 6,  |  FSB: TO, -0.6682   |  FSB: TO, -0.6682  | 
| UB < 0.24122  |  Utility: TO, **-0.6359** | Utility: TO, **-0.6359**  |  
| Node 6,  |  |  FSB: verified, 217s  |
| UB < 0.54122  |  | Utility: verified, **125s**  |  
| --- | --- | --- | 
| Node 7,  |  FSB: TO, - 0.8094 | FSB: TO, - 0.8094   | 
| UB < 0.4426  |  Utility: TO, **-0.7248**        | Utility: TO, **-0.7248**  |   
| Node 7,  |  | FSB: TO, - 0.0105   | 
| UB < 0.7426  |      | **Utility: verified, 119s**  |   
| --- | --- | --- | 
| Node 8,  |  FSB: TO, -0.6069  |   FSB: TO, -0.6069 | 
| UB < 0.09423  |  Utility: TO, **- 0.5983** | Utility: TO, **- 0.5983**  |   
| Node 8,  |   |   FSB: TO, -0.4069 | 
| UB < 0.29423  |  | **Utility: verified, 148s**  |   
| --- | --- | --- | 

Overall, our utility function to rank nodes to branch on for BaB in alpha,beta CROWN is significantly more accurate (or faster) than when using FSB with the same time out, except for node 2, Time Out 30s. Using TO=300s does not improve except for this  node 2, Utility becomes better than FSB. Also, on the same node 2 it succeeds to verify bound + 0.4 in 66s while FSB fails after timing out at 300s, with a latest bound far from verification (-0.5).

The reason of the discrepency for node 2, TO=30s is because it takes 3s to compute our Utility function. We tested with TO=33s for node 2, and we obtain: Utility=-0.7785 while FSB remains at -0.9094, confirming the 3s delta.
We add another test on simpler verification objectives, for bound + 0.4.

| Node, Objective | FSB | Utility|
| --- | --- | --- | 
| Node 1, UB < 042812 | **17s** |  19s  |
| Node 2, UB < 0.303   | TO 300s  | **81s** | 
| Node 3, UB < 0.5069 | 91s |  **40s**  |
| Node 4, UB <  0.6218   | 24s  | **23s** |
| Node 5, UB <  0.9954  | 32s |  **32s**  |   
| Node 6, UB < 0.6412  | 42s  | **28s**  |  
| Node 7, UB < 0.8426 | 55s | **47s**  |   
| Node 8, UB < 0.4942  | **17s** | 20s  |   
| average | >72s | **36s** |

For some nodes (1,8), FSB is 2-3s faster.
Overall, Utility is >2x faster.

Our Utility objective is unchanged, optimizing the difference (MILP – LP, using the solution of *one* LP solver call) to pick nodes to open for pMILP, without (yet) adaptation to optimize for BaB. So this is very promissing to obtain a very efficient heuristic for BaB as well, thanks to the novel ideas in our paper.
</content>
</thread_object>

</thread>
<thread>
creation date:
1733283706232

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Latest experiment and interesting results for BaB / alpha,beta CROWN. 1/2

comment:
EDIT: We have to break up this comment in 2 as the Table is taking too much space.

We have finished evaluating nodes of layer 3 using pure BaB (in alpha beta Crown), comparing our Utility function with the FSB heuristic to rank nodes to branch on. 

We provide here the interesting experiments with TO=300s, with tightest bound for which at least one of FSB / Utility verifies. See next post for the full table.

Alpha Beta Crown with verification for nodes of layer 3 of 5x100, image 59, time out 300, using FSB or Utility (formula unchanged from our paper) to rank nodes to branch on using pure BaB.

| Node, Objective | FSB | Utility (our) |
| --- | --- | --- | 
| Node 0,  UB < 0.443562 | verified in 253s | verified in **172s** | 
| Node 1, UB < 0.28124 |  Time Out 300s |  **verified in 92s**  |
| Node 2, UB < 0.3036   |    Time Out 300s  | **verified in 66s** | 
| Node 3, UB < 0.40694 |  Time Out 300s  |  **verified in 112s**  |
| Node 4, UB <  0.42181   |   Time Out 300s  | **verified in 233s** |
| Node 5, UB <  0.89545  |     verified in 156s  |  verified in **111s**  |   
| Node 6, UB < 0.54122  |  verified in 217s  | verified in **125s**  |  
| Node 7, UB < 0.7426 |   Time Out 300s        | **verified in 119s**  |   
| Node 8, UB < 0.29423  |    Time Out 300s | **verified in 148s**  |   

Utility is more accurate than FSB for every node, reaching verification when either FSB cannot conclude and Times-out at 300s (node 1,2,3,4,7,8, average time for Utility 128s) or FSB runs 50% slower (nodes 0,5,6, average time 136s for Utility vs 209s for FSB). Over all nodes, Utility needs ~130s in average to reach verification (9/9 objectives), while FSB needs >>270s in average (6/9 nodes are still not verified!). A >>2x speed-up by just plugging in our Utility function unchanged from our paper into alpha,beta CROWN.

There is one small caveat, which is Utility takes 3s more to compute the ranking than FSB (integrated in the reported runtime). This explains why node 2 Time-Out 30s was more accurate for FSB than Utility (see table next post), because Utility needed 3 more seconds for the same number of computations.  With 33s, Utility is more accurate than FSB with 33s. Overall, this runtime overhead is very limited, almost negligible.

Notice that our Utility objective is unchanged, optimizing the difference (MILP – LP, using the solution of one LP solver call) to pick nodes to open for pMILP, without (yet) adaptation to optimize for BaB. **So this is very promissing to obtain a very efficient heuristic for BaB as well, validating further the novel ideas in our paper.**


Original post:

Dear Reviewers,

We hope that this latest experiment will further convince you to recommend acceptance, if you agree that our Utility function is both novel and very accurate. We strongly believe that the reasoning and the experiments in the paper prove that without any doubt (Figure 2 page 8 and fig 5 page16), confirmed by the accuracy results of Hybird MILP (Table 3 page 9). This latest experiment now provides even more promising research direction for the Utility function, and it validates further our novel strategy.

Thanks again for the constructive comments: we didn’t think of comparing our Utility function with BaB branching heuristics because the objectives were not the same.

Again, using FSB or SR branching heuristic to choose nodes to open for pMILP was not good (see page 16 in appendix, with FSB slighty worse than SR worse than Huang et al much worse than Utility). Now, that got us curious how our Utility function was fairing as heuristic to rank nodes to branch on with BaB. For that:

1/2
</content>
</thread_object>

</thread>
<thread>
creation date:
1733308744783

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
Final Wrap Up

comment:
Final Wrap up.

For the last time, we would like to thanks the reviewers for their constructive direction.

We believe we have tremendously improved the paper since submission. 

The discussions revolved around our Utility heuristic, why is it so efficient, and compare it with more heuristics, in particular the ones used to rank nodes to branch on for BaB.

We rewrote the paper focusing on explaining conceptually how different and novel our Utility function, in particular using a primal solution to rank nodes, as well as better and stronger comparison with other heuristics. The final figure 2 (page 8) and 5 (page 16) strongly points to our Utility function being on another level of efficiency compared to the rest of the heuristics when used within a partial MILP framework.

The efficiency of our Utility function results in tangible improvements in accuracy and efficiency for verifying hard DNNs which could not be tackled by previous verifiers. While we agree that many more DNNs would be interesting to consider, we believe the spectre we investigated is sufficient to validate the efficiency of the heuristic, in particular with a quite large CNN-B-Adv with 20 000 activation, where 7% more images can be verified than the state of the art using similar runtime (accounting for GCP-CROWN being 2% more accurate than abCROWN on that CNN-B-Adv), with other networks (6x500) showing even stronger 40% improvement.

Out of curiosity, and because reviewers asked us to compared with BaB heuristic within partial MILP, we lately considered the converse: using our Utility function within a BaB framework (here, alpha, beta Crown), mimicking the setting of Figure 2 (for pMILP). Surprisingly, while the objective of our Utility function was *not* optimized for branching nodes in BaB but rather optimized for pMILP, this Utility function was outperforming heuristics for BaB (FSB and SR), more than twice as fast for the same accuracy (see the next two posts). While this is a restricted framework, this shows a lot of potential to apply our novel primal solution idea in this other context of BaB as well as in the context of pMILP we fully develop in the paper.

Some may wonder why we did not test Utility in alpha beta Crown to verify fully DNNs, and compare with alpha beta Crown using FSB. There are two reasons:

-	Technically, this would require to implement our Utility function ranging over all nodes, not only nodes from the 2 or 3 last layers. Such a function ranking nodes over all layers was not necessary with our pMILP strategy. With the little time remaining, we focused on obtaining results with already implemented tools, which gives another very interesting finding pointing to our methodology to use primal solution being also very promising in the BaB scope, not only for partial MILP.

-	Our paper is within the partial MILP scope, so such tests with BaB are not necessary. The point is mainly to showcase to the reviewers the potential impact of our novel techniques outside of the pMILP realm. We believe that the additional experiments we provided lately on layer 3 using BaB demonstrate just that. The bottom line is: More work is necessary to develop such an efficient and accurate heuristic based on primal solution to rank nodes for BaB, and this is way out of the scope of the paper.
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper studies the neural network verification problem to give guaranteed bounds on neural network outputs. It aims to improve the verification bound by selecting a certain set of important ReLU neurons that will be considered with integer variables in the MIP verification formulation, while other neurons use LP relaxation. A heuristic was proposed to select the set of neurons.

Reviewers rated the paper as a borderline paper. This paper improves upon the state-of-the-art verifier α,β-CROWN in a few settings, which is quite nice. The technical contribution of the paper, although not very significant, is valid and valuable. However, the writing of the paper is quite poor, especially the mathematical notations are not rigorous and often misleading (Section 4), and there are factual errors in the paper (see next paragraph). The quality is clearly below an average ICLR paper in this field. In addition, the scenarios considered in this paper are quite limited (although this is not a main concern for rejection), mostly fully connected MNIST models and very small CIFAR models.

Some claims in the paper are incorrect, e.g., branching heuristics are measuring "sensitivity" (in fact, what is "sensitivity" is unclear). Branching heuristics themselves are also developed to estimate the bound improvements after branching, exactly the same way as in this paper. For example, in the BaBSR paper, the heuristic was derived by calculating the difference between the two bounds, one with the neuron relaxed and one with the neuron fixed. A stronger estimation of bound improvement will lead to better branch-and-bound performance, so the findings during the rebuttal period were not a surprise. I suggest the authors to further explore the potential of their formulation as a branching heuristics. In addition, as also pointed out by Reviewer zhoq, the AC is very confident that Proposition 1 is a well known fact in this field and should not be claimed as a contribution.

Nevertheless, the feedback from the reviewers have greatly helped improve the paper and I encourage the authors to continue working on this subject and improving its quality.