TOWARD RELIABLE NEURAL SPECIFICATIONS
Authors: Chuqin Geng
Nham Le
Xiaojie Xu
Zhaoyue Wang
Arie Gurfinkel
Xujie Si
Venue: Submitted to ICLR 2023 (2023)
Keywords: formal verification
specification
neural network verfication
trustworthy AI
interpretability

Abstract: Having reliable specifications is an unavoidable challenge in achieving verifiable correctness, robustness, and interpretability of AI systems. Existing specifications for neural networks are in the flavor of “data as specification”, that is, the local neighborhood centering around a reference input is considered to be correct (or robust). However, our empirical study shows that such specifications fail to certify any test data points, making it impractical for real-world applications. We propose a new family of specifications called “neural representation as specification”, which uses the intrinsic information of neural networks — neural activation patterns (NAP) rather than input data to specify the correctness and/or robustness of neural network predictions. We present a simple statistical approach to extracting dominant neural activation patterns. We analyze NAPs from a statistical point of view and find that a single NAP can cover a large number of training and testing data points whereas ad hoc data-as-specification can only cover a single training data point and often zero testing data points. To show the effectiveness of discovered NAPs, we formally verify several important properties, such as a particular type of misclassification never happens for a given NAP, and there is no ambiguity among different NAPs. We show that by using NAP, we can verify the prediction of the entire input space, while still recalling 84% of the data. Thus, we argue that using NAPs is a more reliable and extensible specification for neural network verification.

Under review as a conference paper at ICLR 2023
TOWARD RELIABLE NEURAL SPECIHICATIONS
Anonymous authors
Paper under double-blind review
ABSTRACT
Having reliable specifications is an unavoidable challenge in achieving verifiable correctness, robustness, and interpretability of AT systems. Existing specifications for neural networks are in the paradigm of data as specification. That is, the local neighborhood centering around reference input is considered be correct (or ro- bust). However, our empirical study shows that such a specification is extremely overfitted since usually no data points from the testing set lie in the certified region of the reference input, making them impractical for real-world applications. We propose a new family of specifications called neural representation as specifica- tion, which uses the intrinsic information of neural networks neural activation patterns (NAP), rather than input data to specify the correctness and/or robustness of neural network predictions. We present simple statistical approach to mining dominant neural activation patterns. We analyze NAPs from a statistical point view and find that a single NAP can cover large number of training and testing data points whereas ad hoc data-as sattaass-ppeiiication only covers the given reference data point. To show the effectiveness of discovered NAPs, we formally verify several important properties, such as various types of misclassifications will never happen for given NAP, and there is no-ambiguity between different NAPs. We show that by using NAP, we can verify the prediction of the entire input space, while still recalling 84% of the data. Thus, we argue that using NAPs more reliable and extensible specification for neural network verification.
INTRODUCTION
The advances in deep neural networks (DNNs) have brought wide societal impact in many domains such as transportation, healthcare, finance, e-commerce, and education. This growing societal-scale impact has also raised some risks and concerns about errors in AI software, their susceptibility to cyber-attacks, and AI system safety (Dietterich & Horvitz, 2015). Therefore, the challenge of verification and validation of Al systems, as well as, achieving trustworthy AI (Wing, 2021), has attracted much attention of the research community. Existing works approach this challenge by building on formal methods field of computer science and engineering that involves verifying properties of systems using rigorous mathematical specifications and proofs (Wing, 1990). Having formal specification - precise, mathematical statement of what Al system is supposed to do is critical for formal verification. Most works (Katz et al., 2017: 2019; Huang et al., 2017; 2020; Wang al.. 2021) use the specification of adversarial robustness for classification tasks that states that the NN correctly classifies an image as a given adversarial label under perturbations with a specific norm (usually (x)). Generally speaking, existing works use a paradigm of data as specification the robutness of local neighborhoods of reference data points with ground-truth labels is the only specification of correct behaviors. However, from a learning perspective, this would lead to overfitted specification, since only local neighborhoods of reference inputs get certified.
As concrete example, Figure 1 illustrates the fundamental limitation of such overfitted specifica- tions. Specificallyy, a testing input like the one shown in Fig. la can never be verified even if all local neighborhoods of all training images have been certified using the Loo norm. This is because adversarial examples like Fig. Ic fall into much closer region compared to testing inputs (e.g.. Fig. 1a), as a result, the truly verifiable region for a given reference input like Fig. 1b can only be smaller. All neural network verification approaches following such data-as sspeccifiiciin paradigm inherit this fundamental limitation regardless of their underlying verification techniques. In order to avoid such a limitation, new paradigm for specifying what is correct wrong is necessary.

---

Under review as a conference paper at ICLR 2023
(a) A testing image from (b) The closest training (c) An adversarial exam- (d) A testing image, on MNIST, classified 1
image MNIST, whose ple misclassified as 8, which Loe distance to Fig. la whose Loo distance to (for digit 1) disagrees with 0.5294
verified NAP
Fig. lb i.2
the ground truth (i.e., 7)
The limitation of coata-as-specificatii much further away (in Lx) from its closest train input compared to adversarial examples (the upper bound of verifiable local region). The last image shows that even data itself can be imperfect.
Figure I:
First three images show that test input can be
The intrinsic challenge is that manually giving a proper specification on the input space is no casier than directly programming solution to the machine learning problem itself. We envision that promising way to address this challenge is developing specifications directly on top of, instead of being agnostic the learned model.
We propose a new family of specifications, neural representation as specification, where neural activation patterns form specifications. The key observation is that inputs from the same class often share a dominant neural activation pattern (NAP) a carefully chosen sub-sets of neurons that are expected be activated (or not activated) for the majority of inputs. Although two inputs are distant in a certain norm in the input space, the neural activations exhibited when the same prediction is made are very close. For instance, we can find single dominant NAP that is shared by nearly all training and testing images (including Fig. la and Fig. 1b) in the same class but not the adversarial example like Fig. Ic. We can further formally verify that all possible inputs following this particular dominant NAP can never be misclassified. Specifications based on NAP enable successful verification of a broad region of inputs, which would not be possible if the date-as-specification paradigm were used. For the MNIST dataset, find that verifiable dominant NAP mined from the training images could cover up to 84% testing images, a significant improvement in contrast to 0% when using neighhorhoods of training images the specification. To our best knowledge, this is the first time that a significant fraction of unseen testing images have been formally verified. Interestingly, the verified dominant NAP also enables us to "double check" whether ground truth labels given by human beings are indeed reliable. Fig. 1d shows such an example on which our verified NAP disagrees with the ground truth. We have a tunable parameter specialize dominant NAP to avoid accepting such potentially controversial region of inputs when necessary.
This unique advantage of using NAPs as specification is enabled by the intrinsic information (or neural representation) embedded in the neural network model. Furthermore, such information is simple byproduct of a prediction and can be collected easily and efficiently. Besides serving as reliable specifications for neural networks, we foresee other important applications of NAPs. For instance, verified NAPs may serve as proofs of correctness or certificates for predictions. We hope our initial findings shared in this paper would inspire new interesting applications. We summarize our contribution as follows:
We propose a new family of formal specifications for neural networks, neural representa- tion as specification, which use activation patterns (NAPs) as specifications.
We propose simple yet effective method to mine dominant NAPs from neural networks and training dataset.
We show that NAPs be easily checked by out-of-the-box neural network verification tools used in VNNCOMP (2021) the latest neural network verification competition, such Marabou.
2

---

Under review as a conference paper at ICLR 2023
We conduct thorough experimental evaluations from both statistical and formal verification perspectives. Particularly, we show that a single dominant NAP sufficient for certifying significant fraction of unseen testing images.
2 BACKGROUND
2.1 NEURAL NETWORKS FOR CLASSIFICATION TASKS
In this paper, we focus on feed-forward neural networks for classification. A ford-forward neural network N of L layers a set {(W', b') < S L}. where W' and b' are the weight matrix and the bias for layer i, respectively. The neural network N defined function Fx 1R + gd (dg and dp represent the input and output dimension, respectively), defined as Fx((x) = (x).
wherez (z) = z, 2f (x) = W (z))
and a is the activation function. Neurons are indexed linearly by un, #1, ..... In this paper focus only the ReLU activation function, i.e., a(x) max(x, 0) element-wise, but the idea and techniques can be generalized for different activation functions and architectures as well. The jth element of the prediction vector Fx((x) [t] represents the score or likelihood for the jth label, and the one with the highest score (arg max; Py (v(r)) [i] is often considered as the predicted label of the network A. We denote this output label as (z)).. When the context is clear, we omit the subscript N for simplicity.
2.2 ADVERSARIAL ATTACKS AGAINST NEURAL NETWORKS AND THE ROBUSTNESS VERIFICATION PROBLEM
Given a neural network N, the aim of adversarial attacks is to find perturbation 8 of an input x, such that x and x + ô are "similar" according to some domain knowledge, yet O(x) 7 O(x + 8). In this paper, the Lx norm of is small. Under this formulation, finding an adversarial example can be defined solving the following optimization problem:
use the common formulation of "similarity" in the field: two inputs similar if
minl s.t O(x) + O(x +
In practice, it very hard to formally define "similar"" should an image and a crop of it "similar"" Should two sentences differ by one synonym the same? We refer curious readers to the survey (Xu et al., 2020) for a comprehensive review different formulations.
One natural defense against adversarial attacks, called robustness verification, is to prove that min || must be greater than some user-specified threshold e. Formally, given that O(x) = i, verify
Yal B(x, - Vj F(x) F(+)D) >0
where Bix, e) is a Los ball-ball of radius e centered at æ: B(x,e) = {ø' || - l' S t]. Eq. (1) holds, say that x is c-robust.
2.3 MARABOU
For this paper, we use Marabou (Katz et al., 2019), a dedicated state-of-the-art NN verifier. Marabou extends the Simplex (Nelder & Mead, 1965) algorithm for solving linear programming with special mechanisms to handle non-linear activation functions. Internally, Marabou encodes both the ver- ification problem and the adversarial attacks as system of linear constraints (the weighted sum and the properties) and non- mon-linear constraints (the activation functions). Same Simplex. at each iteration, Marabou tries to fix a variable so that doesn't 'ttt violate constraints. While in Simplex, violation can only happen due to variable becoming out-of-bound, in Marabou a violation can also happen when a variable doesn't satisfy activation constraints.
By focusing only neural networks with piecewise-linee linear activation functions, Marabou makes two insights: first, only a small subset of the activation nodes are relevant to the property under consider- ation. Hence, Marabou treats the non-linear constraints lazily and reduces the number of expensive
While there are alternative formulations of adversarial robustness (see Xu al. (2020),, in this paper, adversarial attacks black box, thus, stating one formulation is sufficient.
3

---

Under review as a conference paper at ICLR 2023
case-splits, making it much faster than traditional SMT solvers. Second, Marabou repeatedly refines each variable's s lower and upper bound, hoping that many piecewise-linear constraints can be turned into linear (chase-fied)), reducing further the need for case splitting. Altogether, Marabou achieves state-of-the-art performance on a wide range of benchmarks (VNNCOMP, 2021).
3 NEURAL ACTIVATION PATTERNS
In this section, we discuss in detail neural activation patterns (NAP), what we consider as dominant NAPs and how to relax them, and what interesting properties of neural activation patterns can be checked using Marabou.
3.1 NAPS, DOMINANT NAPS, RELAXED DOMINANT NAPS
In our setting (Section 2), the output of each neuron is passed to the ReLU function before going neurons of the next layer, i.e., =xxx) W (xx=)(((xx) + b¹. We abstract each neuron into two states; activated (if its output is positive) and deactivated (if its output is non-positive). Clearly, for any given input, each neuron can be either activated or deactivated, but not both.
Definition 3.1 (Neural Activation Pattern). A Neural Activation Pattern (NAP) of neural network N a pair Px == (A, D), where A and are two disjoint set of neurons.
We say that an input follows a NAP Pv if after computing Fx(xx), the neurons in A are all activated, and neurons in D are all deactivated. We denote this as Pv(()) = True. Note that A and D are not required to contain all activated and deactivated neurons, thus for a given / an input can follow multiple NAPs. Our intuition is that for some NAPs, all inputs following them should be classified correctly. We call such NAPs the dominant NAPs.
Definition 3.2 (Dominant NAP with respect to label f). Given label l and neural network N,, we define a dominant NAP with respect to - denoted p as
P/. = (A s.t Vo - O(x) = + Pk((1) = True
Note that x: is quantified over all the input space, not restricted to Toxe ball train test set. The dominant NAP certificate for the prediction: any input that follows (fx(()) must be classified as L by A. However, dominant NAPs very hard to find (as hard as verifying the robustness property for the whole imput space), or may not exist at all. Thus, we wish to relax the definition of dominant NAPs: First, instead of quantifying x over the input space, we limit x to dataset. Second, we break the strong < condition, keeping only the condition ((r) = L we relax the implication even further, by allowing neuron to be added to the NAP even when is
(x((x) = True. Finally,
not activated/deactivate in all inputs of the same label. We call this relaxed version the d-relaxed dominant NAP.
Definition 3.3 (8-relaxed dominant NAP). Let S be the dataset, and Se be the of data labeled as l. Clearly VL, S₁ S 5 and U. S; = S. We introduce a relaxing factor 5 E [0, 1]. A d-relaxed dominant NAP for the label ( denoted 8.P is defined through construction (mining)
1. Initialize two counters 0g and dę for each neuron Uk-
2. Vz E St, compute (x), let ag += uk is activated; let de += if un deactivated.
3. A + {uk
2 5) D + {ox
de ST 2 1 1--0 5}
|
4. 6.P DC)
Intuitively, for each neuron, we ask: how often is this neuron activated/deactivated upon seeing inputs from a label I. controls how precise we want to be: should we add a neuron to our NAP only if is activated in all the inputs labeled f, 95% of the inputs is enough? Thus, as â increases, we expect the size of NAPs also to increase. Choosing the right has a huge impact on how useful the relaxed dominant NAPs can be. Table gives some intuition why. For MNIST, the table shows how many test images from a label l follow 8.Pº, together with how many test images from other labels that also follow the same 8.pt. For example, there 980 images in the test set with
4

---

Under review as a conference paper at ICLR 2023
Table 1: The number of the test images MNIST that follow a given 6.NAP. For a label i, i represents images with labels other than yet follow 8.NAP'. The leftmost column is the values of 5. The top row indicates how many images in the test set are of label.
(980)
(1135)
(1032)
(1010)
(987)
(892)
(958)
(1028)
(974)
(1009)
997
32
0:01
775
959
792
767
766
3
677
726
4
800
696
3
828
0:05
261
259
277
0.10
92
144
label (second column). Among them, 967 images follow 0.P0. In addition to that, there are 20 images from the other 9 labels that also follow 0.Po, With the increase of 6, we can see that in both cases, both numbers decrease, suggesting that harder for an image to follow 0. without being classified 0 (the NAP is more precise), at the cost of having many images classified as 0 fail to follow 0.P0 (the NAP recalls worse). Essentially, å controls the precision-
trade-off for the NAP. Note that small increase in 6, such 0.01, can already have huge effect: neuron may be activated in 99% of the input, but the collection of all said neurons is only activated together 79% of the input (775 out of 980), as be seen with label 0 in Table 1.
For the rest of the paper, not explicitly stated, we refer to the d-relaxed dominant NAPs when talking about NAPs. When the context clear, drop any of the 8,Nand & from the notation for clarity.
3.2 NEURAL NETWORK PROPERTIES WITH NEURAL ACTIVATION PATTERNS
We expect that NAPs networks. As the first study on this topic, we introduce here two important ones.
the key component in more reliable specifications of neural
The non-ambiguity property of NAPs We want NAPs to give some confidence about the predicted label of an input, thus a crucial sanity check to verify that no input can follow two different NAPs of different labels. Formally, we verify:
Yr Vi,j(t 5) P'(x)= True ())) False
Note that this property is trivial if either n A/e n Di is non-empty: a single input cannot activate and deactivate the same neuron. If that's not the case, we can encode and verify the property using Marabou.
NAP-augmented robustness property As seen Figure/ and Section 4.1, many cases maximum verifiable e(x,e) does not contain any other input in the dataset. Our key insight is that by adding NAP constraints, we change the problem from verifying a "perfeet" but small Loo ball to "imperfect" but much bigger Loo ball, which may cover more of the input space. We explain this insight in more detail in Section 3.3. Concretely, we formalize our new robustness verification problem follows:
given neural network A and mined Pyv, we check
Va' E (x, P() Vj Ni F(x' F(2)
in which O(x) and
B (T = fa' ||  I'1oo S (,) = True}
Working with NAPs using Marabou NAPs and NAP properties can be encoded using Marabou with little changes to Marabou itself. To force neuron to be activated or deactivated, we add a constraint for its output. To improve performance, we infer ReLU's phases implied by the NAPs, and change the corresponding constraints For example, given a ReLU mar(v,, 0), to enforce 2g to be activated, we remove the constraint from Marabou and add two new onesto; = tk. and v2 2
5

---

Under review as a conference paper at ICLR 2023
Table The frequency of each ReLU and the dominant NAPs for each label. Activated and deacti- vated neurons are denoted by + and respectively, and * denotes an arbitrary neuron state.
Label
Neuron states
#samples
Dominant NAP
8
0 (Green)
(+,*, -,,,
2
,,,,,,
7
(Red)
2
(+, (, -.+)
1
15
15
Class 0 Class 1
NAP for class 0
NAP for class
sample point of class
10
10
Potertiaa adversial
Safe
Unsafe box
0.0
-0.5
(*ttttt))))
-1.0
-10
-1.5
-15
5
-1.0
-0.5
0.0
0.5
1.0
-1.0
-0.5
0.5
100
1.5
(a) Linear regions in different colors are deter- mined by weights and biases of the neural net- work. Points colored cither red or green constitute the training set.
NAPs are more flexible than Loo norm-balls (boxes) in terms covering verifiable regions.
Figure 2: Visualization of linear regions and NAPs as specifications compared to L norm-balls.
3.3 CASE STUDY: VISUALIZING NAPS OF A SIMPLE NEURAL NETWORK
We show the advantages of NAPs as specifications using a simple example of a three-layer feed- forward neural network that predicts class of 20 points located on 2D planc. We trained neural network consisting of six neurons that achieves 100% accuracy in the prediction task. The resulting linear regions as well the training data are illustrated in Fig. 2a. Table 2 summarizes the frequency of states of each neuron based on the result of passing all input data through the network, and NAPs for labels 0 and 1.
Fig. 2b visualizes NAPs for labels and 1, and the unspecified region which provides no guarantees on data that fall into it. The green dot is close the boundary between "o and the unspecified region that some Te norm-balls (boxes) such as the one drawn in the dashed line may contain an adversarial example from the unspecified region. Thus, what we could verify ends up being a small box within pd, However, using pd as a specification allows us to verify much more flexible region than just boxes, as suggested by the aug-augmented robustness property in Section 3.2. This idea generalizes beyond the simple 2D case, and we will illustrate its effectiveness further with a critical evaluation in Section 4.2.
4 EVALUATION
In this section, we validate our observation about the distance between inputs, as well evaluate our NAPs and NAP properties.
Marabou has similar optimization, but the user cannot control when or if is applied.

---

Under review as a conference paper at ICLR 2023
1000
2.24
ddance..
2202
0.22
0.03
0.00
(a) The distribution of Lo-norms between any two (b) The distribution of Loe -noms between any two im- images from the same label. Images of digit (label) ages from the same label. The red line is drawing 0.05 are much similar than that of other digits.
- the largest used in VNNCOMP (2021).
Figure 3: Distances between any two images from the same label (class) are quite significant under different metrics of norm.
4.1 TEST DATA ARE FAR AWAY FROM MAXIMUM VERIFIED BOUNDS
We argue that the maximum verifiable bounds are much smaller than the distance between real data, as illustrated in Figure 1. To show that this is not a special case, we plot the distribution of distances in L2 and Lo norm between any pair of images with the same label from the MNIST dataset, as shown in Figure 3. We obverse that the smallest 2 distance for each label is greater than 0.2, much larger than 0.05, the largest verifiable perturbation used in VNNCOMP (2021).
This strongly verifies our motivation that the data specification paradigm is not sufficient to verify data real-life scenarios. The differences between data of each class are clearly larger than the differences allowed in some certain specifications using Loo norm-balls.
4.2 THE AUGMENTEE ROBUSTNESS PROPERTY
We conduct two experiments to demonstrate the NAP -ugmanemented robustness property. Both exper- iments use the MNIST dataset and a 4-layers fully connected network used in VNNCOMP (2021), with 256 neurons for each layer. All checks run with 10-minute time limit, 5565U laptop with 16GBs of RAM. The results are shown in Table and Table 4. For each label é E [0, 9]. 'Y" and 'N' indicate that the network is robust for l (i.e., no adversarial example) or not, respectively. 'T'o" means the verification of robustness timed out.
AMD Ryzen
The first experiment circles back to Figure In the figure, we show an image I and its adversarial example that has the distance of 0.2 to I in L space. Using our technique, can we prove that there no adversarial example inside B (Z. 0.2, J.p')? We start with checking if a counter-example exists for any label (first row in Table 3), and somewhat surprisingly, Marabou can only find a counter-example in 3 out of labels within the time limit. Using the most precise NAP O.P, we are able to verify the robustness of I against 2 labels. By increasing ó to 0.01, we are able to verify the robustness against all other labels. In fact, with = 0.01, we are able to verify the whole input spuce (denoted by 1.0 in the last row)! We ack acknowledge "fineprint" that by using ó = 0.01, we only recall about 84% of the test set (Table 1). but this is still a significant result. To the best of knowledge, this is the first time significant region of the input space has been formally verified.
For the second experiment, we verify the all six (z, e) tuples in MNIST dataset that are known to be not robust from VNNCOMP-2021. We start with augmenting those examples with O.P. Using O.P, we can prove the robustness of one input against all other labels and block adversary examples in many labels for other inputs (Table 4). We also note that adversarial examples still exist against certain labels, indicating that 0.P may be too weak. Indeed, by slightly relaxing the NAP (5 = 0.01), all of the chosen inputs can be proven to be robust. Furthermore, with 8 0.01, we can verify the robustness for 5 of the inputs (TTble 4) with e = 0.3 - an order of magnitude bigger bound than before. Unfortunately, we are not able to verify bigger e, except for 2 and 25 (that can be verified in
The Tag metric is not commonly used by the neural network verification research community as they less computationally efficient than the Too metric.
7

---

Under review as a conference paper at ICLR 2023
Table 3: Verify the robustness the example in Figure
0
2
3
5
6
7
9
0.2, no NAP
N
T/o
T/o
T/o
T/o
Tlo
N
T/o
0.2, = 0
N
N
Y
T/o
T7o
Y
T/o
N
N
0.2,8 = 0.01
Y
Y
Y
Y
Y
Y
Y
Y
Y
6 1.0,8 0.01
Y
Y
Y
Y
Table Inputs that are not robust can be augmented with a NAP be robust. We index the known non-robust inputs from MNIST zo to 25, and augment them with NAP.
0
( =
c 0.03,0
Y
Y
Y
Y
6 =
Y
Y
Y
Y
Y
Y
Y
Y
Y
с 0.05,0=0
Y
Y
Y
Y
Y
Y
Y
N
Y
6 0.3,6= 0.01
Y
Y
Y
( 0
0.05,
T/o
T/o
Y
T/o
T/o
Y
N
T/o
T/o
C 0.3,6= 0.01
Y
Y
Y
Y
Y
Y
((rg)
E 0.05,
N
T/o
Y
Y
T/o
T/o
Y
N
T/o
C 0.3. = 0.01
Y
Y
Y
Y
Y
Y
Y
Y
O
6 0.05,
T/o
Y
Y
0.3, 0.01
Y
T/o
T/o
Y
N
Y
T/o
T/o
T/o
O(16)
6 0.05,
Y
Y
Y
N
N
0.3, 8 0.01
Y
Y
Y
Y
Y
Y
the whole input space, as demonstrated with the previous experiment). One might tempt to increase 5 even further to verify bigger but one must remember that comes with sacrificing the recall of the NAP. Thus, choosing an appropriate is crucial for having useful NAPs.
4.3 THE NON-AMBIGUITY PROPERTY OF MINED NAPS
We evaluate the non-ambiguity of our mined NAP at different ds. At 0, Marabou construct inputs that follow any pair of NAP, indicating that the 0-relaxed dominant NAPs not satisfy the property. However, by setting NAPs, through both trivial cases and invoking Marabou. Like the previous experiment, we observe the benefit of relaxing 5 here: the most precise NAPs contain few ReLUs that it very easy to violate the non non-ambin -obbiiiiyt property, thus relaxing 8 is crucial for the NAPs to be more useful.
0.01,
able to prove the non-ambiguity for all pair of
The non-ambiguity property of NAPs holds an important prerequisite for neural networks achieve a sound classification result. Otherwise, if two labels share the same NAP, the final prediction of inputs with these two labels may also become indistinguishable. We argue that NAPs mined from well-trained neural network should demonstrate strong con-ambiguity properties and ideally, all inputs with the same label should follow the same P'. However. this strong statement may fail even for accurate model when the training dataset itself is problematic, as what we observed in Fig. 1d as well many examples in Appendix C. These examples are not only similar the model but also humans despite being labeled differently. The experiential results also suggest mined NAPs do satisfy the strong statement proposed above if excluding these noisy samples.
To conclude, in this section present study that verifies our hypothesis about L-norm distances between data points in the MNIST dataset, thus explaining the limitation of using L-norm in verify- ing neural networks' robustness. Then, conduct experiments to show that our d-relaxed dominant NAPs can used to verify a much bigger region in the input space, which has the potential to gen- eralize to wal-world scenarios.
8

---

Under review as a conference paper at ICLR 2023
5 RELATED WORK AND FUTURE DIRECTIONS
Abstract Interpretation in verifying Neural Networks The software verification problem is un- decidable in general (Rice, 1953). Given that a Neural Network can also be considered a program, verifying any non-trivial property of a Neural network is also undecidable. Prior work on neural network verification includes specifications that are linear functions of the output of the network: Abstract Interpretation (AbsInt) (Cousot & Cousot, 1977) pioneered happy middle ground: by sacrificing completeness, an AbsInt verifier can find proof much quicker, by aver-approximating reachable states of the program. Many NN-verifiers have adopted the same technique, such as Deep- Poly (Singh et al., 2019), CROWN (Wang et al., 2021). NNV (Tran et al., 2021), etc. They all share the same insight: the biggest bottle neck in verifying Neural Networks is the non-linear activation functions. By abstracting the activation into linear functions as much as possible, the verification can be many orders of magnitude faster than complete methods such Marabou. However, there is no free lunch: Abstract- based verifiers are inconclusive and may not be able to verify properties even when they are correct." A On the other hand, the neural representation as specification paradigm proposed in this work can be naturally viewed as a method of Abstract Interpretation, in which we abstract the state of each neuron only activated and deactivated by leveraging NAPs. We would like to explore more refined abstractions such as {--o), (0, 1], (1, oo]} in future work.
Neural Activation Pattern in interpreting Neural Networks There are many attempts aimed to address the black-box nature of neural networks by highlighting important features in the input, such as Saliency Maps (Simonyan et al., 2014; Selvaraju et al., 2016) and LIME(Ribeiro et al., 2016). But these methods still pose the question of whether the prediction and explanation can be trusted or even verified. Another direction is to consider the internal decision-making process of neural networks such as Neural Activation Patterns (NAP). One popular line of research relating to NAPs is to leverage them in feature visualization (Yosinski et al., 2015; Bäuerle et al., 2022; Erhan et al.. 2009), which investigates what kind of imput images could activate certain neurons in the model. Those methods also have the ability to visualize the internal working mechanism of the model to help with transparency. This line of methods is known activation maximization. While being great at explaining the prediction of a given input, activation maximization methods do not provide a specification based on the activation pattern: best they can establish correlation be- tween seeing a pattern and observing an output, but not causality. Moreover, moving from reference sample to revealing neural network activation pattern is limiting as the portion of NAP uncovered is dependent on the input data. This means that it might not be able to handle cases of unexpected test data. Conversely, our method starts from the bottom up: from the activation pattern, we uncover what region of input can be verified. This property of our method grants the capability to be general- ized. Motivated by our promising results, we would like to generalize our approach to modern deep learning models such as Transformers (Vaswani et al., 2017), which employ much more complex network structures than a simple feed-forward structure.
6 CONCLUSION
We propose a new paradigm of neural network specifications, which we call neural representation as specification, as opposed to the traditional data specifications. Specifically, we leverage neural network activation patterns (NAPs) to specify the correct behaviours of neural networks. We argue this could address two major drawhacks of "data as specifications". First, NAPs incorporate intrin- sic properties of networks which data fails to do. Second, NAPs could cover much larger and more flexible regions compared to Lox norm-balls centred around reference points, making them appeal- ing to real-world applications. We also propose simple method to mine relaxed dominant NAPs and show that working with NAPs can be easily supported by modern neural network verifiers such as Marabou. Through a simple case study and thorough valuation on the MNIST dataset, we show that using NAPs as specifications not only address major drawbacks of data as specifications, but also demonstrate important properties such as no-ambiguity and one order of magnitude stronger verifiable bounds. We foresee verified NAPs have the great potential of serving as simple, reliable, and efficient certificates for neural network predictions.
'Methods such as alpha-beta beta CROWN (Wang et al., 2021) claim to be complete even when they are A hased hecause the abstraction can be controlled to be as precise as the original activation function, thus reducing the method hack to complete one.
9

---

Under review as a conference paper at ICLR 2023
REFERENCES
Alex Bäuerle, Daniel Jönsson, and Timo Ropinski. Neural activation patterns (naps): Visual ex- plainability of learned concepts, 2022. URL https: aattps://arxiv. .rg/
abwp//bs//222.. http://awxxxi...r/////222....2 10611
Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static anal-
ysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 238-252, 1977.
Thomas G. Dietterich and Eric Horvitz. Rise of concerns about Al: reflections and directions.
Commun. ACM, (8(10))38-44 40, 2015.
D. Erhan, Yoshua Bengio, Aaron C. Courville, and Pascal Vincent. Visualizing higher-layer features of a deep network. 2009.
Xiaowei Huang, Marta Kwiatkowska, Sen Wang. and Min Wu. Safety verification of deep neural networks. In Rupak Majumdar and Viktor Kunčak (eds.), Computer Aided Verification, pp. 3-29, Cham, 2017. Springer International Publishing. ISBN 978-3-319-63387--
Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp. Youcheng Sun, Emese Thamo, Min Wu, and Xinping Yi. A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretabillity. Computer Science Review, 37:100270, 2020. ISSN 1574-0137. doi:
http://do...r/./00.01161....oooo 1002000.0..20000000....000000000 100270. URL https://
wwW. www.eceeeeeeee...c..m. com/ wwccinnceartiiio http:///e.eeerrr..eaaa////////.1
Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kunčak (eds.), Computer Aided Verification, pp. 97-117, Cham, 2017. Springer International Publishing. ISBN 978-3-319-63387-
Guy Katz, Derek A. Huang, Duligur lbeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. The marabou framework for verification and analysis of deep neural net- works. In (I), volume 11561 of Lecture Notes in Computer Science, pp. 443-452. Springer, 2019.
John A. Nelder and Roger Mead. A simplex method for function minimization. Computer Journal, 7:308-313, 1965.
Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. "why should trust you?": Explaining the predictions of any classifier. In Proceedings of the 22nd ACM SIGKDD International Conference Knowledge Discovery and Data Mining, San Francisco, CA, USA, August 13-17, 2016, pp- 1135-1144, 2016
H. G. Rice. Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society, 74(2):358-366, 1953. ISSN 00029947. URL http: / //www. jstor. httgg//taabeee99998899
Ramprasaath Selvaraju, Abhishek Das, Ramakrishna Vedantam, Michael Cogswell, Devi Parikh, and Dhruv Batra. Grad-cam: Why did you say that? visual explanations from deep networks via gradient- based localization. CoRR, abs/1610.02391, 2016. URL http: /ttp:pp//aaxvv..//o wrrg/argaaa.. 1610. 02391.
Karen Simonyan, Andrea Vedaldi, and Andrew Zisserman. Deep inside convolutional networks: Visualising image classification models and saliency maps. In Yoshua Bengio and Yann Le- Cun (eds.), 2nd International Conference on Learning Representations, ICLR 2014, Banff. AB, Canada, April 14-16. 2014, Workshop Track Proceedings, 2014. URL http: /ttt:///rxivi orq/ abs/1312, 6034.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certi- fying neural networks. Proc. ACM Program. Lang., 3(PPPL), jan 2019. doi: 145/324429 URL https::/p/.............tt. /ow.i .or.//r...... httpg/....1//399990
10

---

Under review as a conference paper at ICLR 2023
Hoang-Dung Tran, Neelanjana Pal, Patrick Musau, Diego Manzanas Lopez, Nathaniel Hamilton, Xiaodong Yang, Stanley Bak, and Taylor T. Johnson. Robustness verification of semantic seg- mentation neural networks using relaxed reachability. In Computer Aided Verification: 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part I, pp- 263-286, Berlin, Heidelberg, 2021. Springer-Verlag. ISBN 378-3-0330-8184-- 778-3-030-81168--.J1 URL https: /doiidii.////// www./o/g./o....o..o 1007 97 http::://oi..rg/1..10000000 12.
doi: 10.1007/ 8068-1180------11111111111
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In NIPS, pp. 5998-6008, 2017.
VNNCOMP. Vnncomp, 2021. URL https: /ttp:::://sittsss
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Advances in Neural Information Processing Systems, 34, 2021.
Jeannette M. Wing. A specifier's ' introduction to formal methods. Computer, 23(9):8-22) 24, 1990.
Jeannette M. Wing. Trustworthy Al. Commun. ACM, 64(10):64-71,222) 2021.
Han Xu, Yao Ma, Haochen Liu, Debayan Deb, Hui Liu, Jiliang Tang, and Anil K. Jain. Adversarial attacks and defenses in images, graphs and text: review. International Journal of Automation and Computing, 17:151-178, 2020.
Jason Yosinski, Jeff Clune, Anh Nguyen, Thomas Fuchs, and Hod Lipson. Understanding neural net- works through deep visualization, 2015. URL https: /awxivivvvv./////i///aa///aaaava arg/

---

Under review as a conference paper at ICLR 2023
0.1ag 0.62)
90 0.1ag 0.621
-4.3%0 + 4.4m1
-4.33am -4.3%o + 4.4x1
12 4.2xg-
4.2xg
4.2
Fg maz(po, 0)
93 vD
mar("1,0) 0)
84 maur("1: 0)
mar((".
RAU
RUU
RAU
9.9wg + 6.7
0.4v4 4.80g 3.9v6 + 6.7
-0.403 + 3.90, 4.80g 7.4
#1
20 0.1 A. 2 0.02
20 2.0
0.1 A. 2 0.02
21 5.3 5.33A. 2.0
48
0
2.0
(a) XNET: A NN that computes the analog XOR function.
(b) Marabou's system of constraints verifying that XNET is 0.04-robust at (0.06, 0.06)
Check if pl ((zo), () and D (0) (22)) are non ambiguous the first quadrant using Marabou
Figure 4: Using Marabou to verify NAP properties of XNET.
A A RUNNING EXAMPLE
To help with illustrating later ideas, we present two-layer feed-forward neural network XNET (Figure 4a) to approximate analog XOR function ((n, [[0, |0.7, 1]]2 - {0, 1) such that faro x1) = iff (Io 0.3 21 2 0.7) or (zo 2 0.7 A æ1 S 0.3). The network computes the function
(x) W max(W"(()) (z) + bb.0) +
where x [ ,. and values of W W b" b² are shown in edges of Figure 4a. O(x) 0 (x) Fx)))(x)(1], (xx) otherwise.
Note that the network is not arbitrary. We have obtained it by constructing two sets of 1 100 ran- domly generated inputs, and training on one and validating the other until the NN achieved perfect FI-score of 1.
B OTHER EVALUATIONS
B. LI-NORMS OF DISTANCE
Figure shows the distributions of Lı-norms of all image pairs from the same class, similar to Fig. 3, the distances between image pairs from class 1 are much smaller compare to other classes.
B.2 OVERLAP RATIO
Table 5: The maximum overlap ratio for each label (class) on given S.NAP for MNIST. Fach cell obtained by max; 5 col NN / where Né is the set of neurons the dominant pattern for the label (class) in the header of the column of the selected cell with the given 8, N; is the set of neurons the dominant pattern for the label (class) with the given ó.
0
2
3
4
5
6
7
8
9
0.00
0.959
0.928
0.963
0.966
0.972
0.973
0.930
0.965
0.957
0.981
0.01
0.844
0.834
0.911
0.901
0.881
0.898
0.895
0.884
0.880
0.908
0.05
0.864
0.885
0.909
0.904
0.915
0.908
0.899
0.897
0.890
0.893
0.10
0.877
0.900
0.910
0.901
0.921
0.910
0.890
0.899
0.900
0.901
0.15
0.876
0.904
0.904
0.900
0.919
0.913
0.893
0.907
0.904
0.900
0.25
0.893
0.922
0.913
0.912
0.928
0.925
0.905
0.916
0.916
0.913
0.50
0.903
0.905
0.925
0.923
0.926
0.923
0.907
0.918
0.927
0.927
12

---

Under review as a conference paper at ICLR 2023
200
distance (4 norm)
150
100
50
0
2
3
4
6
7
8
class
Figure 5: The distribution of Ln-nomms of all image pairs for each class.
Figure 6 shows the heatmap of the overlap ratio between any two classes for 6 8 values. For the grid in each column of the NAPs of the class labelled for the row and the column divided by the number of neurons in the NAP of the class labelled for the column, which is why the values in the heatmaps are not symmetric along the diagonal. Based the shade of the colors in heapmap, we can see that, during the process increasing ò, the overlapping ratios decrease first and then increase general, it might because that, with the loose of restriction more neurons are included in the NAP, which means more constrains, but at the same time, for two NAPs of any two classes, it more likely that they have more neurons appearing in both NAPs.
heatmap, the overlap ratio is calculated by the number of overlapping neurons
when neuron is considered as activated/inactiiated.
315
SXL
375
(a) 8 0.00
(b) 8 0.01
(c) 0.05
DXY
KGS
SNT
(d) 8 = 0.10
(e) 8 0.15
(1) 8 0.50
Figure 6: Overlap ratio of the dominant pattern of two labels (classes) on a given d.NAP. Values in each grid obtained by [ o N l/ where N is the set of neurons in the dominant pattern for the label (class) of the column of the selected grid with the given 8, Nrow is the set of neurons in the dominant pattern for the label (class) of the row of the selected grid with the given 5.
13

---

Under review as a conference paper at ICLR 2023
Table 5 shows the maximum overlap ratio for one class, that is, for reference class, the maximum overlap ratio between this reference class and any other class. This table basically extracting the maximum values of each column other than the on the diagonal in our heatmap in Fig. 6, in the each column of our table, also follows the pattern that the value of overlap ratio decreases first and then increase with the increase of 6.
C MISCLASSIFICATION EXAMPLES
In this section, display interesting exmaples from the the MNIST test that follow the NAP of some class other than their ground truth, which means these images are misclassified. We consider these samples interesting because, instead of misclassification, it is more reasonable to say that these images are given wrong ground truth from human perspective.
delta-0.0, C.O, pred-0, gb-5
delta-0.0, pred=O, gt=B
delta-0.0, pred=0, gt=3
O
9
(a) A testing image from MNIST with ground truth 5, classified
(b) A testing image from MNIST with ground truth classified
(c) A testing image from MNIST with ground truth classified as
Figure 7: Some interesting test images from MNIST that are misclassified as 0 and also follow the NAP of class O.
deltam0.00 D, pred=1
della=0.0, pred=1.
0elta=000. pred=1,
1
(a) A testing image from MNIST with ground truth 6, classified
(b) A testing image from MNIST with ground truth classified as
(c) A testing image from MNIST with ground truth classified as
Figure 8: Some interesting test images from MNIST that misclassified as I and also follow the NAP of class 1.
14

---

Under review as a conference paper at ICLR 2023
predm2. gim]
della-0.00 predm2, gim3
gim?
7
(a) testing image from MNIST with ground truth 1, classified as 2
(b) testing image from MNIST
(c) A testing image from MNIST with ground truth 7, classified as
with ground truth 3, classified as
2
2
Figure 9: Some interesting test images from MNIST that are misclassified as 2 and also follow the NAP of class 2.
delta=0.0, pred=3, gt-5
della=0.0, pred=3, gt=7
delta=0.0, pred=3, gt=
57
(a) A testing image from MNIST with ground truth 5, classified
(b) A testing image from MNIST with ground truth classified
(c) A testing image from MNIST with ground truth classified
Figure 10: Some interesting test images from MNIST that are misclassified 3 and also follow the NAP of class 3.
delta-6.00 prode4, gt-2
delta-0.0. prod=4, gt-6
delta-0.0, pred=4, gt-3
4
Q
C(
(a) A testing image from MNIST with ground truth 2, classified 4
(b) A testing image from MNIST with ground truth 6, classified as 4
(c) A testing image from MNIST with ground truth 9, classified as 4
Figure II: Some interesting test images from MNIST that are misclassified as 4 and also follow the NAP of class 4.
15

---

Under review as a conference paper at ICLR 2023
5redm5, g
delta-0.00 gtmb
glm@
36
(a) testing image from MNIST with ground truth 3, classified as
(b) testing image from MNIST with ground truth 6, classified as
A testing image from MNIST with ground truth 8, classified as
5
5
5
Figure 12: Some interesting test images from MNIST that are misclassified and also follow the NAP of class 5.
delta=0.0, pred-6, gt-0
della=0.0, pred=6, gt=2
della=0.0, pred=6, gt=5
G
2
5
(a) A testing image from MNIST with ground truth 0, classified
(b) A testing image from MNIST
(c) A testing image from MNIST
with ground truth classified
with ground truth classified
Figure 13: Some interesting test images from MNIST that are misclassified 6 and also follow the NAP of class 6.
delta-6.0, 7rod=7, gt-2
delta-0.0, prod=7, gt-3
delta-0.0, pred-7, gt-2
2
7
S
(a) A testing image from MNIST with ground truth 2, classified 7
(b) A testing image from MNIST with ground truth 3, classified as
(c) A testing image from MNIST with ground truth 9, classified as
7
Figure 14: Some interesting test images from MNIST that are misclassified as 7 and also follow the NAP of class 7.
16

---

Under review as a conference paper at ICLR 2023
delta=0.0, pred=8, gt=1
delta=0.0, pred=8, gt=3
(a) testing image from MNIST with ground truth I, classified as 8
(b) testing image from MNIST with
ground truth 3, classified as 8
Figure 15: Some interesting images from MNIST that are misclassified and also follow the NAP of class 8.
delta=0.0, pred=9, gt=4
delta=0.0, pred=9, gt=7
(a) testing image from MNIST with ground truth 4, classified as 9
(b) testing image from MNIST with ground truth classified as
Figure 16: Some interesting images from MNIST that misclassified 9 and also follow the NAP of class 9.
17


Reviews:
[{"review_id": "q6GPsFeom2D", "reviewer": "Reviewer_uPcc", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "This paper proposes a novel robustness specification for neural networks. Unlike canonical specifications where pre-conditions are defined as constraints on the neural network input,  the specification used in this paper are defined as particular activation patterns. The paper presents a strategy to extract activation patterns, shows how the specification can be checked with existing verifiers, and how this specification achieves better coverage of the test set. ", "summary_of_the_review": "Overall, I think the paper contains several good and novel ideas and could motivate future work both in application and verification techniques.", "strength_and_weaknesses": "Strength:\n\nI really like this work. Adding activation patterns to the pre-conditions of the specification is a simple but clever extension. It seems to be able to cover more test images than the canonical way does, where the constraint is only put on the input. Instead of only having the activation patterns as the pre-condition, still specifying a (now larger) epsilon ball in the input region not only makes the specification more relevant (as it focus the verification on valid images of digits instead of some noise input) but also likely to make the verification task easier. \nThis work might also motivation development of verification techniques that can handle constraints on NAP more effectively. \n \nWeakness:\n\nThe experiment is performed only on small neural networks. The verification is in general challenge, and using tools other than Marabou is unlikely to suddenly allow us to scale to SoTA perception networks. However, I would still be curious to see how scalable the NAP extraction procedure is and what the neural specifications look like on more complex image dataset and networks.\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "nSSS_92C3TU", "reviewer": "Reviewer_F47b", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "###  Problem\nThe paper tackles the problem of neural network verification, which aims to give guarantees of whether a trained NN follows certain specifications.\n\n###  Proposed method\nThe authors claim that the current adversarial robustness specification used by the verification community is improper. Their claim is that this specification does not allow verification of test set inputs as they lie outside the verified region.\n\nAuthors propose neural representation as specification. Essentially, they propose to use neural activation patterns as specifications.\n\n### Experimental Validation\nExperiments are conducted on the MNIST dataset, where it shows that with the proposed specification, the certified region can go well beyond adversarial examples and even verify test set inputs.\n\n### My one line understanding\nAuthors claim to have found a condition which:\n1. adversarial examples don't follow, so verification won't stop at them and will be able to go beyond\n2. test examples from same class follow, so test set examples can be verified", "summary_of_the_review": "It is important to look for alternate specification.\n\nBut the assumptions made in this work feel incorrect and are not properly validated, so I cannot draw a conclusion from the current version.", "strength_and_weaknesses": "## STRENGTHS\n1. Finding alternative specifications is a good direction to explore\n\n## WEAKNESSES\n\n1. Writing needs to be improved\n- Not put into context properly: Doing adversarial verification is not necessarily an *overfitted* specification, as you call it. There are many applications where we also want to verify against adversarial examples. I don't think you need to belittle previous work. Your work is complementary, and that is how you should write the paper.\n- I don't agree with the entire 'data as specification' vs 'neural representation as specification' angle.  Because if one looks at equations in Sec3.2, you have the same formulation, but an extra constraint/specification. So you can write we add a new specification, instead of saying one vs the other.\n- Many equations are not numbered. How should I refer to them?\n\n2. Strong and probably incorrect assumptions\n- What is the guarantee that test examples will definitely follow same NAP?\n- What is the guarantee that adversarial examples will not follow NAP\n- Isn't such an assumption against the whole point of verification?\n\n3. Weak experimental validation\n- One main limitation of adv verification methods is their inability to scale beyond small epsilons. This is especially critical for your work because for going upto the test inputs, you would require large epsilon. Current methods don't allow that. So your method might not work on bigger datasets at all. Whereas, adv verification will still work on big datasets with small epsilon. \n- The experiments are only conducted on the MNIST dataset. I feel that MNIST is too easy and that is why your assumptions hold there. Since your assumptions are so strong, can you validate them on a bigger dataset?", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "Xwc1tNKZh2m", "reviewer": "Reviewer_epj3", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "The paper introduces a novel specification for neural network verification,\nwhere instead of checking whether sets of inputs are classified equivalently by\na network, it concerns checking the robustness of networks when their behaviour\nis restricted to certain neural activation patterns.", "summary_of_the_review": "Whilst the paper introduces novel neural network specifications that are\nimportant to check in practice, the overall novelty and significance of the\nempirical evaluation are weak.", "strength_and_weaknesses": "+ The specifications introduced present in my opinion a step towards obtaining\nstronger neural network robustness guarantees when used in conjunction with\nexisting specifications.\n\n- Unsound claim that standard specifications are impractical for real world\n  applications. I think that checking small perturbations radiuses which do not\n  alter the semantics of the input is important for any application.\n\n- Not surprising empirical results. As the specifications proposed are\n  restricted to certain activation patterns, it is expected that the\n  perturbation radiuses that can be verified will be bigger when compared to\n  standard specifications. \n\n- The evaluation is limited in that it only concerns one benchmark.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "1238XyWQKx", "reviewer": "Reviewer_rBXu", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "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": "", "main_review": "", "summary_of_the_paper": "The paper proposed neural activation patterns as a replacement for adversarial robustness specifications to reason about the robustness of the network. The paper argues that this resolves the problem that test samples don't fall into certified regions of an adversarially robust verified network.", "summary_of_the_review": "Interesting concept of overcoming the problem of certified adversarial regions having little relevance for the test data. Insufficient experimental validation of whether the proposed specifications are actually reasonable in practice.", "strength_and_weaknesses": "# Strengths:\n- The paper highlights an important issue in adversarial robustness certification (the adversarial robustness verification only covers a minuscule part of the entire input space).\n- The paper introduces a novel set of specifications and shows that it covers a larger part of the test inputs.\n\n# Weaknesses:\nThe main issue with the submission is the lack of proper evaluation of the proposed specifications. Particularly, the paper validates the specification on a 2D example and MNIST. The MNIST dataset is severely outdated and known to have artifacts that are not present in other datasets, such as prototypical samples or high certifiable accuracy (compared to, for instance, CIFAR where the top accuracy and the top certified accuracy have a huge gap).\nAdditionally, the paper only assesses MLP networks. \nConsequently, the paper provides insufficient experimental validation of whether the proposed specifications are actually useful and reasonable in practice. It is vital to check if the hypothesized NAP specification works on larger and more diverse datasets, different types of data, and different structures of networks \n\nMoreover, neural activation patterns have already been used in the verification literature of neural networks [1], making the concept less novel.\n\n\n[1] Henzinger et al. Outside the Box: Abstraction-Based Monitoring of Neural Networks. 2020", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}]

Author rebuttal:

Decision: Reject