Relational Verification Leaps Forward with RABBit

We are addressing the remaining concerns (after Q4) with additional clarification here.

Q5: The worst-case UAP certified by RABBit in Table 1 is higher than the standard accuracy (Table 3). What do the reported UAPs indicate?

R5: In Table 3 of the paper, we aim to report the standard accuracies (without $\epsilon$) of each of the networks from Table 1 on the CIFAR and MNIST datasets. We realized that we miscalculated the standard accuracies for the MNIST networks and accidentally included the $\epsilon$ column. We have corrected Table 3 from the paper and updated it below in the following table, Table 8.

Table 8: Standard accuracy for evaluated DNNs

As described in line 357, for each network, similar to the relational verifier RACoon [1], we filter out the images that were misclassified by the network and do not consider them for computing UAP accuracy. Thus, the reported UAP accuracy in Table 1 of the paper is computed on the correctly classified images. Overall, the UAP accuracy of the network (that does not filter out misclassified images) will be the standard accuracy $\times$ UAP accuracy from Table 1. We will clarify this in the revised version and report standard accuracy $\times$ UAP accuracy as well.

[1] "Relational DNN Verification With Cross Executional Bound Refinement", D. Banerjee, et. al., ICML, 2024.

Q6: Code is insufficiently documented and buggy.
R6: Thank you for pointing this out. We have fixed the reported issues and shared an anonymized repository with the Area Chair.

Q7: The paper is not sufficiently self-contained. In particular, it does not provide sufficient details on RACoon which it builds upon.
R7: We will add the necessary background for RACoon in the revised version of the paper.

Q8: I find the structure of the paper confusing. I only understood Section 4 after reading Section 5. I think presenting Algorithm 1 before Strong Bounding and Strong Branching would be more clear.

R8: Thanks for the suggestion. We will update it in the revised version of the paper.

Q9: Add a description of what the BaBSR score estimates and of certified adversarial training approaches.

R9: Thanks for pointing this out. We will add a detailed description of these topics in the revised version of the paper.

Q10: Table 2: What are the full architectures or where can I find them?

R10: As mentioned in line 341 of the paper, the ConvSmall and ConvBig architectures are taken from the ERAN repository [1] and the ResNet-2B architecture is from the $\alpha,\beta$-CROWN repository [2].

[1] https://github.com/eth-sri/eran

[2] https://github.com/Verified-Intelligence/alpha-beta-CROWN

Q11: Bibliography Issues and Typos.
R11: Thanks for pointing out the bibliography issues and typos. We will correct all mistakes with citations, spelling, grammar, and figure sizes in the revised version.

Q1: Comparison with SOTA non-relational baseline MNBaB.

R1: We compared the performance of RABBit with the proposed baseline MNBaB across all ConvSmall CIFAR10 networks listed in Table 1 of the paper. The comparison used the same $\epsilon$ values, hardware, and timeout values as mentioned in Section 6.1. While MNBaB outperforms $\alpha,\beta$-CROWN on 3 of the 4 networks, it remains significantly less precise than RABBit, as shown in Table 4. Runtime comparisons are presented in Table 5. For each property, the runtime of a verifier is the timestamp when the verifier first achieves its maximum UAP accuracy within the time limit.

Table 4 UAP accuracy of RABBit vs baselines including MNBaB

Table 5 Average runtime of RABBit vs baselines including MNBaB

Q2: Analyse the sensitivity to randomly sampled problem instances. Report the standard deviations, minima, maxima, and 25%, 50%, and 75% quartiles?

R2: We report the standard deviations and quartiles of the worst-case UAP accuracy for the ConvSmall CITRUS [1] MNIST and CIFAR10 in Tables 6 and 7 respectively. We used the same experimental setup described in section 6.1 of the paper and the same 10 properties from Table 1 in the paper. For all the quartiles, RABBit significantly outperforms all the baselines. We will report the results for all networks in the revised version of the paper.

Table 6: Worst-case UAP accuracy statistics for CIFAR10 ConvSmall CITRUS [1]

Table 7: Worst-case UAP accuracy statistics for CIFAR10 ConvSmall CITRUS [1]

[1] "Cross-Input Certified Training for Universal Perturbations", C. Xu, et. al., ECCV, 2024.

Q3: What are the actual runtimes of RABBit?

R3: Please refer to the answer to Q2 in the common response for the detailed runtime analysis of RABBit and the baselines. The overall time limit given to RABBit is $k=50$ minutes and the result of any MILP instance that was not completed in the given time limit ($k$ minutes) was not considered in the final result. Also, for efficiency, each MILP instance is formulated in either line 16 or line 25 of Algo. 1 is executed in a different thread in parallel to the BaB and does not block subsequent iterations of the loops (lines 10 and 20 of Algo. 1) In all cases, RABBit's runtime is always bounded by $k$ minutes.

Q4: Table 1: How were the perturbation radii chosen?

R4: The perturbation radii used in this work are based on the existing relational verifier RACoon [1]. Other non-relational verifiers like MNBaB [2] also use the same perturbation radii for networks with the same architecture. We also have evaluated the performance of RABBit with different $\epsilon$ values in Figure 3 of the paper.

[1] "Relational DNN Verification With Cross Executional Bound Refinement", D. Banerjee, et. al., ICML, 2024.

[2] "Complete Verification via Multi-Neuron Relaxation Guided Branch-and-Bound", C. Ferrari, et. al., ICLR, 2022.

Q1: In lines 221-224, I cannot follow how to derive $m^{1/n}$ and $m/n$. Please give me an example.

R1: Please refer to the answer to Q3 in the common response.

Q2: In the MILP encoding of RABBIt, What are the new terms/constraints compared to RACoon?

R2: The MILP encoding in RABBit includes additional constraints derived from both strong bounding and strong branching, which are not utilized in RACoon.

• Strong branching constraints: For each target $L_{i}^{j}$, we add a new lower bound constraint $o_i \geq L_{i}^{jT}(\pmb{x_i} + \pmb{\delta}) + b^{j}_{i}$ where $b^{j}\_{i}$ is obtained by strong branching and $o_i = \pmb{c_i}^{T}N(\pmb{x_i} + \pmb{\delta})$. This is discussed in the line 319 of the paper.
• Strong bounding constraints: Suppose for any subset of executions $S \subseteq [k]$, strong bounding proves the absence of common perturbation. We add the following lower bound constraint $\sum_{i \in S} z_{i} \geq 1$. Here $z_i = (o_i \geq 0)$ is a binary variable that indicates whether the constraints $\pmb{c_i}^{T}N(\pmb{x_i} + \pmb{\delta}) \geq 0$ is satisfied or not. The lower bound constraint $\sum_{i \in S} z_{i} \geq 1$ follows from the fact for any $\|\pmb{\delta}\|_{\infty} \leq \epsilon$ at least one execution from $S$ remains correctly classified. This is discussed in the lines 313 - 316 of the paper.

Q3: Strong bounding provides tighter bounds than RACoon and $\alpha,\beta$-CROWN. Although the experiments validate this claim, the paper offers no proof. This claim might not hold, especially considering the $k_t$ and the time limit used in Algorithm 1.

R3: Strong bounding is a BaB method that uses cross-executional bounding as the bounding step. Given RACoon uses the same bounding methods and does not employ branching, for the same time limit, strong bounding will be at least as precise as RACoon. However, as correctly pointed out, for some cases $\alpha,\beta$-CROWN can outperform strong bounding. However, our experiments show that for practical scenarios, strong bounding outperforms $\alpha,\beta$-CROWN.

Q4: In Section 4.2, the strong branching method seems to me only a preprocessing rather than a counterpart to the strong bounding method. Is the strong branching method only to guarantee that RABBIt's bound is tighter than $\alpha,\beta$-CROWN bound?

R4: Strong bounding can only prove the absence of common perturbation for a set of executions $S \subseteq [k]$. Hence, with strong bounding, we can only show at least 1 execution from $S$ is correctly classified. However, this approach is suboptimal for cases where the number of correctly classified executions from $S$ is $> 1$. In contrast, strong branching extracts the same target linear approximation for all subproblems, allowing us to formulate an efficiently optimizable MILP instance with these targets. This MILP instance can address cases where more than one execution from $S$ is correctly classified. Also, strong branching allows us to explore more branches per execution as explained in answer to Q3 in the common response. Strong branching is not a preprocessing step and is important for improving the precision of RABBit, as demonstrated by the results in Table 1 of the paper.

Q5: Missing related work.

R5: Thanks for pointing out. We will add it to the revised version of the paper.

Q6: In Section 4.2, $N(\pmb{x_i} + \pmb{\delta})$ is a vector but $\pmb{L_{j}}^{T}(\pmb{x_i} + \pmb{\delta}) + b^{*}\_j$ is a scalar. Does the paper want to express $\pmb{c_{i}^{T}}N(\pmb{x_i} + \pmb{\delta})$?

R6: Thanks for pointing out. In section 4.2, it should be $\pmb{c_{i}^{T}}N(\pmb{x_i} + \pmb{\delta})$ instead of $N(\pmb{x_i} + \pmb{\delta})$. We will correct it in the revised version of the paper.

Q7: Presentation of the paper.

R7: We will provide a formal definition of worst-case UAP accuracy and the MILP optimization problem used to compute it before they are cited. We will also correct the citation issues noted in the revised version.

Q1: Do you have experiments w.r.t. other relational properties? If not, would you be willing to adjust the title and content of the paper to focus on UAP properties? -- In either case, I would be willing to raise my score to Accept.

R1: Please refer to the answer to Q1 in the common response.

Q2: "All complete non-relational verifiers are also incomplete for relational properties since they do not track any dependencies between executions" - Completeness depends on the specific relational property.

R2: We agree that completeness depends on the specific relational property being verified. In this case, we refer to relational properties such as robustness against UAP, where it is important to track dependencies between perturbed inputs across different executions to achieve completeness. Existing complete verifiers like $\alpha,\beta$-CROWN, which are designed for verifying input-specific robustness, will be incomplete if they verify each execution independently without tracking these dependencies. Please refer to lines 168-173 of the paper, where we describe a scenario in which input-specific adversarial perturbations exist for individual inputs, but no common adversarial perturbation exists. We will rephrase the highlighted sentence to clarify this.

Q3: Can the heuristics employed by RABBit and RACoon lead to incompleteness when it comes to providing exact UAP bounds?

R3: RACoon does not use any branching and is incomplete. In RABBit, for scalability, we greedily select subsets of executions and run strong bounding only on the selected subsets. For this reason, the current implementation of RABBit is also incomplete and only computes a sound lower bound on the worst-case UAP accuracy. However, it is possible to make RABBit complete by considering all possible subsets of executions and then formulating the MILP formulation.

Q4: Do I correctly assume that your comparison with $\alpha,\beta$-CROWN uses a problem formulation based on a product NN and the k-UAP linear constraint formulation?

R4: Yes, $\alpha,\beta$-CROWN is applied to the product DNN. However, unlike the strong bounding approach proposed in RABBit, the bounding method of $\alpha,\beta$-CROWN does not track any dependencies. As a result, even when $\alpha,\beta$-CROWN is executed on the product DNN, it computes the lower bound $\pmb{c_i}^TN(\pmb{x_i} + \pmb{\delta})$ for each execution independently and loses precision.

Q5: Questions about $m^{1/n}$ and $m/n$ subproblems.

R5: Please refer to the answer to Q3 in the common response. We will add a more explicit description in the revised version.

Q6: Minor notes on the presentation of the paper.

R6: Thanks for pointing out. We will add the suggested changes in the revised version of the paper.

Q1: In Table 1, how long does it take to run each verification?

R1: Please refer to the answer to Q2 in the common response.

Q2: In Table 1, why the non-relational verifier $\alpha,\beta$-CROWN outperformed the SOTA relational verifier RACoon? Is it because $\alpha,\beta$-CROWN uses BaB?

R2: SOTA relational verifier RACoon is incomplete and utilizes a single bounding step without branching. Although RACoon is significantly more precise than $\alpha$-CROWN, the bounding step used in $\alpha,\beta$-CROWN, $\alpha,\beta$-CROWN outperforms it by exploring a large number of branches with BaB. We discuss this limitation of RACoon in lines 47--48 of the paper.

Q3: Are there relational properties other than UAP that can be verified and evaluated?

R3: Please refer to the answer to Q1 in the common response.

Q4: Are there 10 different versions of UAP or 10 unique use cases of relational verification in general?

R4: We consider 10 different instances of the UAP verification problem where each instance is defined on a set of 50 images as described in line 356. For the details on another relational property that can be verified by RABBit, please refer to the response to Q1 in the common response.

Q5: Grammatical errors and typing mistakes.

R5: We apologize for the grammatical and typing errors and will correct them in the revised version of the paper.

Dear AC and reviewers,

As the discussion period comes to an end, we want to express our gratitude for your time. We believe that our comments have addressed all concerns or questions. We are summarizing the clarifications to the major concerns here, and we hope that they will be taken into account when making the final decision.

• Code - We have fixed the installation issues and provided all networks and detailed instructions for reproducing the experimental results. Thanks, reviewer aDbJ for confirming that the updated version of code is working.
• non-relational verifiers: $\alpha,\beta$-CROWN is one of the most popular and strongest non-relational verifiers, and our submitted paper already includes a detailed comparison with it. However, as suggested by reviewer aDbJ, we included comparisons with both MNBaB and GCP-CROWN on CIFAR10 networks. In both cases, RABBit significantly outperforms the corresponding non-relational verifier (see Table 10 of the rebuttal). Beyond the experiments, we discuss why non-relational verifiers are theoretically limited for relational properties. We append these additional results and explanations to further substantiate our claims.
• Sensitivity and experimental setup: We show that the gains obtained by RABBit are statistically significant (see Table 11 of the rebuttal). Furthermore, the papers on various DNN verifiers, including GCP-CROWN and RACoon, use the same or even fewer inputs and relational properties in their evaluations. We also clarified that the experimental setup, including timeout values, matches what was described in the paper. We have not changed the experimental setup and proposed algorithm.
• Comment on Resubmission by Reviewer aDbJ: It is a standard practice at top-tier ML conferences like NeurIPS, ICML, and ICLR to provide extra results/details as requested by the other reviewers. For example, this was the case for both GCP-CROWN [1] and MnBab [2] which the reviewer asked us to compare against. Moreover, issues related to software installation are not uncommon, even for widely used tools like alpha-beta CROWN [3] and ERAN [4], which have publicly documented installation problems on GitHub. We have already resolved the installation issues in our code, and reviewer aDbJ confirmed that the updated version of the code works. Since the concerns have already been addressed, incorporating the changes does not necessitate resubmission, as with other papers.

[1] https://openreview.net/forum?id=5haAJAcofjc

[2] https://openreview.net/forum?id=l_amHf1oaK

[3] https://github.com/Verified-Intelligence/alpha-beta-CROWN/issues

[4] https://github.com/eth-sri/eran/issues

The provided code is still buggy. The README in the zip archive linked above describes creating a conda environment with Python 3.7 (RABBit-main/src/abc/complete_verifier/environment.yml), but the code does not compile under Python 3.7

python -m unittest -v tests.test_rabbit.TestUAP.test_cifar_uap_diffai
Traceback (most recent call last):
  File "/home/vboxuser/miniconda3/envs/rabbit2/lib/python3.7/runpy.py", line 193, in _run_module_as_main
    "__main__", mod_spec)
  [...]
    from src.metaScheduler import MetaScheduler
  File "/home/vboxuser/RABBit (copy)/RABBit-main/src/metaScheduler.py", line 565
    return all_tuples, all_refined_tuples, orig_scores, *self.process_selected_tuples(selected_tuples, selected_refined_tuples)

Dear Reviewers aDbJ and uEoH,

It appears the issue may be related to the Python version you are using. Our experiments were conducted using Python 3.10.10. We have provided an updated version along with instructions on how to install the dependencies (see below and in the README file). After installation, please verify that the installed Python version is 3.10.10. Additionally, ensure that you have the Gurobi license installed on your device; instructions for obtaining the license are included in the README file.

annonymized link to the code: https://figshare.com/s/9dfe74654ea6f5a5ee24

# Remove any environment named rabbit if it exists
conda remove -n rabbit --all
# create the new environment from the RABBit directory
conda env create -f environment_rabbit.yml --name rabbit
# activate the environment
conda activate rabbit
# Check the correct python version "3.10.10" is installed or not 
python --version

If you encounter any issues with the code, please let us know. We will be happy to assist you.