Interpreting Robustness Proofs of Deep Neural Networks
Authors: Debangshu Banerjee
Avaljot Singh
Gagandeep Singh
Venue: ICLR 2024 poster (2024)
Keywords: Neural Network Verification
Robustness
Certification
Primary area: neurosymbolic & hybrid AI systems (physics-informed, logic & formal reasoning, etc.)

Abstract: In recent years numerous methods have been developed to formally verify the robustness of deep neural networks (DNNs). 
Though the proposed techniques are effective in providing mathematical guarantees about the DNNs' behavior, it is not clear whether the proofs generated by these methods are human-understandable. 
In this paper, we bridge this gap by developing new concepts, algorithms, and representations to generate human understandable insights into the internal workings of DNN robustness proofs. 
Leveraging the proposed method, we show that the robustness proofs of standard DNNs rely more on spurious input features as compared to the proofs of DNNs trained to be robust. 
Robustness proofs of the provably robust DNNs filter out a larger number of spurious input features as compared to adversarially trained DNNs, sometimes even leading to the pruning of semantically meaningful input features.
The proofs for the DNNs combining adversarial and provably robust training tend to achieve the middle ground

Published as a conference paper at ICLR 2024
INTERPRETING ROBUSTNESS PROOFS OF DEEP NEU- RAL NETWORKS
Debangshu Banerjee', Avaljot Singh', Gagandeep Singh 1.2 University of Illinois Urbana-Champaign, *VMware Research (db21, jot,, ggnds pillinois. edu
ABSTRACT
In recent years numerous methods have been developed to formally verify the robustness of deep neural networks (DNNs). Though the proposed techniques are effective in providing mathematical guarantees about the DNNs' behavior, it is not clear whether the proof's generated by these methods are human- uumnan--undrttadaabl.. In this paper, we bridge this gap by developing new concepts, algorithms, and representations to generate human understandable insights into the internal work- ings of DNN robustness proofs. Leveraging the proposed method, we show that the robustness proofs of standard DNNs rely more on spurious input features compared to the proofs of DNNs trained to be robust. Robustness proofs of the provably robust DNNs filter out a larger number of spurious input features as compared to adversarially trained DNNs, sometimes even leading to the pruning of semantically meaningful input features. The proofs for the DNNs combining adversarial and provably robust training tend to achieve the middle ground.
INTRODUCTION
The black box construction and lack of robustness of deep neural networks (DNNs) are major obstacles to their real-world deployment in aafett-critical applications like autonomous driving (Bojarski et al. 2016) or medical diagnosis (Amato al. 2013). To mitigate the lack of trust caused by black-box behaviors, there has been a large amount of work on interpreting individual DNN predictions to gain insights into their internal workings. Orthogonally, the field of DNN verification has emerged to formally prove or disprove the robustness of DNNs in particular input region capturing an infinite set of inputs. Verification can be leveraged to train more robust models (Balunovic & Vechev 2020).
We argue that while DNN verification does improve reliability to a certain degree, it does not give any semantically meaningful insights into the working of the generated proof. This is in contrast to standard program verification tasks where proofs capture the semantics of the program and the verified property. like deducing the inductive invariants while proving the termination of a program (Alias al. 2010). Such deductions can be helpful in order to improve the trust of the system and enhance interpretability. Existing techniques (Bau et al. 2017 Nguyen et al. 2016 Mordvintsev let al. 2015) can extract neuron-level details to generate better understanding of the DNN only on individual inputs. DNN verification techniques lift the reasoning on individual inputs to an infinite set of inputs, usually represented in terms of constraints. So, instead of generating single output, these methods generate elaborate complex proof's that certify the DNN's correctness. The primary objective of this work is to dissect and interpret the proof generated by a DNN verifier.
Key Challenges. The proofs generated by of-tee- DNN verifiers (DeepZ (Singh et al. 2018a), CROWN (Zhang al., 2018) etc.) encode nigh-dimensional complex convex shapes defined over thousands of neurons in the DNN, thereby making it difficult to interpret them. Therefore, it imperative to dissect the proof into smaller pieces called proof features that can be interpreted independently and look only at subset of more important proof features. This subset should be less intricate than the original proof while still effectively approximating it. The key challenge here is to identify different features of the proof, concretize the importance of each of these features, and measure how well a set of proof features can approximate the original proof. As we describe in Section 4 this leads to intricate tradeoff size vs. effective approximation vs. the importance of proof feature set.
Our Contributions, We make the following contributions to overcome these challenges:

---

Published as a conference paper at ICLR 2024
We introduce a novel concept of proof features by dissecting a complex high- high-dimensiooal proof into smaller parts that can be interpreted independently. We propose a priority function over the proof features that signify the importance of each proof feature w.L. complete proof.
For proof interpretation, first we design a general algorithm - ProFlt (ProoF Interpretation Technique) for extracting a set of proof features that is (a) small (easy to interpret), (b) retains only the more important parts of the proof, and (c) preserves the property (Section Finally, we adapt the existing visualization techniques (Sundararajan et al., 2017) map extracted proof features to gumman-understnndabb visualizations (Section (4.4.
Using the proposed framework, we observe an interesting discrepancy in the semantic meanings captured by the proofs for DNNs trained using different techniques. We compare visualizations of the extracted proof features for standard DNNs and state-of-the-art robustly trained DNNs for the MNIST and CIFAR10 10 datasets. We observe that the proof features for the standard DNNs rely on spurious regions of the input images while the proof features of adversarially trained DNNs (Madry jet al. 2018) filter out some of the spurious parts of the input. Further, the proofs for networks trained with certifiable training (Zhang et al.) 2020) do not rely on any spurious parts of the input but they also miss out on some meaningful parts. Proofs for training methods that combine both empirical and certified robustness (Balunovic & Vechev 2020) provide a common ground. They not only preserve meaningful input parts but also selectively filter out spurious ones. We empirically show that these observations are not contingent on any specific DNN verifier.
We believe that trustworthy DNNs should not only be robust, but their robustness proof' should capture human-aligned internal representations. The feedback from ProFIt can be leveraged as criterion to differentiate among DNNs achieving similar levels of robustness. ProFIt code is available at httttps: /tpps://qithute com/ wwtp/uuuc-aae
2 RELATED WORK
DNN interpretability and debugging. There has been an extensive effort to develop interpretability tools for investigating and debugging the internal workings of DNNs. These include feature attribution techniques like saliency maps (Sundararajan et al.] [017:: Smilkov et al.. 2017), using surrogate models to interpret local decision boundaries (Ribeiro et al. 2016), finding influential (Koh Liang
2017). prototypical (Kim et al., 2016). or counterfactual inputs (Goyal et al.] 2019). training sparse
decision layers (Wong et al. 2021). utilizing robustness analysis (Hsich et al. (021)). ). Most of these interpretability tools focus on generating local explanations that investigate how DNNs work on individual inputs. Another line of work, instead of explaining individual inputs, identifies specific concepts associated with a particular neuron (Simonyan al., 2014 Bau et al.) 2020). However, to the best of our knowledge, there is no existing work for interpreting DNN robustness proofs.
DNN verification. Unlike DNN interpretability methods, prior works in DNN verification focus on formally proving whether a DNN satisfies desirable properties like robustness (Singh et al. 2019c Wang et al. 202Tb). fairness (Mazzucato & Urban 2021), etc. The DNN verifiers are broadly categorized into three main categories (i) sound but incomplete verifiers which may not always prove property even it holds (Gehr et al. 2018 Singh et al. 2018a| [019b]a a /hang et al. 2018 Xu
et al. 2020 [almmnn et al. (2019). (ii) complete verifiers that can always prove the property if it holds
(Wang et al.
2018 Gehr et al. 2018 Bunel et al. 2020aa b Bak et al. 2020 Ehlers 2017 Ferrari
et al. 2022a
Fromherz et al. 2021 Wang et al. 202 laj Palma et al. 202 Anderson et al. 2020
Zhang et al.
2022) and (ii) verifiers with grobabilistie guarantees (Cohen et al. 2019).
Robustness training. Existing works (Madry al. 2018 Balunovic & Vechev 2020 Zhang et al.,
2020) in developing robust training methods for neural networks provide a framework to produce
networks that are inherently immune to adversarial perturbations in input.
PRELIMINARIES
In this section, we provide the necessary background on DNN verification and existing works on debugging DNNs with sparse decision layers. While our method is applicable to general architectures. for simplicity, we focus on a l-layer feedforward DNN N R + R44 for the rest of this paper. Each layer except the final one applies the transformation X; = (W, X + B.) where W: E Rd, Rd.x and B, E Rd. are respectively the weights and biases of the affine transformation and o; is a non- non-linear activation like ReLU, Sigmoid, etc. corresponding to layer i. The final layer only applies the affine transformation and the network output is vector Y = W X + B,. DNN verification. At a high level, DNN verification involves proving that the network outputs y == N(X) corresponding to all inputs X from an input region specified by o, satisfy logical
2

---

Published as a conference paper at ICLR 2024
specification v. For DNN robustness, the output specification is written as (Y) (C 0) where C' E Rd defines the linear inequality for encoding the robustness property. For the rest of the paper, we refer to the imput region & and output specification & together property (ő, eb). Next, we briefly discuss how DNN verifiers work. A DNN verifier V computes a possibly over- approximated output region A C TRdi containing all possible outputs of N corresponding to Φ. Let, A(A) = miny A C Y denote the minimum value of C where Y E A. Then N satisfies property (ó, +) if A(A) 2 O. Most existing DNN verifiers (Zhang et al. 2018), for non-linear activation functions, compute convex regions that over approximate the output of the activation function. Note that, due to the over-approximation
DNN verifiers are sound but not complete the verifier may not always prove property even if it holds. For piecewise linear activation functions like ReL.U, complete verifiers exist handling the activation exactly. Nevertheless, complete verification in the worst case takes exponential time. In the rest of the paper, we primarily focus on deterministic, sound, and incomplete verifiers which are more scalable than complete verifiers.
Analyzing DNN inferences with sparse decision layer. For analyzing individual DNN inferences, only looking at the output of the DNN hides key details about how the final output was computed by combining the output of each individual neuron (Nguyen et al.) [016 Wong et al. 2021). Conversely, DNNs considered in this paper, have complex multi-layer structures, making them harder to analyze while retaining per neuron-level information. Instead of analyzing neurons from each layer of the DNN, recent works (Wong et al. 2021; Liao & Cheung, 2022) treat DNNs as the composition of a deep feature extractor and an affine decision layer. The output of each neuron of the penultimate layer represents a single deep feature and the final affine layer linearly combines these deep features to compute the network output. This perspective enables us to identify the set of deep features used by the network to compute its output and to investigate their semantic meaning using the existing feature visualization techniques (Ribeiro et al., 2016)). However, visualizing each deep feature is practically infeasible for large DNNs where the penultimate layer can contain thousands of neurons. To address this, the work of (Wong et al. 2021) tries to identify a smaller set of features that are sufficient to maintain the performance of the network. This smaller but sufficient feature set retains only the most important features corresponding to a given input. (Wong et al. 202T) empirically shows that a small subset of deep features (S 10) is sufficient to maintain the accuracy of state-of-the-art models.
4 INTERPRETING DNN ROBUSTNESS PROOFS
Next, we describe our approach for interpreting DNN robustness proofs.
Proof features. Similar to traditional methods used for interpreting DNN inferences described above (Wong et al.] 2021), for interpreting proofs, we propose to segregate the final affine layer from the network and look at the neuron-level features extracted at the penultimate layer. However, proof's generated by DNN verifiers are over an input region (Ø) consisting of infinitely many inputs instead of single input as handled by existing works. In this case, for given input region o, we look at the symbolic shape (for example- - zonotopes, polytopes, etc.) computed by the verifier at the penultimate layer and then compute its projection on each dimension of the penultimate layer. These projections yield an interval [L,, [,,] containing all possible output values of the corresponding neuron n. w.r.t Φ-
Definition 1 (Proof Features). Given a network N, input region & and neural network verifier V. for each neuron n; at the penultimate layer of N, the feature Fug extracted at that neuron n. is an interval [Z,,, Uny] such that VX E Φ. the output at n; always lies in the range [!,., bndl
Note that, the computation of the proof features is verifier dependent, i.e., for the same network and input region, different verifiers may compute different values L, and un for a particular neuron n. Similarly, even two output-equivalent networks that produce the same output on all possible inputs but have different architectures can have different proofs and subsequently different proof features. For any input region é, the first (I 1) layers of N along with the verifier V act as the proof feature extractor. For the rest of this paper, we use F to denote the set of all proof features at the penultimate layer and F, to denote the proof features corresponding to I S [d:-1] i.e. F, (F.,, i E r). Suppose is formally verified by the verifier V to satisfy the property (ò. v)) Then in order to gain insights about the proof generated by V. we can directly investigate (described in section 4.4) all the extracted proof features F. However, the number of proof features for contemporary networks can be very large (in thousands). Many of these proof features may not be important for the proof. Similar to how DNNs are interpreted w.r. individual inferences, we want to identify a smaller set of proof features that are more important for the proof of the property (ó. v)).
3

---

Published as a conference paper at ICLR 2024
4.1 PROBLEM FORMULATION FOR PROOF INTERPRETATION
Before delving into the details, first, we lay out our expectations for the proof feature set that will be used for interpreting the proof and explain why these expectations are relevant. In section [3.2] we empirically validate that the proof feature set extracted by ProFlt fulfills these expectations.
A. Small size. The size of the proof feature set Fs should be minimized so that investigating the
constituent proof features becomes easier. Otherwise, investigating the entire set F is always a valid but expensive option considering the size of F is large (in thousands) for contemporary DNNs.
B. Sufficiency. Beyond the small size, we argue that any candidate proof feature set Fs F must at least prove the property (ø, 1)) with verifier V. Otherwise, it does not make sense to interpret a proof feature set that itself does not satisfy the property. Next, we introduce the novel concepts of proof feature pruning to formally define sufficient proof feature set below:
Definition 2 (Proof feature Pruning). Pruming any proof feature Fr., F corresponding to neuron n, the penultimate layer involves setting weights of all its outgoing connections so that given any input X E & the final outpui of N no longer depends on the outpul of ni.
Once, proof feature Fr, is pruned the verifier V no longer uses Fr, to prove the property (é, ()). Definition (Sufficient proof feature set), For the proof of property (sb 1b on DNN N with verifier V. nonempty set Fs F of proof features is sufficient if the property still holds with verifier V even all the proof features not in F.g are pruned.
Before detailing other properties we expect the proof feature set used for interpreting the proof to satisfy, we explain how we can algorithmically check whether any proof feature set Fs is sufficient or not. Let, Wi[:: i] E Rdd denote the i-th column of the weight matrix W of the final layer N₁. Pruning any proof feature Fn, results in setting all weights in [i[:, i] to O. For any proof feature set Fs S F. let W(S E Idi xdi-1 be the weight matrix of the pruned final layer that only retains proof features corresponding Fs. Then columns of Wi) are defined below where is constant all-zero vector
Wi[:.a] i] E
(i()) 1
otherwise
The proof feature set Fg is sufficient iff the property (ø, v/) can be verified by V on N with the pruned weight matrix (S)). Let, the verifier V compute an over-approximated output region A of N over the imput region ø. Given that we never change the input region and the proof feature extractor composed of the first 2 - layers of N and the verifier V. the output region A of the pruned network only depends on the pruning done at the final layer. Now let A(W,, S) denote the over-approximated output region corresponding to WS)).. The neural network N can be verified by V on the property (é, b with (S) iff the lower bound A(A(W,, 2 0.
C. Importance. The notion of sufficiency and minimality of Fs alone does not enforce that Fs always includes proof features that are "important" for the proof. To resolve this issue. we define priority P(Fn.) for every proof feature Fn, that captures its importance w.r.t the proof. Given sufficient proof features set Fs, for a proof feature Fr,, E Fs. we compute its priority by estimating the absolute change F() that occurs A A(A(W,,, if Fr, is pruned from Fs. At a high level, for each proof feature Fn, contained in a sufficient feature set, the priority of Fr. tries to estimate whether pruning F,, violates the property (ø, 1²) or not. Pruning a proof feature Fn; with small A(Fr, FFs) only results in a small absolute change in the verifier output and the remaining proof features Fs's {Fr,) will likely satisfy the property. Moreover, in this case, the set Fs \ {Fr,) precisely approximate (the absolute change is small) the verifier output A(A(W,, S)) computed with the entire set Fs. Let, the over-approximated output region computed by verifier V corresponding to Fs \ (Fn,) } be A(Wi, \ (i)) then FF,,FF)) is defined as follows
A(Fr,, FF) A(A(W,, S)) - A(A(W,, S \ {i)))
However, A(F n. Fs) depends on the particular sufficient proof set Fs and does not estimate the global importance of Fr,, independent of the choice of Fs. Hence to define the priority P(F,,) of proof feature Fn, we take the maximum of A(Fr,. FF) over all sufficient feature sets Fs containing Fu,. Let, S(Fn.) denote set of all sufficient Fs containing Fr,- Then, P(Fn,) is as follows
P(F..))
max J's B(F..)
A(F
(2)
Overall, for proof interpretation, we want to extract a proof feature set Fs, that is as small as possible, sufficient, and retains important proof features. However, there is a tradeoff between the three criteria.
4

---

Published as a conference paper at ICLR 2024
For example, the entire proof feature set F is always sufficient but it is not small. Similarly, if C" B, 2 0 (B; is the bias of the final layer) the minimum sized sufficient proof feature set will always be empty. In this case, although the empty set is the smallest and sufficient it does not retain any important proof features. This tradeoff between size, sufficiency, and importance makes it hard to find F.. Moreover, the search space for Fso is prohibitively large containing 2d:- possible candidates, and computing Fs, with an exhaustive search is infeasible. Even just computing the priority P(Fn.) for a proof feature Fn, can be expensive considering the set S(F,.) can be exponentially large. So, we first design an approximation of P P(Fn.) that is easy to compute.
4.2 APPROXIMATE PRIORITY OF PROOF FEATURES
As described above, finding the maximum value of A(Fr, Fs) over S(Fn.) ) is practically infeasible. So compute an upper bound (n.(F of P(Fn.) by estimating a global non-trivial upper bound of AFF,, n., Fs). that holds VFss E ((.n.). The proposed global upper bound is independent of the choice of Fs E S(Fr.) and therefore removes the need to iterate over S(F,,) enabling efficient computation. For the network, N and input region o let A1-1 1 denote the over-approximate symbolic region computed by V at the penultimate layer. Then vJss E s(Fn,) the global uppper bound of A(F Fs)
can be computed as follows where for any X E Rd 1, x3 denotes its i-th coordinate:
A(Fn,, S max XEAL-1
(CC - C'WI(S \ (()))) = max (i(;) x:)l
XEAL11
P(F)))
max F.E)(F..))
max XEA:-1
-x:]
Now, any proof feature Fr. = 1,,, Jn,] computed by V contains all possible values of I; where X E A1-1. Leveraging this observation, we can further simplify the upper bound (us(Fa.) of P(Fn.) as shown below.
s max [.E(Mn
(CCTW,. |as|| = ICC Wil:. a]I max( Ium,, (n.(F (3)
This simplification ensures that (F.) for all Fr, can be computed with 1(d--1) elementary vector operations and single verifier call that computes the intervals [n, Un.]-
4.3 PROFIT ALGORITHM
Next, describe how we approximately compute Fs. that is sufficient, small in size, and retains proof features Fn; with higher priorities (us() To reduce the size of the proof feature set, a trivial step is to just prune all the proof features from F whose Pub is O. These features do not have any contribution to the proof of the property (ó, Φ)) by the verifier V. This step forms a trivial algorithm. However, this is not enough. We can further prune more proof features leading to a yet smaller set. For this, we propose an iterative algorithm ProFIt shown in Algorithm ! which maintains two set namely, Fs, and Fs. Fs. contains the features guaranteed to be included in the final answer computed by ProFit and Fs contains the candidate features yet to be pruned by the algorithm. At every step, the algorithm ensures that the set Fs J Fso is sufficient and iteratively reduces its size by pruning proof features from Fs. The algorithm iteratively prunes the feature Fr with the lowest value of (F..) from Fs while retaining features with higher priorities in Fs U Fs.. At Line in the algorithm, Fs, and Fs are initialized as empty set ({)) and F respectively. We note that checking the sufficiency of any arbitrary proof feature set Fs (Definition 3) is not trivial and requires expensive verifier invocations. Since we are modifying only the final layer, we use incremental verification (Ugare et al.. 2022 2023 2024) that can efficiently verify the property without starting from scratch. Still removing a single feature in each iteration and checking the sufficiency of the remaining features in the worst case leads to ((d-1) increeental verification calls which are expensive. Instead, at each step, from Fs our algorithm greedily picks top-|S) /2 features (line 10) Fs, based on their priority and invokes the verifier V to check the sufficiency of Fs. U Fs, (line 12). If the feature set Fs. J Fs. sufficient (line 13), ProFlt removes all features in Fs Fs, from Fs and therefore Fs is updated as Fs, in this step (line 14). Otherwise, if Fs, U Fs, does not preserve the property (6.15 (line 15), ProFit adds all feature in Fs, to Fs, (line 16) and replaces Fs with Fs Fs, (line 17). The algorithm terminates after all features in Fs are exhausted. Since at every step, the algorithm reduces size of Fs by half, it always terminates within Olog(dd (d)-1)) incremental verifier calls. As mentioned before, the empty proof feature set is sufficient iff C* B, 2 0, in this case, ProFIt extracts smallest non-empty sufficient proof feature set which like all other cases includes proof features with the higher priority. In Appendix A we derive mathematical guarantees about the correctness and efficacy
5

---

Published as a conference paper at ICLR 2024
Algorithm 1 Approximate minimum proof feature extraction
1: Input: DNN N, property (é, v), verifier V.
11:
Fs₂ Fs Fs,
2: Output: approx. minimum proof features
12:
Check sufficiency of Fs. Fs, with
Fs..
13:
if Fs. U Fs, is sufficient then Fs Ps.
3: if V can not verify on ()) then
14:
4: return
15:
else
5: end if
16:
Fs. Fs. U Fs,
6: Calculate all proof features for input region Φb 17:
Fş Fsz
7: Calculate priority Pus(Fnn) all proof features. 18:
end if
8: Initialization: Fs.- (). Fs- =
19:
end while
9: while Fs is not empty do
20: return proof features Fs..
Fs. top-|S1/2 features based on Put (F.))
of Algorithm|] ! For correctness, we prove that the feature set Fs, is always sufficient (Definition 3). For efficacy, we theoretically find non-trivial upper bound the size of Fso.
4.4
VISUALIZATION OF EXTRACTED PROOF FEATURES
Once the proof features are extracted, we want to map them to a human interpreetterreee format. There exists plethora of works (Sundararajan et al., 2017 Smilkov et al. (017) that generate human- interpretable visualizations of the output of individual neurons w.r.t single inputs. However, these techniques are insufficient to generate explanations w.r.t an input region. To resolve this, we adapt the existing local gradient-based visualization techniques (Sundararajan et al. (017)) for visualizing the extracted proof features. As shown in existing works (Mirman et al. 2018), common incomplete DNN verifiers (Xu et al.) 2021 (ingh et al. 2019b) can be represented differentiable programs. This enables us to use the gradients on the differentiable programs for visualization. For any proof feature
Fn = |n, un.] both bn, uh can be expressed as differentiable functions I, = T.n (x) x1 ......... 27 do =2))) and Un (2t x " It do .rdo) where Vi do xf I; and x 2; are the lower and upper bound the i-th input cooridinate, x; is the unperturbed value, e; is amount of perturbation. To measure the sensitivity of proof feature Fn w.r.t change in i-th imput coordinate,
take the gradient _ مL 8Ua) of the mean (also the midpoint) (1++)))) of Fr w.r.t eG. This gradient Br; ör; captures the change in the mean value of the proof feature w.r.t the change in i-th input coordinate. However, complete DNN verifiers such as SMT-based (Katz et al. (017) or LP/MIL-P-based verifiers differentiable programs. For a non-differentiable
(Singh al., (018b) cannot be represented DNN verifier, we propose an alternative visualization technique in Appendix B based on statistical estimation of the mean gradient over inputs satisfying Φ.
4.5 LIMITATIONS
The scalability of our method is ultimately limited by the scalability of the existing DNN verifiers. Therefore, ProFIt currently cannot handle large DNNs (e.g. vision transformers (Dosovitskiy et al.) 202T). ImageNet classifiers, etc.). Nonetheless, ProFIt general and compatible with any verification algorithm. Therefore, ProFIt will benefit from any future advances to enable the DNN verifiers to scale to larger DNNs and datasets. We focus on the proof features extracted at the penultimate layer but not other hidden layers. ProFIt only handle deterministic verifiers and does not currently work with probabilistic verifiers like randomized smoothing (Cohen et al.) (2019). These extensions will require defining priority for proof features and devising algorithms extract them.
EXPERIMENTAL EVALUATION
5.1 EXPERIMENTAL SETUP
For evaluation we use convolutional networks trained on two popular datasets MNIST (LeCun) et al. 1989) CIF (Krizhevsky 2009) shown in Table [ The networks are trained with standard training and three state-of-the-a robust training methodologies adversarial training (PGD training) (Madry et al. 2018), certified robust training (CROWN-IBP) (Zhang et al. 2020) and a combination of both adversarial and certified training (COLT) (Balunovic & Vechev 2020). For experiments, pre-trained publically available networks the standard and PGD networks are from the

---

Published as a conference paper at ICLR 2024
Dutasct
Training Method
Input Region (6)
No. of
Original Feature Count
Mcan Proof Feature Count
No. of proofs with <
No. of proofs
proved properties
eps (c)
proof features (PmoFtt
proof features
Random
Gradient
PmoFit
(ProFh)
MNIST
Standard
0.02
459
100
20.31
5.25
1.96
449
457
PGD Trained
0.02
415
1000
93.29
13.73
6.02
315
364
COLT
0.02
480
100
14.45
5.43
3.46
401
CROWN-IBP
0.02
482
100
9.51
6.73
6.16
240
401
MNIST
PGD Trained
0.1
191
1000
162.39
35,79
3.29
131
149
COLT
281
100
29.57
12.22
3.16
240
271
CROWN IBP
0.1
473
100
10.09
7.36
6.23
232
384
CIFAR-10
Standard
0.2/255
277
100
30.36
18.28
11.12
127
173
PGD Trained
0,2/255
298
100
31.22
16.58
9.74
173
210
COLT
0.2/255
267
250
30.10
18.13
9.03
170
204
CROWN-IBP
0,2/255
265
256
7.96
7.49
5.30
172
221
CIFAR-10
PGD Trained
2/255
173
100
39.57
24.46
6.19
122
144
COLT
2/235
229
250
34.64
23,25
7.76
146
181
CROWN
2/255
206
256
9.41
9.21
5.10
140
176
Table 1: ProFIt Efficacy Analysis
ERAN project (Singh et al., 2019c COLT, and CROWN-IBP networks taken from their official repositories (Balunovic Vechev| 2020; Zhang et al., 2020). Similar to the existing works on DNN verification (Zhang al.) 2018), use Loe -bssed local robustness properties (Carlini & Wagner 2017). Here, the input region @ contains all images obtained by perturbing the intensity of each pixel in the input image independently within bound c. 1/ specifies region where the network's output for the correct class higher than all other classes. Ctrain = 0.1 and Grran = 8/255 are used while training all robustly trained MNIST and CIFAR-10 networks respectively. Unless specified otherwise, the proofs are generated by running the state-of-the-ar incomplete verifier a-Crown (Xu et al. 2021). We run all experiments on 16-core 12th-gen i7 machine with 16 GB of RAM.
5.2 EFFICACY OF PROFIT ALGORITHM
In this section, we experimentally evaluate the efficacy of ProFIt in terms of the size of the extracted sufficient proof feature sets and also assess the usefulness of the proposed priority ordering (Eq. 3 in extracting important proof features. The size of the extracted sufficient proof feature set captures the ease of interpreting the extracted feature set that preserves the proof. Considering there is no existing work for property-presee preserving pruning of proof features, we run ProFIt with two natural heuristics that define the priority of the proof features and use them as baselines. These are (i) random ordering of the proof features and (ii) computing the gradient of the verifier output w.r.t each proof feature and sorting the proof features in the decreasing order of the corresponding gradient magnitude. The gradient magnitude-basee priority order has already been successfully applied (Lis et al., 2019)) to traditional DNN pruning used for reducing the size of the networks. We note that incomplete verifiers like a- a-Crown are differentiable. Moreover, pruning proof features with gradient- brased priority heuristics can be viewed as applying existing feature extraction techniques assuming the underlying verifier is differentiable. For each network, we use the first 500 images from their corresponding test sets for defining input specification db We conduct experiments with two different e values define Loo input region. The values used for MNIST networks are 0.02 and 0.1 and that for CIFAR-I 10 networks are 0.2/255 /55 and 2/ 2/255. For experiments with high e values (0.1 for MNIST and 2/255 for CIFAR-10), we omit standard networks as they do not satisfy local robustness properties defined with high e values. In comparing proof feature sizes, we exclude "zero" features where both lower and upper bounds (1 and u) are zero, as they can be removed without affecting the verifier's 's output.
Mean extracted proof feature set size comparison: In Table we summarize the results of the experiments for different networks and different values. We show that the mean size of the proof feature set computed using ProFIt (column 8) is significantly smaller than that of both the baselines (columns 6 and respectively). This shows proof feature sets computed using ProFIt are easy to interpret. The distributions of extracted proof feature sets size for all DNNs are in Appendix C.1
Evaluation of proof feature priority: Next, we evaluate the efficacy of the priority ordering of proof features (defined in Eq. 3) in identifying important proof features and compare against the random and gradient- based priority ordering defined above. For these experiments, we fix the proof feature set size and compare the extracted proof feature sets with the fixed size based on two metrics - (i) % cases the extracted proof feature set preserves the property (cb, vb) that was satisfied initially and
7

---

Published as a conference paper at ICLR 2024
1% of Srooe preserree
pood
Prtta
Ransiem
No. of Proof features
No. Proot features
No. of Proof festures
(a) PGD Network
(b) Colt Network
(c) Crown-IBP Network
Figure 1: Percentages of proofs preserved by different priority heuristics robust MNIST networks.
Profi
PigFi
Pioft
Random
Random
Random
Gradient
Gendierr
Geadler
No. of Proof features
No. of Proof features
No. of Proof features
(c) Crown-IBP Network Figure 2: Relative change in verifier output with different heuristics robust MNIST networks.
(a) PGD Network
(b) Colt Network
(ii) mean relative change in verifier output after every proof feature, not part of the extracted set is removed. Since we fixed the extracted proof feature set size, the feature set is no longer guaranteed to be sufficient. For proof feature set size varying from 2 to 20, compared to both the baselines,
show that the priority ordering used by ProFIt preserves a higher % of proofs (Fig. [ while more precisely approximating the original verifier output (the relative change from original verifier output is smaller) (Fig. 2) These plots are generated on robust MNIST networks for = 0.1. Plots for standard MNIST network and CIFAR-10 networks are shown in Appendix C.2 Additionally, in Appendix C.3 we provide a qualitative evaluation of the priority ordering of proof features where we show that visualizations of proof features with higher priority capture meaningful input features while visualizations of proof features with lower priority are less informative. This shows the proposed priority of the proof features (Eq. 3 is indeed effective in identifying their importance w.r.t the proof.
5.3 QUALITITIVE COMPARISON OF ROBUSTNESS PROOFS
TTippas et al. 2019) observed that the standardly trained networks rely on some spurious input features to gain a higher accuracy and result, are not very robust against adversarial attacks. In contrast, the PGD trained networks rely more on human- human-understandable features and are, therefore, more robust against attacks. This empirical robustness comes cost of reduced accuracy. So, there is an inherent dissimilarity between the types of input features that the standard and adversarially trained networks rely on while classifying a single input. Also, certified robust trained networks are more robust than the empirically trained ones, however, they report even less accuracy (Müller et al. 2021). In this section, we interpret proof features extracted with ProFIt and use the obtained visualizations to qualitatively check for the existence of such dissimilarities among different proofs of the same robustness property on standard and robustly trained networks. We also study the effect of certified robust training methods like CROWN-IBP, empirically robust training methods like PGD, and training methods that combine both adversarial and certified training like COLT on the proof features. For local input region é. we say that a robustness proof is semantically meaningful if focuses on the input features relevant to the output class for images in 6 and not on the spurious features. In the case of MNIST or CIFAR- 10 images, spurious input features are the pixels coming from the image background, whereas important input features are the pixels that are a part of the actual object being identified by the network. The gradient map the extracted proof features w.r.t. the change in input pixels (see Section 4.4) identifies the input pixels that the proof focuses
In Fig. 3 we compare the gradient maps corresponding to the top proof feature (the one having the highest priority P.s (ur(F..)) )) networks from Table I on representative images of different output classes in the MNIST and CIFARIO test sets. These experiments lead us to interesting observations even if some property is verified for both the standard network and the robustly trained network, there
8

---

Published as a conference paper at ICLR 2024
Imsge
Slandard
RGD
COLT
CROWNIBP
Image
Stundard
PGD
COLT
CROWN-IB
3
2
(a) Gradient maps generated MNIST DNNs. (b) Gradient maps generated on CIFAR-I0 DNNs.
Figure 3: Gradient map corresponding to the top proof feature corresponding to DNNs trained using different methods rely different imput features.
a difference in the human interpretability of the types of input features that the proofs rely The standard networks and the provably robust trained networks like CROWN-IBP are the two extremes of the spectrum. For the standard networks, we observe that although the top-proof feature does depend on some of the semantically meaningful regions of the input image, the gradient at several spurious input features is also non-zero. In contrast, the top proof feature corresponding to state-of tatte-of-the-ar art provably robust training method CROWN-IBP filters out most of the spurious features, but it also misses out on some meaningful features. The proofs of PGD-trained networks filter out the spurious features and are, therefore, more semantically aligned than the standard networks. The proofs of the training methods that combine both empirical robustness and provable robustness like COLT in way provide the best of both worlds by not only selectively filtering out the spurious features but also highlighting the more human interpretable features. So, as the training methods tend to regularize more for robustness, their proofs become more selective in the type of input features that they rely on. To substantiate our observation, we show additional visualizations of the top proof features in Appendix C.4] and visualizations for the entire proof feature set in Appendix C.5 The extracted proof features set and their gradient maps computed w.r.t high values (c = 0.1 for MNIST and = 2/255 for (IFAR-10) are similar to those generated with smaller shown in Appendix C.6
5.4 ABLATION STUDIES
Different verifiers: The proof features extracted by ProFIt are specific to the proof generated by the verifier. To show the qualitative analysis presented in section 5.3 is not contingent on a- a-Crown we run ProFIt with different verifiers including DeepZ (Singh et al. 2018a). Crown (Zhang et al., 2018) and ofte-off-hhearr complete verifier o. 3-Crrwn (Wang et al. (202bb) and compare the top proof feature. We use networks shown in Table Table the same properties as before. We observe that in more than 95% of cases, the top proof feature extracted with different verifiers remains the same. Further, the visualizations of the top proof feature w.r.t different differentiable verifiers also align with the observation in section 5.3 In this case, for different verifiers though the proof features Fr, = -Im,,, [tn,] change, their relative priority ordering computed by Eq. remains the same. Note, while comparing proof features from two different verifiers only consider those properties that be proved by both the verifiers. The results are in Appendix C.7 and visualizations in Appendix C.8
compare proofs generated on networks with the same architecture trained with different training methods to validate that the underlying network architecture does not affect in the conclusions presented in Section 5.3 We also analyze the sensitivity of the extracted proof features to the training parameter Crain that is used to define the L,x. region during training (Appendix 1O). We observe that networks trained with higher étrain are more robust and the top-proof feature filters out more input features that align with the observations in Section 5.3
Training parameters: Appendix C.9
CONCLUSION
We developed novel method called ProFIt to interpret DNN robustness proofs. We empirically establish that even if property holds for DNN, the proof for the property may rely on spurious or semantically meaningful internal representations depending on the training method. We believe that ProFIt can be applied for diagnosing the trustworthiness of DNNs inside their development pipeline.

---

Published as a conference paper at ICLR 2024
7 ACKNOWLEDGEMENT
We thank the anonymous reviewers for their insightful comments. This work was supported in part by NSF Grants No. CCF-2238079, CCF-2316233, CNS-2148583, and Google Research Scholar award.
REFERENCES
Christophe Alias, Alain Darte, Paul Feautrier, and Laure Gonnord. Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In Radhia Cousot and Matthieu Martel (eds.), Static Analysis, pp. 117-133, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. ISBN 978-3-642-157699
Filippo Amato, Alberto López, Eladia María Peñia-Méndez, Petr Vañhara, Aleš Hampl, and Josef Havel. Artificial neural networks in medical diagnosis. Journal of Applied Biomedicine, 11(2), 2013.
Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixedd-ntteger programming formulations for trained neural networks. Mathematical Programming, 2020.
Stanley Bak, Hoang-Dung Tran, Kerianne Hobbs, and Taylor T. Johnson. Improved geometric path enumeration for verifying relu neural networks. In Shuvendu K. Lahiri and Chao Wang (eds.), Computer Aided Verification 332dd International Conference, CAV 2020, Los Angeles, CA, USA, July 2/-24, 2020, Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pp. L4 URL /esttp::/doi..rrre
66-96. Springer, 2020. doi: 10. 1007/978 3-00 -3288-822288
Mislav Balunovic and Martin T. Vechev. Adversarial training and provable defenses: Bridging the gap. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. OpenReview.net, 2020.
David Bau, Bolei Zhou, Aditya Khosla, Aude Oliva, and Antonio Torralba. Network dissection: Quantifying interpretability of deep visual representations. In Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 6541 65599, 2017.
David Bau, Jun Zhu, Hendrik Strobelt, Agata Lapedriza, Bolei Zhou, and Antonio Torralba. Understanding the role of individual units in deep neural network. Proceedings of the National 2020.
Academy of Sciences, 11704))3007113007
Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, et End end learning for self-driving cars. arXiv preprint arXiv: 1rXiv:1604.07316 2016.
Christopher Brix, Mark Niklas Müller, Stanley Bak, Taylor T. Johnson, and Changliu Liu. First three years of the international verification of neural networks competition (vnn-comp), 2023.
Rudy Bunel, Jingyue Lu, lIker Turkaslan, Pushmeet Kohli, P Torr, and P Mudigonda. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21 (2020), 2020a.
Rudy R Bunel, Oliver Hinder, Srinadh Bhojanapalli, and Krishnamurthy Dvijotham. An efficient non- convex reformulation of stagewise convex optimization problems. Advances in Neural Information Processing Systems, 33, 2020b.
Nicholas Carlini and David Wagner. Towards evaluating the robustness of neural networks. In 2017 ieee sympositm on security and privacy (sp), pp. 39-57. Icce, 2017.
Jeremy Cohen, Elan Rosenfeld, and Zico Kolter. Certified adversarial robustness via randomized smoothing. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference Machine Learning, volume 97 of Proceedings of Machine Learning Research, pp. 1310-1320, PMLR, 09-15 Jun 2019. URL https: httpp:://proceddngg. mlr
preas/v97/cont cohen 9c. html
10

---

Published as a conference paper at ICLR 2024
Alexey Dosovitskiy, Lucas Beyer, Alexander Kolesnikov, Dirk Weissenborn, Xiaohua Zhai, Thomas Unterthiner, Mostafa Dehghani, Matthias Minderer, Georg Heigold, Sylvain Gelly, Jakob Uszkoreit, and Neil Houlsby. An image is worth 16x16 words: Transformers for image recognition at scale. In International Conference on Learning Representations, 2021. URL http:: htttps://openreiieee met//oruu wtw.:mmmmdiiiccccTTcmT
Ruediger Ehlers. Formal verification of wiee linear feed-forward neural networks. In Interna- lional Symposium on Automated Technology for Verification and Analysis, 2017.
Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanović, and Martin Vechev. Complete verification via multi-neuron relaxation guided branch-and-bound. In International Conference on Learning Representations, 2022a. URL
ew net. forum? wttpmmmid=___eeee am oark
Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanović, and Martin Vechev. Complete verification via multi-neuron relaxation guided branch-and-bound. In International Conference on Learning Representations, 2022b. URL /
net/ forum?id=] _amHf faaefloaa loak
Aymeric Fromherz, Klas Leino, Matt Fredrikson, Bryan Parno, and Corina Pasareanu. Fast geo- metric projections for local robustness certification. In International Conference on Learning Representations, 2021. URL http::://ppeerevieeet net/ http://wwweee//ooormoooooo--=xee
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), 2018.
Yash Goyal, Ziyan Wu, Jan Ernst, Dhruv Batra, Devi Parikh, and Stefan Lee. Counterfactual visual explanations. In International Conference on Machine Learning, pp. 2376-2384. PMLR, 2019.
Cheng-Y Yu Hsieh, Chih-Kuan Yeh, Xuanqing Liu, Pradeep Kumar Ravikumar, Seungyeon Kim, Sanjiv Kumar, and Cho-Jui Hsich. Evaluations and methods for explanation through robustness analysis. In International Conference on Learning Representations, 2021. URL https: / nntt/
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I 30, pp. 97-117. Springer, 2017.
Been Kim, Rajiv Khanna, and Oluwasanmi Koyejo. Examples are not enough, learn to criticize! criticism for interpretabilltyy Advances in neural information processing systems, 29, 2016.
Pang Wei Koh and Percy Liang. Understanding black-box predictions via influence functions. In International conference on machine learning, pp. 1885-1894, PMLR, 2017.
Alex Krizhevsky. Learning multiple layers of features from tiny images. 2009.
Yann LeCun, Bernhard E. Boser, John Denker, Donnie Henderson, Richard Howard, Wayne E. Hubbard, and Lawrence D. Jackel. Handwritten digit recognition with a back-propagation network. In NIPS. pp. 396-404, 1989.
Zukang Liao and Michael Cheung. Automated invariance testing for machine learning models using sparse linear layers. In ICML 2022: Workshop on Spurious Correlations, Invariance and Stability, 2022. URL bttpp:://ppereviiiiie otttt//oooooo.2/-AAAAA 1
net/ forum?
Mieszko Lis, Maximilian Golub, and Guy Lemieux. Full deep neural network training on a pruned weight budget. In A. Talwalkar, V. Smith, and M. Za- haria (eds.), Proceedings of Machine Learning and Systems, volume 1, pp. 252-263. org/paper wwwps//papeeeee///./.. 2019 .pdf]
2019. URL htttps://rroceedings. .mw.ss.mmms......mm https///s..ssssss../.p........e File/7 (tt.7/11de22eeee 9d22b51 (15
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In Proc. International Conference Learning Representations (ICIR), 2018
11

---

Published as a conference paper at ICLR 2024
Denis Mazzucato and Caterina Urban. Reduced products of abstract domains for fairesss tification of neural networks. In Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi (eds.), Static Analysis 28th International Symposium, SAS 2021, Chicago. IL. USA, October 17-19, 2021, Proceedings, volume 12913 of Lecture Notes in Computer Science, pp. 308-322. Springer, 2021. doi: 10. 001779778-3030-88800 978 3- 030
15. URL hht.tss://do.... 00tp://000...00100.0/00.0000
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In Jennifer Dy and Andreas Krause (eds.), Proceedings of the 35th International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning mlr
Research, pp. -587--586... PMLR, 10-15 Jul 2018. URL
html
A. Mordvintsev, Christopher Olah, and Mike Tyka. Inceptionism: Going deeper into neural networks. 2015. URL httpl:ttt///apaat seaant icscholar. wwtp/oogg///..o. 69951972
Mark Niklas Mueller, Franziska Eckert, Mare Fischer, and Martin Vechev. Certified training: Small boxes are all you need. In The Eleventh International Conference on Learning Representations, 2023. URL
ew, hwt.:/ettooouaoae wtrmm/rrrmmmmmmmm w=t.:/dttooFotu.....
Christoph Müller, François Serre, Gagandeep Singh, Markus Püschel, and Martin Vechev, Scaling polyhedral neural network verification gpus. In A. Smola, A. Dimakis, and I. Stoica (eds.). Proceedings of Machine Learning and Systems. volume 3. pp. 733-746, 2021. URL https::/ .mlssssssmssss....m..m.......... wwtp:/ppppppp./..........p /iile/ ca ca46c1b95 2a (a833555533555565222252
.pdff
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschell and Martin Vechev. Prima: General and precise neural network certification via scalable convex hull approximations. Proc.
ACM Program. Lang., 6(POPL), jan 2022. doi: 10. 10.1145/3498704, URL [RtL/ttts////ii..o
10.1145/349877
Anh Nguyen, Alexey Dosovitskiy, Jason Yosinski, Thomas Brox, and Jeff Clune. Synthesizing the preferred inputs for neurons in neural networks via deep generator networks. Advances in neural information processing systems, 29, 2016.
Alessandro De Palma, Harkirat S. Behl, Rudy R. Bunel, Philip H. S. Torr, and M. Pawan Ku- mar. Scaling the convex barrier with active sets. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021,
Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. why should i trust you?" explaining the predictions of any classifier. In Proceedings of the 22nd ACM SIGKDD international conference on knowledge discovery and data mining, pp. 1135-1144, 2016
Hadi Salman, Greg Yang. Huan Zhang, Cho-Jui Hsich, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurlPS 2019, December 8-14, 2019, Vancouver, BC, Canada, 2019.
Karen Simonyan, Andrea Vedaldi, and Andrew Zisserman. Deep inside convolutional networks: Visualising image classification models and saliency maps. In Yoshua Bengio and Yann LeCun (eds.), 2nd International Conference on Learning Representations, ICLR 2014, Banffi AB, Canada, April 16, 2014, Workshop Track Proceedings, 2014. URL http::/ org/ 1312. 6034
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. Advances in Neural Information Processing Systems, 31, 2018a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification of neural networks. In International conference learning representations, 2018b.
Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems, 2019a.
12

---

Published as a conference paper at ICLR 2024
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(PPLL), 2019b.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Robustness certification with refinement. In International Conference on Learning Representations, 2019c. URL https
//openreviee eew wttpiieee.eet.ttteeeeeee wtt.://eeoooormiiiooeeeeeeeeeeea
Daniel Smilkov, Nikhil Thorat, Been Kim, Fernanda B. Viégas, and Martin Wattenberg. Smoothgrad: removing noise by adding noise. CoRR, abs//106.03825, 2017. URL UtRLhtttp:/arxllvooo
abs/1706.00 03825
Mukund Sundararajan, Ankur Taly, and Qiqi Yan. Axiomatic attribution for deep networks. In International conference on machine learning, pp. 3319-3328, PMLR, 2017.
Dimitris Tsipras, Shibani Santurkar, Logan Engstrom, Alexander Tumer, and Aleksander Madry, Ro- bustness may be odds with accuracy. In International Conference on Learning Representations, 2019. URL http://///ppeeeeeeee.e..eeeeee
ew. new. formm? Ftt.er//ooorrrrmmmmooaax d=Sxxbb30cy)
Shubham Ugare, Gagandeep Singh, and Sasa Misailovic. Proof transfer for fast certification of multiple approximate neural networks. Proc. ACM Program. Lang, 6(0OPSLAI), apr 2022. doi: 10.1 10.1344//527319, URL / wwo.oo/g//ooo 11450112113333311111
Shubham Ugare, Debangshu Banerjee, Sasa Misailovic, and Gagandeep Singh. Incremental verifica- tion of neural networks. Proc. ACM Program. Lang., 7(PLDI), 2023. doi: 10. N9.1145/359122 1299.
URL httpp:://o// /tt///oo..or/111111////33333
Shubham Ugare, Tarun Suresh, Debangshu Banerjee, Gagandeep Singh, and Sasa Misailovic. Incre- mental randomized smoothing certification. In The Twelfth International Conference on Learning Representations, 2024. URL
net forum ?id (o-ouummdd-dddA-iiin
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems, 2018.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta- crown: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. arXiv preprint arXiv:2103.0660 2021a.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsich, and J Zico Kolter. Beta- CROWN: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. In A. Beygelzimer, Y. Dauphin, P. Liang, and J. Wortman Vaughan (eds.). Advances in Neural Information Processing Systems, 2021b. URL htttts:://opereeeeeeee tttt:fformiiddahii RBeCFw
Eric Wong, Shibani Santurkar, and Aleksander Madry. Leveraging sparse linear layers for debuggable deep networks. In International Conference on Machine Learning, pp. 1 11205-11216. PMLR, 2021.
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai- Kei-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. 2020.
Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations, 2021. URL
httpps://openrevier net/ /ttp//oommmmmommtaaaaltl 6
Huan Zhang, Tsui- Weng, Pin- Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in neural information processing systems, 2018
Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane S. Boning, and Cho-Jui Hsich. Towards stable and efficient training of verifiably robust neural networks. In Proc. International Conference Learning Representations, ICLR, 2020.
13

---

Published as a conference paper at ICLR 2024
Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter, General cutting planes for gound-rooaggttonn based neural network verification. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho (eds.), Advances in Neural Information Processing Systems, 2022. URL httpt::tpss................ss... /ownn//veeeeeeeeeeeeeeeeeeeeeeee net http://formmmmi=hhaaaaaa jo
14

---

Published as a conference paper at ICLR 2024
A THEORETICAL GUARANTEES OF PROFIT
A.1 PROOF OF SUFFICIENCY OF THE EXTRACTED PROOF FEATURE SET
Theorem 1. If the verifier V can prove the property (é, v) on the network N, then Fs, computed by Algorithm sufficient (Definition)
Proof. Proof theorem by induction on the number of steps of the while loop.
Induction Hypothesis: At each step of the loop, Fs, U Fss is sufficient. Base Case: At step 0, i.c., at initialization, Fs, = and F'g = F. So, Fs. Fs F. Given that V proves the property (di vb) N, from Definition F is sufficient. Induction Case: Let Fs, U F3 be sufficient for n-th step of the loop. Consider the following cases for (n + 1) step of the loop.
1. Let Fs. Fs, be sufficient at line 12. this case, Fs is updated by Fs, (line 14). So, Fs, U Fs is sufficient.
2. Let Fso U Fs, be not sufficient line 12. this case, Fs. and Fs are updated as in lines 16 and 17. Let the new Fs. and Fs be F's, and F'g. So, F = Fs. U Fs. and F's Fs.. So, F's. UF's Fs. U Fs, U Fs.- Also, Es, U Fs, = Fs. So, Fs, U F = Fso U Fs. So, from induction hypothesis, F's, F is sufficient.
A.2 UPPER BOUND ON THE SIZE OF THE EXTRACTED PROOF FEATURE SET
Lemma 1. AS S dd-1) if S then (A(A(W,,)) - A(A(W, (()))
max [(C XEA: 1
()) xzl. For any vector X R Dz RR denotes its i-th coordinate.
Proof. Without loss of generality let assume, A(A(W,,S)) S A(A(W,, \ (i))). Suppose, A(A(W,,)) = C² (S)) where Xmin E A
A(A(W,, S)) S A(AWW, S\ (i))) CT CT) I A(A(W,, S\ (()) & CT (1)) AAAAWW) S)) - A(A(W, S\ (()) (CTWi(S) A(A(W, S\ (())) S WC)TW((S) - CT (())X (1))Xman
S max XEAL1
(C(TW((;) mil
Lemma 2. VFs F.F A(Fs) E Pur(Fa.) where Pus(Fa.) is defined in equation 3 and Fn,EFIFs
A(Fs) (A(A) - A(A(WI, For any vector X dR Dy B. denotes its i-th coordinate.
15

---

Published as a conference paper at ICLR 2024
Proof.
A(Fs) IA(A) A(A(WW,
Σ (C ()) æ.l
MAN
XEALI
EFFEFIEE
Σ
1(C (l) zzl
max XEA:
EF
Σ
1(C 8) Fzl
max XEAL-1
FF
Σ (n)(F
From equation 3
Lemma 3. A feature set Fs C F with A(Fs) S A(A) is sufficient provided A(A) 2 0 where
(FFs) = A(A) A(A(W,,)))
Proof. (FFs) IA(A) - MA(WW, So, there can be two cases:
A(A(W,, S)) = A(A) + A(Fs). Since, A(A) 2 and A(Fs) 2 0. A(A(W, S)) 2
So. Fs is sufficient.
2. A(A(W,, = A(4) A(Fs)
A(Fs) < A(A).
So, A(A(WI,S)) 2 0. So, Fs is sufficient.
Lemma Let, Pmox denote the maximum of all priorities (F.( over If S F and
FF S A(A) Pmnc ), then proof feature set F = F Fs is sufficient provided A(A) 2 0.
Proof.
VJ,, E F, Pub(Fr.)) S Pmaz
From Lemma 2
A(FS) I [Fs Pmaz
A(A)
Also, [Fs < P Pmax
So, A (FF)) < A(A)
From Lemma
Fg is sufficient.
Definition 4. Zero proof features set Z(F) denotes the proof features Fr; E F with Put Theorem 2. Let, Pmez denote the maximum of all priorities Pws (Fn,) over F. Given any network N is verified on (Ø, v) with verifier V then Fsal < di- - [Z(F) - A(A)
Pmer
The algorithm arranges the elements of the proof feature set F decreasing order according to the priority defined by P.b. Let F' be the ordered set corresponding to F. So. F Frg concatenation.
Proof of theorem] 2
Frmm where :: is the list
The elements Z(F) will be at the end this ordering. So, F can be written as F" :: Z(F) where Z(F) Fres1 F a... and F" Fry " F ny and p be some of the last elements of F"
16

---

Published as a conference paper at ICLR 2024
s.t. the sum of their priorities just less than
A(A)
maax i.e.,
p Jng :: :: Fr,, such that
k
(F. - A(A)
Σ
(us A(A)
i=--1
Further, let p' p: Z(F), ie.. p/ Fng ::.::: Frm
Since Pub is 0 for all elements of ((F),
A(A) Pmnax
Σ (us(Fri) S
(I)
Also, in this case, lp|
AGA) and [p'| lpl + |2(F)
Pmap
We show that FFs _ d Ip'| which implies Fsol I di-1 -
AGA) Pmas
[Z(F))
Now, we prove by induction on the number of steps of the while loop in the algorithm that the set Fs. never contains any elements from p' which implies Induction Hypothesis: Fs. np' = =
Fss. S d Ip'l.
Base Case: At initialization, Fs, (.. So, the induction hypothesis holds trivially. Induction Step: Let the induction hypothesis be true for the n-th step of the algorithm I For the (n 1) step, let the new Fs, and F's be F's, and F'g respectively. Consider the following two cases:
1. Let Fs, Fs, be sufficient line 12. In this case, F Fs. So, the induction hypothesis holds.
2. Let Fs. U Es, not sufficient at line 12.
Claim: Fs, np' 0
Let the above claim be false.
Op' + 0 (Fs. U C'''
Σ
Pub
A(A) < < Pmax
[From (1))
FriEF((Fs, ((Fs. UFs,)
(Fs, U.F. UFs,, is sufficient. (From Lemma 4
Contradiction.
So, Fs, Ng = 0. In this step, F',, Fs, U Es, Also, from induction hypothesis, Fs, Op' (). Therefore, the induction hypothesis holds, i.e., Fss, Op 0-
17

---

Published as a conference paper at ICLR 2024
B VISUALIZATION FOR NON-DIFFERENTIABLE VERIFIER
For non-differentiable verifiers (Ktzz et al. 2017 we adapt the existing local visualization techniques (Sndararaaaa et al. 2017 Smilkov al. 2017) for visualizing the extracted proof features with a sampling-based statistical estimation method. Given proof feature Fn,, we intend to compute ((. Φ) = Ex- (n,, X) which is the mean gradient of the output n, w.r.t the inputs from 6. For each input dimension (pixel in case of images) j E [do] the j-th component of ([Fn.. Φ) estimates its relevance w.r.f proof feature Fu, with higher gradient values representing higher relevance. Given that the input region ø contains infinitely many inputs, instead of exactly computing g[Fn,: () we statistically estimate by a reasonably large sample drawn uniformly from Φ.
C ADDITIONAL EXPERIMENTS
C.I DISTRIBUTION PLOTS OF THE SIZE OF THE EXTRACTED SUFFICIENT PROOF FEATURE SET
In this section, show plots for the distribution of the sufficient proof feature set size extracted by ProFIt and two baseline methods based on random and gradient- priority heuristics. In the following histograms, the x-axis represents the size of the extracted proof feature set and the y-axis represents the number of local robustness properties. The results show that ProFIt consistently outperforms both the baselines and extracts sufficient proof feature sets that are smaller in size. All the plots in this section are generated on 500 local robustness properties with a-Crown verifier.
Random
Gradient
ProFit
Number of Proofs
200
Number of Proofs
200
40
150
150
30
of
100
100
20
10
50
0
04
0
15
30
45
60
75
10
20
30
40
50
5
10
15
20
25
Proof Feature Count
Proof Feature Count
Proof Feature Count
(a) Random
(b) Gradient
(c) ProFIt
Figure 4: Distribution of the extracted proof feature set size
Standard MNIST network & 0.02.
Random
Gradient
ProFit
250
300
50
Number of Proofs
Number Proofs
Number Proofs
250
150
200
150
20
100
10
50
140
100
Proof Feature Count
Proof Feature Count
Proof Feature Count
(a) Random
(b) Gradient
(c) ProFIt
Figure 5: Distribution of the extracted proof feature set size PGD MNIST network & c = 0.02.
18

---

Published as a conference paper at ICLR 2024
Random
Gradient
ProFit
200
250
Number of Proofs
Number of Proofs
Number of Proofs
200
30
150
20
100
100
10
50
50
0
10 15 20
25
30 35 40
5
10
15
20
25
30
35
0
5
10
15
20
25
30
Proof Feature Count
Proof Feature Count
Proof Feature Count
(a) Random
(b) Gradient
(c) ProFlt
Figure 6: Distribution of the extracted proof feature set size Colt MNIST network & 0.02.
Random
Gradient
ProFit
100
125
Number of Proofs
60
Number of Proofs
80
Number Proofs
100
60
20
25
10
20
25
5
10
15
Proof
Proof Feature
Proof
(a) Random
(b) Gradient
(c) ProFIt
Figure 7: Distribution of the extracted proof feature set size Crown-IBP MNIST network & e 0.02.
Random
Gradient
ProFit
15.0
80
Number of Proofs
12.5
Number Proofs
60
7.5
Number
40
5.0
40
20
170
100
Proot Feature Count
Proof Feature Count
Proof Feature Count
(a) Random
(b) Gradient
(c) ProFIt
Figure 8: Distribution of the extracted proof feature set size PGD MNIST network & c = 0.1.
19

---

Published as a conference paper at ICLR 2024
Random
Gradient
ProFit
60
20
50
Number of Proofs
Number of Proofs
15
60
10
Number
40
20
10
20
30
40
50
10
20
30
40
50
12
15
Proof Feature Count
Proof Feature Count
Proof Feature Count
(a) Random
(b) Gradient
(c) ProFIt
Figure 9: Distribution of the extracted proof feature set size
Colt MNIST network & 0.1.
Random
Gradient
ProFit
Number of Proofs
50
Number Proofs
80
Number Proofs
40
30
40
20
20
20
10
20
25
Proof Feature Count
Proof Feature Count
Proof Feature Count
Random
(b) Gradient
(c) ProFIt
Figure 10: Distribution of the extracted proof feature set size 0.1.
Crown-IBP MNIST network &
Random
Gradient
ProFit
50
Number of Proofs
15
Proofs
40
Number Proats
10
20
5-
10
20
12
36
48
0
22
44
Proof Feature Count
Proof Feature Count
Proof Feature Count
Random
(b) Gradient
(c) ProFIt
Figure 11: Distribution the extracted proof feature set size Standard Cifar- 10 network & 0.2/255.
20

---

Published as a conference paper at ICLR 2024
Random
Gradient
ProFit
60
Number of Proofs
Number of Proofs
100
80
10
Number
5-
20
10
20
12
24
60
22
33
44
55
18
27
36
45
Proof Feature Count
Proof Feature Count
Proof Feature Count
(a) Random
(b) Gradient
(c) ProFIt
Figure 12: Distribution of the extracted proof feature set size PGD Cifar- 10 network e 0.2/255.
Random
Gradient
ProFit
30
25
50
Number of Proofs
Number Proofs
Number of Proofs
20
40
100
15
30
10
25
17
34
68
85
14
28
56
70
12
24
36
Proof Feature Count
Proof Feature Count
Proof Feature Count
(a) Random
(b) Gradient
(c) ProFIt
Figure 13: Distribution of the extracted proof feature set size Colt Cifar- 10 network e = 0.2/255.
Random
Gradient
ProFit
Number of Proofs
60
Number Proofs
Number Proats
40
30
20
20.
10
10
15
20
5
10
15
20
25
Proof Feature Count
Proof Feature Count
Proof Feature Count
Random
(b) Gradient
(c) ProFIt
Figure 14: Distribution of the extracted proof feature set size 0.2/255.
Crown-IBP Cifar- 10 network &
21

---

Published as a conference paper at ICLR 2024
Random
Gradient
ProFit
12.
Number of Proofs
10
Number Proofs
25
Number of Proofs
20
15
10
20
2-
14
28
56
70
14
28
56
70
16
24
32
40
Proof Feature Count
Proof Feature Count
Proof Feature Count
(a) Random
(b) Gradient
(c) ProFIt
Figure 15: Distribution of the extracted proof feature set size
PGD Cifar- 10 network & 2/255.
Random
Gradient
ProFit
30
100
Number of Proofs
Number Proefs
80
20
15
Number
10
5-
20
19
76
17
34
68
48
60
Count
Proof
(a) Random
(b) Gradient
ProFIt (c)
Figure 16: Distribution of the extracted proof feature set size Colt Cifar-10 10 network & 2/255.
Random
Gradient
ProFit
30
50
Number of Proofs
25
Number Proofs
Number Proofs
20
20
15
10
Proof Feature Count
Proof Feature Count
Proof Feature Count
(a) Random
(b) Gradient
(c) ProFIt
Figure 17: Distribution of the extracted proof feature set size Crown-IBP Cifar- 10 network &
2/255.
22

---

Published as a conference paper at ICLR 2024
C.2 ADDITIONAL PLOTS FOR PRIORITY ORDER EVALUATION
In this section, we evaluate the efficacy of the priority ordering of proof features defined in Eq. against the random and gradient-based priority ordering Cifar-10 networks and the standard MNIST network. We use
0.2/255 for all Cifar-10 networks and = 0.02 for the standard MNIST network. We show that the priority ordering used by ProFIt preserves higher % of proofs while better approximating the original verifier output i.c. achieving a lower relative change compared both the baselines. All the plots in this section generated on 500 local properties with a- e-Crown verifier.
poodf
No. of Proof features
No. Proof features
No. of Proot features
(a) PGD Network
(b) Colt Network
(c) Crown-IBP Network
Figure 18: Percentages of proofs preserved by different heuristics on robust CIFAR-10 networks.
Profit Random Craedant
RifFtt
Rifft
Retotive change 0.220
Randam Cracleerr
Randam Cradlerr
(b) Colt Network Figure 19: Relative change in verifier output with different heuristics on robust CIFAR-10 10 networks.
(a) PGD Network
(c) Crown-IBP Network
23

---

Published as a conference paper at ICLR 2024
% of proof preserved
% of proof preserved
70
60
80
hefft
Prott
20
10
No. of Proof features
No. of Proof features
Standard MNIST Network
(h) Standard CIFAR-10 Network
Figure 20: Percentages proofs preserved by different heuristics on standard networks.
2.0
5.5
Peft Grudect
Pott
Relative change in coupppt
output
Gradien
4.4
2.5
0.
14
No. of Proof features
No. of Proof features
Standard MNIST Network
(b) Standard CIFAR-10 Network
Figure 21: Relative change in verifier output with different hcuristics on standard networks.
24

---

Published as a conference paper at ICLR 2024
C.3
QUALITATIVE EVALUATION OF THE PRIORITY ORDERING OF THE PROOF FEATURES
Retained Features
Retained Features
Pruned Features
Pruned Features
Image
7
7
4
4
3
5
Figure 22: Comparing gradients of the top proof features retained by the ProFIt algorithm to pruned proof features with a low priority. The columns are sorted decreasing order of priority with the right-most proof feature having the lowest priority. As expected, proof features with low priority are noisier (as column 4). The proof features which are further down in the priority order do not give any relevant information about the input (column 5 completely white). This shows that the proposed algorithm extracts proof features that are important to the proof while removing insignificant and uninformative proof features. The shown gradients are computed COLT-trained MNIST network.
25

---

Published as a conference paper at ICLR 2024
C.4
ADDITIONAL PLOTS FOR THE TOP PROOF FEATURE VISUALIZATION
Standard
PGD
COLT
Standard
CROWN
4
6
3
5
(a) Gradient maps generated on MNIST networks (b) Gradient maps generated on CIFAR-IE networks
Figure 23: Additional plots for the top proof feature visualization (in addition to Fig. Visualization of gradient map top proof feature (having highest priority) generated for networks trained with different training methods. It is evident that the top proof feature corresponding to the standard network highlights both relevant and spurious input features. In contrast, the top proof feature of the provably robust network does filter out the spurious imput features, but it comes at the expanse of some important input features. The top proof features of the networks trained with PGD filter more spurious features as compared to standard networks. Finally, the top proof features of the networks trained with COLT filter out the spurious input features and also correctly highlight the relevant input features.
26

---

Published as a conference paper at ICLR 2024
C.5
VISUALIZATION OF THE ENTIRE EXTRACTED PROOF FEATURE SET
PED
CROWN IBF
7
7
(a) Gradient maps generated on MNIST networks
(b) Gradient maps generated on CIFAR- 10 networks
Figure 24: Visualization of gradient maps of entire proof features set consisting of 4 proof features extracted for networks trained with different robust training methods. The gradient maps of the proof features are presented in decreasing order of priority with the top row showing the gradient map corresponding to the top proof feature each network.
Image
Image
7
7
7
7
7
(a) Gradient maps generated on MNIST networks
(b) Gradient maps generated on CIFAR- -0 networks
Figure 25: Visualization of gradient maps of entire proof features consisting of proof features extracted for networks trained with different robust training methods. The gradient maps of the proof features are presented decreasing order of priority with the top row showing the gradient map corresponding to the top proof feature of each network.
27

---

Published as a conference paper at ICLR 2024
C.6
VISUALIZATION OF THE TOP PROOF FEATURE FOR HIGHER VALUES
PED
CROWN
COUT
CROWN IBF
S
5
S
2
6
(a) Gradient maps generated on MNIST networks
(b) Gradient maps generated CIFAR- networks
Figure 26: Visualization of gradient map of top proof feature (having highest priority) generated for networks trained with different robust training methods. For these networks, we define local properties with higher values. For MNIST networks and CIFAR-IO networks, we take 0.1 and = 2/255 respectively.
28

---

Published as a conference paper at ICLR 2024
C.7 COMPARING THE PROOF FEATURES EXTRACTED BY DIFFERENT VERIFIERS
As described earlier, the extracted proof features are specific to the proof generated by particular verifier. In this section, we examine whether the proof features corresponding generated by different verifiers are the same. In Table we compare the top proof features (ordered by the priority order described in Eq. of the proofs generated by the DeepZ Singh al. (2018a) verifier and a- a-Crown verifier. We observed that more than 97% of the cases the top feature remains the same. In this case, for different verifiers though the proof features F.; [Z,, un,,] change, their relative priority ordering computed by Eq. 3 remains the same. For this experiment, we use 500 local robustness properties for each network and each value. Note, while comparing proof features from two different verifiers we only consider those properties that can be proved by both the verifiers.
different proofs
Daraset
Training Method
Ingut Region (6)
% properties proved by DeepZ
% properties proved by Crown
pronfs with the sume top feature
proofs with the sume top-5 5 feature
f6 proods with the same top- feature
eps (c)
MNIST
Standard
0.02
90.0%
91.8 %
99.8 46
98.4 %
98.3 %
PGD Trained
0,02
82.0
83.0 %
99.75
99.0 4
98.0 %
COLT
99.50
CROWN-IBP
0.02
96.4 %
96.4 %
99.8
99.0
95.9 %
MNIST
PGD Trained
0.1
32.6
38.2 %
99.38 46
95.7 46
91.41 %
COLT
0,1
43.0
56.2 %
98.6
93.95
$7.90 %
CROWN-IBP
0.1
CO
Standard
0.2/555
51.0%
58.0 %
99.5
98.3 %
98.0 %
PGD Trained
0.2/255
47.0%
62.5 9
99.7 4g
98.5 %
97.8 %
COLT
0,2/255
53.0%
53.0 %
100.0
99.5 4
98.2 %
CROWN-IBP
0.2/255
98.90
CI
PGD Trained
2/255
26.5 %
32.5 %
99.7
95.45
92.45
COLT
2/255
45.5 %
46.0 96
99.8 46
98.9 46
97,3 %
CROWN-IBP
2/255
37.5%
38.0 %
99.6 %
97.92
95.89 %
Table 2: Comparing extracted proof features of Deep7. & a-Crown
Next, in Table 3 we compare the top proof feature (having the highest priority) corresponding to the proofs generated by DeepZ, Crown (Zhang et al. 2018), a-Crown and faate-of-the-aa complete verifier a, 3-Crown (Wang al. 202 the property. We use PGD and Colt MNIST network for
this experiment. We evaluate 200 local robustness properties defined with e = 0.02. We observed that for these two networks, more than 99% of the cases the top feature remains the same.
Verifier
DeepZ
Crown
a-Crown
8-Crown
Verifier
DeepZ
Crown
o-Crown
3-Coow
DeepZ
100.0 %
99.55 %
99.75 %
99.50 %
DeepZ
100.0 %
99.50 %
99.50 %
99:40 %
Crown
99.55 %
100.0
%
Crown
99.50
100.0
100.0
99.70
a-Crown
99.75 %
99.80 %
100.0 %
99.80 %
a-Crown
99.50
100.0 %
100,0 %
99.70 %
a, 9-Crown
99.50 %
99.60 %
99.80 %
100.0 %
a, B.B-Crown
99.40
99.70 %
99.70
100.0 %
(a) PGD MNIST Network Table 3: % cases different verifiers have the same top proof feature
(b) Colt MNIST Network
29

---

Published as a conference paper at ICLR 2024
C.8 COMPARING VISUALIZATION OF THE PROOF FEATURES EXTRACTED DIFFERENT DIFFERENTIABLE VERIFIERS
Image
Standard
CROWN
2
2
7
6
6
(a) Gradient maps generated with CROWN
(b) Gradient maps generated with a-CROWN
Figure 27: Visualization of gradient map of top proof feature extracted by two different differentiable verifiers CROWN and a-CROWN. In both cases, the visualizations align with the observations in section 5.3
30

---

Published as a conference paper at ICLR 2024
C.9
COMPARING PROOFS ON NETWORKS WITH SAME ARCHITECTURE
Image
Standard
COLT
CROWN-IBP
7
7
2
?
0
5
L
Figure 28: Gradient maps generated on MNIST networks trained with different training methods (Standard, COLT, CROWN-IBP) with the same architecture. The gradient maps show that obser- vations in Section 5.3 and in Figure 3 of the paper also hold on different networks with the same architecture.
31

---

Published as a conference paper at ICLR 2024
C.10
PLOTS FOR SENSITIVITY ANALYSIS W.R.T Ctrain
Image
PGD (0.1)
(0.3)
COU (0.1)
COU (0.3)
5
4
2
Figure 29: Plots for visualizing gradients of the top proof feature for PGD and COLT networks trained using different values of éxrain E {0.1, 0.3) The gradient map corresponding to the networks trained with the higher value of Etrain filter out more input features than the ones trained with smaller Etrasn value.
32

---

Published as a conference paper at ICLR 2024
C.11 PLOTS FOR THE TOP PROOF FEATURE VISUALIZATION OF SABR NETWORKS
Imge
2
6
di
(a) Gradient maps generated on MNIST networks (b) Gradient maps generated on CIFAR-10 networks
Figure 30: Visualization of gradient maps of the top proof feature (having highest priority) generated for networks including those trained with recent state-of-the-art training method SABR (Mueller et al. 2023). For the SABR CIFARIO network, the gradient map the top feature highlights semantically meaningful features while successfully removing spurious background pixels. However, for the SABR MNIST network, the gradient map of the top proof feature is not human-aligned. This is potentially because the SABR MNIST networks are over-regularized to achieve high robust accuracy.
D WORST-CASE RUNTIME ANALYSIS OF PROFIT
In this section, We provide formal worst-case analysis of the ProFIt.
Theorem 3. If the size of the penultimate layer is di-1 then the number of incremental verifier calls made by Proflt is always S d:-] 1.
Proof. Every iteration of the while loop (Algorithm 1 on page of the paper) makes single incremental verifier call. So, first, we calculate the maximum number of incremental verifier calls made in the while loop. At the end of each iteration F3 is replaced by either Fs, (line 14 of Algorithm or Fs, (line 17 of Algorithm the cardinality of set. Initially, Fs = F and Fs while loop the following inequality holds Fss S iterations of the while loop. Given the while loop only executes when F3 is non-empty (line 9 of Algorithm 1), 1 1 E/=1
Now, max Fs Fs,1)
denotes = F d Then after ith iteration of the di-1 Σ}=1 Let, denote the total number of 2'
< (( + 1)/2 where
() < [logdi-1] = [log di-1l 1.
Hence, the total number of incremental verifier calls is always S [log d--1 + Note, since we only modify the final layer we run incremental verification that avoids rerunning verification on the entire network from scratch. However, computing proof features (line of Algorithm 1) requires a single verifier call which can not be run incrementally.
For network with n neurons and layers a single incremental DeepZ (Singh et al. 2018a Sa) verifier call in the worst case takes (nz²) time whereas single call to incremental CROWN (hang et al. 2018) verifier in the worst case takes O n²3) time. The cost for a single non con-incrementll DeepZ verifier call is in the worst case Oll x n² whereas for CROWN it is O(12 x n²²). Overall, the complexity of ProFIt with CROWN is O(log di-1 + 1) x l n²). We will update our paper with detailed proof of the worst-case runtime of ProFlt.
33

---

Published as a conference paper at ICLR 2024
Dataset
Netwock
Training
LLayers
Params Theorctical Bocand
Avg. Veriller calls
Arg. CPU time
Avg. GPU time
MNIST
ConeSmall
Standard
90K
7.81
0.85s
0.14s
ConeSmall
COLT
90K
7:25
0.39%
0.114
IBP Small
CROWN-IBP
SOK
6.99
0.34s
0.09s
ConeRig
7.12
2.57%
ConeSuper
DiTAI
10M
11
7.08
6.28%
0.30s
CIEARIO
ConeSmall
Standard
5.36
0.30s
0.07s
ConsSmall
PGD
120K
6.04
0.32s
0.09%
ConeSmall
COLT
120K
10
5.64
0.52s
0.155
IBP-Small
CROWN-IB
0,48%
ConvBig
DITAI
2.5M
11
7.8
3.93s
0.50s
Table 4: ProFIt Runtime Analysis
E EXPERIMENTAL RESULTS ON PROFIT RUNTIME
E.1 EXPERIMENT SETUP
We run ProFIt on multiple networks including those mentioned in Table both CPUs and GPUs. For CPU-related experiments, we use the same setup mentioned in Section 5.1 In GPU-related experiments, we utilize single NVIDIA A100-PCI GPU with 40 GB RAM. We use the state-of-the- art incomplete verifier e-CROWN from auto-LiRPA (Xu et al. (2020) toolbox and show results for 100 local Los robustness properties. As done in the paper, for MNIST and CIFARIO networks, we 0.02 and 0.2/255 respectively define Loe input regions.
E.2 SIZE AND ARCHITECTURE OF THE NETWORKS:
We present the runtime analysis of ProFIt on the DNNs used in Table and also showcase results on some of the largest verifiable network architectures, namely DiffAi trained (Mirman al. 2018) ConvBig and ConvSuper. These architectures are de facto benchmarks employed for testing the scalability of state-of-the-arr verifiers (Ferrari et al. 2022b Müller et al. (022) and are featured in the International Verification of Neural Networks Competition (Brix et al. (023). All the networks used this experiment are selected from ERAN (Singh et al.) (019b), and CROWN-IBP (Zhang et al. 2020) repositories and belong to the category of convolutional neural networks (CNNs).
E.3
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 auto-LiRPA (Xu et al. 2020). We show the runtime improvement of ProFIt with GPUs below. Runtimes on GPUs are up to 20x shorter than those on CPUs.
E.4 EXPERIMENTAL RESULTS:
We present results for all networks in Table Column shows the dataset, column 2 displays the network name, column 3 outlines the training method, and columns and describe the network's structure. Column 6 indicates the worst-case bound the number of incremental verifier calls, as described in Theorem 3 while column 7 displays the average number of incremental verifier calls per property. Columns 8 and present the average runtime seconds for ProFIt on CPU and GPU, respectively. Notably, on GPUs, the average runtime for ProFIt is less than second for all the networks. Note that, for Conv architectures, the timeout used in the International Verification of Neural Networks Competition (Brix et al.] 2023) is in minutes. In comparison, ProFIt with a-CROWN significantly faster.
34


Reviews:
[{"review_id": "UvJ1C0VZPf", "reviewer": "Reviewer_rPr5", "summary": "This paper aims to analyze the robustness proof generated by a DNN verifier. Given a neural network and a DNN verifier (deterministic, sound, and incomplete verifiers, such as DeepZ and CROWN), the paper presents an algorithm ProFlt to extract a set of proof features (defined as the reachable interval of neurons in the penultimate layer) that is small, sufficient, and retains important proof features. Based on the top-proof feature extracted using the proposed algorithm, the paper then visualizes the gradient maps for different neural networks and DNN verifiers and explains why they differ.", "questions": "1. What is the computational complexity of the proposed _ProFit_ algorithm and the reliance on the dependent factors? \n\n2. The gradient map visualizations shown in Figure 3 seem interesting. Still, I do not understand the corresponding explanations: \"CROWN-IBP filters out most of the spurious features, but it also misses out on some meaningful features.\" 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?\n\n3. How can the extracted top proof features benefit the development of better DNN verifiers or robust training methods?\n\n\n============== Post Rebuttal Comments ==============\n\nI appreciate the authors' feedback and additional experimental results. I would be interested to see how ProFIt analysis can contribute to building more robust DNNs.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "The paper is well-structured and technically solid. To the best of my knowledge, most existing works focus on debugging neural networks and explaining how they make predictions. In contrast, this paper proposes to identify the most influential proof features for a DNN verifier, which is different and new. I also like how the paper presents the problem formulation for proof dissection, where the three expectations are discussed in great detail. The proposed ProFit algorithm and how it approximates the priority of proof features are well-explained.", "weaknesses": "While I most enjoyed reading the paper, the significance of generating human-understandable proof features and the user case of the extracted proof features need to be explained more clearly. A DNN verifier is supposed to provide a mathematically sound robustness certificate, so by design, it gives a result that can be trusted. However, this paper aims to identify important/human-understandable proof features that can explain how the DNN verifier works, so I wonder why we need a DNN verifier to be explainable in the first place. The following question is: after we obtain the top proof feature (e.g., the one returned by your algorithm), how can we use the extracted insight to assist the DNN verification procedure or the development of adversarially robust models? \n\nWithin the proposed problem formulation, the paper did quite a good job explaining the relevant concepts of proof features and developing a well-motivated algorithm to prioritize the proof features. I hope that the authors can better explain the underlying motivation of the considered problem.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "6Nb0wtuwnJ", "reviewer": "Reviewer_zRr5", "summary": "This paper proposes to verify the robustness of neural classifiers by finding the \"robust features\" via pruning the penultimate layer features based on their \"priority\". The resulting \"ProFIt\" algorithm guarantees sufficiency and reduces the number of proof features required to certify an area around the input, reducing the complexity of the certificate. The authors also show that high-priority robust features can visualize the neural classifier attention and use such a property to compare various robust models.", "questions": "- Is the certificate issued by ProFIt related to the robust accuracy in any way? My impression after reading the paper is that since $\\it{F}_{S_0}$ returned by Algorithm 1 is always sufficient, the percentage of data that can be certified will be the same as the verifier $\\mathcal{V}$. Is this correct?\n- I see that the experiments and calculations are performed using a CPU. Is the proposed algorithm also compatible with GPU acceleration?", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "The paper proposes a theoretically-inspired heuristic algorithm that seems to work as expected. The algorithm provides improved interpretability to the robust verification problem. Furthermore, the qualitative comparisons are constructive. The paper is generally well-structured, the notations are mostly well-defined, and the experiment results are clearly presented. The proposed algorithm is general and is compatible with existing certification methods.", "weaknesses": "- I find the motivation of this work to be a little ambiguous. Specifically, the author argues that the challenge this work aims to address here is \"investigating the entire set $\\mathcal{F}$ is always a valid but expensive option considering the size of $\\mathcal{F}$\". However, Algorithm 1 needs to iteratively query the verifier on subsets of $\\mathcal{F}$, with the subset in the first couple of iterations potentially quite large. Particularly, at the first iteration, the cardinality of $F_{S_0} \\cup F_{S_1}$ seems to be half of $\\mathcal{F}$. Therefore, it is not immediately clear to me how the proposed algorithm reduces the overall computational complexity, and some additional explanation would be preferred.\n- While the visualizations in Figure 3 are nice, it would be helpful and more meaningful if they could be generated from commonly used model architectures, as ConvNets and vision transformers may attend to different parts of the input image compared with the feed-forward networks used in this paper. Are there any challenges for applying the proposed methods to these more sophisticated networks, since these models usually also have a linear layer as the final layer? I believe that this paper will benefit from a more diverse empirical evaluation.\n- Some typos: \"uppper\" on page 5; \"both the baselines\" on page 8.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Ng3R6B4lZN", "reviewer": "Reviewer_YfNd", "summary": "The authors consider the problem of making proofs of neural network robustness more human understandable. In particular, the authors consider recent verification methods developed for computing neural networks robustness and extract proof features from these methods by analysing the ranges of the outputs of each neuron at the penultimate layer. Then, they proceed by finding a small subset of these features that are sufficient to explain the verification result. The authors show the effectiveness of their results on experiments on the MNIST and CIFAR datasets.", "questions": "- Can the method also be applied to other certification methods such as randomised smoothing [Cohen, Jeremy, Elan Rosenfeld, and Zico Kolter. \"Certified adversarial robustness via randomized smoothing.\" international conference on machine learning. PMLR, 2019.]?", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- The paper is well written\n\n- The problem of analysing and explain the decisions of the various methods developed to verify neural networks is of interest to the ICLR community and to the best of my knowledge novel\n\n- The algorithm is sound and experimental results seem to show improvement compared to state of the art", "weaknesses": "- The experimental setting is not totally clear to me: \n\n1) how is the original feature count in Table 1 computed? Should not this be just the size of the penultimate layer? Also why is this 10 times larger for PGD trained networks on MNIST compared to PGD trained networks on CIFAR? \n\n2) As ProFIt has a  subroutine that needs to check for sufficiency of a feature set, It would be good to perform experiment to analyse the scalability of the proposed method on various architectures for the various robustness methods considered in the paper (and to report computation times).\n\n- The computational complexity of ProFIt should be discussed more clearly.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "S3osBQH70R", "reviewer": "Reviewer_UvmS", "summary": "This paper proposes the method ProFIt to extract a set of proof features by retaining only the more important parts of the proof that preserves the property and then conducts experiments to explore the selected features for standard trained / adversarial trained / certifiable trained neural networks.", "questions": "See the weaknesses.", "limitations": "", "rating": 6, "confidence": 3, "soundness": 3, "presentation": 2, "contribution": 2, "strengths": "- The proposed method is novel and theoretically guaranteed.\n- The experiments validate the sufficiency of the proposed method.", "weaknesses": "- The proposed algorithm seems only valid for the linear property, how can we deal with the nonlinear properties?\n- My main concern is the meaning of this task.\n  - The selected features are the most relevant to the predefined linear property. However, there are many other properties of a neural network, different properties lead to different sufficient proof features. So, the features selected by one property may only reflect one perspective of the neural network. Such a \"local\" interpretation may be misleading.\n  - Can sufficient proof features provide intuitions on how to design a training method to train a model with such a property? I think this need to be discussed.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (poster)