Interpreting Robustness Proofs of Deep Neural Networks

Q1. how can we deal with the nonlinear properties?

R1: Existing works [1, 2] that handle non-linear properties typically compute a linear approximation of these properties and utilize existing DNN verifiers designed for linear specifications. For instance, in [1], when verifying robustness against geometric perturbations like rotation, an overapproximated convex input region is computed, specified by a set of linear inequalities encompassing all rotated images. Subsequently, existing DNN verifiers are applied. A similar approach is employed in [2] for non-linear output specifications. Both these cases with linear approximations of non-linear input and output specification can be handled with ProFIt. In general, for DNN verification, nonlinear specifications are rare, and most of the common norm-based local robustness properties can be specified as a conjunction of linear inequalities, and the corresponding proofs can be analyzed with ProFIt.

[1] "Certifying Geometric Robustness of Neural Networks", M. Balunovic, NeurIPS, 2019.
[2] "Verification of Non-Linear Specifications for Neural Networks", C. Qin, ICLR, 2019.

Q2. Different properties lead to different sufficient proof features. So, the features selected by one property may only reflect one perspective of the neural network.

R2: ProFIt analyzes and generates a human-understandable explanation of the proof of a specific property. Different properties capture different behaviors of the DNN and therefore, the proof and subsequently human-understandable explanation generated by ProFIt will reflect these differences. To elaborate, for robustness we want the DNN output to remain correct when input changes. In contrast, for monotonicity we want the output of DNN to change in a certain manner with respect to the change in input. So, it is natural that the proof of different properties on the same DNN will rely on different proof features. In this paper, we focus on proof dissection of the common local robustness properties and leave the dissection of proofs of other properties such as monotonicity to future work.

Q3. Can sufficient proof features provide intuitions on how to design a training method to train a model with such a property?

R3: Please refer to the response to Q2 in the common response.

Q1. how is the original feature count in Table 1 computed? Why the size of the penultimate is different for MNIST and CIFAR10 PGD-trained networks?

R1: As pointed out, the original feature count is the same as the size of the penultimate layer. In Table 1, we opted for publicly available state-of-the-art pre-trained networks from official repositories [1, 2, 3] to prevent training networks ourselves and introducing unintended bias in the process. Therefore, the networks in Table 1 do not always share the same architecture and may have different sizes at the penultimate layer. The experiments on networks with the same architecture are in Appendix C.9.
[1] ERAN - https://github.com/eth-sri/eran
[2] CROWN-IBP - https://github.com/huanzhang12/CROWN-IBP
[3] COLT - https://github.com/eth-sri/colt \

Q2. Scalability analysis of ProFIt

R2: Please refer to the response to Q1 in common response.

Q3. The computational complexity of ProFIt

R2: Please refer to the response to Q1 in common response.

Q4. Can the method also be applied to probabilistic certification methods such as randomised smoothing?

R4: ProFIt is designed for deterministic DNN verifiers and currently cannot handle probabilistic verifiers like randomized smoothing. To extend ProFIt to accommodate probabilistic verifiers, we would first need to define the priority ordering of the proof features w.r.t the proof generated by probabilistic verifiers. Additionally, determining how to generate visualizations of the proof features poses a challenge since, unlike common incomplete verifiers, the computation of randomized smoothing cannot be represented as differentiable programs. Both of these aspects require further investigation, and we leave them as subjects for future work. We will update Section 4.5 of the paper to include this limitation.

Q1. It is not immediately clear to me how the proposed algorithm reduces the overall computational complexity, and some additional explanation would be preferred.

R1: First, let us clarify the statement: "Investigating the entire set $\mathcal{F}$ is always a valid but expensive option, considering the size of $\mathcal{F}$." For DNNs, the proof feature set $\mathcal{F}$ may comprise thousands of proof features, making it impractical to manually investigate each one (e.g., by examining the gradient maps) individually. For this reason, one of our objectives is to automatically extract a proof feature set that is small (the first of three expectations outlined in Section 4.1) and, consequently, easy to manually investigate. In Table 1 of the paper, we demonstrate that ProFIt successfully extracts a small yet sufficient and important proof feature set, containing fewer than 10 proof features. This significantly reduces the effort required for the manual investigation of all constituent proof features. We will provide further clarification in the revised version of the paper.

Q2. Can ProFIt be used for ConvNets and vision transformers?

R2: All the networks used in the experiments in Table 1 of the paper, are convolutional. We have provided detailed information about the architecture of the DNNs, handled by ProFIt, in the response to Q1 in the common response. For even larger networks like vision transformers, the state-of-the-art deterministic DNN verifiers do not scale. As the scalability of ProFIt is ultimately constrained by the limitations of existing DNN verifiers, it currently does not scale to vision transformers. However, it's crucial to note that ProFIt is a general tool compatible with any deterministic DNN verification algorithm. Therefore, ProFIt will benefit from any future advances to enable the deterministic DNN verifiers to scale to vision transformers. We have discussed this limitation in Section 4.5 of the paper.

Q3. Is the certificate issued by ProFIt related to the robust accuracy in any way?

R3: ProFIt analyzes the proof only if the underlying verifier $\mathcal{V}$ can prove the property. So, the percentage of cases ProFIt generates proof dissection is the same as the robust accuracy of the DNN with verifier $\mathcal{V}$.

Q4. Is the proposed algorithm also compatible with GPU acceleration?

R4: Yes, ProFIt is compatible with GPU acceleration. We provide the runtime analysis of ProFIt with GPUs in the response to Q1 in the common response. We will add these runtimes in the revised version of the paper.

Q5. Typographical errors in page 5 and page 8.

R5: Thanks for pointing out we will fix this in the revised version of the paper.

Thank you for the response, which clarified most of my questions. Overall, I think this paper presents a coherent story but the motivation is less clear and prominent. Therefore, I stand on the fence about this manuscript and keep my rating of 6.

Q1. Since the DNN verifier is supposed to provide a mathematically sound robustness certificate, explain the motivation for dissecting DNN proofs.

R1: The primary objective of ProFIt is to explain why the verifier successfully proves a property on the given DNN. This motivation aligns with traditional DNN interpretation techniques, where, given a DNN correctly computes the output, the goal is to comprehend the decision-making process of the DNN. In contrast to existing DNN verifiers that often act as black boxes, traditional program verifiers do offer insights into why certain properties are proven for the given program. For instance, in programs featuring loops, loop invariants characterize the expected behavior of the program after each iteration, making the proof human understandable (discussed in Section 1 of the paper). We want to check whether the proofs generated by DNN verifiers provide similar insights or not. As shown in Section 5.3, even if a DNN is robust for some $L_{\infty}$ region, the input features, the proof relies on can be different. Moreover, dissection results obtained by ProFIt can serve as a qualitative metric to compare different DNNs achieving similar levels of robustness. For example, proofs generated on standard DNNs highlight spurious input features that are part of the background rather than those associated with the actual object. In contrast, the proof generated on COLT networks relies on input pixels that are part of the actual object. These applications emphasize the importance of delving into proof dissection techniques.

Q2. What is the computational complexity of the proposed ProFit algorithm and the reliance on the dependent factors?

R2: Please refer to response to Q1 in the common response.

Q3. What do you mean by "spurious" and "meaningful" features in the context of gradient maps? Does the provably robust training method CROWN-IBP have a much lower standard accuracy because it overly filters the meaningful features?

R3: As defined in Section 5.3 in the paper, for gradient maps generated on MNIST and CIFAR10 images, spurious input features are the pixels coming from the image background, whereas meaningful input features are the pixels that are a part of the actual object being identified by the DNN. Robustly trained networks generally report lower standard accuracy than commonly trained networks [1]. Additionally, certifiably robust DNNs (CROWN-IBP) generally report smaller standard accuracy when compared to empirically robust DNNs (PGD-trained) [2]. It appears that the loss in standard accuracy is due to the fact that the certifiably robust networks overly filters the meaningful input features.

[1] "Robustness May Be at Odds with Accuracy", D. Tsipras. ICLR, 2019.

[2] "Certified Training: Small Boxes are All You Need ", M. Mueller, ICLR, 2023.

Q4 How can the extracted top proof features benefit the development of better DNN verifiers or robust training methods?

R4: Please refer to the response to Q2 in the common response.

Experimental evaluation of ProFIt runtime:

• Experiment setup: We run ProFIt on multiple networks including those mentioned in the paper on both CPUs and GPUs. For CPU-related experiments, we use the same setup as mentioned in Section 5.1 in the paper. In GPU-related experiments, we utilize a single NVIDIA A100-PCI GPU with 40 GB RAM. We use the state-of-the-art incomplete verifier $\alpha$-CROWN from auto_LiRPA [6] toolbox and show results for 100 local $L_{\infty}$ robustness properties. As done in the paper, for MNIST and CIFAR10 networks, we use $\epsilon = 0.02$ and $\epsilon =0.2/255$ respectively to define $L_{\infty}$ input regions.

• Size and architecture of the Networks: We present the runtime analysis of ProFIt on the DNNs used in the paper and also showcase results on some of the largest verifiable network architectures, namely ConvBig and ConvSuper. These architectures are de facto benchmarks employed for testing the scalability of state-of-the-art verifiers [1, 2, 3] and are featured in the International Verification of Neural Networks Competition [4]. All the networks used in this experiment are selected from the ERAN [8], and CROWN-IBP [11] repositories and belong to the category of convolutional neural networks (CNNs).

• Compatibility with GPU acceleration: ProFIt is not restricted to CPUs and works with DNN verifiers whose computation can benefit from GPU acceleration. For example, ProFIt can be run with GPU implementation of auto_LiRPA [6]. We show the runtime improvement of ProFIt with GPUs below. Runtimes on GPUs are up to 20x shorter than those on CPUs.

• Experimental Results: We present results for MNIST networks in Table 1 and results for CIFAR networks in Table 2. Column 1 displays the network name, column 2 outlines the training method, and columns 3 and 4 describe the network's structure. Column 5 indicates the worst-case bound on the number of incremental verifier calls, as described in Theorem 1, while column 6 displays the average number of incremental verifier calls per property. Columns 7 and 8 present the average runtime in seconds for ProFIt on CPU and GPU, respectively. Notably, on GPUs, the average runtime for ProFIt is less than 1 second for all the networks. Note that, for ConvBig architectures, the timeout used in the International Verification of Neural Networks Competition [4] is in minutes. In comparison, ProFIt with $\alpha$-CROWN is significantly faster.

Table 1 on MNIST Networks

Table 2 on CIFAR10 Networks

[1] “PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations”, M. Muller, POPL, 2022.

[2] “Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification”, C. Ferrari, NeurIPS 2021.

[3] "Multi-neuron relaxation guided branch-and-bound", C. Wang, ICLR 2022.

[4] https://sites.google.com/view/vnn2023

[5] "Scaling Polyhedral Neural Network Verification on GPUs", C. Muller, MLSys, 2021.

[6] https://github.com/Verified-Intelligence/auto_LiRPA

[7] "Differentiable Abstract Interpretation for Provably Robust Neural Networks", M. Mirman, ICML, 2018.

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

[9] "Fast and Effective Robustness Certification", G. Singh, NeurIPS 2018.

[10] "Efficient Neural Network Robustness Certification with General Activation Functions", H. Zhang, NeurIPS 2018.

[11] https://github.com/huanzhang12/CROWN-IBP