Hybrid MILP to efficiently and accuratly solve hard DNN verification instances
Safety; Neural Netowrks; Verification; robustness; MILP
First I want to apologize for the misused of cited paper [1]. The issue was there were several [1] used in your original review, and I mistakenly took the wrong one (which also train networks and certifiy them, so it was easy to confuse). Anyway, our point is that there are many networks out there, we cannot test them all, and in real life you cannot necessarily choose the best one learnt for a specific task. 

We choose to experiment with standard DNNs already tested with abCROWN such that we can compare and use already mature configuration files.

> the number of MILP calls

This is 2 (one for lower bound, one for upper bound) per node, thus the O(N), for all DNNs per image per epsilon.
For Figure 2, we have time to query ~6 different epsilon in 10 000s, in a binary search.

> average and maximum time per MILP call

We did not keep the statistic you are asking for. 
For average, it is easy to approximate accurately:
average run time per  image x 20 (threadhs in parallel) / [ 2 (min and max) x Number of nodes].
This gives: 

6x 100: 0.92s

6x 200: 0.71s

9x 100: 0.76s

9x 200: 0.49s

6x 500: 1.34s

CNN-B-Adv: 0.8s

maximum is a lot higher. In particular for output nodes which have a higher number of open nodes, in particular for CNN-B-Adv. We will run our prototype on 1 image of each case to report that.


>Why didnt you try ith Refined $\beta$-CROWN/ERAN for this experiment

Refer to line 467: Last but not least, Refined β-Crown cannot scale to larger instances (6×500, CNN-B-Adv), while Hybrid MILP can.  

Specifically, the engine return a 'not implemented' when we tried to run it. Anyway, running >500 nodes with full MILP would be extremely slow (this would be just for the first layer using MILP);

> Specifically, I am interested in the $\epsilon$ values close to the best falsifiable epsilon, but the network cannot be attacked.

Again, we didnt save this data, but we will rerun on some interesting case and report. This is of course much higher, but not your average situation. Figure 2 shows that still Hybrid MILP can certify images quite close to this boundary, much closer than abCROWN.
> In [1], the trained to be certifiable for robustness CIFAR10 ResNet 4B certification results is around 54% with epsilon= 1/255,(table 3 page 7 of https://openreview.net/pdf?id=7GEvPKxjtt).

It seems there might have been a misunderstanding. I would kindly suggest that the authors review the cited papers more carefully before responding. Specifically, I referred to the paper "Certified Training: Small Boxes are All You Need" (https://openreview.net/forum?id=7oFuxtJtUMH, see Table 1). The certified accuracy at $2/255$ is reported as $62.84$%, which is higher than the upper bound of $62.0$% mentioned by the authors. That said, I do agree that there are certain benchmarks (networks) and specific properties (such as $\epsilon$ values) where using a MILP formulation can indeed help reduce the number of unverified instances. 

> Figure 2 page 10

I may have overlooked the runtime details. Could you please point me to or provide specifics on the runtime, such as the number of MILP calls, average and maximum time per MILP call, and the hyperparameter values used? Additionally, could you share the same details for the other networks presented in Table 1? Furthermore, is there a particular reason why the authors did not consider Refined $\beta$-CROWN/ERAN for this experiment, as it also utilizes an LP/MILP-based approach?

> $\epsilon$ values

"It depends on the distance to the frontier between certifiable and falsifiable. asking for epsilon >> best falsifiable epsilon would return very fast a (negative) answer, similarly if epsilon << best certifiable epsilon." - I completely agree with this. However, I wanted to see the runtime details (e.g., MILP calls, hyperparameters, etc.) for different $\epsilon$ values in the range [best certifiable epsilon, best falsifiable epsilon]. Specifically, I am interested in the $\epsilon$ values close to the best falsifiable epsilon, but the network cannot be attacked.
>Technical concern (major concern), 

let us investigate before providing an answer - we will.

On other concerns:

>Motivation (minor concern): "CIFAR-10 show verified accuracies higher than the upper bound in Table 1."

This is factually incorrect.

In [1] , the trained to be certifiable for robustness CIFAR10 ResNet 4B certification results is around 54% with epsilon= 1/255,(table 3 page 7 of https://openreview.net/pdf?id=7GEvPKxjtt).

The upper bound for CIFAR10 CNN-B-Adv is at 62%, which is higher than 54%, not lower as claimed. 
Even more importantly, the upper bound is for A MUCH HARDER epsilon=2/255 (perturbation twice as high). 
Notice that with epsilon= 3/255 [1] reaches 0% of certification (epsilon= 2/255 is not reported in  [1], so direct comparison is not that easy). We will report upper bound for epsilon=1/255 for CNN-B-Adv for comparison.

Even better, Hybrid MILP actually succeeds to certify 51% certified robustness for CIFAR 10 CNN-B-Adv for the MUCH HARDER epsilon= *2*/255, with perturbations twice as large than epsilon= 1/255. This is a much stronger result than the 
54% of certification with epsilon= 1/255, and this can be cerified thanks to Hybrid MILP.

More generally, in academic world, we can train our own networks, but in the real world, you have to do with the network trained by the industrial partner, and the training pipeline often cannot be changed. This is also what is advocated in Dathathri et al. (2020). As we said, you cannot expect all the networks to be specifically trained to be easy to verify: some will be, some will not be - and we need new methods to tackle them all.

What we did is that we experimented on standard benchmarks of the community.

> Pseudo code and complexity: "The worst-case complexity, is too high even for small networks. This approach is feasible only when the number of unsettled neurons is low."

Factually, the experimental results point to the exact opposite direction :) : 

pMILP efficiently certifies CNN-B-Adv, which has 20, 000 neurons and quite a lot of unsettled neurons (otherwise, abCROWN would have very few undecided images).


pMILP is computing bounds for 20 neurons in parallel, very similar to PRIMA or Refined bCROWN (16 neurons in parallel), and much less than using >4000 GPU core in standard abCROWN.

Several things to consider:
1) The complexity  allows to understand what is the crucial parameter to keep in track. Here, it is the number K of open nodes. And this is exactly what our main contribution does: identifying few very important nodes. If K is small, then the complexity is manageable efficiently even for large network (complexity polynomial in N).

2) worst-case complexity IS in the worst case. The average case is usually behaving better. We use the Gurobi solver, which has powerful heuristic which avoids the worst case complexity most of the time. That being said, our prototype is much more efficient than any previous verifier primarily using Gurobi, so this sole factor is only a small part of the reason.

>  I strongly recommend that the authors provide a runtime analysis using a higher  values, for example, 
 values say  for the MNIST  network (Table 1 row 1), using higher  epsilon values. This is necessary to understand the scalability of the algorithm.

You should look at figure 2 page 10: we certified some instances with epsilon as high as 0.1, for the complex 6x500 networks.
Obviously, scaling to larger epsilon is not an issue. Actually, runtime does not depend directly on epsilon. It depends on the distance to the frontier between certifiable and falsifiable. asking for epsilon >> best falsifiable epsilon would return very fast a (negative) answer, similarly if epsilon << best certifiable epsilon.
Thanks for the prompt reply. 

**Motivation (minor concern)**
The main point behind the motivation question was that none of the networks' verified accuracies could match those of a certifiably robust, state-of-the-art (SOTA) model (even with a perfect verifier). For reference, "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, I wanted to understand the practical importance of solving these challenging instances for an ML practitioner, given that there are already better models with higher verified and, in many cases, standard accuracy [1].
 
**Technical concern (major concern)**
The technical concerns have not been addressed. The authors should clearly highlight the key technical contributions, especially considering that the following contributions are already known in the verification community:
- Proposition 1 is established in prior works.
- Selectively encoding unsettled ReLU nodes with binary variables improves verification accuracy.
- Bound tightening of intermediate layer neurons (as shown in Figure 3 [A]) improves verification accuracy.
- Utility functions, in principle, appear similar to branching heuristics (e.g., BaBSR).

[A] "Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers",  ICLR, 2021.

**Pseudo code and complexity** 
Thanks for providing the pseudo-code. However, it is still incomplete and does not mention any hyperparameters or whether iterations of the inner loop are executed parallelly.
The worst-case complexity, $O(N \cdot MILP(N, K))$, is too high even for small networks. This approach is feasible only when the number of unsettled neurons is low. I strongly recommend that the authors provide a runtime analysis using a higher 
$\epsilon$ values, for example, $\epsilon$ values say $\epsilon \in [0.03, 0.035, 0.04, 0.05, ...]$ for the MNIST $5 \times 100$ network (Table 1 row 1). This is necessary to understand the scalability of the algorithm.
>Q1) The key part of my question is after ab-CROWN. I.e. how does pMILP compare to full MILP (and other utility functions) when run after ab-CROWN using the resulting relatively tight intermediate bounds.

Two answers: 
a) we do not use any intermediate bounds computed from ab-CROWN when running pMILP. This might be doable, but would need a low level integration. In our prototype, ab-CROWN is only used to solve easy instances. Hard instances (that is, instances for which abCROWN fails to answer) are restarted from scratch. This is already very efficient, although it could be made even more efficient by using intermediate abCROWN bounds.

In this respect, on 6x100, full MILP did not solve any of the hard instances not solved by a fast run of ab-CROWN, although the time out was 10.000s.

b) We tried 6x100 with computing intermediate bounds using full MILP (iterative full MILP). 
Some hard instances not solved by abCROWN can be solved by this iterative full MILP, but the runtime to solve such instances is 20x higher than what is achieved by pMILP, without solving more images than pMILP. 

> Q2: 

We will answer with more explicit numbers once the experiment finish.

> Q4) While Table 5 provides details on the number of open neurons and timeouts, ab-CROWN has a large number of further parameters that are not reported.

The networks we experiment with have already been tested by abCROWN.
We thus use the configuration files which come for each network in abCROWN (except for time-out which we explicitly mention).

e.g.: for CNN-B-Adv:
https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/complete_verifier/exp_configs/beta_crown/cifar_cnn_b_adv.yaml
"solver:
  batch_size: 512
  beta-crown:
    iteration: 20"

and

for 6x100:
https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/complete_verifier/exp_configs/beta_crown/mnist_6_100.yaml

"solver:
  batch_size: 1024
  beta-crown:
    iteration: 20"

Our experimental results are in line with published numbers.

> Q5) A single equation containing the whole (inductive) definition of the utility function instead of individual terms distributed across half a page of writing would improve clarity.

Understood. We will provide a simpler form definition.

> Q6) The ResNet is irrelevant given its training and poor accuracy and 20k neurons is quite small for recent verification methods. 

Number of neurons is not the only parmeter to take into account. What you are saying is true for EASY instances. For hard instances, as we shown, even small networks cannot be tackled fully by current verification methods. 

Our tool scales to  at least 20k neurons. 

> "20k neurons is quite small for recent verification methods. The CIFAR-10 networks from Ferrari et al. could be interesting."

From Ferrari et al,  2 CIFAR10 Networks stand out as being "harder to verify":
ResNet6A  (20% undecided images) and ResNet8A (47% undecided images), Table 1 page 7 of https://arxiv.org/pdf/2205.00263 .

For other CIFAR10 networks in Ferrari et al., current methods are efficient enough(<4% undecided images), and better accuracy wont tremendously change the picture.

These 2 networks ResNet6A and ResNet8A actually have LESS neurons (<12k, Table 3 page 14 of https://arxiv.org/pdf/2205.00263 ) than CNN-B-Adv (~20k), so I do not really understand the comment: "20k neurons is quite small for recent verification methods."

Thanks for pointing out more <20k neurons networks which are not easy to verify, this actually makes our point stronger.

That being said, I perfectly understand where you come from, as I had the same belief before working on this paper: 
"current verification tools are fine up to ~100 000 neurons." I changed my mind. One of the paper contribution is actually to expose that fact.

The fact is, we tried to be as fair as possible (by using networks where abCROWN has already been tested, with configuration files provided by the abCROWN authors, with results matching the published results), and what we found suprised at least ourselves.
I thank the authors for their quick reply. However, it unfortunately does not address the majority of my questions. In particular:

Q1) The key part of my question is *after ab-CROWN*. I.e. how does pMILP compare to full MILP (and other utility functions) when run after ab-CROWN using the resulting relatively tight intermediate bounds.

Q2) No, Table 3 does not address this question, as solve time and number of encoded neurons are only loosely correlated for real solvers (some neurons are very easy to stabilize via cutting planes). A "cactus plot" would be the best way to visualize this.

Q4) While Table 5 provides details on the number of open neurons and timeouts, ab-CROWN has a large number of further parameters that are not reported.

Q5) A single equation containing the whole (inductive) definition of the utility function instead of individual terms distributed across half a page of writing would improve clarity.

Q6) The ResNet is irrelevant given its training and poor accuracy and 20k neurons is quite small for recent verification methods. The CIFAR-10 networks from Ferrari et al. could be interesting.
Thanks for your very detailled review.

Some answers now to the questions (which are already in the paper), more later:

>Q1: Can you include experiments using a full-MILP encoding 

full MILP is well known not to scale. Still, we reported an experiment on the smallest of the network (6x100): see Table 2 page 2 "full MILP", realized with a very long 10.000s per image: 50% undecided inputs (90%-40%) for average 6100s per image, compared with 13% undecided images and 46s using Hybrid MILP. And this is the smallest network.
 The analysis is stoppedf for each output neuron (which is not the predicted class) as soon as we have ceritification  or falsitication of robustness, which is the most efficient complete test. Do you think it is necesarry to perform this test for larger networks? The outcome is extremely obvious.

> and different partial MILP encodings using other utility functions 

the only other utility function proposed was by Huang et al. 2020. Table 3 page 8 gives actually a more precise picture that just raw % of robustness, by looking at precise accuracy results. Again, we can do it on say 6x100, but the outcome is also extremely obvious (accuracy number from alpha beta CROWN alone, because the accuracy of pMILP with other utility function and the same number of nodes is very poor). Unless we push the number of nodes of pMILP with other utility function to much higher number, but then, the runtime will be extremely high. We will provide both results to give an exact picture. But again, the overall picture is already very clear from Table 3.


>Q2 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).

Isnt Table 3 page 8 answering this question as well? 
The max line corresponds to full MILP. Specifically, Read line 420 and 421: opening 35 neurons with our utility function reaches 95% of the accuracy of full MILP (all 116 unstable nodes open).

>Q3 How is the solve time in Table 3 affected by the choice of neurons? 

We will report that later. The complexity analysis tells us that it is exponential in the number of chosen neurons.

> And how do the results change if no exact MILP bounds but only LP bounds are available for Layer 2?

We will report such numbers. We expect the number of open nodes in layer 3 has to be considerably higher to reach the same accuracy. Notice that computing bounds in layer 2 is fast (even full MILP can actually be done for layer 2 in short time).
In our prototype, we open 48 nodes for layer 2, and the accuracy is >99.99% of full MILP. But we understand it as ablation study to  see the impact of it on accuracy.


>Q4 Can you discuss the experimental details as per the weaknesses?
"Key parameters of the experimental setup for the main experiment in Table 4 are not discussed"

Well, this is provided in Table 5, page 13 (appendix).

>Q5 Can you include a formulation of the inductive definition of the utility function?

Do you mean for more than 2 layers back?

>Q6 Can you include experiments on larger networks to investigate the limitations of the proposed method?

CNN-B-Adv has ~20.000 neurons, CIFAR Resnet has almost ~100,000 neurons.
We will certainly not scale past what alpha, beta Crown is capable of. 
Our method is meant to be more accurate than alpha beta Crown, not faster or more scalable.
Thanks a lot for your  comments.

1) MaxPool can be treated using MILP, see (Huang et al. 2020). The coding is however more complex, and I doubt we will have time to implement that during the short discussion period.

2) Concerning complexity analysis of pMILP, it is as follows:

O(N · MILP(N, K)), where N is the number of nodes of the DNN, and MILP(N, K) is the complexity of solving a MILP program with 
K binary varialbes and N-K linear variables. We have that MILP(N, K) < 2^K LP(N), where LP(N) is the complexity of running LP, polynomial in N, thus the exponential is only on K. The key factor is thus to keep K as small as possible, which our Utility function enables (see Table 3).

This explains why pMILP is so efficient.

For reference, here is the pseudo code the analysis is based on.
HybridMILP pseudo-code:

    Run Alpha-Beta Crown with small time out (e.g. 10s).

    If image undecided then run pMILP.

pMILP code:

Input: Bounds [α_m, β_m] for input nodes m at layer 0 (input neighbourhood)

Output: Bounds [α_n, β_n] for every output node n

for layer k = 1 · · · K do

       for neuron n in layer k do

           Compute the set Z of the K most important nodes before n according to Utility(n)

          Run partial MILP(Z as binary, nodes / Z as linear variables, with constraints every node m<n satisfy x_m \in [α_m, β_m]  ) 
         to obtain bounds [α_n, β_n] for node n.

return Bounds [α_n, β_n] for every output node n
Thanks a lot for all the pointers.
We are going to consider all of them, in particular run test on GCP-CROWN  on at least some of the benchmarks.

However, to run our independant experiments, IBM CPLEX solver is needed to run GCP-CROWN. 
We just required the permission to use IBM CPLEX solver and waiting for the approval. We will run experiements when its done.

What we can say for now: 
from [General Cutting Planes for Bound-Propagation-Based Neural Network Verification, NeurIPS 2022]:

On CNN-B-ADV, GCP-CROWN is 2% more accurate than alpha,beta CROWN while taking 50% more time.
At least on this important benchmark, this will not change the conclusion tremendously: we have 11% of undecided images vs 20-22% for alpha beta CROWN depending on the time-out duration. Our improvement is much larger than the 2% between alpha,beta CROWN and GCP-CROWN. 


On Parameters used when running abCROWN:
The networks tested have already been tested by abCROWN.
We thus use the configuration files which come for each network in abCROWN (except for time-out which we explicitly mention).

e.g.: for CNN-B-Adv:
https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/complete_verifier/exp_configs/beta_crown/cifar_cnn_b_adv.yaml
"solver:
  batch_size: 512
  beta-crown:
    iteration: 20"

and

or for 6x100:
https://github.com/Verified-Intelligence/alpha-beta-CROWN/blob/main/complete_verifier/exp_configs/beta_crown/mnist_6_100.yaml

"solver:
  batch_size: 1024
  beta-crown:
    iteration: 20"

Our experimental results are in line with published numbers.
So far we did not use GCP-CROWN nor cuts.



Q1:  Two important things. 
1) "This work focuses on networks that are challenging to verify because they are not robustly trained".
This is factually incorrect. Consider for instance CNN-B-Adv. It has been trained to be robust against Adversarial attacks.
Also, we spent quite some time in the introduction to explain that while training to be robust and/or to be more easily verifiable is indeed possible, this can be done only up to a point before hurting accuracy, which is worst than being non robust. 
We certaintly agree that  for easy instances, alpha, beta Crown is very good, this is our point indeed. Then you have the not so easy (but not complexity worst case) instances where alpha, beta CROWN (and every other verifier we tested) does not work that well. And that is our focus (as the easy case can be considered "solved").  Please read the paragraph in the introduction starting at line 052 and ending by "one cannot expect only
easy verification instances: hard verification instances need to be explored as well".
Similar argument is made in the excellent Dathathri et al. (2020).

2) The fact that there are indeed some (rare) truely hard instances is not an excuse for alpha,beta-CROWN (and every other current verifiers we tested) for performing so poorly on so many instances. These instances where alpha,beta CROWN fails are also not "hard" instances in terms of worst case complexity, since our prototype succeeds into solving them in reasonable time (and our prototype does nothing magical - it is just carefully designed). This is a proof that alpha,beta Crown has some important gaps we try to solve (which is the case of MN-Bab also obviously ). We will test to see if it is the case for GCP-CROWN as well, and report on the results.

Concerning the pseudo code:

HybridMILP pseudo-code:

    Run Alpha-Beta Crown with small time out (e.g. 10s).

    If image undecided then run pMILP.

pMILP pseudo code:

Input: Bounds [α_m, β_m] for input nodes m at layer 0 (input neighbourhood)

Output: Bounds [α_n, β_n] for every output node n

for layer k = 1 · · · K do

       for neuron n in layer k do

           Compute the set Z of the K most important nodes before n according to Utility(n)

          Run partial MILP(Z as binary, nodes / Z as linear variables, with constraints every node m<n satisfy x_m \in [α_m, β_m]  ) 
         to obtain bounds [α_n, β_n] for node n.

return Bounds [α_n, β_n] for every output node n



The complexity for pMILP is the following:

O(N · MILP(N, K)), where N is the number of nodes of the DNN, and MILP(N, K) is the complexity of solving a MILP program with 
K binary varialbes and N-K linear variables. We have that We have that MILP(N, K) < 2^K LP(N), where LP(N) is the complexity of running LP, polynomial in N, thus the exponential is only on K.

The key factor is thus to keep K as small as possible, which our Utility function enables (see Table 3).
Yes
No ethics review needed.
Refer to the Weaknesses section
- 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.
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.
**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`