# Learning Minimal NAP Specifications for Neural Network Verification

Chuqin Geng<EMAIL_ADDRESS>McGill UniversityCanada ,  Zhaoyue
Wang<EMAIL_ADDRESS>McGill UniversityCanada ,  Haolin Ye
<EMAIL_ADDRESS>McGill UniversityCanada ,  Saifei Liao
<EMAIL_ADDRESS>University of TorontoCanada and  Xujie Si
<EMAIL_ADDRESS>University of TorontoCanada

(2018; 20 February 2007; 12 March 2009; 5 June 2009)

###### Abstract.

Specifications play a crucial role in neural network verification. They define
the precise input regions we aim to verify, typically represented as
L-infinity norm balls. While recent research suggests using neural activation
patterns (NAPs) as specifications for verifying unseen test set data, it
focuses on computing the most refined NAPs, often limited to very small
regions in the input space. In this paper, we study the following problem:
Given a neural network, find a minimal (coarsest) NAP that is sufficient for
formal verification of the network’s robustness. Finding the minimal NAP
specification not only expands verifiable bounds but also provides insights
into which neurons contribute to the model’s robustness. To address this
problem, we propose several exact and approximate approaches. Our exact
approaches leverage the verification tool to find minimal NAP specifications
in either a deterministic or statistical manner. Whereas the approximate
methods efficiently estimate minimal NAPs using adversarial examples and local
gradients, without making calls to the verification tool. This allows us to
inspect potential causal links between neurons and the robustness of state-of-
the-art neural networks, a task for which existing verification frameworks
fail to scale. Our experimental results suggest that minimal NAP
specifications require much smaller fractions of neurons compared to the most
refined NAP specifications, yet they can significantly expand the verifiable
boundaries to several orders of magnitude larger.

Do, Not, Us, This, Code, Put, the, Correct, Terms, for, Your, Paper

††copyright: acmlicensed††journalyear: 2018††doi: XXXXXXX.XXXXXXX††conference:
Make sure to enter the correct conference title from your rights confirmation
emai; June 03–05, 2018; Woodstock, NY††booktitle: Woodstock ’18: ACM Symposium
on Neural Gaze Detection, June 03–05, 2018, Woodstock, NY††isbn:
978-1-4503-XXXX-X/18/06††ccs: Do Not Use This Code Generate the Correct Terms
for Your Paper††ccs: Do Not Use This Code Generate the Correct Terms for Your
Paper††ccs: Do Not Use This Code Generate the Correct Terms for Your
Paper††ccs: Do Not Use This Code Generate the Correct Terms for Your Paper

##  1\. Introduction

The growing prevalence of deep learning systems in decision-critical
applications has elevated safety concerns regarding AI systems, such as their
vulnerability to adversarial attacks (Goodfellow et al., 2015; Dietterich and
Horvitz, 2015). Therefore, the verification of AI systems has become
increasingly important and attracted much attention from the research
community. The field of neural network verification largely follows the
paradigm of software verification – using formal methods to verify desirable
properties of systems using rigorous mathematical specifications and proofs
(Wing, 1990). Most existing works (Katz et al., 2017, 2019; Huang et al.,
2017a, 2020; Wang et al., 2021b) utilize $L_{\infty}$ ball specifications for
verifying robustness guarantees, i.e., verify if neural networks consistently
predict the same label within local neighborhoods ($L_{\infty}$ balls) of
reference data points.

Figure 1. The comparison between the NAP specification (depicted by the green
region) and the $L_{\infty}$ ball specification (represented by the gray
region) in the MNIST dataset. Image $a$ is the reference image, and image $c$
is the closest image to $a$ with an $L_{\infty}$ distance of 0.5294. However,
image $c$ cannot be verified using the $L_{\infty}$ ball specification because
an adversarial example $b$ can be found at an $L_{\infty}$ distance of 0.2. In
contrast, the NAP specification enables verification of inputs that are
semantically close despite their geometric distance being far apart, such as
image $c$.

While this type of specification provides a fair and effective testbed for
evaluating neural networks’ robustness, those verifiable $L_{\infty}$ balls
are usually too tight, making them unlikely to cover unseen test set data
(Geng et al., 2023). For instance, the $L_{\infty}$ maximum verifiable bounds
in the MNIST dataset is smaller than 0.2, whereas the smallest distance among
images sharing the same label is greater than 0.5. Thus, narrowing the gap
between verifiable regions and real data distribution to further enable
verification in real-world settings poses a challenge.

To this end, Geng et al. (2023) proposes using neural activation patterns
(NAPs) as specifications. Neural activation patterns can be viewed as an
abstraction of each neuron’s state. For ReLU activation, it can be categorized
into an activation state and a deactivation state. Since NAPs represent the
intrinsic decision-making processes of neural networks, geologically distant
data usually share the same NAPs if they belong to the same class. Compared to
conventional local neighborhood specifications, NAP specifications cover much
more flexible and potentially larger regions, as illustrated in Figure 1. This
allows the verification of unseen real data rather than synthesized data from
local neighbourhoods, paving the way for real-world application verification.

However, it is noteworthy that the current approach to computing NAPs relies
on a simple statistical method that assumes each neuron contributes to
certifying the robustness behaviors of neural networks. Consequently, the
computed NAPs are often the most refined ones. However, this is an overly
restrictive assumption, as many studies (Frankle and Carbin, 2019; Lu et al.,
2019; Liang et al., 2021; Wang et al., 2021a) have revealed that a non-trivial
portion of neurons in neural networks may not play a substantial role. This
motivates us to address the following challenge: Given a neural network, find
a minimal (coarsest) NAP that is sufficient for formal verification of the
network’s robustness. This problem is important for the following reasons: i)
Minimal NAP specifications correspond to potentially much larger regions in
the input space compared to the finest ones, this increases the potential of
verification of unseen data; ii) Minimal NAP specifications provide insight
into which neurons are responsible for the model making robust predictions,
helping us to reveal the black-box nature of neural networks.

To find the minimal NAP specifications, we introduce two basic algorithms:
Refine and Coarsen. These algorithms exhaustively check all possible
candidates using off-the-shelf verification tools, such as Marabou (Katz et
al., 2019). While these approaches provide correctness guarantees, they are
not efficient for verifying large neural networks as calls to the verification
tool are usually very expensive. To tackle this inefficiency, we propose
statistical versions of Refine and Coarsen — Sample_Refine and Sample_Coarsen
that leverage sampling and statistical learning principles to find the minimal
NAP specification in a more efficient manner. However, current verification
tools cannot scale up to state-of-the-art neural network models, limiting the
ability of verification-dependent approaches to compute the minimal NAP
specification.

This motivates us to study estimation methods that do not rely on verification
tools. To this end, we find that adversarial examples and local gradients can
provide valuable information about mandatory neurons, which are the essential
building blocks of minimal NAPs. We then translate these findings into two
approximate approaches: Adversarial_Prune and Gradient_Search. They can be
used together to estimate mandatory neurons of state-of-art neural networks
such as VGG-19 (Simonyan and Zisserman, 2014) and inspect possible links
between models’ robustness performance and internal neurons, a task that
existing verification frameworks struggle to scale for.

Moreover, previous research has claimed that NAP specifications cover
significantly larger regions compared to $L_{\infty}$ ball specifications, yet
this assertion lacks empirical evidence. In this paper, we address this gap by
introducing a simple approach to estimate the volume of regions corresponding
to NAP specifications. Furthermore, this method provides us with a rough
approximation of the volumetric change from refined NAP specifications to
minimal NAP specifications. Our experimental results demonstrate significant
volumetric changes, thereby underscoring the efficacy of minimal NAP
specifications in real-world verification scenarios. We summarize our
contributions as follows:

  * •

We propose the problem of learning the minimal NAP specification and
illustrate its importance in neural network verification. We present two
simple approaches that leverage the verification tool with correctness
guarantees.

  * •

We introduce several key concepts related to the problem of learning minimal
NAP specifications, including the abstraction function, NAP specification, and
mandatory neurons. We demonstrate that the problem can be easily solved with
access to mandatory neurons and propose two efficient estimation approaches to
learn them.

  * •

We propose two statistical learning approaches to the minimal NAP
specification problem. They leverage sampling and estimation techniques as
heuristics to achieve better efficiency.

  * •

We present a simple approach for estimating the volume of regions
corresponding to NAPs. This helps us understand the volumetric change in
verifiable space between the minimal NAP specifications and the refined NAP
specifications.

  * •

Our experiments indicate that the minimal NAP specifications involve much
smaller fractions of neurons compared to the most refined NAPs. And they
significantly expand the verifiable bound by several orders of magnitude.

##  2\. Background

In this section, we introduce basic knowledge and notations of adversarial
attacks and neural network verification, with an emphasis on verification
using NAP specifications. This may help readers better understand the
importance of learning minimal NAP specifications.

###  2.1. Neural Networks for Classification Tasks

In this paper, we focus on feed-forward ReLU neural networks. Generally
speaking, a feed-forward network $N$ is comprised of $L$ layers, where each
layer performs a linear transformation followed by a ReLU activation. We
denote the pre-activation value and post-activation value at the $l$-th layer
as $z^{(l)}(x)$ and $\hat{z}^{(l)}(x)$, respectively. The $l$-th layer
computation is expressed as follows:
$z^{(l)}(x)=\mathbf{W}^{(l)}\hat{z}^{(l-1)}(x)+\mathbf{b}^{(l)}$,
$\hat{z}^{(l)}(x)=\mathbf{ReLu}(z^{(l)}(x))$, with $\mathbf{W}^{(l)}$ being
the weight matrix and $\mathbf{b}^{(l)}$ representing the bias for the $l$-th
layer. We denote the number of neurons in the $l$-th layer as $d_{l}$, and the
$i$-th neuron in layer $l$ as $N_{i,l}$. The pre-activation value and post-
activation value of $N_{i,l}$ at input $x$ is computed by $z_{i}^{(l)}(x)$ and
$\hat{z}_{i}^{(l)}(x)$. The network can also be viewed as a function
$\mathbf{F}^{<N>}:=\mathbb{R}^{d_{0}}\rightarrow\mathbb{R}^{d_{L}}$ such that
$\mathbf{F}^{<N>}(x):=z^{(L)}(x)$, where
$\mathbf{F}^{<N>}_{i}(x):=z_{i}^{(L)}(x)$ represents the output of $i$-th
neuron in the last layer. We will omit $N$ when the context is clear. In a
multi-class classification task with $C$ as the set of classes, when provided
with an input $x$, the neural network predicts class/label $c\in C$ if the
output of the $c$-th neuron $\textbf{F}_{c}(x)$ is the highest among the
neurons in the $L$-th layer.

###  2.2. Adversarial Attacks and Neural Networks Verification Problem

Given a neural network $\mathbf{F}$ and a reference point $x$, adversarial
attacks aim to search for a point $x^{\prime}$ that is geometrically close to
the reference point $x$ such that $x^{\prime}$ and $x$ belong to different
classes. Here, we use the canonical specification, that is, we want to search
in the local neighborhoods ($L_{\infty}$ norm balls) of $x$, formally denoted
as $B(x,\epsilon):=\\{x^{\prime}\mid||x-x^{\prime}||_{\infty}\leq\epsilon\\}$,
where $\epsilon$ is the radius. For certain $\epsilon$, given we know $x$
belongs to class $j$, we say an adversarial point is found if:

(1) $\displaystyle\exists x^{\prime}\in B(x,\epsilon)\quad\exists i\in
C\quad\mathbf{F}_{i}(x^{\prime})-\mathbf{F}_{j}(x)>0$

In practice, the change from the original data $x$ to adversarial data
$x^{\prime}$ should be imperceptible, so they are more likely to be recognized
as the same class/label from a human perspective. There are also metrics other
than the $L_{\infty}$ norm to represent the ”similarity” between $x$ and
$x^{\prime}$, such as the $L_{0}$ and $L_{2}$ norms (Xu et al., 2020).
However, almost all of them fall into the local neighborhood specification
paradigm. This is different from the NAP specification, as we will discuss
later.

Neural networks have been shown to be vulnerable to adversarial attacks. Even
imperceptible changes could easily alter the predicted outcome. This
highlights the importance of neural network verification. The neural network
verification problem can be seen as the flip side of adversarial attacks. When
it can be formally proven that no adversarial point exists in $B(x,\epsilon)$,
the neural network verification problem is considered solved. Formally, we
want to verify:

(2) $\displaystyle\forall x^{\prime}\in B(x,\epsilon)\quad\forall i\neq
j\quad\mathbf{F}_{j}(x^{\prime})-\mathbf{F}_{i}(x^{\prime})>0$

For a simpler presentation, we assume that $\mathbf{F}(x)$ is a binary
classifier. For any given specification, $\mathbf{F}(x)\geq 0$ indicates that
the model is verified; otherwise, we can find an adversarial example. Solving
such a problem is known to be NP-hard (Katz et al., 2017), and current state-
of-the-art approaches rely on specialized solvers. The difficulty escalates
significantly as the number of neurons in neural networks increases, limiting
successful verifications to only very small neural networks. Therefore,
achieving scalability in verification remains an ongoing challenge.

###  2.3. Neuron Abstractions and Neural Activation Patterns

To better discuss robustness verification using NAP specifications, we first
introduce the relevant concepts of neuron abstractions, neuron abstraction
functions, and neural activation patterns.

#### Neuron Abstractions

Given a neural network $N$, for an arbitrary internal neuron $N_{i,l}$ where
$0\leq i\leq d_{l}$ and $1\leq l\leq L-1$, its post-activation value
$\hat{z}_{i}^{(l)}(x)$ can be abstracted into finite states. Formally, this
can be viewed as a mapping from $\mathbb{R}$ to $\mathbb{S}$, where
$\mathbb{S}$ represents a set of abstraction states
$\\{s_{1},s_{2},\ldots,s_{n}\\}$. As we focus on the ReLU activation function
in this paper, a simple and natural abstraction is a binary abstraction, which
consists of two states $s_{0}$ and $s_{1}$, where $s_{0}:=0$ and
$s_{1}:=(0,\infty)$. $s_{0}$ and $s_{1}$ are often referred to as deactivation
and activation states, which also serve as the neuron’s characteristics from a
statistical point of view. In addition, we can further abstract these two
states to a unary state $s_{*}:=[0,\infty)$, where the interval covers the
entire range of post-activation. This is essentially an identity mapping of
$\hat{z}_{i}^{(l)}(x)$. It means that the neurons can be in either state
$s_{0}$ or state $s_{1}$. Formally, we introduce a partial order $\preceq$
among the states. $s_{0}\preceq s_{*}$ and $s_{1}\preceq s_{*}$ indicates that
$s_{*}$ is an abstraction of $s_{0}$ and $s_{1}$, and that $s_{0}$ and $s_{1}$
are refinements of $s_{*}$. Clearly, $s_{*}\preceq s_{*}$. For convenience, we
omit $s$ in representation and use $\mathbf{0}$, $\mathbf{1}$, and
$\mathbf{*}$ to refer to these abstractions respectively.

###### Definition 2.1 (Neuron Abstraction Function).

Given a neural network $N$ and the abstraction state set $\mathbb{S}$. A
neuron abstraction function is the mapping
$\mathcal{A}:N\rightarrow\mathbb{S}$. Formally, for an arbitrary neuron
$N_{i,l}$ where $0\leq i\leq d_{l}$ and $1\leq l\leq L-1$, the function
abstracts $N_{i,l}$ to some state $s_{k}\in\mathbb{S}$, i.e.,
$\mathcal{A}(N_{i,l})=s_{k}$.

The above characterization of neuron abstraction , it does not instruct us on
how to perform binary abstraction in the absence of neuron values. Thus, we
include the input(s) $x$ or $X$ as a new parameter in $\mathcal{A}$, and it is
omitted when the context is clear. Here, we discuss three types of
$\mathcal{A}$: the unary abstraction function function $\dot{\mathcal{A}}$,
the binary abstraction function $\ddot{\mathcal{A}}$, and the statistical
abstraction function $\widetilde{\mathcal{A}}$.

#### The unary $\dot{\mathcal{A}}$ function

The unary abstraction function always maps all inputs to the coarsest state
$\mathbf{*}$. Formally:

(3) $\displaystyle\dot{\mathcal{A}}(N_{i,l},x)=\mathbf{*}$

#### The binary $\ddot{\mathcal{A}}$ function

When an input $x$ is passed through an internal neuron $N_{i,l}$, we can
easily determine the binary abstraction state of $N_{i,l}$ based on its post-
activation value $\hat{z}_{i}^{(l)}(x)$. This motivates us to define the
binary abstraction function as follows:

(4)
$\displaystyle\ddot{\mathcal{A}}(N_{i,l},x)=\begin{cases}\mathbf{0}&\text{if
}\hat{z}_{i}^{(l)}(x)=0\\\ \mathbf{1}&\text{if }\hat{z}_{i}^{(l)}(x)>0\\\
\end{cases}$

#### The statistical $\widetilde{\mathcal{A}}$ function

The binary $\ddot{\mathcal{A}}$ function is limited in calculating a single
input, and meets a challenge when multiple inputs come into play, as two
distinct inputs may lead to disagreements in a neuron’s abstraction state. We
then approach this problem statistically by introducing the
$\widetilde{\mathcal{A}}$ function defined as follows:

(5)
$\displaystyle\widetilde{\mathcal{A}}(N_{i,l},X)=\begin{cases}\mathbf{0}&\text{if
}\frac{|\\{x_{j}|\ddot{\mathcal{A}}(N_{i,l},x_{j})=\mathbf{0},\text{ }x_{j}\in
X\\}|}{|X|}\geq\delta\\\ \mathbf{1}&\text{if
}\frac{|\\{x_{j}|\ddot{\mathcal{A}}(N_{i,l},x_{j})=\mathbf{1},\text{ }x_{j}\in
X\\}|}{|X|}\geq\delta\\\ \mathbf{*}&\text{otherwise}\\\ \end{cases}$

where $\delta$ is a real number from $[0,1]$, and $X$ represents a set of
inputs, i.e., $X:=\\{x_{1},x_{2},...,x_{n}\\}$. The parameter $\delta$
represents an error ratio to accommodate possible disagreements on neuron
states between multiple inputs. Intuitively, the introduction of $\delta$
allows multiple inputs $x_{1},...,x_{n}$ to vote on a neuron’s state. For
instance, when $\delta$ is set to 0.99, then 99% or more of the inputs must
agree that a neuron is activated for the neuron to be in the $\mathbf{1}$
state.

(a) A simple 2x2 fully connected neuron network.

(b) A subset of the NAP $\mathcal{P}$ family forms a binary tree. Each child
subsumes its parent, and the root is the most abstracted NAP. The leaf node
represents the most refined NAPs, where each neuron is either $\mathbf{1}$ or
$\mathbf{0}$. From the root, the tree is spanned by abstracting each neuron in
an order of $N_{0,1},N_{1,1},N_{0,2},N_{1,2}$. Setting a different order will
create a different tree of NAPs.

Figure 2. A simple 2x2 fully connected neural network and a subset of its NAP
in a binary tree structure.

###### Definition 2.2 (Neural Activation Pattern).

Given a neural network $N$ and a neuron abstraction function $\mathcal{A}$. A
neural activation pattern (NAP) $P$ is a tuple that consists of the
abstraction state of all neurons in $N$. Formally,
$P:=\langle\mathcal{A}(N_{i,l})\text{ }|\text{ }N_{i,l}\in
N,\mathcal{A}\in\\{\ddot{\mathcal{A}},\dot{\mathcal{A}}\\}\rangle$, also
denoted as $\mathcal{A}(N)$. The neuron $N_{i,l}$’s abstraction state
specified by NAP $P$ is represented as $P_{i,l}$, i.e.,
$P_{i,l}=\mathcal{A}(N_{i,l})$.

#### Partially ordered NAP

We denote the power set of NAPs in $N$ as $\mathcal{P}$. The number of all
possible NAPs in $N$ scales exponentially as the number of neurons increases.
For such a large set, if we aim to find the minimal NAP — the central problem
in this work, we first have to establish an order so that NAPs can be
compared. To this end, we define the following partial order:

###### Definition 2.3 (Partially ordered NAP).

For any given two NAPs $P,P^{\prime}\in\mathcal{P}$, we say $P^{\prime}$
subsumes $P$ if, for each neuron $N_{i,l}$, its state in $P$ is an abstraction
of that in $P^{\prime}$. Formally, this can be defined as:

(6) $\displaystyle P^{\prime}\preccurlyeq P\text{ }\iff\text{
}P^{\prime}_{i,l}\preceq P_{i,l}\text{ }\text{ }\forall N_{i,l}\in N$

Moreover, two NAPs $P,P^{\prime}$ are equivalent if $P\preccurlyeq P^{\prime}$
and $P^{\prime}\preccurlyeq P$.

To give a concrete example, Figure 2(b) depicts a subset of NAPs of a simple
neural network consisting of 2 hidden layers and 4 neurons, as presented in
Figure 2(a).

It is interesting to see that a subset of the NAP $\mathcal{P}$ family can
form a complete binary tree given an order of abstraction in neurons. In this
example, we use the order of $N_{0,1},N_{1,1},N_{0,2},N_{1,2}$. Setting a
different order will create a different tree of NAPs. The root of the tree is
the coarsest NAP $\langle\mathbf{*},\mathbf{*},\mathbf{*},\mathbf{*}\rangle$.
Increasing the depth means that $\ddot{\mathcal{A}}$ applies to more neurons,
and when reaching the leaf node, all neurons have been abstracted by
$\ddot{\mathcal{A}}$. The leaf nodes represent the most refined NAPs, and
there are $2^{|N|}$ of them in total. In addition, each child node always
subsumes its parent. By transitivity, a leaf node always subsumes its
ancestors along the path. For instance,
$\langle\mathbf{1},\mathbf{0},\mathbf{1},\mathbf{0}\rangle\preccurlyeq\langle\mathbf{1},\mathbf{0},\mathbf{1},\mathbf{*}\rangle\preccurlyeq\langle\mathbf{1},\mathbf{0},\mathbf{*},\mathbf{*}\rangle\preccurlyeq\langle\mathbf{*},\mathbf{*},\mathbf{*},\mathbf{*}\rangle$.
However, the children under the same parent are not comparable. For instance,
$\langle\mathbf{1},\mathbf{0},\mathbf{*},\mathbf{*}\rangle\mathrel{\ooalign{$\preccurlyeq$\cr\kern
1.2pt$\mathrel{\raisebox{-0.95pt}{$\rotatebox[origin={c}]{-315.0}{\scaleobj{0.55}{-}}$}}$}}\langle\mathbf{1},\mathbf{1},\mathbf{*},\mathbf{*}\rangle$.
This is because these NAPs sit on different branches formed by splitting
certain ReLUs.

#### Region Outlined by NAPs

One key requirement for verification specification is its ability to represent
a specific region within the input space.

For the canonical local neighbor specifications, these specifications define
$L_{\infty}$ norm balls using explicit formulas like
$B(x,\epsilon):=\\{x^{\prime}\mid||x-x^{\prime}||_{\infty}\leq\epsilon\\}$. On
the other hand, NAP specifications outline certain regions in the input space
implicitly. We define the region specified by $P$ as $R_{P}$ which is a set of
inputs whose activation pattern subsumes the given NAP $P$. Formally, we have
$R_{P}:=\\{x\mid{\mathcal{A}(N,x)\preccurlyeq P}\\}$. To provide a concrete
example, Figure 3 illustrates the NAP family of the simple neural network in
Figure 2(a). These NAPs essentially correspond to regions bounded by
hyperplanes created by neurons. The most refined NAPs correspond to individual
linear regions from (1) to (11). For example. linear region (9) represents
$\langle\mathbf{0},\mathbf{1},\mathbf{1},\mathbf{1}\rangle$. Since the
coarsest state $\mathbf{*}$ abstracts the binary states $\mathbf{0}$ and
$\mathbf{1}$, a NAP with more $\mathbf{*}$ covers a larger region in the input
space, and this region can be concave. Take the NAP
$\langle\mathbf{*},\mathbf{*},\mathbf{1},\mathbf{*}\rangle$ as an example; it
corresponds to the union of linear regions (1), (5), (7), (9), and (10). It is
interesting to note that the number of linear regions is less than the size of
the NAP family. Similar findings have been reported in (Geng et al., 2022;
Hanin and Rolnick, 2019a, b).

Figure 3. Linear regions are shattered by the simple 2X2 neural network. Each
linear region corresponds to a most refined NAP, but not necessarily vice
versa. More abstracted NAPs are formed by ignoring lines/hyperplanes created
by neurons.

###  2.4. NAP Specifications for Robustness Verification

This subsection illustrates how NAP specifications can be utilized for
robustness verification. We discuss how the abstraction states of neurons can
serve as signatures of distinct classes with the introduction of the class NAP
definition.

###### Definition 2.4 (Class NAP).

In a classification task with the class set $C$, for any class $c\in C$, a
class NAP $P^{c}$ is a NAP comprising abstract states outputted by an
abstraction function given $X_{c}$, where $X_{c}$ denotes the set of inputs
belonging to class $c$. Formally,
$P^{c}:=\langle\mathcal{A}(N_{i,l},X_{c})\mid N_{i,l}\in
N,\mathcal{A}\in\\{\widetilde{\mathcal{A}},\dot{\mathcal{A}}\\}\rangle$. The
power set of $P^{c}$ is denoted as $\mathcal{P}^{c}$.

Recall that robustness verification can be thought of as proving that no
adversarial examples exist in the local neighbourhoods of some reference point
$x$. Intuitively, for NAP specifications, it is equivalent to show that no
adversarial examples exist in the class NAP $P^{c}$; in other words, inputs
exhibiting the NAP $P^{c}$ must be predicted as class $c$. Geng et al. (2023)
argues that class NAPs must satisfy several essential requirements to qualify
as NAP specifications. And finding qualified NAP specifications implies the
underlying robustness problem is verified. We formally frame these
requirements into the following properties:

#### The non-ambiguity property

Since we want class NAPs to serve as certificates for a certain class, they
must be distinct from each other. Otherwise, there could exist an input that
exhibits two class NAPs, which leads to conflicting predictions. Formally, we
aim to verify the following:

(9) $\displaystyle\forall x\quad\forall c_{1},c_{2}\in C\text{ s.t. }c_{1}\neq
c_{2}\quad\mathcal{A}(N,x)\preccurlyeq
P^{c_{1}}\Longrightarrow\mathcal{A}(N,x)\mathrel{\ooalign{$\preccurlyeq$\cr\kern
1.2pt$\mathrel{\raisebox{-0.95pt}{$\rotatebox[origin={c}]{-315.0}{\scaleobj{0.55}{-}}$}}$}}P^{c_{2}}$

From a geological perspective, there must be no overlaps between class NAPs.
In other words, it is also equivalent to verifying:

$\forall c_{1},c_{2}\in C\text{ s.t. }c_{1}\neq c_{2}\quad
R_{P^{c_{1}}}\bigcap R_{P^{c_{2}}}=\emptyset$

We empirically observe that successful models, particularly neural networks
that have achieved high accuracy in classification tasks, naturally exhibit
this property. Because successful models tend to avoid confusion in
predictions, their class NAPs are usually very distinct from each other.

#### The NAP robustness property

To serve as NAP specifications, class NAPs $P^{c}$ ensure that if an input
exhibits it, i.e., $\mathcal{A}(N,x)\preccurlyeq
P,\mathcal{A}\in\\{\ddot{\mathcal{A}},\dot{\mathcal{A}}\\}$, the input must be
predicted as the corresponding class $c$. Formally, we have:

(10) $\displaystyle\forall x\in R_{P^{c}}\quad\forall k\in C\text{ s.t. }k\neq
c\quad\mathbf{F}_{c}(x)-\mathbf{F}_{k}(x)>0$

in which

(11) $\displaystyle R_{P^{c}}=\\{x\mid{\mathcal{A}(N,x)\preccurlyeq P^{c}}\\}$

In contrast to canonical $L_{\infty}$ norm balls, class NAPs are more flexible
in terms of size and shape. Additionally, there is no need to specify a
reference point, since the locations of potential reference points are also
encoded by class NAPs. However, it is possible that no class NAP $P^{c}$ in
$\mathcal{P}^{c}$ satisfies this property. This can be mitigated by meeting
the subsequent weaker property.

#### The NAP-augmented robustness property

Instead of relying solely on class NAPs as specifications, local neighbours
can still be employed in conjunction for verification. This hybrid form of
specification has several advantages: 1) It narrows down the scope of
verifiable regions when no class NAPs can meet the NAP robustness property; 2)
NAP constraints essentially fix ReLU states, refining the search space for
verification tools; 3) It focuses on the verification of valid test inputs
rather than adversarial examples. Formally, this property can be stated as:

(12) $\displaystyle\forall x^{\prime}\in B(x,\epsilon)\bigcap
R_{P^{c}}\quad\forall k\in C\text{ s.t. }k\neq
c\quad\mathbf{F}_{c}(x)-\mathbf{F}_{k}(x)>0$

in which

(13) $\displaystyle
B(x,\epsilon)=\\{x^{\prime}\mid||x-x^{\prime}||_{\infty}\leq\epsilon\\}\quad
R_{P^{c}}=\\{x^{\prime}\mid{\mathcal{A}(N,x^{\prime})\preccurlyeq P^{c}}\\}$

To summarize, we state that a class NAP can serve as a NAP specification if it
satisfies either the NAP robustness property or the NAP-augmented robustness
property. Clearly, the former property is stronger, and it is possible that we
can’t find a class NAP $P^{c}$ in $\mathcal{P}^{c}$ to satisfy this property.
Fortunately, we can always find NAPs that satisfy the latter property by
narrowing the verifiable region using additional $L_{\infty}$ norm ball
specifications. Moreover, NAP specifications can be easily encoded with most
of the state-of-the-art verification tools such as Marabou. In this paper, we
will not dive into NAP encodings. Interested readers can refer to Geng et al.
(2023) for more details.

##  3\. The minimal NAP specification problem

In this section, we formulate the problem of learning minimal NAP
specifications and present two naive approaches for solving this problem.
Since our approaches require interactions with verification tools, we begin by
introducing relevant notations describing the relationships between NAPs and
verification tools.

Figure 4. A DAG representing all possible NAPs, with green nodes signifying
they can serve as a specification, while red nodes indicate they cannot.
Within each node, a black circle means the corresponding neuron is abstracted
by $\widetilde{\mathcal{A}}$, whereas the white circle means it is abstracted
by $\dot{\mathcal{A}}$. Thus, the top node represents the coarsest NAP, while
the bottom node entails the most refined one. Our goal is to find the NAP that
resides in the green nodes while its size is minimal.

###  3.1. Problem Formulation

Let $(\mathcal{P}^{c},\preccurlyeq)$ be a partially ordered set corresponding
to a family of class NAPs regarding some class $c\in C$. For simplicity, we
omit the superscript $c$ and refer to class NAPs simply as NAPs when the
context is clear. We assume we have access to a verification tool,
$\mathcal{V}:\mathcal{P}\to\\{0,1\\}$, which maps a class NAP
$P\in\mathcal{P}$ to a binary set. Here, $\mathcal{V}(P)=1$ denotes a
successful verification of the underlying robustness query, while 0 indicates
the presence of an adversarial example. From an alternative perspective,
$\mathcal{V}(P)=1$ also signifies that $P$ is a NAP specification, i.e., it
satisfies NAP(-augmented) robustness properties; whereas $\mathcal{V}(P)=0$
implies the opposite.

It is not hard to see that $\mathcal{V}$ is monotone with respect to the NAP
family $(\mathcal{P},\preccurlyeq)$. Given $P\preccurlyeq P^{\prime}$ and
$\mathcal{V}(P^{\prime})=1$, it follows that $\mathcal{V}(P)=1$. However,
given $P\preccurlyeq P^{\prime}$ and $\mathcal{V}(P)=1$, we cannot determine
$\mathcal{V}(P^{\prime})$. In other words, refining a NAP (by increasing the
number of neurons abstracted to $\mathbf{0}$ or $\mathbf{1}$) can only enhance
the likelihood of successful verification of the underlying robustness query.

###### Definition 3.1 (The minimal NAP specification problem).

Given a family of NAPs $\mathcal{P}$ and a verification tool $\mathcal{V}$,
the minimal NAP specification problem is to find a NAP $P$ such that

$\underset{P\in\mathcal{P},\mathcal{V}(P)=1}{\arg\min}|P|$

where $|P|$ is defined as the size of $P$, representing the number of neurons
that are abstracted to the $\mathbf{0}$ or $\mathbf{1}$, i.e.,
$|\\{N_{i,l}\mid P_{i,l}=\mathbf{0}\text{ or }\mathbf{1}\\}|$. The (largest)
minimal NAP specification’s size is denoted as $s$.

When $P$ is minimal, it implies that for any NAP $P^{\prime}$ that is strictly
more coarse than $P$, $\mathcal{V}(P^{\prime})=0$. Formally, this can be
expressed as: $\forall P\preccurlyeq P^{\prime},P^{\prime}\neq
P:\mathcal{V}(P^{\prime})=0$. Thus, there could exist multiple minimal NAP
specifications. In such cases, we only need to choose one of them. On the
other hand, it is possible that even the most refined NAPs cannot verify the
robustness query. In such cases, we claim that no minimal NAP specifications
exist. Additionally, since the computation using verification tools is usually
expensive, we are interested in methods that efficiently find a minimal NAP
specification, i.e., minimizing the number of calls to $\mathcal{V}$.

We present two naive approaches to solving the problem. Since these approaches
involve refining and coarsening the NAP, we will first formally define these
two actions.

#### Refine and Coarsen Action of NAP

Recall our definition of NAP, the coarsest NAP is the one using
$\dot{\mathcal{A}}$ to abstract each neuron in $N$. We denote this NAP as
$\dot{P}:=\langle\dot{\mathcal{A}}(N_{i,l})\text{ }|\text{ }N_{i,l}\in
N\rangle$. $\dot{P}$ is the smallest NAP with $|\dot{P}|=0$. In addition, we
define the most refined NAP as the one that applies $\widetilde{\mathcal{A}}$
to abstract each neuron in $N$. We denote it as
$\widetilde{P}:=\langle\widetilde{\mathcal{A}}(N_{i,l})\text{ }|\text{
}N_{i,l}\in N\rangle$. $\widetilde{P}$ is the largest NAP with size with
$|\widetilde{P}|\leq|N|$. Clearly, $\widetilde{P}\preccurlyeq\dot{P}$. Given
any NAP $P$, if we want to refine $P$ through a specific neuron $N_{i,l}$, we
apply the $\widetilde{\mathcal{A}}$ function to $N_{i,l}$. We denote this
refinement action as $\widetilde{\Delta}(N_{i,l})$. This action will either
increase or leave unchanged $|P|$. Similarly, we denote the coarsen action as
$\dot{\Delta}(N_{i,l})$. This action will either decrease or leave unchanged
$|P|$. We present the semantics of these actions as follows:

$P\vdash\cdot\Downarrow P$

$P\vdash\Delta_{1}\Downarrow P^{\prime}$ $P^{\prime}\vdash\Delta_{2}\Downarrow
P^{\prime\prime}$ $P\vdash\Delta_{1};\Delta_{2}\Downarrow P^{\prime\prime}$

$P_{i,l}=\mathbf{*}$ Refine
$P\vdash\widetilde{\Delta}(N_{i,l})\Downarrow\widetilde{\mathcal{A}}(N_{i,l})\cup
P\setminus P_{i,l}$ $P_{i,l}\in\\{\mathbf{0},\mathbf{1}\\}$ Coarsen
$P\vdash\dot{\Delta}(N_{i,l})\Downarrow\dot{\mathcal{A}}(N_{i,l})\cup
P\setminus P_{i,l}$

where $P,P^{\prime},P^{\prime\prime}$ are from the NAP family $\mathcal{P}$,
and $N$ is the underlying neural network. $\Delta_{1}$ and $\Delta_{2}$ are
any two sequences of refine and coarsen actions.

###  3.2. The Refine Approach

Conceptually, the Refine approach iteratively increases the number of refined
neurons in NAP $P$ until $\mathcal{V}(P)=1$, i.e., $P$ is able to prove the
underlying robustness query. In other words, we gradually increase the size
parameter $k$ and iterate over each NAP $P$ of size $k$ to check if
$\mathcal{V}(P)=1$, as illustrated in Algorithm 1. To determine if a solution
to the problem exists, we first check if the most refined NAP can succeed in
verification. We proceed to iterative refinement only if
$\mathcal{V}(\widetilde{P})=1$. However, the algorithm is not efficient and
requires $2^{|N|}-1$ calls to $\mathcal{V}$ in the worst case, as proven in
Theorem 3.2. Please refer to the proof in Appendix A. Therefore Refine is only
practical when the search space of the NAP family $\mathcal{P}$ is small.

######  Theorem 3.2.

The algorithm Refine returns a minimal NAP specification with
$\mathcal{O}(2^{|N|})$ calls to $\mathcal{V}$.

###  3.3. The Coarsen Approach

In contrast to the Refine approach, the Coarsen approach starts from the most
refined NAP and then gradually coarsens it. We first check if the problem is
well-defined by verifying if the most refined NAP $\widetilde{P}$ succeeds in
verification. Then, for each neuron, we attempt to coarsen it using
$\dot{\mathcal{A}}$; if the resulting NAP no longer verifies the query, we
refine it back using $\widetilde{\mathcal{A}}$; otherwise, we keep the
coarsened NAP. We describe the above procedure in Algorithm 2. The algorithm
could require $|N|$ calls to $\mathcal{V}$ in the worst case, as proven in
Theorem 3.3. Please refer to the proof in Appendix A.

######  Theorem 3.3.

The algorithm Coarsen returns a minimal NAP specification with
$\mathcal{O}(|N|)$ calls to $\mathcal{V}$.

1

Input: The neural network $N$

Output: A minimal NAP specification $P$

2

3Function  _Refine(N)_

4 $P\leftarrow\widetilde{\mathcal{A}}(N)$

5 if  _$\mathcal{V}(P)==0$_ then

return $None$ ;

/* Return None if even the most refined NAP fails verification */

6

7 else

8 for  _$k$ from 1 to $|N|$_ do

$P\leftarrow\dot{\mathcal{A}}(N)$

/* Refinement starts from the coarsest NAP $\dot{P}$ */

$K\\_comb\leftarrow$ $Pick\\_K\\_Neurons(k,N)$

/* Returns all combinations of size k */

9 for  _$comb\textbf{ in }K\\_comb$_ do

10 for  _$N_{i,l}\textbf{ in }comb$_ do

$P\leftarrow\widetilde{\Delta}(N_{i,l})$

/* Refine neurons in the chosen combination */

11

12 if  _$|\mathcal{V}(P)|==1$_ then

return $P$

/* Found the minimal NAP */

13

14

15

16

17

Algorithm 1 refine

Input: The neural network $N$

Output: A minimal NAP specification $P$

1 Function  _Coarsen(N)_

2 $P\leftarrow\widetilde{\mathcal{A}}(N)$

3 if  _$\mathcal{V}(P)==0$_ then

return $None$ ;

/* Return None if the most refined NAP fails verification */

4

5 else

6 for  _$N_{i,l}$ in $N$_ do

$P\leftarrow\dot{\Delta}(N_{i,l})$ ;

/* Try to abstract this neuron using $\dot{\Delta}$ */

7 if  _$\mathcal{V}(P)==0$_ then

$P\leftarrow\widetilde{\Delta}(N_{i,l})$ ;

/* Refine the neuron back if the verification fails */

8

9

10 return $P$;

11

Algorithm 2 Coarsen

##  4\. Verification Free Approaches

While the Refine and Coarsen algorithms can find minimal NAP specifications
with correctness guarantees, their inefficiency poses challenges with the
verification of large neural networks. To address this issue, we introduce two
efficient approaches for estimating minimal NAP specifications without
requiring expensive calls to the verification tool. Unlike verification-based
approaches, these estimation methods are deeply linked to mandatory neurons, a
key concept in dissecting the minimal NAP specification problem, as discussed
below.

###### Definition 4.1 (Mandatory neuron).

A neuron $N_{i,l}\in N$ is considered mandatory if it cannot be coarsened to
$\mathbf{*}$ in any minimal NAP specification. We denote the set of all
mandatory neurons as $M$, defined by:

$M=\\{N_{i,l}\mid P_{i,l}\in\\{\mathbf{0},\mathbf{1}\\},P\textit{ is
minimal}\\}$

Note that $M$ is the union of the set of mandatory neurons from all minimal
NAP specifications. It follows that $|M|\geq s$, where $s$ denotes the size of
the largest minimal NAP specification.

The minimal NAP specification problem can be solved trivially if we gain
access to $M$. Thus, our verification-free approaches are designed to
determine mandatory neurons and estimate $M$. To better understand these our
approaches, we first discuss the properties of mandatory neurons. Recall that
verifying a robustness query given a NAP specification $P$ is equivalent to
showing that $\mathbf{F}(x)\geq 0$ for input $x$ in region $R_{P}$. Thus, the
necessary conditions of a mandatory neuron $N_{i,l}$ can be written as
follows:

  1. (1)

If $N_{i,l}$ is in state $\mathbf{0}$, it implies when
$\hat{z}_{i}^{(l)}(x)=0,\mathbf{F}(x)\geq 0$. In addition, $\exists x\text{
s.t. }\hat{z}_{i}^{(l)}(x)>0,\mathbf{F}(x)<0$.

  2. (2)

If $N_{i,l}$ is in state $\mathbf{1}$, it implies $\forall x\text{ s.t.
}\hat{z}_{i}^{(l)}(x)>0,\mathbf{F}(x)\geq 0$. In addition, when
$\hat{z}_{i}^{(l)}(x)=0,\mathbf{F}(x)<0$.

As for non-mandatory neurons in $P$, since they can be coarsened to
$\mathbf{*}$, it implies $\mathbf{F}(x)\geq 0$ regardless of the value of
$\hat{z}_{i}^{(l)}(x)$. Formally, this can be written as: If $N_{i,l}$ is in
state $\mathbf{0}$ or $\mathbf{1}$, it implies that $\forall
x,\mathbf{F}(x)\geq 0$. In our current approaches, including the Refine and
Coarsen algorithms, we rely on interaction with the verification tool
$\mathcal{V}$ to identify mandatory neurons. Since calls to $\mathcal{V}$ are
typically computationally expensive, it would be advantageous to estimate $M$
in a more cost-effective manner. This motivates us to study the following two
verification-free approaches.

###  4.1. Adversarial-guided Prune

We first introduce Adversarial_Prune to identify mandatory neurons.
Intuitively, it attempts to show a neuron $N_{i,l}$ is mandatory by providing
an adversarial example $x^{\prime}$ exists.

When an adversarial example $x^{\prime}$ is found, it immediately indicates
that the NAP $\ddot{\mathcal{A}}(N,x^{\prime})$ fails the verification, i.e.,
$\mathcal{V}(\ddot{\mathcal{A}}(N,x^{\prime}))=0$. Moreover, it also implies
that any NAP subsumed by $\ddot{\mathcal{A}}(N,x^{\prime})$ fails
verification. For instance, suppose an adversarial example $x^{\prime}$ is
found for a simple one-layer four-neuron neural network and
$\ddot{\mathcal{A}}(N,x^{\prime})$ is
$\langle\mathbf{1},\mathbf{0},\mathbf{1},\mathbf{0}\rangle$. We can infer that
NAPs like $\langle\mathbf{1},\mathbf{0},\mathbf{1},\mathbf{*}\rangle$,
$\langle\mathbf{1},\mathbf{0},\mathbf{*},\mathbf{*}\rangle$,
$\langle\mathbf{1},\mathbf{*},\mathbf{*},\mathbf{0}\rangle$, and
$\langle\mathbf{1},\mathbf{0},\mathbf{*},\mathbf{0}\rangle$ fail the
verification. This information is particularly useful when determining if a
neuron is mandatory. For example, if we know that NAP
$P:=\langle\mathbf{1},\mathbf{0},\mathbf{*},\mathbf{1}\rangle$ is a
specification, i.e., $\mathcal{V}(P)=1$, then we can easily deduce that the
fourth neuron $N_{4,1}$ is mandatory. This is because that coarsening the
fourth neuron would expand $P$ to
$\langle\mathbf{1},\mathbf{0},\mathbf{*},\mathbf{*}\rangle$, which would
include the adversarial example $x^{\prime}$ and thus fail the verification,
as illustrated in Figure 5(a). It is evident that the neuron where $P$ and
$\ddot{\mathcal{A}}(N,x^{\prime})$ disagrees must be mandatory.

However, when the two NAPs disagree on multiple neurons, things become a
little bit different. Suppose the NAP specification $P$ is
$\langle\mathbf{1},\mathbf{1},\mathbf{*},\mathbf{1}\rangle$, i.e.,
$\mathcal{V}(\langle\mathbf{1},\mathbf{1},\mathbf{*},\mathbf{1}\rangle)=1$. We
know
$\mathcal{V}(\langle\mathbf{1},\mathbf{0},\mathbf{*},\mathbf{0}\rangle)=0$ by
the adversarial example $x^{\prime}$. In this case, if we coarsen the second
and fourth neurons, $N_{2,1}$ and $N_{4,1}$, the NAP specification will expand
to $\langle\mathbf{1},\mathbf{*},\mathbf{*},\mathbf{*}\rangle$, which will
cover the $\langle\mathbf{1},\mathbf{0},\mathbf{*},\mathbf{0}\rangle$, thus
failing the verification. In this case, $N_{2,1}$ and $N_{4,1}$ could both be
mandatory neurons or either one of them is mandatory, as illustrated in
Figures 5(b), 5(c), 5(d). So, we simply let $\\{N_{2,1},N_{4,1}\\}$ be the
upper bound of mandatory neurons (learned from $x^{\prime}$). Formerly, given
a NAP $P$, we say a neuron $N_{i,l}$ is in the upper bound of mandatory
neurons $M$ if satisfies the following condition:

  1. (1)

$N_{i,l}$ must be in the binary states, i.e.,
$P_{i,l}\in\\{\mathbf{0},\mathbf{1}\\}$

  2. (2)

There exists $x^{\prime}$ such that $\ddot{\mathcal{A}}(N_{i,l},x^{\prime})$
XORs with $P_{i,l}$, i.e., $\exists x^{\prime}\text{ such that
}\ddot{\mathcal{A}}(N_{i,l},x^{\prime})\oplus P_{i,l}=1$

(a) $N_{4,1}$ is mandatory.

(b) $N_{4,1},N_{2,1}$ are mandatory.

(c) $N_{4,1}$ is mandatory.

(d) $N_{2,1}$ is mandatory.

Figure 5. Geometric interpretation of NAPs on mandatory neurons. The first
subfigure represents the case when the two NAPs disagree on $N_{4,1}$. The
other three subfigures represent the three cases when the two NAPs disagree on
$N_{4,1},N_{2,1}$. Regions colored green pass verification, whereas red
indicates an adversarial example exists. Here, we omit states for
$N_{1,1},N_{3,1}$ in those NAPs for simplicity.

The field of adversarial attacks has been extensively studied, offering a
wealth of methods that we can leverage. These approaches are usually
computationally efficient, making it easy to access a large collection of
adversarial examples. Therefore, we can compute the upper bound of mandatory
neurons efficiently by simply taking the union of upper bounds learned for
each adversarial example, as illustrated in Algorithm 3.

Input: The neural network $N$, the input dataset $X$

Output: A collection of mandatory neurons

1

2Function  _Adversarial_Prune( $N$, $X$)_

3 $Mand\leftarrow\emptyset$ ; $P\leftarrow\widetilde{\mathcal{A}}(N)$

4 for  _$x_{j}$ in $X$_ do

5 $x^{\prime}_{j}\leftarrow Adversarial\\_Attack(x_{j})$

6 for  _$N_{i,l}$ in $N$_ do

7 if  _$P_{i,l}\in\\{\mathbf{0},\mathbf{1}\\}$ and
$\ddot{\mathcal{A}}(N_{i,l},x^{\prime}_{j})\oplus P_{i,l}$_ then

$Mand\leftarrow Mand\cup\\{N_{i,l}\\}$

/* Create mandatory neurons for $x^{\prime}_{j}$ */

8

9

10 return $Mand$

11

Algorithm 3 Adversarial_Prune

###  4.2. Gradient-guided Search

We introduce another approach called Gradient_Search to identify mandatory
neurons. Similar to Adversarial_Prune, Gradient_Search avoids costly
interactions with the verification tool. Instead, it leverages gradient
estimations to analyze the structure of $\mathbf{F}$.

Recall our definition of a neural network in Section 2.1, where the output
$\mathbf{F}(x)$ can be seen as a function of the post-activation value of any
internal neuron $\hat{z}_{i}^{(l)}$. We denote this function as
$\mathbf{F}(\hat{z}(x))$, omitting $i$ and $l$ for simplicity. The function
$\mathbf{F}(\hat{z})$ is non-linear and operates within an input range of
$\hat{z}\in[0,+\infty)$. It is worth noting that the gradient
$\frac{\partial\mathbf{F}}{\partial\hat{z}}$ can provide valuable insights
into the local structure of $\mathbf{F}$. This insight may help determine the
necessity condition of mandatory neurons by checking if there exists a
$\hat{z}$ such that $\mathbf{F}(\hat{z})<0$ for the corresponding neuron. To
be more specific, given some sampled data $\hat{z}_{1},\ldots,\hat{z}_{n}$, we
can compute their corresponding function values
$\mathbf{F}(\hat{z}_{1}),\ldots,\mathbf{F}(\hat{z}_{n})$ along with their
gradients
$\frac{\partial\mathbf{F}}{\partial\hat{z}}|_{\hat{z}_{1}},\ldots,\frac{\partial\mathbf{F}}{\partial\hat{z}}|_{\hat{z}_{n}}$.
Then if there exists a $\hat{z}_{j}$ such that $|\mathbf{F}(\hat{z}_{j})|$ is
sufficiently small, yet the norm of its gradient
$|\frac{\partial\mathbf{F}}{\partial\hat{z}}|_{\hat{z}_{j}}|$ is significantly
large, then it is very likely that $\mathbf{F}$ will go below zero nearby, as
illustrated in Figure 6. Then, if we happen to know that the corresponding
neuron $N_{i,l}$ is in state $\mathbf{0}$, it is highly likely that $N_{i,l}$
is mandatory. Conversely, if a neuron $N_{i,l}$ is in state $\mathbf{1}$, and
we sample an $x$ such that $\hat{z}_{i}^{(l)}=0$ and $\mathbf{F}(x)<0$, we
immediately recognize that the neuron is mandatory. Algorithm 4 presents
pseudocode for estimating whether a neuron is mandatory based on the
discussions above.

Figure 6.  The gradient provides insights into the local structure of
$\mathbf{F}$. When the gradient is large and the function value is small, it
strongly suggests that $\mathbf{F}$ will go below zero nearby.

Input: The neural network $N$, the input dataset $X$, and thresholds $\beta$,
$\gamma$

Output: A collection of mandatory neurons

1

2Function  _Gradient_Search( $N$, $X$, $\beta$, $\gamma$)_

3 $Mand\leftarrow\emptyset$ ; $P\leftarrow\widetilde{\mathcal{A}}(N)$

4 for  _$N_{i,l}$ in $N$_ do

5 for  _$x_{j}$ in $X$_ do

6 $\hat{z}_{j}\leftarrow\hat{z}_{i}^{(l)}(x_{j})$

7 if  _$\hat{z}_{j} >0$ _ then

8 if  _ $|\mathbf{F}(\hat{z}_{j})|<\beta$ and
$|\frac{\partial\mathbf{F}}{\partial\hat{z}_{i}^{(l)}}|_{\hat{z}_{j}}|>\gamma$
and $P_{i,l}==\mathbf{0}$_ then

$Mand\leftarrow Mand\cup\\{N_{i,l}\\}$

/* Neuron is in state $\mathbf{0}$, can’t coarsen */

9

10

11 else

12 if  _$\mathbf{F}(\hat{z}_{j}) <0$ and $P_{i,l}==\mathbf{1}$_ then

$Mand\leftarrow Mand\cup\\{N_{i,l}\\}$

/* Neuron is in state $\mathbf{1}$, can’t coarsen */

13

14

15

16

17 return $Mand$

18

Algorithm 4 Gradient_Search

Both the estimation method Gradient_Search and Adversarial_Prune can be used
together. Taking the intersection of their estimated results may provide us
with a better overall estimate. In addition, the estimated mandatory neurons
can serve as an initial starting point in our statistical versions of the
Refine and Coarsen approaches introduced in Section 5.

Our experimental results regarding these two estimation approaches indicate a
notable trend: neurons from deeper layers are more likely to be mandatory.
This observation aligns with commonly-held beliefs that deeper neurons are
generally linked to high-level feature representation, and thus play a more
important role than shallow neurons in final classification decisions. This
observation leads us to a valuable heuristic: prioritizing deeper neurons over
shallower ones as we iterate through neurons in our implementations of the
Refine and Coarsen algorithms.

##  5\. Statistical Learning Approaches

In this section, we introduce two new algorithms that address the minimal NAP
specification problem. While they share the same overarching concept as refine
and coarsen, these methods employ sampling and statistical learning principles
to efficiently learn a minimal NAP specification. Recall that the set of
mandatory neurons $M$ is the union of all neurons that appears in any minimal
specification and is an upper bound of the largest minimal specification.

###  5.1. The Statistical Refine Approach

Mandatory neurons are crucial for forming NAP specifications, as their binary
states play a critical role in determining the neural network’s robustness
performance. We leverages this property to find mandatory neurons
statistically. To be more specific, suppose we sample some NAPs
$P_{1},P_{2},\ldots,P_{n}$ from the NAP family $\mathcal{P}$. For those NAPs
that qualify as specifications (i.e., $\mathcal{V}(P)=1$), mandatory neurons
should appear more frequently in them than in those NAPs that fail the
verification tool (i.e., $\mathcal{V}(P)=0$).

Based on this insight, we propose an approach called Sample_Refine that relies
on non-repetitive sampling to identify mandatory neurons for solving the
minimal NAP problem. We start with the coarsest NAP and iteratively collect
the most probable mandatory neurons. In every iteration, we sample $k$ NAPs by
refining unvisited neurons with some probability $\theta$. The sampled NAPs
are then fed to the verification tool, and the neuron that appears most
frequently in verifiable NAPs is the most probable mandatory neuron in this
iteration. The neuron is marked as visited, and the process stops when either
we collect $s$ neurons (assuming that $s$ is known), or the current mandatory
neurons form a NAP specification $P$, i.e., $\mathcal{V}(P)=1$. Finally, we
return the learned NAP, obtained by applying $\widetilde{\mathcal{A}}$ to the
collected neurons. The algorithm 5 provides an overview of the above
procedure.

It is worth noting that Sample_Refine doesn’t guarantee correctness, as we may
end up collecting only the $s$ most probable mandatory neurons, which may not
be sufficient to form a specification. Another concern regarding this
algorithm is sampling efficiency, specifically the potential for the number of
samples required to grow exponentially with the size of the minimal NAP
specification $s$. To understand why this is problematic, consider a scenario
where the only minimal NAP specification $P$ consists of all mandatory
neurons; in this case, all $|M|$ neurons must be selected for $P$ to be
learned. If $\theta$ is set to a constant value, then the expected number of
samples needed to obtain the NAP specification is $(\frac{1}{\theta})^{|M|}$.
To address this, we set $\theta=\left(\frac{|M|}{|M|+1}\right)^{|M|}$. This
choice ensures that the sampling efficiency is polynomial in both $|M|$ and
$s$, as proven in Theorem 5.1. Please refer to the proof in the Appendix B. In
addition, Theorem 5.1 also shows that with high probability, a mandatory
neuron will be found with $O(log|N|)$ calls to $\mathcal{V}$.

######  Theorem 5.1.

With probability $\theta=|(\frac{|M|}{|M|+1})|^{|M|}$, Sample_Refine has
$1-\delta$ probability of outputting a minimal NAP specification with
$\Theta\left(|M|^{2}(\log|N|+\log(s/\delta))\right)$ examples each iteration
and $O(s|M|^{2}(\log|N|+\log(s/\delta)))$ total calls to $\mathcal{V}$.

###  5.2. The Statistical Coarsen Approach

The Coarsen algorithm begins with the most refined NAP and progressively
coarsens each neuron until the verification process fails. Enhancing the
algorithm’s performance is possible by coarsening multiple neurons during each
iteration. However, a fundamental question emerges: How do we determine which
set of neurons to coarsen in each round?

We present Sample_Coarsen to answer this question. In this approach, we assume
that each neuron is independent of the others and select neurons to coarsen in
a statistical manner. Specifically, in each iteration, we randomly coarsen a
subset of refined neurons in the current NAP simultaneously to see if the new
NAP can pass verification. We repeat this process until the NAP size reaches
$s$. Algorithm 6 provides the pseudocode for Sample_Coarsen.

Input: The neural network $N$, the probability $\theta$, sample size $k$, and
the size $s$

Output: A minimal NAP specification $P$

1

2Function  _Sample_NAPs( $unvisited$, $\theta$)_

$P\leftarrow\dot{\mathcal{A}}(N)$

/* Use the coarsest NAP as a blank template */

3 for  _$N_{i,l}$ in $unvisited$_ do

4 $rand\leftarrow\text{random}(0,1)$

5 if  _$rand\leq\theta$_ then

$P\leftarrow\widetilde{\Delta}(N_{i,l})$

/* Refine unvisited neurons using $\widetilde{\Delta}$ with probability
$\theta$ */

6

7

8 return $P$

9

10

11Function  _Sample_Refine( $visited$, $\theta$, $k$, $s$)_

12

13 while  _$|visited| <s\text{ and }\mathcal{V}(P)==0$ _ do

14 $unvisited\leftarrow N\setminus visited$

$ctr=dict()$

/* Create a counter for each neuron in $unvisited$ */

15 for  _$\\_$ in $range(k)$_ do

$P\leftarrow Sample\\_NAPs(unvisited,\theta)$

/* Sample $k$ NAPs */

16 for  _$N_{i,l}$ in $unvisited$_ do

17 if  _$P_{i,l}==\widetilde{\mathcal{A}}(N_{i,l})$ and $\mathcal{V}(P)==1$_
then

$ctr[N_{i,l}]$ += 1

/* Count successful NAPs for each neuron */

18

19

20

$N_{mad}\leftarrow\operatorname*{argmax}_{N_{i,l}\in
unvisited}\\{ctr[N_{i,l}]\\}$

/* Pick potential mandatory neuron */

21 $visited\leftarrow visited\cup\\{N_{mad}\\}$

22

23 return $\widetilde{\mathcal{A}}(visited)$

24

25

26$P\leftarrow\widetilde{\mathcal{A}}(N)$

27 if  _$\mathcal{V}(P)==0$_ then

return $None$

/* Return None if the most refined NAP fails verification */

28

29 else

30 if  _heuristics_ then

31 $visited\leftarrow Gradient\\_Search(N)\cap Adversarial\\_Prune(N)$

32 else

$visited\leftarrow\emptyset$

/* Start from the coarsest NAP */

33

34 $Sample\\_Refine(visited,\theta,k,s)$

35

36

Algorithm 5 Sample_Refine

Similar to Sample_Refine, Sample_Coarsen also faces the same challenge related
to sample efficiency. To better illustrate this, suppose a minimal NAP
specification $P$ with size $s$ can be found after one iteration of
refinement. Then, the probability of selecting the exact number of $s$
mandatory neurons in $P$ is $\theta^{s}$. Consequently, if $\theta$ is set to
a constant value, the expected number of samples needed to find the NAP is
$(\frac{1}{\theta})^{s}$. Unlike Sample_Refine, we know the refinement will
always ensure the resulting NAP can pass verification. So, once such a NAP is
learned, we can narrow down the estimated mandatory neurons by an expected
factor of $\theta$. In this way, the expected number of samples and the
expected number of iterations are inversely related, yet their product is the
total number of calls to $\mathcal{V}$. We demonstrate that by setting
$\theta=e^{-\frac{1}{s}}$, we not only make the expected number of samples
polynomial in $s$, but also minimize the total number of calls to
$\mathcal{V}$, as proven in Theorem 5.2. Please refer to the proof in Appendix
B.

######  Theorem 5.2.

With probability $\theta$=$e^{-\frac{1}{s}}$, Sample_Coarsen learns a minimal
NAP specification with $\mathcal{O}(slog|N|)$ calls to $\mathcal{V}$.

Input: The neural network $N$, the probability $\theta$, and the size $s$

Output: A minimal NAP specification $P$

1

2Function  _Sample_Coarsen( $mand\\_neurons$, $\theta$, $s$)_

3 $P\leftarrow\widetilde{\mathcal{A}}(N)$; $mand\\_neurons\leftarrow N$

4 if  _$\mathcal{V}(P)==0$_ then

return $None$

/* Return None if the most refined NAP fails verification */

5

6 else

7 while  _$|P| >s$_ do

8 $P\leftarrow Sample\\_NAPs(mand\\_neurons,\theta)$

9 if  _$\mathcal{V}(P)==1$ _ then

10 $found\\_neurons\leftarrow\emptyset$

11 for  _$N_{i,l}$ in $N$_ do

12 if  _$P_{i,l}==\widetilde{\mathcal{A}}(N_{i,l})$_ then

13 $found\\_neurons\leftarrow found\\_neurons\cup\\{N_{i,l}\\}$

14

$mand\\_neurons\leftarrow found\\_neurons$

/* Reduce search space */

15

16 else

$P\leftarrow Sample\\_Naps(mand\\_neurons,\theta)$

/* Sample a new NAP */

17

18

return $P$

/* Return the minimal NAP of size $s$ */

19

20

21

Algorithm 6 Sample_Coarsen

#### Setting the sample probability $\theta$

Setting $s$ poses a challenge in practice, as we assume that $s$ is always
provided in Sample_Refine and Sample_Coarsen. However, this can be addressed
by dynamically updating $\theta$ based on the result of $\mathcal{V}(P)$
(Liang et al., 2011). With $\theta$ from theorem 5.2, Sample_Coarsen finds a
NAP specification with probability $\left(e^{-1/s}\right)^{s}=e^{-1}$. Recall
that theorem 5.1 state that Sample_Refine finds a NAP specification with
probability $\left(\frac{|M|}{|M|+1}\right)^{|M|}$. The probability approaches
$e^{-1}$ asymptotically. Thus, we aim to set $\theta$ such that the
$Pr(\mathcal{V}(P)=1)=e^{-1}$. Intuitively, if a sampled NAP $P$ is a
specification, we decrease $\theta$ so less neurons will be refined or more
neurons will be coarsened. Similarly, if $P$ is not a specification, $\theta$
needs to be increased.

Given that $\theta\in[0,1]$, we can parameterize it using the Sigmoid function
$\sigma(\lambda)=\left(1+e^{-\lambda}\right)^{-1}$, where
$\lambda\in(-\infty,\infty)$. Since $Pr(\mathcal{V}(P)=1)$ depends on $\theta$
as well, we express it as a function of $\lambda$,
$g(\lambda)=Pr(\mathcal{V}(P)=1)$. Then, setting $Pr(\mathcal{V}(P)=1)=e^{-1}$
can be achieved through the following minimization problem:

(14) $L(\lambda)=\frac{1}{2}(g(\lambda)-e^{-1/s})^{2}$

The loss function $L(\lambda)$ can be minimized by statistical learning using
stochastic gradient descent. With a step size $\eta$, update $\lambda$ using
$\lambda\leftarrow\lambda-\eta\frac{dL}{d\lambda}$. Note that
$\frac{dL}{d\lambda}$ can be expressed as:

(15) ${\frac{dL}{d\lambda}}=(g(\lambda)-e^{-1/s})\frac{dg(\lambda)}{d\lambda}$

Given $g(\lambda)=Pr(\mathcal{V}(P)=1)$, we can replace $g(\lambda)$ with
$\mathcal{V}(P)$ for stochastic gradient update. Additionally, since
$\frac{dg(\lambda)}{d\lambda}>0$, we simply ignore it as its multiplication
effect can be represented by $\eta$. Therefore, the final update rule is given
by:

(16) $\lambda\leftarrow\lambda-\eta(\mathcal{V}(P)-e^{-1})$

##  6\. Volume Estimation of $R_{P}$

Figure 7. Volume Estimation of $R_{P}$ using an orthotope in a 2-dimensional
case. The gray rectangle represents the input space, with the training set
depicted by a collection of data points $+$. The polygon corresponds to some
NAP $P$. Initially, we identify an anchor point, denoted by $+$. Then, we
construct the orthotope, represented by the green rectangle, by extending
upper and lower bounds starting from the anchor point until it extends beyond
$P$.

Conceptually, NAP specifications typically correspond to significantly larger
input regions compared to local neighbourhood specifications. This serves as
the primary motivation for utilizing NAPs as specifications. However, previous
work lacks sufficient justification or evidence to support this claim. In this
section, we propose a simple method for approximating the volume of $R_{P}$,
i.e., the region corresponding to a NAP $P$. This allows us to: 1) quantify
the size difference between $R_{P}$ and $L_{\infty}$ ball specifications; 2)
gain insights into the volumetric change from the most refined NAP
specification to the minimal NAP specification.

Computing the exact volume of $R_{P}$ is at least NP-hard, as determining the
exact volume of a polygon is known to be NP-hard (Dyer and Frieze, 1988).
Moreover, computing the exact volume of $R_{P}$ can be even more challenging
due to its potential concavity. To this end, our method estimates the volume
of $R_{P}$ by efficient computation of an orthotope that closely aligns with
$R_{P}$, as illustrated in Figure 7. We briefly describe it as follows:

#### Finding an anchor point

The first step is to find an anchor point to serve as the center of the
orthotope. Ideally, this anchor point should be positioned close to the center
of $R_{P}$ to ensure a significant overlap between the orthotope and $R_{P}$.
However, computing the actual center of $R_{P}$ is costly. Thus, we look for a
pseudo-center from the training set $X$ that resides in $R_{P}$. This pseudo-
center can be computed by finding the point that uses the smallest
$L_{\infty}$ ball to cover other data points, solved as the following
optimization problem:

$c_{\text{pseudo}}=\underset{x\in R_{P}}{\arg\min}\max_{x^{\prime}\in
R_{P}}\|x-x^{\prime}\|_{\infty}$

where $R_{P}=\\{x\mid\mathcal{A}(N,x)\preccurlyeq P,x\in X\\}$. When $|X|$ is
small, $c_{\text{pseudo}}$ can be computed directly; for larger $|X|$, a
statistical computation strategy is required.

#### Constructing the orthotope

Once the pseudo-center $c_{\text{pseudo}}$ is determined, we want to create an
orthotope around $c_{\text{pseudo}}$ to closely align with $R_{P}$. The
orthotope is constructed by determining pairs of upper and lower bounds
$U^{(i)}$ and $L^{(i)}$ for each dimension $i$. Specifically, $U^{(i)}$ and
$L^{(i)}$ are computed through expansion in two opposite directions from
$c_{\text{pseudo}}$ along dimension $i$ until they extend beyond $R_{P}$. This
expansion can be expressed as:

$\max_{U^{(i)}}\\{x^{\prime}\in
R_{P}\,|\,x^{\prime}:=c_{\text{pseudo}}+U^{(i)}\\}\text{ ;
}\max_{L^{(i)}}\\{x^{\prime}\in
R_{P}\,|\,x^{\prime}:=c_{\text{pseudo}}-L^{(i)}\\}$

Here, $U^{(i)}$ and $L^{(i)}$ represent the upper and lower bounds in
dimension $i$ respectively, originating from $c_{\text{pseudo}}$. These bounds
can be efficiently calculated with binary search.

The choice of the archer point is crucial in our approach. If it is located at
a corner of $R_{p}$, the volume calculation will be highly biased. This can
pose a problem when we seek to understand the volumetric change from the most
refined NAP specification to the minimal NAP specification. Additionally,
using the orthotope as an estimator provides convenience in understanding the
volumetric change simply by examining differences in each input dimension.

##  7\. Evaluation

In this section, we conduct a comprehensive evaluation of our methods for
learning minimal NAP specifications across a range of benchmarks, spanning
from a simple binary classifier to the state-of-the-art image classification
model. We illustrate that minimal NAP specifications usually involve only a
fraction of neurons compared to the most refined NAPs, yet they dramatically
extend the verifiable bounds to several magnitudes larger.

#### Experiment Setup

All experiments in this section were conducted on an Ubuntu 20.04 LTS machine
with 172 GB of RAM and an Intel(R) Xeon(R) Silver Processor. For verification,
we utilized Marabou (Katz et al., 2019), a dedicated state-of-the-art neural
network verifier. We configured a timeout of 10 minutes for each call to the
verification tool. If the timeout is exceeded, the current neuron is retained
in the minimal NAP specification even if its status cannot be determined.

Table 1. Overview of the size of learned minimal NAP specifications using various approaches on the WBC benchmark. The columns represent different labels, while each row corresponds to a different algorithm. —$P$— denotes the size of the learned NAP, and #$\mathcal{V}$ represents the number of calls to $\mathcal{V}$ (”-” indicates not applicable). The remaining columns, train and test, report the percentile ($\%$) of train and test data covered by $P$.  | 0 | 1
---|---|---
| —$P$— | #$\mathcal{V}$ | train | test | —$P$— | #$\mathcal{V}$ | train | test
The $\widetilde{\mathcal{A}}$ function | 102 | - | 78.11 | 81.40 | 93 | - | 87.06 | 80.28
Coarsen | 31 | 102 | 98.22 | 95.35 | 32 | 93 | 99.65 | 94.37
Adversarial_Prune | 61 | - | 81.06 | 88.37 | 54 | - | 87.06 | 80.28
Gradient_Search | 43 | - | 82.84 | 88.37 | 39 | - | 93.37 | 87.32
Sample_Refine | 53 | 187 | 92.43 | 89.37 | 56 | 264 | 89.86 | 88.51
Sample_Coarsen | 42 | 47 | 94.69 | 92.34 | 45 | 41 | 94.15 | 91.52

#### Wisconsin Breast Cancer with Binary Classifier

We conduct our first experiment using a four-layer neural network as a binary
classifier, where each layer consists of 32 neurons. This classifier is
trained on the Wisconsin Breast Cancer (WBC) dataset (William et al., 1995),
representing a decision-critical task where robustness is essential. Our
trained model achieves a test set accuracy of 95.61%. We calculate the most
refined NAP specifications $\widetilde{P}^{0}$ and $\widetilde{P}^{1}$ for
labels 0 and 1 using the statistical abstraction function
$\widetilde{\mathcal{A}}$ with a confidence ratio of $\delta=0.95$. The size
of $\widetilde{P}^{0}$ and $\widetilde{P}^{1}$ are 102 and 93, respectively.
In contrast, the sizes of the minimal NAP specifications learned by the
Coarsen algorithm for labels 0 and 1 are significantly reduced to 31 and 32,
respectively. It is worth mentioning that our estimation approaches provide a
fairly accurate estimate of the mandatory neurons, despite computing rather
loose upper bounds. To be more specific, Adversarial_Prune and Gradient_Search
compute 61 and 43 mandatory neurons for label 0, respectively. Together, they
cover 25 out of the 31 mandatory neurons appearing in the minimal NAP
specification for label 0. For label 1, Adversarial_Prune and Gradient_Search
compute 54 and 39 mandatory neurons, respectively, covering 25 out of the 32
mandatory neurons appearing in the minimal NAP specification for label 1.

Regarding the statistical approaches, Sample_Refine computes NAP
specifications of size 53 and 56 for label 0 and label 1, respectively. This
is achieved while making 187 and 264 calls, respectively. Although these
numbers are quite large, it is expected since it has to sample multiple trials
in each iteration. In contrast, Sample_Coarsen is significantly more
efficient. It can learn NAP specifications of size 42 and 45 for label 0 and
label 1 using only 47 and 41 calls, respectively.

Recall that one of the main motivations for learning the minimal NAP
specifications is their potential to verify larger input regions compared to
the refined NAP specifications. To support this claim, we compute the
percentile of unseen test data that can be verified using these NAPs. We
choose test data as they are sampled from the input space and can be viewed as
a proxy to understand the verifiable bounds of different NAPs. We observe that
the most refined NAP specifications $\widetilde{P}^{0}$ and
$\widetilde{P}^{1}$ can cover 81.40% and 80.28% of the test data for labels 0
and 1, respectively. In contrast, this coverage significantly increases to
95.35% and 94.37% of the test data for the minimal NAP specifications of
labels 0 and 1, respectively. To intuitively understand the extent of change
in verifiable regions from the refined NAP specifications to the minimal NAP
specifications, we also compare their estimated volume of the corresponding
region $R_{P}$. The estimated volumetric changes are substantial, with label 0
experiencing an increase 58324.35 times larger and label 1 showing an increase
3053.53 times larger, respectively. To comprehend this change in each
dimension, Figure 8 illustrates the comparison of verifiable input ranges
between the refined NAP specifications and the minimal NAP specifications for
labels 0 and 1, referencing the anchor point.

(a) Comparing verifiable input ranges for label 0

(b) Comparing verifiable input ranges for label 1

Figure 8. Comparison of verifiable input ranges between the refined NAP
specifications and the minimal NAP specifications for labels 0 and 1 on the
Wisconsin Breast Cancer dataset, with reference to the anchor point. The
minimal NAP specifications enable verification over a larger input range for
all dimensions. Table 2. Overview of the size of learned minimal NAP
specifications on the MNIST benchmark.

| 0 | 1 | 4
---|---|---|---
| —$P$— | #$\mathcal{V}$ | train | test | —$P$— | #$\mathcal{V}$ | train | test | —$P$— | #$\mathcal{V}$ | train | test
The $\widetilde{\mathcal{A}}$ function | 751 | - | 79.50 | 80.51 | 745 | - | 86.01 | 85.11 | 712 | - | 77.54 | 80.24
Coarsen | 480 | 751 | 98.68 | 98.78 | 491 | 745 | 98.90 | 98.59 | 506 | 712 | 98.51 | 97.45
Adversarial_Prune | 618 | - | 83.13 | 71.32 | 630 | - | 79.02 | 76.51 | 699 | - | 82.66 | 84.12
Gradient_Search | 195 | - | 92.1 | 91.80 | 237 | - | 89.73 | 88.39 | 169 | - | 87.59 | 88.51
Sample_Refine | 564 | 4059 | 90.03 | 87.91 | 570 | 3663 | 88.36 | 86.84 | 581 | 4532 | 82.90 | 83.46
Sample_Coarsen | 532 | 33 | 93.19 | 93.01 | 559 | 27 | 94.12 | 93.68 | 562 | 25 | 93.89 | 93.64

#### MNIST with Fully Connected Network

To show that our insights and approaches can be applied to more complicated
datasets and networks, we conduct the second set of experiments using the
mnistfc_256x4 model (VNNCOMP, 2021), a 4-layer fully connected network with
256 neurons per layer trained on the MNIST dataset. We specifically focus on
classes 0, 1, and 4, as the most refined NAPs for other labels either
encounter timeouts or fail the verification. We compute the most refined NAP
specifications $\widetilde{P}^{0}$, $\widetilde{P}^{1}$, and
$\widetilde{P}^{4}$ for labels 0, 1, and 4 using the $\widetilde{\mathcal{A}}$
function with a confidence ratio of $\delta=0.99$. The size of
$\widetilde{P}^{0}$, $\widetilde{P}^{1}$, and $\widetilde{P}^{4}$ are 751, 745
and 712, respectively, which aligns with the results from (Geng et al., 2023).

In contrast, the sizes of the minimal NAP specifications learned by the
Coarsen algorithm for labels 0, 1, and 4 are significantly reduced to 480,
491, and 506, respectively. Moreover, our estimation approaches provide highly
accurate estimates of the mandatory neurons present in minimal NAP
specifications. For instance, considering label 0, Adversarial_Prune and
Gradient_Search identify 618 and 195 mandatory neurons, respectively. And 445
and 160 out of the 480 mandatory neurons presented in the minimal NAP
specification are discovered by Adversarial_Prune and Gradient_Search,
respectively.

In terms of statistical approaches, Sample_Coarsen outperforms Sample_Refine
in both the size of learned NAP specifications and the number of calls made to
$\mathcal{V}$. Specifically, it requires only around 30 calls, while
Sample_Refine makes more than 100 times more calls. It’s interesting to note
that the mandatory neurons presented in the learned minimal NAP specifications
using different algorithms are primarily located within the
$3\textsuperscript{rd}$ and $4\textsuperscript{th}$ layers. This observation
aligns with widely-held beliefs that neurons in deeper layers are typically
responsible for high-level feature representation and thus play a critical
role in making classification decisions.

Moreover, the learned minimal NAP specifications correspond to significantly
larger verifiable regions compared to the refined NAP specifications. Using
the percentile of test data as a metric, the minimal NAP specifications
increase the coverage ratio from 80.51% to 98.78%, 85.11% to 98.59%, and
80.24% to 97.45% for labels 0, 1, and 4, respectively. From the perspective of
estimated volume, the volumetric changes are on the order of $10^{8}$ times
larger.

#### ImageNet with Deep Convolutional Neural Networks

Current verification approaches struggle to scale to state-of-the-art neural
networks such as deep convolutional neural networks, making them inapplicable
for verifying certain critical systems like deep learning-based autonomous
driving software. Consequently, our verification-dependent approaches also
face scalability challenges. However, we can still assess the network’s
robustness from a neuron-centric perspective using our estimation approaches,
an aspect not well-studied in the current literature.

Thus, for the third experiment, we choose a deep convolutional network,
specifically VGG-19 trained on the ImageNet dataset, as the benchmark for
estimating mandatory neurons. We select neurons from fully connected
layers111We leave NAP computation for other layers such as convolutional
layers for future work. of VGG-19, which contains a total of 8192 neurons, to
compute NAPs. The original ImageNet includes 1000 classes with millions of
images. We also narrow our focus to the top five largest classes in ImageNet.
Each class consists of around 1000 training images and 300 test images. Table
3 presents the results of the learned NAP using verification-free approaches.

To show that these estimated mandatory neurons are indeed meaningful, we
employ several approaches from the model interpretability domain such as Grad-
CAM (Selvaraju et al., 2017) and saliency maps (Simonyan et al., 2014a). We
observe a strong correlation between neurons exhibiting high interpretability
under certain metrics and our estimated mandatory neurons computed by
Adversarial_Prune and Gradient_Search. However, we also find that some
mandatory neurons do not seem to participate significantly in
interpretability, yet they are indeed necessary for the robustness of models.
We find this interesting and plan to investigate those neurons in future work.

Although we cannot definitively determine if these NAPs can serve as
specifications, these NAPs do cover significant portions of unseen test data.
For example, the NAP formed by mandatory neurons learned through
Gradient_Search can cover $87.01\%$ of unseen test data. This aspect makes
them a promising basis for computing NAP specifications, especially if
verification tools become accessible for such large models in the future.

Table 3. Overview of the size of learned minimal NAP specifications on the
ImageNet benchmark.

| box_turtle | spiny_lobster | acorn_squash | confectionery | stone_wall
---|---|---|---|---|---
| —$P$— | test | —$P$— | test | —$P$— | test | —$P$— | test | —$P$— | test
The $\widetilde{\mathcal{A}}$ function | 1978 | 39.42 | 1006 | 39.61 | 1003 | 29.23 | 878 | 33.84 | 971 | 31.54
Adversarial_Prune | 1863 | 39.42 | 955 | 39.61 | 823 | 25.68 | 845 | 23.07 | 865 | 39.61
Gradient_Search | 611 | 53.30 | 572 | 87.01 | 301 | 52.40 | 256 | 44.23 | 260 | 54.90

##  8\. Related Work

###  8.1. Neural Network Verification

Neural network verification has attracted much attention due to the
increasingly widespread applications of neural networks in safety-critical
systems. it’s NP-hard nature resulting from the non-convexity introduced by
activation functions (Katz et al., 2017) makes it a challenging task. Thus
most of the existing work on neural network verification focuses on designing
scalable verification algorithms. For instance, while initially proposed
solver-based approaches (Huang et al., 2017b; Ehlers, 2017; Cheng et al.,
2017; Tjeng et al., 2019) were limited to verifying small-scale neural
networks with fewer than 100 neurons, state-of-the-art approaches (Xu et al.,
2021; Wang et al., 2021c; Lu and Kumar, 2019) can verify more complex neural
networks. It is worth mentioning that most existing work adopts local
neighborhood specifications to verify the robustness properties of neural
networks (Shapira et al., 2023). Despite being a reliable measure, using
specifications that define local neighborhood of reference data points may not
cover any test data, let alone generalizing to the verification of unseen test
set data. Yet evidently, being able to verify the neural network on test data
is an important task in real-world applications. The development of NAP
specification (Geng et al., 2023) sheds light on this challenge. While
previous work on NAP specifications proves its effectiveness, it assumes that
all neurons contribute equally to the model’s robustness. In this paper, we
challenge this assumption by demonstrating that only a small fraction of
neurons are crucially related to robustness. This not only allow us study
robustness from the neurons’ perspective but also significantly pushes the
known verifiable boundaries.

###  8.2. Abstract Interpretation

Abstract interpretation (Cousot and Cousot, 1977) is a fundamental concept in
software analysis and verification, particularly for approximating the
semantics of discrete program states. By sacrificing precision, abstract
interpretation typically enables scalable and faster proof finding during
verification (Cousot and Cousot, 2014). Although abstract interpretation for
neural network verification has been proposed and studied in previous
literature (Gehr et al., 2018; Mirman et al., 2018), abstract interpretation
of neural activation patterns for verification is a relatively new field.
Perhaps the most related work from the perspective of abstract interpretation
is learning minimal abstractions (Liang et al., 2011). While our work shares
similarities in problem formulation and statistical approaches, we address
fundamentally different problems. One limitation in our work is that our
abstraction states may be too coarse: value in range $(0,+\infty)$ is
abstracted into one state. This approach could over-approximate neuron
behavior and thus fail to prove certain properties. We observe that neuron
values exhibit different patterns in range for different input classes,
suggesting the potential existence of more abstraction states. We plan to
explore this direction in our future work.

###  8.3. Neural Activation Patterns

Neural activation patterns have commonly been used to understand the internal
decision-making process of neural networks. One popular line of research is
feature visualization (Yosinski et al., 2015; Bäuerle et al., 2022), which
investigates which neurons are activated or deactivated given different
inputs. This is also naturally related to the field of activation maximization
(Bau et al., 2017; Simonyan et al., 2014b; Erhan et al., 2009), which studies
what kind of inputs could mostly activate certain neurons in the neural
network. In this way, certain prediction outcomes may be attributed to the
behavior of specific neurons, thereby increasing the interpretability of the
underlying models. In summary, most of existing works focus on learning
statistical correlations between either NAPs and inputs or NAPs and prediction
outcomes. However, whether such correlations can be trusted or even verified
is not fully studied. To this end, we propose the concept of mandatory neurons
and highlight their importance in the robustness of model predictions. Such
causal links between neurons and prediction outcomes are not only identified
but also verified. We believe this ”identify then verify” paradigm can be
extended to existing research on NAPs to certify our understanding of neural
networks. And we leave the exploration of this direction for our future work.

##  9\. Conclusion

We introduce a new problem — learning the minimal NAP specification, and
discuss its importance in neural network verification. Finding minimal NAP
specification not only enables the verification of larger input regions
compared to existing methods but also provides a means of inspecting when and
how neural networks can make reliable and robust predictions. To solve this
problem, we first propose two simple approaches Refine and Coarsen, which
leverage off-the-shelf verification tools that find the minimal NAP
specification with correctness guarantees. We also propose the statistical
version of Refine and Coarsen, that combine sampling and statistical learning
principles to achieve correctness in an more efficient manner. However, these
approaches depend on underlying verification tools that are computationally
expensive. To this end, we propose two approximate approaches,
Adversarial_Prune and Gradient_Search. These methods utilize adversarial
attacks and local gradient computation to efficiently investigate potential
causal relationships between specific neurons and the model’s robustness. This
is a task that current verification frameworks struggle to accomplish.
Finally, to appreciate the volumetric change from the most refined NAP
specification to the minimal NAP specification, we propose a simple method for
estimating the volume of the region corresponding to a NAP. Our experiments
indicate that minimal NAP specifications utilize much smaller fractions of
neurons compared to the most refined NAPs. Nevertheless, they enable a
substantial expansion of the verifiable boundaries by several orders of
magnitude.

## References

  * (1)
  * Bau et al. (2017) David Bau, Bolei Zhou, Aditya Khosla, Aude Oliva, and Antonio Torralba. 2017.  Network Dissection: Quantifying Interpretability of Deep Visual Representations. In _2017 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2017, Honolulu, HI, USA, July 21-26, 2017_. IEEE Computer Society, 3319–3327.  https://doi.org/10.1109/CVPR.2017.354
  * Bäuerle et al. (2022) Alex Bäuerle, Daniel Jönsson, and Timo Ropinski. 2022.  Neural Activation Patterns (NAPs): Visual Explainability of Learned Concepts.  _CoRR_ abs/2206.10611 (2022).  https://doi.org/10.48550/arXiv.2206.10611 arXiv:2206.10611
  * Cheng et al. (2017) Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. 2017.  Maximum Resilience of Artificial Neural Networks. In _Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings_ _(Lecture Notes in Computer Science, Vol. 10482)_ , Deepak D’Souza and K. Narayan Kumar (Eds.). Springer, 251–268.  https://doi.org/10.1007/978-3-319-68167-2_18
  * Cousot and Cousot (1977) Patrick Cousot and Radhia Cousot. 1977.  Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In _Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977_ , Robert M. Graham, Michael A. Harrison, and Ravi Sethi (Eds.). ACM, 238–252.  https://doi.org/10.1145/512950.512973
  * Cousot and Cousot (2014) Patrick Cousot and Radhia Cousot. 2014.  Abstract interpretation: past, present and future. In _Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014_ , Thomas A. Henzinger and Dale Miller (Eds.). ACM, 2:1–2:10.  https://doi.org/10.1145/2603088.2603165
  * Dietterich and Horvitz (2015) Thomas G. Dietterich and Eric Horvitz. 2015.  Rise of concerns about AI: reflections and directions.  _Commun. ACM_ 58, 10 (2015), 38–40.  https://doi.org/10.1145/2770869
  * Dyer and Frieze (1988) Martin E. Dyer and Alan M. Frieze. 1988.  On the Complexity of Computing the Volume of a Polyhedron.  _SIAM J. Comput._ 17, 5 (1988), 967–974.  https://doi.org/10.1137/0217060
  * Ehlers (2017) Rüdiger Ehlers. 2017.  Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks.  _CoRR_ abs/1705.01320 (2017).  arXiv:1705.01320 http://arxiv.org/abs/1705.01320
  * Erhan et al. (2009) D. Erhan, Yoshua Bengio, Aaron C. Courville, and Pascal Vincent. 2009.  Visualizing Higher-Layer Features of a Deep Network.
  * Frankle and Carbin (2019) Jonathan Frankle and Michael Carbin. 2019.  The Lottery Ticket Hypothesis: Finding Sparse, Trainable Neural Networks. In _7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019_. OpenReview.net.  https://openreview.net/forum?id=rJl-b3RcF7
  * Gehr et al. (2018) Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. 2018.  AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. In _2018 IEEE Symposium on Security and Privacy (SP)_. 3–18.  https://doi.org/10.1109/SP.2018.00058
  * Geng et al. (2023) Chuqin Geng, Nham Le, Xiaojie Xu, Zhaoyue Wang, Arie Gurfinkel, and Xujie Si. 2023.  Towards Reliable Neural Specifications. In _International Conference on Machine Learning, ICML 2023, 23-29 July 2023, Honolulu, Hawaii, USA_ _(Proceedings of Machine Learning Research, Vol. 202)_ , Andreas Krause, Emma Brunskill, Kyunghyun Cho, Barbara Engelhardt, Sivan Sabato, and Jonathan Scarlett (Eds.). PMLR, 11196–11212.  https://proceedings.mlr.press/v202/geng23a.html
  * Geng et al. (2022) Chuqin Geng, Xiaojie Xu, Haolin Ye, and Xujie Si. 2022.  Scalar Invariant Networks with Zero Bias.  _CoRR_ abs/2211.08486 (2022).  https://doi.org/10.48550/ARXIV.2211.08486 arXiv:2211.08486
  * Goodfellow et al. (2015) Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. 2015.  Explaining and Harnessing Adversarial Examples. In _3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings_ , Yoshua Bengio and Yann LeCun (Eds.).  http://arxiv.org/abs/1412.6572
  * Hanin and Rolnick (2019a) Boris Hanin and David Rolnick. 2019a.  Complexity of Linear Regions in Deep Networks. In _ICML_ _(Proceedings of Machine Learning Research, Vol. 97)_. PMLR, 2596–2604.
  * Hanin and Rolnick (2019b) Boris Hanin and David Rolnick. 2019b.  Deep ReLU Networks Have Surprisingly Few Activation Patterns. In _NeurIPS_. 359–368.
  * Huang et al. (2020) Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu, and Xinping Yi. 2020.  A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability.  _Comput. Sci. Rev._ 37 (2020), 100270.  https://doi.org/10.1016/j.cosrev.2020.100270
  * Huang et al. (2017a) Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017a.  Safety Verification of Deep Neural Networks. In _Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I_ _(Lecture Notes in Computer Science, Vol. 10426)_ , Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 3–29.  https://doi.org/10.1007/978-3-319-63387-9_1
  * Huang et al. (2017b) Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. 2017b.  Safety Verification of Deep Neural Networks. In _Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I_ _(Lecture Notes in Computer Science, Vol. 10426)_ , Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 3–29.  https://doi.org/10.1007/978-3-319-63387-9_1
  * Katz et al. (2017) Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. 2017.  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_ _(Lecture Notes in Computer Science, Vol. 10426)_ , Rupak Majumdar and Viktor Kuncak (Eds.). Springer, 97–117.  https://doi.org/10.1007/978-3-319-63387-9_5
  * Katz et al. (2019) Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljic, David L. Dill, Mykel J. Kochenderfer, and Clark W. Barrett. 2019.  The Marabou Framework for Verification and Analysis of Deep Neural Networks. In _Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I_ _(Lecture Notes in Computer Science, Vol. 11561)_ , Isil Dillig and Serdar Tasiran (Eds.). Springer, 443–452.  https://doi.org/10.1007/978-3-030-25540-4_26
  * Liang et al. (2011) Percy Liang, Omer Tripp, and Mayur Naik. 2011.  Learning minimal abstractions. In _Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011_ , Thomas Ball and Mooly Sagiv (Eds.). ACM, 31–42.  https://doi.org/10.1145/1926385.1926391
  * Liang et al. (2021) Tailin Liang, John Glossner, Lei Wang, Shaobo Shi, and Xiaotong Zhang. 2021.  Pruning and quantization for deep neural network acceleration: A survey.  _Neurocomputing_ 461 (2021), 370–403.  https://doi.org/10.1016/J.NEUCOM.2021.07.045
  * Lu and Kumar (2019) Jingyue Lu and M. Pawan Kumar. 2019.  Neural Network Branching for Neural Network Verification.  _CoRR_ abs/1912.01329 (2019).  arXiv:1912.01329 http://arxiv.org/abs/1912.01329
  * Lu et al. (2019) Lu Lu, Yeonjong Shin, Yanhui Su, and George E. Karniadakis. 2019.  Dying ReLU and Initialization: Theory and Numerical Examples.  _CoRR_ abs/1903.06733 (2019).  arXiv:1903.06733 http://arxiv.org/abs/1903.06733
  * Mirman et al. (2018) Matthew Mirman, Timon Gehr, and Martin T. Vechev. 2018.  Differentiable Abstract Interpretation for Provably Robust Neural Networks. In _International Conference on Machine Learning_.  https://api.semanticscholar.org/CorpusID:51872670
  * Selvaraju et al. (2017) Ramprasaath R. Selvaraju, Michael Cogswell, Abhishek Das, Ramakrishna Vedantam, Devi Parikh, and Dhruv Batra. 2017.  Grad-CAM: Visual Explanations from Deep Networks via Gradient-Based Localization. In _2017 IEEE International Conference on Computer Vision (ICCV)_. 618–626.  https://doi.org/10.1109/ICCV.2017.74
  * Shapira et al. (2023) Yuval Shapira, Eran Avneri, and Dana Drachsler-Cohen. 2023.  Deep Learning Robustness Verification for Few-Pixel Attacks.  _Proc. ACM Program. Lang._ 7, OOPSLA1, Article 90 (apr 2023), 28 pages.  https://doi.org/10.1145/3586042
  * Simonyan et al. (2014a) Karen Simonyan, Andrea Vedaldi, and Andrew Zisserman. 2014a.  Deep Inside Convolutional Networks: Visualising Image Classification Models and Saliency Maps. In _2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Workshop Track Proceedings_ , Yoshua Bengio and Yann LeCun (Eds.).  http://arxiv.org/abs/1312.6034
  * Simonyan et al. (2014b) Karen Simonyan, Andrea Vedaldi, and Andrew Zisserman. 2014b.  Deep Inside Convolutional Networks: Visualising Image Classification Models and Saliency Maps. In _2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14-16, 2014, Workshop Track Proceedings_ , Yoshua Bengio and Yann LeCun (Eds.).  http://arxiv.org/abs/1312.6034
  * Simonyan and Zisserman (2014) Karen Simonyan and Andrew Zisserman. 2014.  Very Deep Convolutional Networks for Large-Scale Image Recognition.  _CoRR_ abs/1409.1556 (2014).  https://api.semanticscholar.org/CorpusID:14124313
  * Tjeng et al. (2019) Vincent Tjeng, Kai Yuanqing Xiao, and Russ Tedrake. 2019.  Evaluating Robustness of Neural Networks with Mixed Integer Programming. In _7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019_. OpenReview.net.  https://openreview.net/forum?id=HyGIdiRqtm
  * VNNCOMP (2021) VNNCOMP. 2021.  VNNCOMP.  https://sites.google.com/view/vnn2021
  * Wang et al. (2021b) Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. 2021b.  Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. In _Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual_ , Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (Eds.). 29909–29921.  https://proceedings.neurips.cc/paper/2021/hash/fac7fead96dafceaf80c1daffeae82a4-Abstract.html
  * Wang et al. (2021c) Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J. Zico Kolter. 2021c.  Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. In _Advances in Neural Information Processing Systems 34: Annual Conference on Neural Information Processing Systems 2021, NeurIPS 2021, December 6-14, 2021, virtual_ , Marc’Aurelio Ranzato, Alina Beygelzimer, Yann N. Dauphin, Percy Liang, and Jennifer Wortman Vaughan (Eds.). 29909–29921.  https://proceedings.neurips.cc/paper/2021/hash/fac7fead96dafceaf80c1daffeae82a4-Abstract.html
  * Wang et al. (2021a) Zi Wang, Chengcheng Li, and Xiangyang Wang. 2021a.  Convolutional Neural Network Pruning With Structural Redundancy Reduction. In _IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2021, virtual, June 19-25, 2021_. Computer Vision Foundation / IEEE, 14913–14922.  https://doi.org/10.1109/CVPR46437.2021.01467
  * William et al. (1995) Wolberg William, Mangasarian Olvi, Street Nick, and Street W. 1995.  Breast Cancer Wisconsin (Diagnostic).  UCI Machine Learning Repository.  DOI: https://doi.org/10.24432/C5DW2B.
  * Wing (1990) Jeannette M. Wing. 1990.  A Specifier’s Introduction to Formal Methods.  _Computer_ 23, 9 (1990), 8–24.  https://doi.org/10.1109/2.58215
  * Xu et al. (2020) Han Xu, Yao Ma, Haochen Liu, Debayan Deb, Hui Liu, Jiliang Tang, and Anil K. Jain. 2020.  Adversarial Attacks and Defenses in Images, Graphs and Text: A Review.  _Int. J. Autom. Comput._ 17, 2 (2020), 151–178.  https://doi.org/10.1007/s11633-019-1211-x
  * Xu et al. (2021) Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. 2021.  Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers. In _9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021_. OpenReview.net.  https://openreview.net/forum?id=nVZtXBI6LNn
  * Yosinski et al. (2015) Jason Yosinski, Jeff Clune, Anh Mai Nguyen, Thomas J. Fuchs, and Hod Lipson. 2015.  Understanding Neural Networks Through Deep Visualization.  _CoRR_ abs/1506.06579 (2015).  arXiv:1506.06579 http://arxiv.org/abs/1506.06579

##  Appendix A Proofs of simple approaches

######  Theorem A.1 (Property of Refine).

The algorithm Refine returns a minimal NAP specification with
$\mathcal{O}(2^{|N|})$ calls to $\mathcal{V}$.

###### Proof.

Let $P$ be the returned NAP. We prove this by contradiction. Suppose we can
further refine $P$, meaning there exists a NAP $P^{\prime}$ such that
$|P^{\prime}|\leq|P|$ and $\mathcal{V}(P^{\prime})=1$. However, the algorithm
states that any $P^{\prime}$ smaller than $|P|$ fails verification, which
contradicts $\mathcal{V}(P^{\prime})=1$.

In the worst case, the NAP size $k$ runs up to $|N|$. For each $k$, we need to
check $\binom{|N|}{k}$ number of NAPs. In total, this number of NAPs we need
to check is $\binom{|N|}{1}+\binom{|N|}{2}+\cdots+\binom{|N|}{|N|}=2^{|N|}-1$
according to the binomial theorem, resulting in a runtime complexity of
$\mathcal{O}(2^{|N|})$.

∎

######  Theorem A.2 (Property of Coarsen).

The algorithm Coarsen returns a minimal NAP specification with
$\mathcal{O}(|N|)$ calls to $\mathcal{V}$.

###### Proof.

Let $P$ be the NAP returned by Coarsen. Our goal is to show that any
$P^{\prime}$ smaller than $P$ results in $\mathcal{V}(P^{\prime})=0$. To
construct such a smaller $P^{\prime}$, we need to apply the refine action
$\widetilde{\Delta}$ on $P$ through some neuron $N_{i,l}$, i.e.,
$P^{\prime}:=\widetilde{\Delta}(N_{i,l})=\widetilde{\mathcal{A}}(N_{i,l})\cup
P\setminus P_{i,l}$. According to the algorithm, $\mathcal{V}(P^{\prime})=0$.
In the worst case, the algorithm needs to iterate through each neuron in $N$,
resulting in a runtime complexity of $\mathcal{O}(|N|)$. ∎

##  Appendix B Proofs of statistical approaches

Our proofs of properties of Sample_Refine and Sample_Coarsen mainly follow
those in (Liang et al., 2011). Interested readers may refer to it for detailed
proofs.

######  Theorem B.1 (Property of Sample_Refine).

With probability $\theta=|(\frac{|M|}{|M|+1})|^{|M|}$, Sample_Refine has
$1-\delta$ probability of outputting a minimal NAP specification with
$\Theta\left(|M|^{2}(\log|N|+\log(s/\delta))\right)$ examples each iteration
and $O(s|M|^{2}(\log|N|+\log(s/\delta)))$ total calls to $\mathcal{V}$.

###### Proof.

Considering the size of the minimal specification $s$, Sample_Refine will
execute $s$ iterations. If we sample $k$ times in each iteration, then the
probability of selecting a mandatory neuron is at least $1-\frac{\delta}{s}$.
Consequently, by applying a union bound, the algorithm will identify a NAP
specification with a probability of at least $1-\delta$.

Now, let’s delve deeper into one iteration of the process. The fundamental
concept is that a mandatory neuron $m$ demonstrates a stronger correlation
with proving the robustness query ($\mathcal{V}(P)=1$) compared to a non-
mandatory one. This enhanced correlation increases the probability of its
selection significantly when $k$ is sufficiently large.

Let’s revisit the notion of $M$, representing the set of mandatory neurons
with a size of $|M|$. Now, let’s focus on a specific mandatory neuron
$n^{+}\in M$. We define $B_{j-}$ as the event indicating
$k_{n^{-}}>k_{n^{+}}$, and $B$ as the event where $B_{j-}$ holds for any non-
mandatory neuron $n^{-}\in N\setminus M$. Importantly, if $B$ fails to occur,
then the algorithm will correctly identify a mandatory neuron. Hence, our
primary objective is to establish that $Pr(B)\leq\frac{\delta}{s}$. Initially,
employing a union bound provides:

(17) $\displaystyle
Pr(B)\leq\sum_{n^{-}}Pr(B_{n^{-}})\leq|N|\max_{n^{-}}Pr(B_{n^{-}})$

Let’s delve into each training example $P^{(i)}$ and introduce the notation
$X_{i}=(1-\mathcal{V}(P^{(i)}))(P_{n^{-}}^{(i)}-P_{n^{+}}^{(i)})$. It’s worth
emphasizing that $B_{n^{-}}$ manifests precisely when
$\frac{1}{n}(k_{n^{-}}-k_{n^{+}})=\frac{1}{n}\sum_{i=1}^{n}X_{i}>0$. Our
objective now is to bound this quantity utilizing Hoeffding’s inequality,
considering the mean as:

(18)
$\displaystyle\mathbb{E}[X_{i}]=Pr(\mathcal{V}(P)=1,P_{n^{-}}\in\\{\mathbf{1},\mathbf{0}\\})-Pr(\mathcal{V}(P)=1,P_{n^{+}}\in\\{\mathbf{1},\mathbf{0}\\})$

and the bounds are $-1\leq\mathbb{E}[X_{i}]\leq 1$ . Setting
$\epsilon=-\mathbb{E}[X_{i}]$, we get:

(19) $\displaystyle Pr(B_{n^{-}})\leq e^{\frac{-k\epsilon^{2}}{2}},n^{+}\in
M,n^{-}\notin M.$

Substituting (16) into (15) and rearranging terms, we can solve for $k$:

(20) $\displaystyle\frac{\delta}{s}\leq|N|e^{\frac{-k\epsilon^{2}}{2}}\text{
implies }k\geq\frac{2(log|N|+log(\frac{s}{\delta}))}{\epsilon^{2}}$

Our attention now shifts towards deriving a lower bound for $\epsilon$, which
intuitively reflects the discrepancy (in terms of correlation with proving the
robustness query) between a mandatory neuron and a non-mandatory one. It’s
noteworthy that $Pr(P_{n}\in{\\{\mathbf{1},\mathbf{0}}\\})=\theta$ for any
$n\in N$. Furthermore, since $n^{-}$ is non-mandatory, we can assert that
$Pr(\mathcal{V}(P)=1|P_{n^{-}}\in\\{\mathbf{1},\mathbf{0}\\})=Pr(\mathcal{V}(P)=1)$.
By leveraging these observations, we can express:

(21)
$\displaystyle\epsilon=\theta(Pr(\mathcal{V}(P)=1|P_{n^{+}}\in\\{\mathbf{1},\mathbf{0}\\})-Pr(\mathcal{V}(P)=1))$

Let’s view $C$ as the collection of minimal NAP specifications. We can treat
$C$ as a set of clauses in a Disjunctive Normal Form (DNF) formula:
$\mathcal{V}(P;C)=\neg\bigvee_{c\in C}\bigwedge_{n\in c}P_{n}$, where we
explicitly specify the dependence of $\mathcal{V}$ on the clauses $C$. For
example, if $C={{1,2},{3}}$, it corresponds to
$\mathcal{V}(P)=\neg[(P_{1}\land P_{2})\lor P_{3}]$. Now, let $C_{j}={c\in
C:n\in c}$ denote the clauses containing $n$. We reformulate
$Pr(\mathcal{V}(P)=1)$ as the sum of two components: one originating from the
mandatory neuron $n^{+}$ and the other from the non-mandatory neuron:

(22) $\displaystyle Pr(\mathcal{V}(P)=1)$
$\displaystyle=Pr(\mathcal{V}(P;C_{n^{+}})=1,\mathcal{V}(P;C\setminus
C_{n^{+}})=0)$ (23) $\displaystyle\quad+Pr(\mathcal{V}(P;C\setminus
C_{n^{+}})=1)$

Calculating $Pr(\mathcal{V}(P)=1|P_{n^{+}}\in\\{\mathbf{1},\mathbf{0}\\})$
follows a similar process. The only distinction arises from conditioning on
$P_{n^{+}}\in\\{\mathbf{1},\mathbf{0}\\}$, which introduces an extra factor of
$\frac{1}{\theta}$ in the first term because conditioning divides by
$Pr(P_{n^{+}})=\theta$. The second term remains unchanged since no $c\notin
C_{n^{+}}$ is mandatory in $P_{n^{+}}$. Substituting these two outcomes back
into the equation yields:

(24)
$\displaystyle\epsilon=(1-\theta)Pr(\mathcal{V}(P;C_{n^{+}})=1,\mathcal{V}(P;C\setminus
C_{n^{+}})=0)$

Now, our objective is to establish a lower bound for (22) across all possible
$\mathcal{V}$ (equivalently, $C$), where $n^{+}$ is permitted to be mandatory
in $C$. Interestingly, the worst possible $C$ can be obtained by either having
$|M|$ disjoint clauses ($C={{n}:n\in M}$) or a single clause ($C={M}$ if
$s=|M|$). The intuition behind this is that when $C$ consists of $|M|$
clauses, there are numerous possibilities ($|M|-1$ of them) for some $c\notin
C_{n^{+}}$ to be true, making it challenging to determine that $n^{+}$ is a
mandatory neuron; in such cases,
$\epsilon=(1-\theta)\theta(1-\theta)^{|M|-1}$. Conversely, if $C$ comprises a
single clause, then letting this clause be true becomes exceedingly
challenging; in this scenario, $\epsilon=(1-\theta)\theta^{|M|}$.

Let’s consider the scenario where $C$ comprises $|M|$ clauses. We aim to
maximize $\epsilon$ concerning $\theta$ by setting the derivative
$\frac{d\epsilon}{d\theta}=0$ and solving for $\theta$. This optimization
yields $\theta=\frac{1}{|M|+1}$ as the optimal value. Substituting this value
into the formula of $\epsilon$, we obtain
$\epsilon=\frac{1}{|M|+1}(\frac{|M|}{|M|+1})^{|M|}$. Note that
$(\frac{|M|}{|M|+1})^{|M|}$ can be lower bounded by $e^{-1}$, implying that
$\epsilon^{-2}=\mathcal{O}(|M|^{2})$. Substituting this result to equation
(18) will conclude the proof. ∎

######  Theorem B.2 (Property of Sample_Coarsen).

With probability $\theta$=$e^{-\frac{1}{s}}$, Sample_Coarsen learns a minimal
NAP specification with $\mathcal{O}(slog|N|)$ calls to $\mathcal{V}$.

###### Proof.

Let’s first estimate the number of calls that Sample_Coarsen makes to
$\mathcal{V}$. We denote the number of calls as $\mathcal{C}(P^{L})$, where
$P^{L}$ is the most refined NAP. Then $\mathcal{C}(P^{L})$ can be computed
recursively using the following rule:

(25) $\displaystyle\mathcal{C}(P^{L})=\begin{cases}|P|&\text{ if }|P^{L}|\leq
s+1\\\
1+\mathbb{E}[(1-\mathcal{V}(P))\mathcal{C}(P)+\mathcal{V}(P)\mathcal{C}(P^{L})]&\text{
otherwise }\\\ \end{cases}$

where $P$ is the sampled NAP. By assumption, there exists a NAP
$P^{S}\preccurlyeq P$ of size $s$ that passes the verification. Define
$G(P)=\neg(P^{S}\preccurlyeq P)$, which is 0 when $P^{S}$ subsumes $P$, i.e.,
all mandatory neurons in $P^{S}$ shows up in the sampled $P$. This follows
that $Pr(G(P)=0)=Pr(P^{S}\preccurlyeq P)=\theta^{s}$. Note that
$G(P)\geq\mathcal{V}(P)$, as the NAP $P^{S}$ suffices to prove the robustness
query. We can estimate the upper bound of $\mathcal{C}(P^{L})$ by replacing
$\mathcal{V}$ with $G$:

(26) $\displaystyle\mathcal{C}(P^{L})$ $\displaystyle\leq
1+\mathbb{E}[(1-G(P))\mathcal{C}(P)+G(P)\mathcal{C}(P^{L})]$ (27)
$\displaystyle\leq 1+\theta^{s}\mathbb{E}[\mathcal{C}(P)|P^{S}\preccurlyeq
P]+(1-\theta^{s})\mathcal{C}(P^{L})$ (28)
$\displaystyle\leq\mathbb{E}[\mathcal{C}(P)|P^{S}\preccurlyeq P]+\theta^{-s}$

We now denote $\mathcal{C}(n)=max_{|P|=n}\mathcal{C}(P)$ as the maximum over
NAP of size $n$. Note that given $P^{S}\preccurlyeq P$, $|P|=s+N$ where $N$ is
a binomial random variable with $\mathbb{E}(N)=\theta(n-s)$.

Using the bound
$\mathcal{C}(n)\leq(1-\theta^{n})\mathcal{C}(n-1)+\theta^{n}\mathcal{C}(n)\theta^{-s}$,
we can observe that $\mathcal{C}(n)\leq\frac{\theta^{-s}}{1-\theta^{n}}\cdot
n$. In addition, when $n$ is large enough, $\mathcal{C}(n)$ is concave, then
by use Jensen’s inequality:

(29)
$\displaystyle\mathcal{C}(n)\leq\mathcal{C}(\mathbb{E}[s+N])+\theta^{-s}=\mathcal{C}(s+\theta(n-s))+\theta^{-s}$

To solve the recurrence, this gives us:

(30)
$\displaystyle\mathcal{C}(n)\leq\frac{\theta^{-s}logn}{log\theta^{-1}}+s+1$

The equation above illustrates a tradeoff between reducing the number of
iterations (by increasing $\log\theta^{-1}$) and reducing the number of
samples (by decreasing $\theta^{-s}$). To minimize $\mathcal{C}(n)$, we need
to set $\theta$ so that the gradient of $\mathcal{C}(n)$ w.r.t $\theta^{-1}$
is $0$. This gives us: $\frac{sx^{s-1}}{\log x}-\frac{x^{s-1}}{\log^{2}x}=0$,
solving this gives us $\theta=e^{-\frac{1}{s}}$. Consequently, the upper bound
becomes $\mathcal{C}(n)=es\log n+s+1=O(s\log n)$. ∎