Relational Verification Leaps Forward with RABBit

Authors: tarun  suresh
debangshu  banerjee
gagandeep  singh
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-15 13:38:23

Abstract: We propose RABBit, a Branch-and-Bound-based verifier for verifying relational properties defined over Deep Neural Networks, such as robustness against universal adversarial perturbations (UAP). Existing SOTA complete $L_{\infty}$-robustness verifiers can not reason about dependencies between multiple executions and, as a result, are imprecise for relational verification. In contrast, existing SOTA relational verifiers only apply a single bounding step and do not utilize any branching strategies to refine the obtained bounds, thus producing imprecise results. We develop the first scalable Branch-and-Bound-based relational verifier, RABBit, which efficiently combines branching over multiple executions with cross-executional bound refinement to utilize relational constraints, gaining substantial precision over SOTA baselines on a wide range of datasets and networks. Our code is at https://github.com/uiuc-focal-lab/RABBit.

Main paper: 
 introduction: 
 Deep neural networks (DNNs) are now widely used in safety-critical fields like autonomous driving and medical diagnosis [Amato et al., 2013] , where their decisions can have serious consequences. However, understanding and ensuring their reliability is difficult due to their complex and opaque nature. Despite efforts to find and address vulnerabilities, such as adversarial attacks [Goodfellow et al., 2014 , Madry et al., 2018 , Moosavi-Dezfooli et al., 2017] and adversarial training techniques [Madry et al., 2018] , ensuring safety remains a challenge. As a result, extensive research is focused on formally verifying the safety of DNNs. However, most of the existing L ∞ robustness verification techniques can not handle relational properties common in practical situations. While significant efforts have been invested in verifying the absence of input-specific adversarial examples within the local neighborhood of test inputs, recent studies [Li et al., 2019a] emphasize that input-specific attacks are impractical regardless. Conversely, practical attack scenarios [Liu et al., 2023 , Li et al., 2019b,a] involve the creation of universal adversarial perturbations (UAPs) [Moosavi-Dezfooli et al., 2017] , which are crafted to impact a substantial portion of inputs from the training distribution. RaVeN [Banerjee et al., 2024b] and subsequently RACoon [Banerjee and Singh, 2024] showed that since the same adversarial perturbation is applied to multiple inputs, the executions on different perturbed inputs are related, exploiting the relationship between different executions significantly improves the precision of the verifier. Despite RaVeN and RACoon's ability to leverage cross-executional dependencies, both of them remain imprecise as they only apply a single bounding step and lack refinement using branching strategies used in SOTA complete non-relational verifiers.Key challenges: For precise relational verification, we need efficient algorithms that can effectively combine branching strategies over multiple executions with bounding techniques that can leverage cross-executional dependencies. Theoretically, MILP (Mixed Integer Linear Programming) can exactly encode DNN executions with piecewise linear activation functions like ReLU over any input regions specified by linear inequalities. However, the associated MILP optimization problem is computationally expensive. For instance, encoding k executions of a DNN with n r ReLU activations introduces O(n r × k) integer variables in the worst case. As the cost of MILP optimization grows exponentially with the number of integer variables, even SOTA off-the-shelf solvers like Gurobi [Gurobi Optimization, LLC, 2018] struggle to verify small DNNs for a relational property over k executions within a reasonable time limit. For scalability, SOTA non-relational verifiers like α, β-CROWN [Wang et al., 2021] design custom "Branch and Bound" (BaB) solvers using more scalable differentiable optimization techniques such as gradient descent. However, these verifiers ignore dependencies between multiple executions, resulting in imprecise relational verification. Conversely, the SOTA relational verifier RACoon uses parametric linear relaxation for each activation to avoid integer variables and employs gradient descent to learn parameters that leverage cross-executional dependencies for verification. This method, however, introduces imprecision due to the replacement of non-linear activations with parametric linear approximations. Therefore, precise relational verification requires scalable algorithms that can: a) scale to the large DNNs used in this paper, b) effectively reduce imprecision from parametric linear relaxations, and c) utilize cross-executional dependencies.Our contributions: We advance the state-of-the-art in relational DNN verification by:• Efficiently combining branching strategies over multiple DNN executions with a cross-executional bounding method that utilizes dependencies between DNN's outputs from different executions while reducing imprecision resulting from parametric linear relaxations. • Developing two "branch and bound" algorithms, each with its own advantages -a) strong bounding:applies cross-execution bounding at each step, branching over all executions. This method provides tighter bounds than RACoon (cross-executional bound refinement without branching) and α, β-CROWN (branching without cross-executional bound refinement), b) strong branching: applies cross-execution bounding only at the start to derive fixed linear approximations for each execution. These approximations are then used to branch independently over each execution, exploring more branches per execution. • Combining strong bounding and branching results into an efficiently optimizable MILP instance that leverages the benefits of both techniques, outperforming each individually. • Performing extensive experiments on popular datasets and various DNNs (standard and robustly trained) to showcase the precision improvement over the current SOTA baselines. 
related works: 
 Non-relational DNN verifiers: Given a logical input specification ϕ and an output specification ψ, DNN verifiers formally prove that for all inputs x satisfying ϕ, the output N (x) of the DNN satisfies ψ. If the verification process fails, the verifier generates a counter-example where the output specification ψ does not hold. DNN verifiers are broadly divided into three main types based on their ability to prove properties: -(i) sound but incomplete verifiers which may not always prove property even if it holds [Gehr et al., 2018 , Singh et al., 2018 , 2019b ,a, Zhang et al., 2018 , Xu et al., 2020 , 2021] , (ii) complete verifiers that can always prove the property if it holds [Wang et al., 2018 , Gehr et al., 2018 , Bunel et al., 2020a ,c, Bak et al., 2020 , Ehlers, 2017 , Ferrari et al., 2022 , Fromherz et al., 2021 , Wang et al., 2021 , Palma et al., 2021 , Anderson et al., 2020 , Zhang et al., 2022a] and (iii) verifiers with probabilistic guarantees [Cohen et al., 2019 , Li et al., 2022] . Beyond the commonly studied L ∞ robustness verification problem, several works adapt DNN verification techniques for specific applications, such as robustness against image rotation [Singh et al., 2019b , Balunovic et al., 2019] , incremental verification [Ugare et al., 2023 [Ugare et al., , 2024]] , interpretability [Banerjee et al., 2024a] , and certifiable training [Mueller et al., 2023 , Palma et al., 2024 , Jiang and Singh, 2024] .Relational DNN verifier: Existing relational verifiers fall into two main categories based on the type of relational properties they can handle: (i) verifiers for properties such as UAP and fairness, which are defined across multiple executions of the same DNN [Zeng et al., 2023 , Khedr and Shoukry, 2023 , Meyer et al., 2024 , Banerjee et al., 2024b , Banerjee and Singh, 2024 , Banerjee et al., 2024c] , and (ii) verifiers for properties like local DNN equivalence, defined over multiple executions of different DNNs on the same input [Paulsen et al., 2020 [Paulsen et al., , 2021]] . For relational properties defined across multiple executions of the same DNN, existing verifiers [Khedr and Shoukry, 2023] reduce the verification problem to an L ∞ robustness problem by constructing a "product DNN" that includes multiple copies of the same DNN. However, the relational verifier in [Khedr and Shoukry, 2023] treats all k executions of the DNN as independent, which results in a loss of precision. On the other hand, [Zeng et al., 2023] (referred to as the I/O formulation) tracks the relationships between inputs used in multiple executions at the input layer, but it does not maintain the relationships between the outputs fed into the subsequent hidden layers. As a result, it achieves only limited improvement over baseline verifiers that treat all executions independently. RaVeN [Banerjee et al., 2024b] uses DiffPoly a abstract intepretation based framework to track linear relationships between the outputs at all layers resulting from multiple executions of the same DNN. While RaVeN is significantly more precise than the I/O formulation, tracking linear constraints at each layer across all DNN executions can be computationally expensive. The SOTA relational verifier RACoon [Banerjee and Singh, 2024] improves the scalability of RaVeN while maintaining RaVeN's precision by introducing a new gradient-descent based bounding strategy called cross-executional bound refinement, as detailed in Section 3. There exist, probabilistic verifiers, [Xie et al., 2021 , Zhang et al., 2022b] based on randomized smoothing [Cohen et al., 2019] for verifying relational properties. However, these works can only give probabilistic guarantees on smoothed models which have high inference costs.Similar to [Banerjee et al., 2024b, Banerjee and Singh, 2024] , in this work, we focus on deterministic relational verifiers for DNNs with ReLU activation. However, RABBit can be extended to activations like Sigmoid with branching methods [Shi et al., 2024] and parametric bounds [Wu et al., 2023] . 
preliminaries: 
 We provide background on "branch and bound" (BaB) based non-relational DNN verification, as well as DNN safety properties that can be encoded as relational properties.Non-relational DNN verification: For a single execution, non-relational DNN verification focuses on proving that, for all perturbations x +δ δ δ of a given input x specified by ϕ, the network's output y = N (x + δ δ δ) meets a specified logical condition ψ. Commonly, safety properties such as L ∞ robustness encode the output condition (ψ) as a linear inequality or a conjunction of linear inequalities over the DNN output y ∈ R n l . For instance, an output property could be expressed as ψ(y) = (c T y ≥ 0), where c ∈ R n l . Generally, even for DNNs with piecewise-linear activation functions and input constraints defined by linear inequalities, complete verification-i.e., always proving the property or finding a counterexample-is an NP-complete problem. Given a DNN N : R n0 → R n l and a property defined by (ϕ, ψ), scalable yet sound (but incomplete) verifiers approximate the network's behavior by computing a linear approximation specified by L ∈ R n0 and b ∈ R. For any input x satisfying ϕ, this linear approximation ensures that L T x + b ≤ c T N (x). The verifier then aims to show that L T x + b ≥ 0 for all x that satisfy ϕ, which implies c T N (x) ≥ 0. While L T x + b provides a valid lower bound for c T N (x), it may lack precision. To enhance this precision for piecewise-linear activations, state-of-the-art non-relational verifiers use a branch-and-bound (BaB) method. In each branching step, the problem is divided into smaller subproblems, while the bounding method computes a valid lower bound for each subproblem.Branching for piecewise linear activation: The non-relational verifier computes L by replacing non-linear activations with linear relaxations, which introduces imprecision. However, for piecewise linear activations like ReLU, it is possible to consider each linear piece separately as different subproblems, avoiding the need for imprecise linear relaxations. For instance, for y = ReLU (x), branching on x and considering the cases x ≤ 0 and x ≥ 0 allows decomposing ReLU (x) into two distinct linear pieces. Still in the worst case decomposing all ReLU nodes in a DNN results in exponential blowup making it practically infeasible. Therefore, SOTA non-relation verifiers like α, β-CROWN [Wang et al., 2021] greedily pick a small subset of ReLU nodes for branching while using linear relaxations for the rest. We explain the bounding step used for each subproblem below.Bounding with parameter refinement: Obtaining sound linear relaxations of activations σ like ReLU, which are not used for branching, involves computing linear lower bounds σ l (x) and upper bounds σ u (x) that contain all possible outputs of σ w.r.t all inputs x satisfying ϕ. That is, for all possible input values x of σ, σ l (x) ≤ σ(x) ≤ σ u (x) holds. SOTA non-relational verifiers, such as α, β-CROWN, improve precision by using parametric linear relaxations instead of static linear bounds and refine the parameters to facilitate verification of the property (ϕ, ψ). For example, for ReLU (x), the parametric lower bound is ReLU (x) ≥ α × x with α ∈ [0, 1]. Since α × x remains a valid lower for any α ∈ [0, 1], this allows optimizing α while ensuring the bound remains mathematically correct. Each branched ReLU say y = ReLU (x), introduces two subproblems each with one additional constraint x ≤ 0 (or, x ≥ 0) where ReLU behaves as a linear function i.e. y = 0 (or, y = x) respectively. To obtain the lower bound of L T x + b over inputs satisfying ϕ with the additional branching constraints α, β-CROWN convert the constrained optimization problem into an unconstrained one by looking at the Lagrangian dual. The dual replaces each branching constraint by augmenting the minimization objective L T x + b with additional terms i.e. L T x + b + β + x for x ≤ 0 or L T x + b + β -x for x ≥ 0 where β + ≥ 0 and β -≤ 0. Overall, at high level, α, β-CROWN computes parametric linear approximations L(α α α, β β β ) T x + b(α α α, β β β ) and refine the parameters α, β to facilitate verification of (ϕ, ψ).DNN relational properties: Relational properties defined for a DNN N : R n0 → R n l defined over k executions of N are specified by the tuple (Φ, Ψ). Here, Φ : R n0×k → {true, f alse} (the input specification) encodes the input region Φ t ⊆ R n0×k encompassing all potential inputs corresponding to each of the k executions of N . Furthermore, the safety property we expect the outputs of all k executions of N to satisfy is specified by Ψ : R n l ×k → {true, f alse} (the output specification). Given N , an input specification Φ and an output specification Ψ, DNN relational verification seeks to formally prove whether ∀x * 1 , . . . ,x * k ∈ R n0 .Φ(x * 1 , . . . , x * k ) =⇒ Ψ(N (x * 1 ), . . . N (x * k ))or otherwise provide a counterexample. The inputs to the k executions of N are denoted by x * 1 , . . . , x * k and the corresponding outputs are denoted by N (x * 1 ), . . . , N (x * k ). For the i-th execution, commonly, the input regionϕ i t is a L ∞ region around a fixed point x i ∈ R n0 defined as ϕ i t = {x * i ∈ R n0 | ∥x * i -x i ∥ ∞ ≤ ϵ} and the corresponding output specification ψ i (N (x * i )) = m j=1 (c i,j T N (x * i ) ≥ 0). Consequently, Φ(x * 1 , . . . , x * k ) = k i=1 (x * i ∈ ϕ i t ) Φ δ (x * 1 , . . . , x * k ) where Φ δ (x * 1 , . . . , x * k ) encodes the relation- ship between the inputs used in different execution and Ψ(N (x * 1 ), . . . , N (x * k )) = k i=1 ψ i (N (x * i )). Following this, we describe relational properties encoding important DNN safety configurations.UAP verification: In a UAP attack, given a DNN N , the adversary aims to find an adversarial perturbation with a bounded L ∞ norm that maximizes the rate at which N misclassifies when the same adversarial perturbation is applied to all inputs from the distribution. The UAP verification problem aims to find the worst-case accuracy of N against the UAP adversary. We refer to this worst-case accuracy as UAP accuracy in the rest of the paper. As shown by Theorem 2 in [Zeng et al., 2023] , it is possible to statistically estimate the UAP accuracy of N with respect to the input distribution if one can determine the UAP accuracy of N on k randomly selected images. We focus on the k-UAP verification problem for the rest of the paper as improving the precision of k-UAP verification directly improves the UAP accuracy on the input distribution [Banerjee and Singh, 2024] . The k-UAP verification problem is fundementally different from local L ∞ robustness verification since the same adversarial perturbation is applied across the set of inputs. Thus, improving precision for the UAP verification problem requires a relational verifier that can exploit dependencies between the perturbed inputs. We provide the Φ and Ψ of the UAP verification problem in Appendix A.1. 
cross-executional bab: 
 The key distinction between relational and non-relational DNN verification is the dependency between different DNN executions, which necessitates that any precise relational verifier utilizes these crossexecution dependencies. For instance, for k-UAP problem with two images x 1 , x 2 consider the scenario where both x 1 and x 2 have valid adversarial perturbations δ 1 δ 1 δ 1 and δ 2 δ 2 δ 2 but no common perturbation say δ δ δ that works for both x 1 and x 2 . In this case, any non-relational verification that does not account for cross-execution dependencies can never prove the absence of a common perturbation given that both x 1 , x 2 have valid adversarial perturbations. This highlights the importance of utilizing cross-executional dependencies. The SOTA relational verifier RACoon [Banerjee and Singh, 2024] leverages cross-execution dependencies to jointly optimize the α α α parameters from different executions, significantly improving the precision of relational verification. However, RACoon only uses parametric linear relaxations for non-linear activations and lacks a branching step, resulting in reduced precision, as confirmed by our experimental results in Section 6. To address this, we propose two separate BaB algorithms, each with its benefits, described in Sections 4.1 and 4.2. Finally, we combine the results to formulate an efficiently optimizable MILP instance in Section 5Before going into the details, we briefly review the cross-executional bound refinement proposed in RACoon. For k-UAP, given any subset S of the k executions, RACoon can verify the absence of any common perturbation that works for all executions in S with cross-executional bound refinement. For all i ∈ S, let (L i (α α α i ), b i (α α α i )) denote the parametric linear approximations corresponding to the i-th execution. Then the optimal value t * = max α α αi,λi -ϵ×∥ i∈S λ i ×L i (α α α i )∥ 1 + i∈S λ i ×a i (α α α i ) ≥ 0 proves the absence of a common perturbation δ δ δ for S. Here, ϵ is the perturbation boundi.e. ∥δ δ δ∥ ∞ ≤ ϵ, a i (α α α i ) = b i (α α α i )+L i (α α α i ) T x i and λ i ∈ [0, 1]with i∈S λ i = 1 are the cross-executional parameters that relate linear approximations from different execution enabling joint optimization over α α α i s. Next, we detail the first BaB method -strong bounding that combines cross-executional bounding with branching methods to verify the absence of common perturbation for any subset of n = |S| executions.Branching and bounding: For n ≤ k executions, we construct a "product DNN" by duplicating the DNN n times, one for each execution. Formally, a product DNN is a function N n : R n0×n → R n l ×n with N n (x 1 , . . . , x n ) = [N (x 1 ), . . . , N (x n )] T . At each branching step, we greedily select a subset of unbranched ReLU activations from the product DNN and branch on them, while using parametric linear relaxations for the rest. We adapt existing greedy branching heuristics, such as BaBSR [Bunel et al., 2020b] , for selecting the candidate ReLU activations. The heuristic computes a score for each unbranched ReLU activation in the product DNN, and we branch on the activations with the highest scores. Next, we detail the bounding method applied to each subproblem resulting from branching. Since the number of subproblems can be large, the bounding method needs to be fast yet capable of leveraging both branching constraints and cross-executional dependencies. However, the crossexecutional bound refinement from RACoon can not handle branching constraints, while the bounding step from α, β-CROWN does not utilize dependencies across executions. Hence, we develop a threestep algorithm for obtaining the optimal value t * with fast gradient descent-based methods. First, we replace these branching constraints by introducing dual variables β β β , resulting in new parametric linear approximations(L i (α α α i , β β β i ), b i (α α α i , β β β i ))for each subproblem for all i ∈ S. Then for each subproblem, we introduce additional variables λ i for each execution with constraints λ i ∈ [0, 1] and i∈S λ i = 1. These λ i s relate linear approximations from different executions capturing cross-executional dependencies. This reduces finding t * for each subproblem to the following optimization problemt * = max α α αi,β β βi,λi -ϵ × ∥ i∈S λ i × L i (α α α i , β β β i )∥ 1 + i∈S λ i × a i (α α α i , β β β i ). Here, a i (α α α i , β β β i ) = b i (α α α i , β β β i ) + L i (α α α i , β β β i ) T x i .Finally, we apply projected gradient ascent to refine parameters (α α α i , β β β i , λ i ). The detailed derivation of the bounding step and the proof of correctness is in Appendix B. Precision gains of strong bounding over the baselines are in Section 6.2. Suppose, F(S) denotes the set of subproblems then Theorem 4.1 proves the absence of common perturbation for the subset of executions S.Theorem 4.1. If min F (S) max α α αi,β β βi,λi -ϵ × ∥ i∈S λ i × L i (α α α i , β β β i )∥ 1 + i∈S λ i × a i (α α α i , β β β i ) ≥ 0 then executions in S do not have a common perturbation δ δ δ ∈ R n0 with ∥δ δ δ∥ ∞ ≤ ϵ.Proof: The detailed proof is in the Appendix B.While strong bounding effectively combines cross-executional refinement with branching, it has the following drawbacks that led to the development of the 2nd BaB method. First, strong bounding branches over all executions simultaneously, which limits the number of branches explored per execution within a fixed timeout compared to branching on individual executions. For instance, if strong bounding solves m subproblems for n executions, then assuming each execution branched uniformly, each execution gets only m 1 n subproblems. In contrast, given the same timeout, branching individually allows exploring m n subproblems per execution. Second, strong bounding only proves the absence of common perturbation, a relaxation of the k-UAP problem. To mitigate this, RACoon uses parameter refinement to obtain linear approximations and formulate a MILP, providing a more precise bound on k-UAP accuracy. However, for strong bounding, as the number of subproblems increases and each subproblem has a different linear approximation, formulating a MILP with each linear approximation is practically infeasible. Restricting the number of linear approximations can help accommodate MILP formulation by compromising on the strong cross-executional bounding.Unlike strong bounding, strong branching explores more branches by branching on each execution independently. Additionally, for each execution, we aim to keep the number of linear approximations small post-branching, ensuring the MILP instance using these approximations remains easy to optimize. To limit the number of linear approximations for each execution i, we fix a set of linear coefficients {L 1 , . . . , L m } called "target coefficients" and for each j ∈ [m], L j ∈ R n0 compute valid lower bound b * j of the following optimization problem min δ δ δ c T N (x i + δ δ δ) -L T j (x i + δ δ δ) with ∥δ δ δ∥ ∞ ≤ ϵ using BaB. In this case, for all δ δ δ ∈ R n0 with ∥δ δ δ∥ ∞ ≤ ϵ the refined bias b * j and L j remain a valid lower bound of c T N (x i + δ δ δ) i.e. L T j (x i + δ δ δ) + b * j ≤ c T N (x i + δ δ δ).Moreover, since we only refine the bias, the number of linear approximations remains the same as at the start of BaB, even after branching. Next, we describe how we utilize cross-execution dependencies while branching on each execution independently.Selecting targets: To select target coefficients, we greedily pick subsets of executions and run cross-executional refinement from RACoon without branching on each subset of executions. We describe the greedy selection strategy in Section 5. For each set of executions, we add the linear approximations obtained by cross-executional refinement to the corresponding executions' target sets. Cross-executional refinement ensures for each execution set the parameters corresponding to the linear approximations are tailored for the relational verification.Bounding and branching: Given a target coefficient L t ∈ R n0 , since finding the exact solution of min δ δ δ c T N (x i + δ δ δ) -L T t (x i + δ δ δ) is computationally expensive, strong branching aims to obtain a tight mathematically correct lower bound on the difference c T N (x i + δ δ δ) -L T t (x i + δ δ δ). For any subproblem, let (L(α α α, β β β ), b(α α α, β β β )) denote the parametric linear approximation. Then for this particular subproblem, for all α α α, β β β , L(α α α, β β β ) T (x i + δ δ δ) + b(α α α, β β β ) ≤ c T N (x i + δ δ δ) and subsequently:max α α α,β β β min ∥δ δ δ∥∞≤ϵ (L(α α α, β β β ) -L t ) T (x i + δ δ δ) + b(α α α, β β β ) ≤ min ∥δ δ δ∥∞≤ϵ c T N (x i + δ δ δ) -L T t (x i + δ δ δ) (1)The optimal solution of the max-min problem in Eq. 1 provides a mathematically correct lower bound of min δ δ δ c T N (x i + δ δ δ) -L T t (x i + δ δ δ) for each subproblem. However, it is hard to solve a max-min problem with scalable differentiable optimization techniques like gradient descent typically used for large DNNs considered in this paper. Instead, we compute a closed form of the inner minimization problem reducing the optimization instance to a more tractable maximization problem (Theorem 4.2).Theorem 4.2. For anyα α α, β β β , if L(α α α, β β β ) ∈ R n0 and b(α α α, β β β ) ∈ R then min ∥δ δ δ∥∞≤ϵ (L(α α α, β β β ) - L t ) T (x + δ δ δ) + b(α α α, β β β ) = -ϵ × ∥L(α α α, β β β ) -L t ∥ 1 + (L(α α α, β β β ) -L t ) T x + b(α α α, β β β ). Proof: The proof is in Appendix C.We apply a projected gradient ascent to optimize the maximization with the closed form obtained above (Appendix C.1). The proof of the correctness of the bounding method is in Appendix C. Note the proof of correctness does not necessitate the optimizer to find the global optimum. This is important since gradient ascent may not always converge to the global optimum. Since strong branching branch on each execution independently we reuse the branching strategy of α, β-CROWN. 
rabbit: 
 In this section, we detail the algorithm (Algo. 1) that combines the results from strong bounding and strong branching to formulate the MILP. Running strong bounding on all 2 k -1 non-empty subsets of k executions is impractical. Therefore, we use a greedy approach to select subsets of executions for strong bounding. Similarly, for strong branching, we greedily select the target linear coefficients. First, we describe both greedy strategies before moving on to the MILP formulation.Elimination of individually verified executions: RABBit maintains a list of unverified indices and eliminates any executions that can be verified individually and does not consider them for subsequent steps (lines 3, 8, and 13 in Algo. 1). For instance, for k-UAP verification, we do not need to consider those executions that are proved to have no adversarial perturbation δ δ δ such that ∥δ δ δ∥ ∞ ≤ ϵ. Pruning individually verified executions improves the runtime without any compromise on the precision of the relational verifier (see Theorem B.1 [Banerjee and Singh, 2024] ).Greedy target coefficient selection: RABBit first runs RACoon which in turn executes an incomplete non-relational verifier α-CROWN [Xu et al., 2021] eliminating the verified executions (line 8 in Algo. 1). Subsequently, for target selection, RABBit greedily picks the first k t (hyperparameter) executions based on s i the lower bound on ψ i (N (x i + δ δ δ)) as computed by α-CROWN, prioritizing executions with higher s i (line 9). Intuitively, for unverified executions, s i measures the maximum violation of the output specification ψ i (N (x i + δ δ δ)) and thus leads to the natural choice of picking executions with smaller violations. For each selected execution i, we choose up to m target coefficients by iterating over all subsets i ∈ S considered by RACoon, and selecting linear approximations corresponding to the top m subsets.The cross-executional lower bound t * from RACoon decides the priority of each subset S. Subsets S with higher t * indicate smaller violations and are more likely to be verified for the absence of a common perturbation, making them suitable for target selection. end if 28: end while 29: return M the cross-executional bound obtained by RACoon on S decides its priority. However, considering all non-empty subsets of I can be expensive. Instead, similar to strong branching, we first pick top-k t executions (I 2 ) from I (Algo 1 line 19). We sort all non-empty subsets S ⊆ I 2 based on their priority and, in each iteration, run strong bounding on the highest-priority subset that has not been scheduled yet (Algo 1 line 22). Given a large timeout, RABBit would eventually select all subsets from I 2 .b * i ← StrongBranching(ϕ i , ψ i , L[i]) 12: if Verified(ϕ i , ψ i , L[i], b * i ) thenThe MILP formulation uses both the refined biases from strong branching (line 11) and the subsets S of executions verified for the absence of common perturbation from strong bounding (line 22) to compute final verified UAP accuracy. RABBit MILP formulation involves three steps. First, we deduce linear constraints between the input and output of N for each unverified execution using linear approximations of N with refined bias obtained by strong branching. Secondly, we add constraints for each subset S verified for the absence of common perturbation with strong bounding. Then, similar to the current SOTA baseline [Banerjee and Singh, 2024] , we encode the output specification Ψ as a MILP objective, introducing only O(k) integer variables. Finally, we use an off-the-shelf MILP solver [Gurobi Optimization, LLC, 2018] to optimize the MILP. Ψ encoding: First, we show the MILP objective M that encodes Ψ. We introduce binary variables z i ∈ {0, 1} for each individually unverified execution in I where for any perturbation δ δ δ ∈ R n0 and ∥δ δ δ∥ ∞ ≤ ϵ, z i = 1 implies ψ i (N (x i + δ δ δ)) = T rue. Then the finding the worst case UAP accuracy is equivalent to the following M = 1 k × (k -|I|) + min ∥δ∥∞≤ϵ i∈I z i . Constraints encoding: We add constraints from strong bounding, strong branching, and from the linear approximation obtained from the call to RACoon (Algo. 1 line 8). Suppose for any subset S ⊆ I, strong bounding verifies the absence of common perturbation. Then for all δ δ δ ∈ R n0 and ∥δ δ δ∥ ∞ ≤ ϵ at least one of the executions from S will always satisfy the corresponding output specification. Hence, for every such S we add the constraint:i∈S z i ≥ 1. Now, let for any i ∈ I, {(L 1 i , b 1 i ), . . . , (L m i , b m i )} denote set of linear approximation with b m i either coming from RACoon or from strong branching. Then we add the following constraintsz i ≥ z ′ i , z ′ i = (o i ≥ 0), o i ≥ L jT i (x i + δ δ δ) + b j i where j ∈ [m],and o i ∈ R, z ′ i are new real and integer variables respectively. Limitations: Although RABBit outperforms SOTA verifiers in relational verification, like all deterministic verifiers, whether relational or non-relational (including ours), do not scale to deep neural networks (DNNs) trained on very large datasets such as ImageNet. RABBit is sound but incomplete, meaning it may not be able to prove certain relational properties even if they are true. Note that all complete non-relational verifiers are also incomplete for relational properties since they do not track any dependencies between executions. 
experimental evaluation: 
 We evaluate the effectiveness of RABBit on multiple relational properties such UAP accuracy ( Table 1 ) and top-k accuracy (Appendix Table 5 ), DNNs, and datasets. In our evaluation, we compare RABBit against SOTA baselines, including non-relational verifiers CROWN [Zhang et al., 2018] , α-CROWN [Xu et al., 2021] , α, β-CROWN [Wang et al., 2021] , MN-BaB [Ferrari et al., 2022] , GCP-CROWN [Zhang et al., 2022a] , as well as relational verifiers I/O Formulation [Zeng et al., 2023] and RACoon. As previously noted, RaVeN adds linear constraints for each layer, which restricts its scalability as the number of executions k increases. Therefore, we compare RABBit with RaVeN for a smaller execution count of k = 5, as shown in Appendix Table 4 . Additionally, we show that: a) given the same time, RABBit always outperforms the SOTA BaB-based non-relational verifier α, β-CROWN; b) strong bounding computes a tighter bound on t * than α, β-CROWN; and c) we provide an ablation study on ϵ and k used by RABBit.Networks. We use standard convolutional architectures, such as ConvSmall and ConvBig, which are used to evaluate both SOTA relational [Banerjee and Singh, 2024] and non-relational verifiers [Wang et al., 2021] (see Table 1 ). We provide the details of the DNN architectures in the Appendix D.1. We use networks trained using both standard training methods and robust training strategies, such as DiffAI [Mirman et al., 2018] , SABR [Mueller et al., 2023] , and CITRUS [Xu and Singh, 2024] .Our experiments utilize publicly available pre-trained DNNs sourced from the CROWN repository [Zhang et al., 2020] , α, β-CROWN repository [Wang et al., 2021] , and ERAN repository [Singh et al., 2019b] . The clean accuracies of these networks are reported in Appendix D.2.Implementation details and hyperparameters. We implemented our method in Python with Pytorch V1.11 on top of SOTA complete non-relational verifier α, β-CROWN [Wang et al., 2021] . We used Gurobi V11.0 as the off-the-shelf MILP solver. For both strong bounding and strong branching, we use Adam [Kingma and Ba, 2014] for parameter learning and run it for 20 iterations on each subproblem. We set the value of k t = 10 for CIFAR-10 and k t = 24 for MNIST networks respectively. We use a single NVIDIA A100-PCI GPU with 40 GB RAM for bound refinement and an Intel(R) Xeon(R) Silver 4214R CPU @ 2.40GHz with 64 GB RAM for MILP optimization.For any relational property with k executions, we give an overall timeout of k minutes (averaging 1 minute/execution) to RABBit and all baselines. Each MILP instance gets a timeout of 10 minutes. We issue the MILP optimization call on line 25 of Algo. 1 in a separate thread for runtime optimization, ensuring that the MILP optimization process does not unnecessarily block the subsequent iterations of the while loop (line 20 of Algo. 1).Effectiveness of RABBit: Table 1 compares the results of RABBit to all baselines across different datasets (column 1) and DNN architectures (column 2) trained with various methods (column 3), with ϵ values defining the L ∞ bound of δ δ δ in column 4. For each DNN and ϵ, we run RABBit and all the baselines on 10 relational properties each defined with k = 50 randomly selected inputs, and report the worst-case UAP accuracy averaged over the 10 properties. Note that for each DNN, we exclude inputs misclassified by the DNN. We compare the performance of RABBit against SOTA relational and complete non-relational verifiers as well as against strong bounding and strong branching.The results in Table 1 demonstrate that strong bounding, strong branching, and RABBit all outperform the existing SOTA verifiers on all DNNs and ϵ. Notably, RABBit gains up to +4.8% and up to +3.2% improvement in the worst-case UAP accuracy (averaged over 10 runs) for CIFAR10 and MNIST DNNs, respectively. RABBit also efficiently scales to the largest verifiable DNN architectures such as ConvBig, conferring up to +1.6% improvement in worst-case UAP accuracy. In some cases, strong bounding outperforms strong branching, while in others, strong branching outperforms strong bounding, highlighting the importance of both methods. RABBit combines the strengths of both strong branching and strong bounding, producing the best results overall. Time vs UAP Accuracy Analysis: Fig. 1 shows timewise the worst-case UAP accuracy (averaged over 10 runs) for different ConvSmall CIFAR10 networks with k = 50 on ϵ values from Table 1 . Note that RABBit invokes RACoon, which in turn calls α-CROWN and eliminates verified executions (Line 7 in Algorithm 1). Hence, for a fair comparison, we also run α-CROWN first for α, β-CROWN and then run α, β-CROWN only on the unverified indices. For all DNNs, RABBit consistently outperforms the SOTA BaB-based non-relational verifier α, β-CROWN at all timestamps. This confirms that the improved precision shown in Table 1 is not dependent on the specific timeout value. 1 . For each network and ϵ, we select 30 executions at random and compute the percentage improvement in t * with strong bounding over RACoon and α, β-CROWN.We also report the average improvement and 95% confidence intervals for all cases in Table 6 in Appendix G. The results demonstrate that the t * with strong bounding is significantly tighter compared to the bounds from the SOTA verifiers α, β-CROWN and RACoon at all timestamps. Furthermore, strong bounding improves t * on average by up to 108.7% for CIFAR10 networks and 57.7% for MNIST networks. These results highlight the importance of leveraging dependencies across executions during both branching and bounding to improve precision. As presented in Fig. 5 , for all k values, RABBit is more precise than both baselines. Expectedly, the worst-case k-UAP accuracy for relational verifiers is higher with larger k values as it is easier to prove the absence of a common perturbation with larger k.  
conclusion: 
 We present RABBit, a general framework for improving the precision of relational verification of DNNs through BaB methods specifically designed to utilize dependencies across executions.Our experiments, on various DNN architectures, and training methods demonstrate that RABBit significantly outperforms both SOTA relational and non-relational verifiers for relational properties.Although we focus on the worst-case UAP accuracy and top-k accuracy RABBit can be extended to properties involving different DNNs, such as local equivalence of DNN pairs Paulsen et al. [2020] or properties defined over an ensemble of DNNs. Now for every subproblem, replacing the branching constraints by introducing dual variables β β β results in the parametric linear approximations of N specified by(L i (α α α i , β β β i ), b i (α α α i , β β β i )) for each execution i ∈ [n].Then the Lagrangian Dual with the parametric linear approximations{(L 1 (α α α 1 , β β β 1 ), b 1 (α α α 1 , β β β 1 )), . . . , (L n (α α α n , β β β n ), b n (α α α n , β β β n ))} is as follows max 0≤λi min ∥δ δ δ∥∞≤ϵ n i=1 λ i × L i (α α α i , β β β i ) T (x i + δ δ δ) + b i (α α α i , β β β i ) where n i=1 λ i = 1 Theorem 4.1. If min F (S) max α α αi,β β βi,λi -ϵ × ∥ i∈S λ i × L i (α α α i , β β β i )∥ 1 + i∈S λ i × a i (α α α i , β β β i ) ≥ 0 then executions in S do not have a common perturbation δ δ δ ∈ R n0 with ∥δ δ δ∥ ∞ ≤ ϵ.Proof. First, we show that minEQUATIONFor fixed α α α i , β β β i , the optimal solution of the LP in Eq. 7 and subsequently of the Lagrangian gives usEQUATIONFor each subproblem, for all α α α i , β β β i min∥δ δ δ∥∞≤ϵ max 1≤i≤n c i T N (x i + δ δ δ) ≥ min ∥δ δ δ∥∞≤ϵ max 1≤i≤n L i (α α α i , β β β i ) T (x i + δ δ δ) + b i (α α α i , β β β i ) Hence, min ∥δ δ δ∥∞≤ϵ max 1≤i≤n c i T N (x i + δ δ δ) ≥ max α α αi,β β βi min ∥δ δ δ∥∞≤ϵ max 1≤i≤n L i (α α α i , β β β i ) T (x i + δ δ δ) + b i (α α α i , β β β i ) ≥ max α α αi,β β βi max 0≤λi min ∥δ δ δ∥∞≤ϵ n i=1 λ i × L i (α α α i , β β β i ) T (x i + δ δ δ) + b i (α α α i , β β β i ) where n i=1 λ i = 1 from Eq. 9 ≥ max α α αi,β β βi,0≤λi n i=1 λ i × a i (α α α i , β β β i ) -ϵ × ∥ n i=1 λ i × L i (α α α i , β β β i )∥ 1 From Eq. 8 (10) Finally, if min F (S) max α α αi,β β βi,λi -ϵ × ∥ i∈S λ i × L i (α α α i , β β β i )∥ 1 + i∈S λ i × a i (α α α i , β β β i ) ≥ 0 then, min ∥δ δ δ∥∞≤ϵ max 1≤i≤n c i T N (x i + δ δ δ)≥ 0 for all subproblems in F(S) using Eq. 10Since, for all subproblems min ∥δ δ δ∥∞≤ϵ max 1≤i≤n c i T N (x i + δ δ δ) ≥ 0, n i=1 ψ i (N (x i + δ δ δ)) holds for all δ δ δ ∈ R n0 and ∥δ δ δ∥ ∞ ≤ ϵ i.e. there does not exist any common perturbation. 
code of ethics: 
 Question: Does the research conducted in the paper conform, in every respect, with the NeurIPS Code of Ethics https://neurips.cc/public/EthicsGuidelines?Answer: [Yes] Justification: Submission meets all ethical guidelines after authors reviewed the NeurIPS Code of Ethics.Guidelines:• The answer NA means that the authors have not reviewed the NeurIPS Code of Ethics.• If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics. • The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction). 
broader impacts: 
 Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed?Answer: [Yes] Justification: See Section 1 and Section 7 for societal impacts of the work.Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations.• The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology. • If there are negative societal impacts, the authors could also discuss possible mitigation strategies (e.g., gated release of models, providing defenses in addition to attacks, mechanisms for monitoring misuse, mechanisms to monitor how a system learns from feedback over time, improving the efficiency and accessibility of ML). 
safeguards: 
 Question: Does the paper describe safeguards that have been put in place for responsible release of data or models that have a high risk for misuse (e.g., pretrained language models, image generators, or scraped datasets)?Answer: [NA] Justification: No data or models with high risk for misuse were used.Guidelines:• The answer NA means that the paper poses no such risks.• Released models that have a high risk for misuse or dual-use should be released with necessary safeguards to allow for controlled use of the model, for example by requiring that users adhere to usage guidelines or restrictions to access the model or implementing safety filters. • Datasets that have been scraped from the Internet could pose safety risks. The authors should describe how they avoided releasing unsafe images. • We recognize that providing effective safeguards is challenging, and many papers do not require this, but we encourage authors to take this into account and make a best faith effort.12. Licenses for existing assets Question: Are the creators or original owners of assets (e.g., code, data, models), used in the paper, properly credited and are the license and terms of use explicitly mentioned and properly respected?Answer: [Yes] Justification: We have only utilized publically available code, models, and datasets and properly cited all relevant works.Guidelines:• The answer NA means that the paper does not use existing assets.• The authors should cite the original paper that produced the code package or dataset.• The authors should state which version of the asset is used and, if possible, include a URL. • The name of the license (e.g., CC-BY 4.0) should be included for each asset.• For scraped data from a particular source (e.g., website), the copyright and terms of service of that source should be provided. • If assets are released, the license, copyright information, and terms of use in the package should be provided. For popular datasets, paperswithcode.com/datasets has curated licenses for some datasets. Their licensing guide can help determine the license of a dataset. • For existing datasets that are re-packaged, both the original license and the license of the derived asset (if it has changed) should be provided. 
 
 Appendix: Theorem 4.2. For any α α α, β β β , if L(α α α, β β β ) ∈ R n0 and b(α α α, β β β ) ∈ R then min ∥δ δ δ∥∞≤ϵ (L(α α α, β β β ) -L t ) T (x + δ δ δ) + b(α α α, β β β ) = -ϵ × ∥L(α α α, β β β ) -L t ∥ 1 + (L(α α α, β β β ) -L t ) T x + b(α α α, β β β ).Proof. min ∥δ δ δ∥∞≤ϵ (L(α α α, β β β ) -L t ) T (x + δ δ δ) + b(α α α, β β β ) = min ∥δ δ δ∥∞≤ϵ (L(α α α, β β β ) -L t ) T δ δ δ + b(α α α, β β β ) + (L(α α α, β β β ) -L t ) T x = b(α α α, β β β ) + (L(α α α, β β β ) -L t ) T x + min ∥δ δ δ∥∞≤ϵ (L(α α α, β β β ) -L t ) T δ δ δ = b(α α α, β β β ) + (L(α α α, β β β ) -L t ) T x -ϵ × ∥(L(α α α, β β β ) -L t )l α i l α i , u α i u α i u α i ] [l β i l β i l β i , u β i u β i u β i ]respectively. This is similar to the approach used in the SOTA non-relational bound refinement α, β-CROWN Wang et al. [2021] . Since λ i ∈ [0, 1] and k i=1 λ i = 1 we replace λ i = sigmoid(xi) k i=1 sigmoid(xi) where x i ∈ R. For any values of (x 1 , . . . , x k ) ∈ R k the corresponding (λ 1 , . . . , λ k ) satisfy λ i ∈ [0, 1] and k i=1 λ i = 1. We then apply gradient ascent (for maximization problem) on (x 1 , . . . , x k ) without any constraints. Justification: See experimental setup in Section 6.Guidelines:• The answer NA means that the paper does not include experiments.• The paper should indicate the type of compute workers CPU or GPU, internal cluster, or cloud provider, including relevant memory and storage. • The paper should provide the amount of compute required for each of the individual experimental runs as well as estimate the total compute. • The paper should disclose whether the full research project required more compute than the experiments reported in the paper (e.g., preliminary or failed experiments that didn't make it into the paper). 


Decision: The reviewers appreciared the importance of the problem considered, and praised the novelty of the approach and the experimental results.  On the other hand, they struggled with the quality of the writing, and with running the code provided.  A number of issues identified by the reviewers were resolved by the rebuttal and the subsequent discussion with the authors.  On balance, I recommend acceptance, however urge the authors to revise the paper carefully based on all the reviews, and in particular to address apparent plagiarism or self-plagiarism in that a number of paragraphs in the paper are identical or almost the same as paragraphs in Banerjee and Singh, "Relational DNN Verification With Cross Executional Bound Refinement", ICML 2024.

Reviews: review: paper_summary: paper_summary: This paper addresses the problem of verifying certain DNN properties that depend on multiple executions of the DNN, known as “relational verification.” The example used throughout the paper is verifying the k-UAP problem, which aims to confirm the absence of a universal adversarial perturbation for a given DNN. This problem requires relational verification because in order to compare the perturbations across multiple inputs, there must be multiple executions of the DNN considered during the verification process. This introduces additional difficulties compared to traditional single execution branch and bound techniques. The authors tackle this problem by introducing a “product DNN”, which is essentially duplicate DNNs for each of the executions in consideration, and propose stronger branching and bounding algorithms on this DNN instance. The results from the branching and bounding algorithms are then used in an MILP formulation, which they call RABBit. The experimental evaluation across pre-trained DNNs on MNIST and CIFAR-10 demonstrate that RABBit outperforms traditional DNN verifiers as well as the individual branching or bounding algorithms independently, highlighting the importance of combining the strengths of both.
strength_weakness: strength_weakness: The paper suffers from a number of grammatical errors, particularly run-on sentences (e.g., page 4 line 171)  and improper use of commas which makes the paper difficult to read. Additionally, the juxtaposition of the actual contributions of the paper compared to prior work in verification is not always clear.

Another major issue throughout the paper is the presentation of “relational verification” as a concept, while only one example of the use case of relational verification (UAP verification) is presented. For example, on page 1 line 21, “relational properties common in practical situations” is never expanded on—what are the practical situations besides UAP? On page 8 line 356, “10 relational properties” are mentioned but are not defined in the paper. Are there 10 different versions of UAP or are there 10 unique use cases of relational verification in general?

## Minor notes

- Page 2 line 80: “constructing ‘product DNN’” → “constructing a ‘product DNN’”
- Page 3 line 123: “upper bound that contain…” → “upper bounds that contain”
- Page 4 line 184: “Let for all i \in S…” → “For all i \in S, let…”
- Page 4 line 186: “proves absence of common perturbation” → “proves the absence of a common perturbation”
- Page 4 line 192: “Formally, product DNN is a function” → “Formally, a product DNN is a function”
- Page 5 line 216: “do not have common perturbation” → “do not have a common perturbation”
- Page 5 line 217: “The detailed proof in the Appendix B” → “The detailed proof is in Appendix B”
- Page 5 line 224: “m/n subproblem per execution” → “m/n subproblems per execution”
- Page 6 line 270: “Alog. 1” → “Algo. 1”
questions: questions: - In Table 1, how long does it take to run each verification?
- In Table 1, why the non-relational verifier alpha-beta-crown outperformed the STOA relational verifier RACoon? Is it because alpha-beta-crown uses BaB?
- Are there relational properties other than UAP that can be verified and evaluated?
limitations: limitations: Yes, the authors addressed the limitations of their work.
paper_summary: paper_summary: The paper proposes a branch and bound technique for the relational verification of neural networks.
To this end, the authors build upon RACoon (Banerjee and Singh [2024]) and $\alpha,\beta$-CROWN (Wang et al. [2021b]).
The work describes two branching mechanisms (strong bounding and strong branching) that form a symbiosis
in the authors' new algorithmic framework RABBit.

Referenced citations below:
- [R1] Sälzer, Marco, and Martin Lange. "Reachability in Simple Neural Networks." Fundamenta Informaticae 189.3-4 (2022): 241-259.
strength_weakness: strength_weakness: Major Opportunity for Improvement:

(O10) In the introduction of the evaluation the paper states "We evaluate [..] on multiple relational properties, DNNs, and datasets."
      Unfortunately, the paper's evaluation focuses entirely on the k-UAP property. While this is an interesting property worth studying,
      it would be necessary to evaluate the approach on additional relational properties to substantiate the claim that the tool is a generally applicable relational verification tool.
      At least, it would be helpful to discuss necessary modifications to adapt the approach to other relational properties.
      Alternatively, the paper's title and story could be focused on Universal Adversarial Perturbation.

**POST REBUTTAL:**  
The authors provided experiments on a second relational property.
The results seem less impressive to me in this case. Nonetheless, this demonstrates the applicability to other relational properties.
I get the impression the approach is particularly valuable when comparing a large number of executions (as done for k-UAP with k>=20 in the paper).

In my initial comment yesterday I said I would raise my score to Weak Accept if the code submission problems are resolved.
I gave this some more thought:
While the results are less impressive in the new experiments, I do believe the community is better off with a verifier that can solve relational properties for large $k$ than it is without such a verifier. Hence, I have decided to raise my score to **Accept**.

Minor Opportunities for Improvement:

(O1) In Line 223 you mention that simultaneously branching over all executions leads to the processing of only $m^{\frac{1}{n}}$ subproblems.
     It would be helpful if you provide some more intuition to the reader about this. My understanding is that we obtain this number, because
     a split for one execution effectively splits the state space for all executions and thus if we split each execution into l subproblems this
     leads to l^n (for n executions) subproblems that have to be handled. This could be said more explicitly here.

**POST REBUTTAL:**  
The authors proposed sufficient improvements.

(O2) In Line 324 you note that "all complete non-relational verifiers are also incomplete for relational properties since they do not track any dependencies between executions."
     In this generality, this statement seems factually wrong. Obviously, completeness also depends on the checked property, however there is
     a large class of properties which can be encoded as linear constraints over a product network. In this case, I see no reason why the completeness guarantee of a non-relational
     verifier should not equally hold for (linear constraint based) relational properties.
     For example Appendix A.1 describes how k-UAP can be formalized via linear constraints.
     While dependency tracking is very useful for efficient relational NN verification, it does not seem to be strictly necessary.
     Can the heuristics employed by RaBBit and RACoon lead to incompleteness when it comes to providing exact UAP bounds?

**POST REBUTTAL:**  
I am not convinced of the authors' answer in this respect.
In Appendix A.1 the authors describe how the k-UAP property can be encoded with linear constraints. Maybe I am missing something here, but even with the authors' clarification, it is not clear to me why verifying this specification on a product NN would not yield a complete verifier for k-UAP. Again, I wholeheartedly agree that tracking relational dependencies is *useful*, but I still do not see why it is *necessary*. As stated in the authors' response (Q3), completeness for UAP is then "just" a matter of checking all possible subsets (which is again an issue independent of dependency tracking).

**POST COMMENTS:**  
In the comments the authors have sufficiently resolved this issue: Indeed, the constraints outlined in A.1 already are cross-executional constraints.

Minor notes:
- Line 52/53: "with *a* cross-executional bound method"
- Line 104: DNN verification is not only NP-hard, but actually (exactly) NP-complete [R1]
- Line 157: "...it is possible to *statistically* estimate..."
- Line 336: You mixed up the citations for relational / non-relational verifiers here
questions: questions: (Q1) 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?

**POST REBUTTAL:**  
The authors clarified this.

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

**POST REBUTTAL:**  
See (O10)
limitations: limitations: Concerning limitations, my main critique is the focus on Universal Adversarial Perturbations in the experimental section (see (O10)).

**POST REBUTTAL:**  
Due to a lack of access to NVIDIA GPUs, I was not able to evaluate the code submission.
However, aDbJ has confirmed that the (updated) code submission allows execution of the code.
paper_summary: paper_summary: The paper presents RABBIt, a general framework for improving the precision of relational verification of DNNs through BaB methods and cross-execution dependencies. RABBIt uses strong bounding and strong branching methods, outperforming BaB methods like $\alpha$-$\beta$-CROWN and RACoon, which only leverages cross-execution dependencies. Experiments show that RABBIt significantly outperforms SOTA verifiers for relational properties on various architectures trained by different training methods.
strength_weakness: strength_weakness: 1. The paper claims that 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.
2. Another concern is the poor presentation of this paper.
   * In Lines 49-50, the bullet points a), b), and c) do not correspond to the order of challenges introduced earlier in the paragraph. c) should come first, then b), and finally, a).
   * In Line 179, the MILP instance appears abruptly. It is confusing because the reader might think of it as the MILP problem introduced in Line 36. The purpose of the MILP instance only becomes clearer after introducing the k-UAP accuracy problem. 
   * However, the k-UAP accuracy is not adequately introduced and abruptly appears in Line 227. 
   * In lines 221-224, I cannot follow how to derive $m^{1/n}$ and $m/n$. Please give me an example.
   * In Section 4.2, $N(x_i+\delta)$ is a vector but $L_j^T(x_i+\delta)$ is a scalar. Does the paper want to express $c_i^T N(x_i+\delta)$?
   * 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?
   * The presentation in Section 4.2 could be better. For example, the paper should relentlessly remind readers that the goal of Lines 243-267 is to compute the lower bound $b_j^*$.
   * In Line 319, the index $j$ is not quantified. 
   * In Line 336, Wang et al. should be non-relational, and Banerjee and Singh should be relational.
questions: questions: 1. In lines 221-224, I cannot follow how to derive $m^{1/n}$ and $m/n$. Please give me an example.
2. In the MILP encoding of RABBIt, What are the new terms/constraints compared to RACoon? 
3. Is the strong branching method only to guarantee that RABBIt's bound is tighter than $\alpha$-$\beta$-CROWN bound?

Comments:
1. Missing related work, [1] provides verification for counterfactual explanation robustness, which is also a relational property of neural networks. 

[1] Verified Training for Counterfactual Explanation Robustness under Data Shift. Anna P. Meyer, Yuhao Zhang, Aws Albarghouthi, Loris D'Antoni
limitations: limitations: The paper discusses its limitations.
paper_summary: paper_summary: The paper proposes bound-tightening techniques for verifying the absence of universal adversarial perturbations for a neural network. The tightened bounds are leveraged in a MILP encoding to perform verification.
strength_weakness: strength_weakness: ### Baselines
The non-relational verifier baselines CROWN [Zhang et al. 2018], $\alpha$-CROWN [Xu et al., 2021], $\alpha,\beta$-CROWN verifier [Wang et al., 2021b] are no longer state of the art. These baselines were outperformed by GCP-CROWN [Zhang et al., 2022] and MN-BaB [Ferrari et al., 2022]. To justify the claims on outperforming the non-relational SOTA, the paper should compare against GCP-CROWN and/or MN-BaB. 

### Sensitivity of Results
For the "Effectiveness of RABBit" and the "Time vs UAP Accuracy Analysis" experiments, the authors use ten randomly sampled problem instances but only report the average results. It remains unclear how sensitive the results are to the sampling. 

### Presentation
- The paper is not sufficiently self-contained. In particular, it does not provide sufficient details on RACoon which it builds upon. 
- 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.
- Important mathematical details are spread throughout the paper. For example, the maximisation in Theorem 4.1 has additional constraints on $\lambda_i$ that are mentioned in lines 206-207 and also constraints on $\boldsymbol{\alpha}$ and $\boldsymbol{\beta}$ that are only mentioned in lines 128 and 135. 

### Code
The code included in the supplementary material is insufficiently documented (what do I have to do to reproduce the experiments? What is "raven"?) and buggy:
- The requirements can not be installed as specified in the README (autoLiRPA 0.4 is not available on PyPI at the time of writing; Can not install the specified PyTorch versions without an `--extra-index-url`).
- The test command that is described in the README fails due to a syntax error in file "raven/src/util.py" at line 247 `(root'', train=train, download=True, transform=transform_test)`.
- The supplementary material does not include the models used in the experiments, describe how to obtain them, or indicate where to place them. 


[Brix et al., 2023]: Christopher Brix, Stanley Bak, Changliu Liu, Taylor T. Johnson: The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results. CoRR abs/2312.16760 (2023)
[Zhang et al., 2022]: Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, J. Zico Kolter: General Cutting Planes for Bound-Propagation-Based Neural Network Verification. NeurIPS 2022.
questions: questions: ### Questions
1. I am confused by the statement "Each MILP instance gets a timeout of 5 minutes" (line 351). With $k=50$ and $k_t=20$ for MNIST, 5 minutes per MILP already add up to 100 minutes (2x the timeout) at the end of the first for loop (line 19), before Algorithm 1 considers the timeout in line 20. What are the actual runtimes of RABBit?
2. Table 1: How were the perturbation radii chosen? 
3. The worst-case UAP certified by RABBit in Table 1 is higher than the standard accuracy (Table 3) for several networks (CIFAR10: ConvSmall+DiffAI, ConvSmall+SABR, ConvSmall+CITRUS, ConvBig+DiffAI, MNIST: all networks). In my understanding, UAP should always be lower than standard accuracy (UAP = "the rate at which N misclassifies when the same adversarial perturbation is applied to all inputs from the distribution", Lines 153-154). What do the reported UAPs actually indicate?
4. Besides the average UAPs "Effectiveness of RABBit" and the "Time vs UAP Accuracy Analysis" experiments, what are the standard deviations, minima, maxima, and 25%, 50%, and 75% quartiles?

### Suggestions and Typos
- The abbreviation SOTA is relatively well known, but I would still suggest introducing it. 
- Line 14: space between "diagnosis" and Amato et al. 
- Line 14 and throughout: Use citep instead of citet. 
- Line 15: What does it mean to "understand [...] their reliability"?
- Line 17: The references Potdevin et al. [2019] and Wu et al. [2023b] seem out of place here since they do not introduce adversarial attacks.
- Line 18: Sotoudeh and Thakur [2020] do not study adversarial attacks.
- Lines 23-26: The discussion in these lines is paraphrasing the discussion in the introduction of Banerjee and Singh [2024]. You should add a citation for this, for example: "As discussed by Banerjee and Singh [2024], recent studies [Li et al, 2019a] emphasize ..."
- Line 52: with *a* cross-executional bound method
- Related Work: I suggest adding a discussion of certified adversarial training approaches, such as [Balauca et al., 2024; De Palma, 2024] since this field is closely related.
- Line 68: prove *a* property 
- Line 104: add a justification or reference for the NP-hardness of NN verification. 
- Lines 127-128: add a citation for parametric linear relaxations
- Line 132: $\alpha,\!\beta$-CROWN *converts*
- Line 136: and *refines* the parameters
- Line 136: last $\alpha,\!\beta$ also bold?
- Line 168: for *a* $k$-UAP problem
- Lines 169-170: bold $\boldsymbol{\delta}$ as in the Preliminaries Section?
- Line 172: highlight*ing*
- Line 185: Then *if* the optimal value $t^\ast \geq 0$ this proves the absence ...
- Lines 185-187: It does not become very clear here that $||\delta||_\infty \leq \epsilon$ and the following equations are constraints to the maximum in line 185. I strongly suggest putting both the max and the constraints in an equation environment. The same also holds for other maximisations and minimisations. 
- Line 191: In the remainder of the paper, the number of executions is $k$, not $n$. 
- Line 192: *the* product DNN 
- Line 195: adapt or adopt?
- Line 197: add a description of what the BaBSR score estimates.
- Line 216: have *a* common perturbation. 
- Line 224: *exploring* $\frac{m}{n}$ subproblem*s*.
- Line 225: absence of *a* common perturbation.
- Line 236: compute *a* valid lower bound.
- Line 270: *Algo*.
- Line 310: Then finding (no *the*)
- Line 311: $min_{||\delta||_\infty \leq \epsilon}$?
- Line 317: denote *the* set
- Figure 2: the title and axis descriptions are barely legible. 
- Line 413: invalid DOI
- Line 416: Where published?
- Line 422: "jan", the other references don't have a month
- Line 448: there is a published version at ICLR 2015 for this article
- Line 495: Conference missing. 
- Lines 510-517: Duplicate entry
- Line 529: Where published?
- Bibliography: incoherent links/no links, sometimes DOI and URL. 
- Line 602: Projected gradient *ascent*
- Table 2: What are the full architectures or where can I find them?

[Balauca et al., 2024]: Stefan Balauca, Mark Niklas Müller, Yuhao Mao, Maximilian Baader, Marc Fischer, Martin T. Vechev:
Overcoming the Paradox of Certified Training with Gaussian Smoothing. CoRR abs/2403.07095 (2024)
[De Palma et al., 2024]: Alessandro De Palma, Rudy R Bunel, Krishnamurthy Dj Dvijotham, M. Pawan Kumar, Robert Stanforth, Alessio Lomuscio: Expressive Losses for Verified Robustness via Convex Combinations. ICRL 2024. https://openreview.net/forum?id=mzyZ4wzKlM
limitations: limitations: The authors adequately discuss limitations and social impact.

Comments: title: Final Review Rating
Questions mostly addressed -- Code problem needs to be addressed
Code Still Buggy
anonymized link to the code
comment: Thank you for your feedback and for raising your score. We will incorporate your suggestions in the revised version of the paper.
Thank you for your feedback and for raising your score. We will incorporate your suggestions in the revised version of the paper.
Thanks for your feedback. We will add your suggestions to strengthen the paper in the revised version.
**Q3: As was discussed, Algorithm 1 does not properly reflect the actual implementation of RABBit. This leads to inconsistencies, for example, with regard to the presented timeout mechanism and the actually deployed timeout mechanism.**

**R3:** As detailed in the paper, the timeout for RABBit and all baselines is set to $k$ minutes, consistent with Algorithm 1. We have already provided the GPU specifications used for BaB and the CPU specifications used for MILP in the paper. Running each CPU-bound MILP optimization in a separate thread allows us to avoid unnecessarily blocking the GPU-bound BaB computation, while still utilizing the same CPU resources available to all baselines. Additionally, as discussed above, all these intermediate MILPs can be replaced with a single MILP that incorporates all available constraints before $(T_{total} - T_{MILP})$. This alternative approach, as demonstrated in Table 9 of the rebuttal, yields results comparable to those in Table 1 of the paper. We will clarify these details in the next revision.




**Q4: Reproducibility of the code .**


**R4:** In the README of the code, we provide detailed instructions on how to install dependencies, all the pre-trained models used for experiments, detailed descriptions of the different hyperparameters used by RABBit and the baselines, various test cases to reproduce the main results and ablations, and instructions on how to run new experiments.

For instance, the following two commands will reproduce the results for the CIFAR10 ConvSmall DiffAI network from Table 1. 

1. `python -m unittest -v tests.test_rabbit.TestUAP.test_cifar_uap_diffai`

2. `python -m unittest -v tests.test_results.TestResults.test_analyze_main_results_cifar_diffai`


These two commands needed to run the experiment and analyze the result are already described in the README of the provided code.
Dear reviewer aDbJ,

Thank you for engaging in this discussion. We are also adding a comparison with GCP-CROWN [2]. We believe that the other concerns raised in the final comment have already been addressed in our previous responses. However, we would like to provide a summary of those responses once more.

**Q1: Non-relational baselines.**

**R1:** As instructed, we have already provided a comparison with MNBaB [1], demonstrating that our proposed method, RABBit, significantly outperforms it. We are also adding a comparison with GCP-CROWN [2]. We compared the performance of RABBit with GCP-CROWN 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 GCP-CROWN outperforms $\alpha,\beta$-CROWN on all networks, it remains significantly less precise than RABBit, as shown in Table 10. 

Table 10 UAP accuracy of RABBit vs baselines including MNBaB and **GCP-CROWN**
| Training         |   $\epsilon$ | $\alpha$-CROWN| RACoon |   $\alpha,\beta$-CROWN |   MNBaB |GCP-CROWN |  RABBit | 
|:-----------------|-------:|:-------------|------:|------:|------:|---------:|---------:|
| DiffAI         |  5/255  | 49.6%|  51.6%|  53.6%|  55.0% |53.8%  | **59.8%**   |
| SABR   | 2/255   | 75.8% | 78.2% | 78.4% | 80.0% | 80.0% |  **84.0%**  |
| CITRUS | 2/255   | 76.0%| 78.8% | 79.0%  | 79.6% | 79.6%  |  **83.6%**  |
| Standard      | 1/255    | 45.4% | 45.4%  | 59.8%  | 55.0%  |61.8% | **62.4%**  |




**Theoretical limitation of non-relational verifiers:** 
Beyond experimental comparisons, any non-relational verifier, including GCP-CROWN [2], developed for verifying input-specific attacks, is limited in verifying relational properties because it ignores cross-executional input dependencies (see lines 168–174 in the paper). 

**Q2: Sensitivity of the results**

**R2:** It is expected that the verified worst-case UAP accuracy for different sets of images of size $k=50$ can be different. However, as shown in Tables 6 and 7 of the rebuttal, for ConvSmall CITRUS [3] for CIFAR10 and MNIST respectively, RABBit significantly outperforms the baselines across all quantiles. Additionally, we compute the difference between RABBit's and $\alpha,\beta$-CROWN's UAP accuracy for ConvSmall CITRUS [3] for both CIFAR10 and MNIST and report the mean, 95% confidence interval, and median in Table 11. The 95% confidence interval substantiates RABBit obtains **statistically significant** improvement over the baseline.

Table 11: Difference (%) between RABBit and $\alpha,\beta$-CROWN's UAP accuracy for ConvSmall CITRUS[3]

| Dataset         |   $\epsilon$ |  Mean |   95% CI |   Median |
|:-----------------|-------:|:-------------|------:|------:|
|CIFAR10| 2.0| 4.6| [1.8, 7.4] | 5.0|
|MNIST| 0.15| 2.2| [0.9, 3.5] | 2.0|

In our evaluation, we run RABBit and baselines on 10 UAP properties each with k = 50 inputs, totaling **500 inputs**. Many DNN verifier papers, such as Refinezono [4], deepG [5], RACoon [6],  and GCP-CROWN [2], **only use 100 inputs** for evaluation. Moreover, the SOTA relational DNN verifier RACoon [6] **also considers 10 UAP properties** in the evaluation section of its paper. 

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

[2] "General Cutting Planes for Bound-Propagation-Based
Neural Network Verification", Zhang, et. al., NeurIPS, 2022.

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

[4] "Boosting Robustness Certification of Neural Networks", Singh, et. al., ICLR, 2019.

[5] "Certifying Geometric Robustness of Neural Networks", Balunovic, et. al., NeurIPS, 2019.

[6] "Relational DNN Verification With Cross Executional Bound Refinement", Banejee, et. al., ICML, 2024.
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
Thank you for the response that clarified my concerns.
I thank the authors for the additional experimental details. The rebuttal addressed many weaknesses of the paper, particularly regarding runtimes, and the authors eventually provided executable code. My main concerns were the baselines, the sensitivity of the results, the presentation, and the code. 

- For the baselines, the authors provided a comparison with MN-BaB, which is a large step towards substantiating their claim of outperforming non-relational SOTA neural network verifiers. However, GPC-CROWN [Zhang et al., 2022] is unarguably *the* state-of-the-art verifier [Brix et al., 2023; Müller et al., 2022], which mandates that the authors compare against it to substantiate their claim of outperforming SOTA in the paper.

- Regarding the sensitivity of the results, the authors have reported detailed summary statistics in the rebuttal. This is great. However, the numbers show that their results are quite sensitive to the sampled properties. This means that a faithful evaluation requires more than the ten properties used by the authors and a careful sensitivity analysis. 

- For the presentation, the authors have acknowledged the issues and plan to correct them. However, in my opinion, the paper requires a major revision, which then has to go through another reviewing process. This particularly concerns the self-containedness of the paper. Additionally, the discussion with the authors has brought up more issues with the presentation: As was discussed, Algorithm 1 does not properly reflect the actual implementation of RABBit. This leads to inconsistencies, for example, with regard to the presented timeout mechanism and the actually deployed timeout mechanism. 

- Finally, the authors now provided executable code, which is a large improvement. However, the code is still insufficiently documented and, therefore, does not allow for adequate reproducibility. 

Overall, the authors have made large strides towards improving the paper. However, I still think that the paper is not yet ready for publication and the major revisions required mandate another reviewing process. Therefore, I maintain my rating (3, Reject). 


[Brix et al., 2023]: Christopher Brix, Stanley Bak, Changliu Liu, Taylor T. Johnson: The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results. CoRR abs/2312.16760 (2023) 

[Müller et al., 2022] Mark Niklas Müller, Christopher Brix, Stanley Bak, Changliu Liu, Taylor T. Johnson: The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results. CoRR abs/2212.10376 (2022)

[Zhang et al., 2022]: Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, J. Zico Kolter: General Cutting Planes for Bound-Propagation-Based Neural Network Verification. NeurIPS 2022.
Dear reviewer aDbJ,

Thanks for your response. We are happy that our response has resolved some of your concerns.

**Q1: Does RABBit use multiple threads that run on a single CPU core or does it leverage multiple CPU cores?**

**R1:** RABBit and all the baselines use Gurobi V11.0 for MILP optimization (as mentioned in line 345 of the paper). By default, Gurobi utilizes multiple cores depending on their availability [1]. We applied the default Gurobi settings for RABBit and all the baselines. 
RABBit, similar to all the baselines, uses a single GPU for BaB-based methods and utilizes the CPU for all MILP tasks. The hardware details can be found in lines 348-349 of the paper. RABBit initiates MILP optimization in a new thread to avoid blocking the GPU-based BaB methods while using the same CPU resources available to the other baselines. The CPU utilization is determined by Gurobi's default settings, which are consistent across all baselines.

Moreover, currently in RABBit, we issue a new MILP everytime a new constraints is added (line 16 and line 25 of Algo. 1). All these intermediate calls can be replaced with a single MILP with all avaialble constraints placed before $(T_{total} - T_{MILP})$. This eliminates the need to invoke the MILP solver in a new thread and reduces the number of MILP calls in RABBit to just one. The final results using this method are comparable to those presented in Table 1 of the paper. 

Table 9 UAP accuracy of RABBit with only 1 MILP call
| Training         |   $\epsilon$ | $\alpha$-CROWN| RACoon |   $\alpha,\beta$-CROWN |   MNBaB |  RABBit | 
|:-----------------|-------:|:-------------|------:|------:|------:|---------:|
| Standard         | 1/255    | 45.4% | 45.4%  | 59.8%  | 55.0%  | **62.4%**  |
| DiffAI         |  5/255  | 49.6%|  51.6%|  53.6%|  55.0% |**59.8%**   |
| SABR   | 2/255   | 75.8% | 78.2% | 78.4% | 80.0% | **84.0%**  |
| CITRUS | 2/255   | 76.0%| 78.8% | 79.0%  | 79.6% | **83.6%**  |

[1] https://support.gurobi.com/hc/en-us/community/posts/4408537958289-CPU-utilization
Thank you for your answer, which addresses some of my concerns. I have a followup question:

> R3: 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.

As far as I can see, this wasn't discussed in the paper. Does RABBit use multiple threads that run on a single CPU core or does it leverage multiple CPU cores?
Dear reviewer uEoH, 

Thanks for your response. We have added clarifications to your questions and will be happy to help if you face any issues with the code.

**Q1: The proposed approach has higher gains when comparing a large number of executions .**

**R1:** We evaluate the performance of RABBit with different values of $k$ in Figure 4 and Figure 7 of the paper. RABBit's performance improvement grows with higher $k$ values, which is anticipated. At a high level, as the size of the set of executions increases, it becomes more challenging to find common adversarial perturbations. This helps RABBit which exploits cross-executional dependencies. 

**Q2: Even with your clarification it is not clear to me why verifying this specification on a product NN would not yield a complete verifier for k-UAP ?**

**R2:** We believe there is a misunderstanding regarding what we meant by tracking dependencies between perturbed inputs. The input specification $\Phi = \bigwedge_{i=1}^{k} \phi_{in}^{i} \bigwedge \Phi^{\delta}$ (line 563 of the paper) for the $k$-UAP property includes the cross-executional input constraint $\Phi^{\delta}$, which defines the relationship between perturbed inputs from different executions. A verifier that ignores the cross-executional input constraints $\Phi^{\delta}$ would still be sound for $k$-UAP by verifying against the weakened input specification $\Phi' = \bigwedge_{i=1}^{k} \phi_{in}^{i}$. However, such verifiers would not be complete. In contrast, as correctly pointed out, verifiers that utilize the full input specification $\Phi$ (as opposed to $\Phi'$) on a product NN and use the constraint $\Phi^{\delta}$ can achieve completeness for $k$-UAP (as illustrated in our response to Q3). We will clarify this in detail in the revised version of the paper.

**Q3: Link the code and networks used for experiments.**

**R3:** We apologize for the missing networks and the faulty link. We have updated the link to our code in the previous thread and are also providing the link here. The networks used for the experiments can be found in the `RABBit/RABBit-main/nets` folder. We have added instructions for reproducing the experiments in the README file. If you encounter any issues while reproducing the code, we will be happy to assist you.

anonymized link to the code: https://figshare.com/s/9dfe74654ea6f5a5ee24
I confirm that the new environment definition allows for executing the code.
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.
Dear authors,

thank you for adressing my questions.

### Concerning (O10)/(Q1):
I appreciate the additional experiments on a second relational property.
While the improvements over the SoTA look less impressive to me in this case, it is nice to see the approach is applicable to other properties.
I get the impression the approach is particularly valuable when comparing a large number of executions (as done for k-UAP with k>=20 in the paper).

### Concerning (O2)/(Q2):
In Appendix A.1 you describe how the k-UAP property can be encoded with linear constraints.
Maybe I am missing something here,
but even with your clarification it is not clear to me why verifying this specification on a product NN would not yield a complete verifier for k-UAP.
Again, I wholehearthedly agree that tracking relational dependencies is *useful*, but I still do not see why it is *necessary*.
As stated in your response (Q3) completeness for UAP is then "just" a matter of checking all possible subsets (which is again an issue independent of dependency tracking).

### Concerning (O1)/(Q5):
Thanks for the clarification which addresses my concern.

### Code
I promised to raise my score if (O10)/(Q1) is addressed and I am still willing to do increase to Weak Accept.
However, I am now somewhat worried about the state of the code submission given the remarks by aDbJ.
Following up on aDbJ's review, I have also tried to execute the original code submission:
While I was able to fix the mentioned issues, the test can indeed not be performed without the NNs available.
To make matters worse (and I do not consider this a fault of the authors), it seems that Google Drive has removed the updated code submission.
Maybe, an anonymous figshare could help here. I sincerely hope this problem can be solved.


### Minor notes:
line 157: "...it is possible to *statistically* estimate..."
Thank you for the response. It addresses all my concerns.
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 AC,

As requested by reviewer aDbJ, we are submitting the following anonymized link to the code for reproducing our experiments:

Anonymized link: https://drive.google.com/file/d/1jIO2b76f9VDkCeZxaAJvnZxobXgGRE18/view?usp=sharing
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
| Dataset | Model      | Train    | Accuracy (%) |
|---------|------------|----------|--------------|
|   CIFAR10      | ConvSmall  | Standard | 62.9         |
| CIFAR10 | ConvSmall  | DiffAI   | 45.9         |
| CIFAR10 | ConvSmall  | SABR     | 63.3         |
|   CIFAR10      | ConvSmall  | CITRUS   | 63.9         |
|   CIFAR10      | ConvBig    | DiffAI   | 53.8         |
|    CIFAR10     | ResNet-2B  | Standard | 67.5         |
|     MNIST    | ConvSmall  | Standard | 97.7         |
|     MNIST    | ConvSmall  | DiffAI   | 96.8         |
| MNIST   | ConvSmall  | SABR     | 97.9         |
|    MNIST     | ConvSmall  | CITRUS   | 98.5         |
|      MNIST   | ConvBig    | DiffAI   | 91.8         |

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.