End-To-End Set-Based Training for Neural Network Verification

Lukas Koller

Technical University of Munich

Tobias Ladner

Technical University of Munich

Matthias Althoff

Technical University of Munich

Neural networks are vulnerable to adversarial attacks, i.e., small input perturbations can result in substantially different outputs of a neural network. Safety-critical environments require neural networks that are robust against input perturbations. However, training and formally verifying robust neural networks is challenging. We address this challenge by employing, for the first time, a end-to-end set-based training procedure that trains robust neural networks for formal verification. Our training procedure drastically simplifies the subsequent formal robustness verification of the trained neural network. While previous research has predominantly focused on augmenting neural network training with adversarial attacks, our approach leverages set-based computing to train neural networks with entire sets of perturbed inputs. Moreover, we demonstrate that our set-based training procedure effectively trains robust neural networks, which are easier to verify. In many cases, set-based trained neural networks outperform neural networks trained with state-of-the-art adversarial attacks.

§ INTRODUCTION

Neural networks achieve impressive results for many complex tasks, such as speech recognition <cit.> or object detection <cit.>. However, many neural networks are sensitive to input perturbations <cit.>: Small, carefully chosen input changes can lead to vastly different outputs. This behavior is problematic for the safe adoption of neural networks in safety-critical scenarios, e.g., autonomous vehicle control <cit.>, airborne collision avoidance <cit.>, or operation of nuclear reactors <cit.>. Thus, the formal verification of the robustness of neural networks gained interest in recent years <cit.>. A neural network is considered robust against a perturbance set if it returns the correct output for every value within the perturbance set, typically an $l_\infty$-ball. Subsequently, we provide a brief overview of related work.

§.§ Related Work

Adversarial Attacks
An adversarial attack is a modified input within a perturbance set that leads to an incorrect output of a neural network. The most prominent approaches to generating adversarial attacks are the fast gradient sign method (FGSM) and projected gradient descent (PGD). FGSM is a single-step gradient-based adversarial attack that efficiently generates adversarial attacks <cit.>. PGD uses multiple iterations of FGSM to compute stronger adversarial attacks <cit.>.

Training Robust Neural Networks
The training objective of a robust neural network is typically formulated as a min-max optimization problem <cit.>: Minimize the worst-case input within a perturbance set. A worst-case input maximizes the error of the corresponding output with respect to a target output. Computing a worst-case input within a perturbance set is computationally difficult <cit.>. Nonetheless, neural networks are effectively trained by approximating worst-case inputs with adversarial attacks, e.g., computed with PGD <cit.>. Other approaches for training robust neural networks are via input gradient regularization <cit.> or neural network destillation <cit.>. However, none of these training approaches incorporate formal verification methods.

Formal Robustness Verification of Neural Networks
The formal robustness verification of neural networks is crucial to safely deploy neural networks in safety-critical scenarios. Most formal verification approaches either formulate the verification problem as an optimization problem or use reachability analysis <cit.>. Optimization-based approaches encode the verification problem as an optimization problem, which is solved using (mixed-integer) linear programming <cit.> or satisfiability modulo theories (SMT) <cit.> solvers. Alternatively, reachability analysis uses efficient set representations, e.g., zonotopes <cit.>, combined with set-based computations to enclose the output set of a neural network for a given input set <cit.>. The output set of a neural network is used to verify its safety.

Combined Training and Robustness Verification of Neural Networks
Many approaches combine the training and formal verification of robust neural networks by enhancing the training using adversarial attacks. In these works, the approximation of a worst-case input is replaced by an upper bound, which can verify that no perturbation will lead to an incorrect output. Different methods for upper-bounding a worst-case input have been proposed: Interval bound propagation (IBP) <cit.>, linear relaxation <cit.>, (mixed-integer) linear programming <cit.>, or abstract interpretation <cit.>. Some approaches use set-based methods to compute upper bounds <cit.>; however, only the upper bound is used for training, discarding much set-based information. Conversely, our approach is end-to-end set-based, meaning we use the entire sets for training. Moreover, training neural networks with adversarial attacks or upper bounds reduces their accuracy for non-adversarial inputs. Hence, there is a trade-off between robustness and accuracy for neural networks <cit.>. This issue can be addressed by combining a regular training objective with a robustness training objective <cit.>.

§.§ Contributions

Our main contribution is a novel set-based training procedure that trains robust neural networks and drastically simplifies their subsequent formal robustness verification. Given a set of inputs with associated perturbance sets, we compute output sets and use the entire output sets for training. To our best knowledge, we present the first end-to-end set-based training approach for neural networks.
Secondly, set-based training is made possible by an image enclosure using linear approximations. With our image enclosure, the output sets for an entire batch of inputs are efficiently computed using matrix operations on a GPU. Moreover, we show that the approximation errors by our image enclosure are always smaller or equal compared to an existing image enclosure.
Thirdly, we evaluate our set-based training with neural networks of various sizes trained on three different datasets. We demonstrate the efficacy of set-based training and that set-based trained neural networks often outperform neural networks trained with state-of-the-art adversarial attacks.

§.§ Organisation

<ref> introduces the required preliminaries. We provide an efficient image enclosure in <ref>, that we use for set-based training. In <ref>, we define our set-based training procedure, which we experimentally evaluate in <ref>. Finally, we conclude our findings in <ref>.

§ PRELIMINARIES

§.§ Notation

Lowercase letters denote vectors and uppercase letters denote matrices. The $i$-th entry of a vector $x$ is denoted by $x_{(i)}$. For a matrix $A$, $A_{(i,j)}$ denotes the entry in the $i$-th row and the $j$-th column, $A_{(i,\cdot)}$ denotes the $i$-th row, and $A_{(\cdot,j)}$ the $j$-th column. The identity matrix is written as $\eye{n}\in\R^{n\times n}$. We use  and  to represent the vector or matrix (with appropriate size) that contains only zeros or ones. The (horizontal) concatenation between two matrices $A\in\R^{m\times n_1}$ and $B\in\R^{m\times n_2}$ is denoted by $\begin{bsmallmatrix} {\displaystyle A} & {\displaystyle B} \end{bsmallmatrix}$. A square matrix with the entries of a given vector on its diagonal is returned by the operation $\diagName:\R^n\to\R^{n\times n}$.
Given a matrix, the operation $\operatorname{sign}:\R^{n\times m}\to\{-1,0,1\}^{n\times m}$ returns the sign of each entry of the matrix.
We denote sets with uppercase calligraphic letters. For a set $\mathcal{S}\subset\R^n$, we denote its projection to the $i$-th dimension with $\mathcal{S}_{(i)}$. Given two sets $\mathcal{S}_1\subset\R^n$ and $\mathcal{S}_2\subset\R^m$, we denote the Cartesian product with $\mathcal{S}_1\times\mathcal{S}_2=\{\begin{bsmallmatrix} {\displaystyle s_1^\top} & {\displaystyle s_2^\top} \end{bsmallmatrix}^\top\mid s_1\in\mathcal{S}_1,\,s_2\in\mathcal{S}_2\}$, and if $n = m$, we write the Minkowski sum as $\mathcal{S}_1\oplus\mathcal{S}_2=\{s_1 + s_2\mid s_1\in\mathcal{S}_1,\,s_2\in\mathcal{S}_2\}$.
For $n\in\N$, $[n]=\{1,2,\dots,n\}$ denotes the set of all natural numbers up to $n$. We denote the natural logarithm with $\ln$.
An $n$-dimensional interval $\mathcal{I}\subset\R^n$ with bounds $l,u\in\R^n$ is denoted by $\mathcal{I} = \left[l,u\right]$.
The continuous uniform distribution between $a\in\R$ and $b\in\R$ with $a \leq b$ is written as $U(a,b)$. We denote a random variable $X$ drawn from $U(a,b)$ by $X\sim U(a,b)$.

§.§ Feed-Forward Neural Networks

A feed-forward neural network consists of a sequence of $\nnNumLayers\in\N$ layers. A layer can either be a linear layer, which applies an affine map, or an activation layer, which applies a nonlinear activation function elementwise.

The $k$-th layer of a neural network is defined as an operation $L_k:\R^{\nnNumNeurons_{k-1}}\to\R^{\nnNumNeurons_k}$,

\begin{equation*}
h_k = L_k(h_{k-1}) = \begin{cases}
W_k\, h_{k-1} + b_k & \text{if $k$-th layer is linear,} \\
\actfun_k(h_{k-1})  & \text{otherwise,}
\end{cases}
\end{equation*}

where $\nnNumNeurons_{k-1}$ denotes the number of input neurons, $\nnNumNeurons_k$ denotes the number of output neurons, $W_k\in\R^{\nnNumNeurons_k\times \nnNumNeurons_{k-1}}$ is a weight matrix, $b_k\in\R^{\nnNumNeurons_k}$ is a bias vector, and $\actfun_k:\R\to\R$ is a nonlinear activation function.

The parameters $\theta$ of a neural network include all weight matrices and bias vectors from its linear layers. Forward propagation computes the output $\nnoutput\in\R^{\nnNumNeurons_\nnNumLayers}$ of a neural network by propagating an input $\nninput\in\R^{\nnNumNeurons_0}$ sequentially through all neural network layers.

The output $\nnoutput\in\R^{\nnNumNeurons_\nnNumLayers}$ of a neural network for an input $\nninput\in\R^{\nnNumNeurons_0}$ is computed by

\begin{align*}
h_0       & = \nninput\text{,}                                       \\
h_k       & = L_k(h_{k-1}) \quad\text{for $k=1,\dots,\nnNumLayers$,} \\
\nnoutput & = h_\nnNumLayers\text{.}
\end{align*}

The function $N_\theta(\nninput) = \nnoutput$ denotes the forward propagation through a neural network with parameters $\theta$.

Training of Neural Networks
We only consider supervised training, where a neural network is trained with a training dataset $\mathcal{D}=\{(\nninput_1,\nntarget_1),\dots,(\nninput_n,\nntarget_n)\}$, that contains inputs $\nninput_i\in\R^{\nnNumNeurons_0}$ with associated target outputs $\nntarget_i\in\R^{\nnNumNeurons_\nnNumLayers}$.
A loss function $\pointLoss:\R^{\nnNumNeurons_\nnNumLayers}\times\R^{\nnNumNeurons_\nnNumLayers}\to\R$ measures how well a neural network predicts the target outputs. Typical loss functions are the half-squared error for regression tasks or the cross-entropy error for classification tasks.

The half-squared error $\pointLoss_{\regrSub}:\R^{\nnNumNeurons_\nnNumLayers}\times\R^{\nnNumNeurons_\nnNumLayers}\to\R$ is defined as

\begin{equation*}
\pointLoss_{\regrSub}(\nntarget,\nnoutput) \coloneqq \frac{1}{2}\sum_{i=1}^{\nnNumNeurons_\nnNumLayers} (\nntarget_{(i)} - \nnoutput_{(i)})^2\text{\kern-\squareLen.}
\end{equation*}

The cross-entropy error $\pointLoss_{\ceSub}:\R^{\nnNumNeurons_\nnNumLayers}\times\R^{\nnNumNeurons_\nnNumLayers}\to\R$ is defined as

\begin{equation*}
\pointLoss_{\ceSub}(\nntarget,\nnoutput) \coloneqq -\sum_{i=1}^{\nnNumNeurons_\nnNumLayers} \nntarget_{(i)}\,\ln(\nnoutput_{(i)}) + (1 - \nntarget_{(i)})\,\ln(1 - \nnoutput_{(i)})\text{.}
\end{equation*}

The training goal of a neural network is to find network parameters $\theta$ that minimize the total loss of the training dataset $\mathcal{D}$ <cit.>:

\begin{equation}\label{eq:nn_training_goal}
\min_\theta \sum_{(\nninput_i,\nntarget_i)\in\mathcal{D}} \pointLoss(\nntarget_i,N_\theta(\nninput_i))\text{.}
\end{equation}

A popular algorithm to train a neural network is gradient descent <cit.>: A random initial set of parameters $\theta^{(0)}$ is iteratively optimized using the gradient of the loss function <cit.>.
For the $j$-th iteration, let us introduce the gradient $g^{(j)}_k$ of the loss function $\pointLoss$ w.r.t. the output of the $k$-th layer $h_k$ for the input $\nninput\in\R^{\nnNumNeurons_0}$:

\begin{equation}\label{eq:backprop-grads}
g_k^{(j)} \coloneqq \frac{\partial \pointLoss(\nntarget,N_{\theta^{(j)}}(\nninput))}{\partial h_k}\text{.}
\end{equation}

In the $j$-th iteration, the weight matrix $W_k$ and bias vector $b_k$ of the $k$-th layer are updated as <cit.>

\begin{align}\label{eq:point_weight_bias_update}
\begin{split}
W_k^{(j+1)} & \gets W_k^{(j)} - \eta\, \frac{\partial \pointLoss(\nntarget,N_{\theta^{(j)}}(\nninput))}{\partial W_k^{(j)}} = W_k^{(j)} - \eta\, \grad_k^{(j)}\, h^\top_{k-1}\text{,} \\
b_k^{(j+1)} & \gets b_k^{(j)} - \eta\, \frac{\partial \pointLoss(\nntarget,N_{\theta^{(j)}}(\nninput))}{\partial b_k^{(j)}} = b_k^{(j)} - \eta\, \grad_k^{(j)} \text{,}
\end{split}
\end{align}

where $\eta\in\R_{>0}$ is the learning rate. For conciseness, we omit the iteration superscript from now on.
The gradients $g_k$ are efficiently computed with backpropagation <cit.>: Utilizing the chain rule, the gradient $g_\nnNumLayers$ of the last layer is propagated backward through all neural network layers.

Let $\nnoutput\in\R^{\nnNumNeurons_\nnNumLayers}$ be an output of a neural network with target $\nntarget\in\R^{\nnNumNeurons_\nnNumLayers}$. If the loss function $\pointLoss$ is the half-squared error or the cross-entropy error, then the gradients $g_k$ are computed in reverse order as

\begin{align*}
g_\nnNumLayers & = \nnoutput - \nntarget\text{,}                                                                            \\
g_{k-1}        & = \begin{cases}
W_k^\top\, g_k                                                       & \text{if $k$-th layer is linear,} \\
\diag{\frac{\mathrm{d}\actfun_k(h_{k-1})}{\mathrm{d} h_{k-1}}}\, g_k & \text{otherwise,}
\end{cases}
\end{align*}

for all $k\in\{\nnNumLayers,\dots,1\}$.

From now on, we refer to the (standard) neural network training as point-based training.

§.§ Set-Based Computation

We represent propagated sets by zonotopes. A zonotope is a convex set representation describing the Minkowski sum of a finite number of line segments.

Given a center $c\in\R^n$ and a generator matrix $G\in\R^{n\times q}$, a zonotope $\zonoName\subset\R^n$ is defined as

\begin{equation*}
\zonoName = \left\{\left.c+\sum_{j=1}^q\beta_{(j)}\,G_{(\cdot,j)}\;\right|\;\beta\in [-1,1]^q\right\} \eqqcolon \zonoDefault\text{.}
\end{equation*}

Subsequently, we define several operations for zonotopes used in our training approach. We first present the tight enclosure of a zonotope by a multi-dimensional interval:

A zonotope $\zonoName = \zonoDefault$ with $c\in\R^n$ and $G\in\R^{n\times q}$ is enclosed by the interval $[l,u]\supseteq\zonoName$, where

\begin{align*}
l & = c - \sum_{j=1}^q \abs{G_{(\cdot,j)}}\text{,} & u & = c + \sum_{j=1}^q \abs{G_{(\cdot,j)}}\text{,}
\end{align*}

where $\abs{\cdot}$ computes the elementwise absolute value. The time complexity of computing an interval enclosure is $\bigO(n\,q)$.

The Minkowski sum of a zonotope $\zonoName = \zonoDefault$ and an interval $\mathcal{I} = [l,u]\subset\R^n$ with $c,l,u\in\R^n$ and $G\in\R^{n\times q}$ is computed as

\begin{equation*}
\zonoName\oplus \mathcal{I} = \zonotope{c + \frac{1}{2}\,(l + u)}{\begin{bmatrix} G & \diag{\frac{1}{2}\,(u - l)} \end{bmatrix}}\text{\kern-\zonoZLen,}
\end{equation*}

and has time complexity $\bigO(n^2)$.

Zonotopes are closed under linear maps.

The result of a linear map $f:\R^n\to\R^m,\,x\mapsto W\,x + b$ with $W\in\R^{m\times n}$ and $b\in\R^m$ applied to a zonotope $\zonoName = \zonoDefault$ with $c\in\R^n$ and $G\in\R^{n\times q}$ is

\begin{equation*}
f(\zonoName) \coloneqq \left\{f(z)\mid z\in\zonoName\right\} = W\,\zonoName + b = \zonotope{W\,c + b}{W\,G}\text{,}
\end{equation*}

and has time complexity $\bigO(m\,n\,q)$.

Determining the volume of a zonotope is computationally demanding <cit.>. However, a norm of a zonotope can effectively approximate the size of a zonotope <cit.>.
The interval norm computes the sum of the lengths of all edges of the interval enclosure of a zonotope.

For a zonotope $\zonoName = \zonoDefault$, the interval norm is

\begin{equation*}
\norm{\zonoName}_{\widetilde{I}} \coloneqq \frac{1}{n}\,\ones^\top\,\abs{\begin{bmatrix} c & G \end{bmatrix}}\,\ones\text{.}
\end{equation*}

Since the volume of a zonotope is invariant over translations, we exclude the center from the computation of the norm. The combined operation of translating the zonotope to the origin and computing the norm is denoted by

\begin{equation}\label{eq:interval_norm}
\norm{\zonoName}_{I} \coloneqq \norm{\zonotope{\zeros}{G}}_{\widetilde{I}} = \frac{1}{n}\,\ones^\top\,\abs{G}\,\ones\text{.}
\end{equation}

§.§ Formal Verification of Neural Networks

In this work, we consider the robustness of neural networks for classification tasks: Each dimension of an output $\nnoutput\in\R^{\nnNumNeurons_\nnNumLayers}$ corresponds to a classification label, and the dimension with the maximum value determines the predicted classification label for an input $\nninput\in\R^{\nnNumNeurons_0}$. An input $\nninput$ is correctly classified by a neural network if the predicted classification label matches the classification label of the target output $\nntarget\in\R^{\nnNumNeurons_\nnNumLayers}$:

\begin{equation}\label{eq:nn_robustness}
\argmax_{k\in[\nnNumLayers]} \nnoutput_{(k)} = \argmax_{k\in[\nnNumLayers]} \nntarget_{(k)}\text{.}
\end{equation}

We call a neural network (locally) robust for a given perturbance set if the neural network correctly classifies every input within the perturbance set. As a perturbance set we use the $l_\infty$-ball of radius $\epsilon\in\R_{>0}$ around an input $\nninput\in\R^{\nnNumNeurons_0}$:

For a perturbation radius $\epsilon\in\R_{>0}$ and an input $\nninput\in\R^{\nnNumNeurons_0}$, the $\epsilon$-perturbance set is defined as

\begin{equation*}
\pi_\epsilon(\nninput) \coloneqq \zonotope{x}{\epsilon\,\eye{\nnNumNeurons_0}} = \left\{\left.\tilde{\nninput}\in\R^{\nnNumNeurons_0}\;\right|\;\norm{\tilde{\nninput} - \nninput}_\infty\leq\epsilon\right\}\text{.}
\end{equation*}

We formally verify the robustness of a neural network by using set-based computations to compute its output set for an input set $\inputSet = \pi_\epsilon(\nninput)$. However, computing an exact output set of a feed-forward neural network is computationally hard; with only rectified linear unit (ReLU) activation functions, it has been shown to be $\textsc{NP}$-hard <cit.>. Thus, we compute an outer approximation $\outputSet\subset\R^{\nnNumNeurons_\nnNumLayers}$ of the true output set $\outputSetExact\coloneqq\left\{N_\theta(x) \mid x\in\inputSet\right\}\subseteq\outputSet$ of a neural network $N_\theta$ for an input set $\inputSet\subset\R^{\nnNumNeurons_0}$.
If $\outputSet$ does not intersect with a region of unsafe outputs $\unsafeSet$, we have formally verified that the neural network only computes safe outputs for every input $x\in\inputSet$. For a classification task with target $\nntarget\in\R^{\nnNumNeurons_\nnNumLayers}$, the unsafe set contains every incorrect classification <cit.>:

\begin{equation}
\unsafeSet\coloneqq\left\{y\in\R^{\nnNumNeurons_\nnNumLayers}\;\left|\;(\eye{\nnNumNeurons_\nnNumLayers} - \ones\,e_l)\,y\nleq\zeros\right.\right\}\text{,}
\end{equation}

where $l\coloneqq \argmax_{k\in[\nnNumLayers]} \nntarget_{(k)}$ and $e_l$ is the $l$-th standard basis vector.
<ref> illustrates the robustness verification of a neural network.

Verifying the local robustness of a neural network.
Verifying the local robustness of a neural network.

To compute an outer approximation $\outputSet$, we evaluate the operations $L_k$ (<ref>) by sets.
We compute the output set of a linear layer for an input set with a linear map <cit.>.
Zonotopes are not closed under nonlinear maps; hence, we enclose the output set of an activation layer by an image enclosure summarized in <ref> <cit.>. We first compute an upper bound and a lower bound for each dimension of the input set (<ref>). The activation function is approximated within the computed bounds using a polynomial regression (<ref>). To ensure the soundness of the approximations, a bound on the approximation errors is computed and added to the result (line:alg_img_enc:error1line:alg_img_enc:error2).
Using <ref>, we define a set-based forward propagation.

$i \gets 1$ $\nnNumNeurons_k$
Find bounds $\mathcal{I}_{k-1(i)}$ of $\hiddenSet_{k-1(i)}$ *<ref>
Find polynomial approximation $p_{k,i}$ of $\actfun_k$ *<cit.>
$d_{k(i)} \gets \max_{x\in\mathcal{I}_{k-1(i)}}\abs{\actfun_k(x) - p_{k,i}(x)}  + \delta$*<cit.>
$\widetilde{\hiddenSet}_{k(i)} \gets $ evaluate $p_{k,i}$ with $\hiddenSet_{k-1(i)}$ *<cit.>
$\hiddenSet_{k(i)} \gets \widetilde{\hiddenSet}_{k(i)} \oplus [-d_{k(i)},d_{k(i)}]$ *<ref>

$\hiddenSet_k \gets \hiddenSet_{k(1)}\times\dots\times\hiddenSet_{k(\nnNumNeurons_k)}$

Image enclosure of an activation layer <cit.>.

For an input set $\inputSet\subset\R^{\nnNumNeurons_0}$, an outer approximation of the output set $\outputSet\subset\R^{\nnNumNeurons_\nnNumLayers}$ of a neural network can be computed as

\begin{align*}
\hiddenSet_0                         & = \inputSet\text{,}                                                                      \\
\hiddenSet_k                         & = L_k(\hiddenSet_{k-1})\text{,}                                                          \\
\outputSet = \hiddenSet_\nnNumLayers & \supseteq\outputSetExact \coloneqq \left\{N_\theta(x) \mid x\in\inputSet\right\}\text{,}
\end{align*}

where for $k=1,\dots,\nnNumLayers$,

\begin{equation*}
L_k(\hiddenSet_{k-1}) = \begin{cases}
W_k\,\hiddenSet_{k-1} + b_k    & \text{if $k$-th layer is linear,} \\
\enclose{L_k,\hiddenSet_{k-1}} & \text{otherwise,}
\end{cases}
\end{equation*}

and the operation $\encloseName$ is specified in <ref>.

§.§ Problem Statement

The training goal for a robust neural network is to minimize the worst-case loss within the $\epsilon$-perturbance set of each input in the training dataset <cit.>:

\begin{equation}\label{eq:robust_training_goal}
\min_\theta \sum_{(\nninput_i,\nntarget_i)\in\mathcal{D}} \max_{\tilde{\nninput}_i\in\pi_\epsilon(\nninput_i)} \pointLoss(\nntarget_i,N_\theta(\tilde{\nninput}_i))\text{.}
\end{equation}

In this work, we derive a end-to-end set-based training procedure that uses set-based computations

* to train robust neural networks and

* to simplify the subsequent robustness verification of the trained neural networks.

§ FAST IMAGE ENCLOSURE OF ACTIVATION FUNCTIONS

The training of neural networks requires many forward propagations, which are costly for set-based forward propagations due to the image enclosures of activation layers.
This makes sampling-based methods <cit.> for the image enclosure impractical.
In contrast, <cit.> derives fast analytical solutions for the approximation errors of a specific linear approximation of s-shaped activation functions. However, these linear approximations create large approximation errors. To address this issue, we derive analytical solutions for the approximation errors of an arbitrary monotonically increasing linear approximation for three typical activation functions: ReLU (<ref>), hyperbolic tangent (<ref>), and logistic sigmoid (<ref>). Secondly, we provide a linear approximation with approximation errors that are smaller or equal to <cit.> while being equally fast to compute.
For the remainder of this section, let $\actfun:\R\to\R$ be a monotonically increasing function which is approximated within an interval $\mathcal{I} = [l,u]\subset\R$.

Within the interval $\mathcal{I}$, we approximate $\actfun$ by a linear function $\approxfun(x) \coloneqq \approxfunSlope\, x + \approxfunYint$, where

\begin{align*}
\approxfunSlope & \coloneqq \frac{\actfun(u) - \actfun(l)}{u - l}\text{,} & \approxfunYint & \coloneqq \actfun\left(\frac{u + l}{2}\right) - \approxfunSlope\, \frac{u + l}{2}\text{.}
\end{align*}

The approximation errors of $\approxfun$ are given by the largest lower distance and upper distance between $\mu$ and $\approxfun$ (see <ref>).

The approximation errors of $\approxfun$ (<ref>) for $\actfun$ within the interval $\mathcal{I}$ are defined as

\begin{align*}
\approxErrorL & \coloneqq \min_{x\in\mathcal{I}} \actfun(x) - \approxfun(x)\text{,} & \approxErrorU & \coloneqq \max_{x\in\mathcal{I}} \actfun(x) - \approxfun(x)\text{.}
\end{align*}

Image enclosure of hyperbolic tangent: (left) Our linear approximation and approximation errors; (right) Comparison of our image enclosure and the image enclosure by <cit.>.
Image enclosure of hyperbolic tangent: (left) Our linear approximation and approximation errors; (right) Comparison of our image enclosure and the image enclosure by <cit.>.

§.§ Approximation Errors for ReLU

The ReLU is defined as $\relu(x)\coloneqq\max(0,x)$. Since ReLU is piecewise linear, it suffices to evaluate $\relu(x) - \approxfun(x)$ at $x = 0$ and the bounds $x\in\{l,u\}$.

The approximation errors of $\approxfun$ for ReLU are computed as

\begin{align*}
\approxErrorL & = \min_{x\in\extremePoints} \relu(x) - \approxfun(x)\text{,} & \approxErrorU & = \max_{x\in\extremePoints} \relu(x) - \approxfun(x)\text{,}
\end{align*}

where $\extremePoints = \left\{l,0,u\right\}\cap\mathcal{I}$.

ReLU is monotonic for $[l,0]$ and $[0,u]$. Thus, the approximation errors are found at $x = 0$ or the bounds $x\in\{l,u\}$.

§.§ Approximation Errors for Hyperbolic Tangent and Logistic Sigmoid

We can efficiently compute the approximation errors for differentiable activation functions by returning the minimum and maximum values of the finite set of extreme points of $\actfun(x) - \approxfun(x)$. If the extreme points are not contained within the interval, we include the boundaries of the interval. For the hyperbolic tangent and logistic sigmoid, we provide the set $\extremePoints$ of all extreme points of $\actfun(x) - \approxfun(x)$.

The approximation errors of $\approxfun$ for $\tanh$ are

\begin{align*}
\approxErrorL & = \min_{x\in\extremePoints} \tanh(x) - \approxfun(x)\text{,} & \approxErrorU & = \max_{x\in\extremePoints} \tanh(x) - \approxfun(x)\text{,}
\end{align*}

where $\extremePoints = \left\{\pm\arctanh\left(\sqrt{1 - \approxfunSlope}\right),l,u\right\}\cap\mathcal{I}$.

The derivative of the hyperbolic tangent is $1 - \tanh(x)^2$. We demand that the derivative of $\tanh(x) - \approxfun(x)$ is $0$ and simplify the terms:

\begin{align*}
&  & 0        & = \frac{\mathrm{d}}{\mathrm{d} x} \left(\tanh(x) - \approxfun(x)\right) \\
\Leftrightarrow &  & 0        & = 1 - \tanh(x)^2 - \approxfunSlope                                      \\
\Leftrightarrow &  & \tanh(x) & = \pm\sqrt{1 - \approxfunSlope}                                         \\
\Leftrightarrow &  & x        & = \pm\arctanh\left(\sqrt{1 - \approxfunSlope}\right)\text{.}\qedhere
\end{align*}

The logistic sigmoid is defined as $\sigmoid(x) \coloneqq \frac{1}{1 + e^{-x}}$ <cit.>.

The approximation errors of $\approxfun$ for $\sigmoid$ are

\begin{align*}
\approxErrorL & = \min_{x\in\extremePoints} \sigmoid(x) - \approxfun(x)\text{,} & \approxErrorU & = \max_{x\in\extremePoints} \sigmoid(x) - \approxfun(x)\text{,}
\end{align*}

where $\extremePoints = \left\{\pm 2\,\arctanh\left(\sqrt{1 - 4\,\approxfunSlope}\right),l,u\right\}\cap\mathcal{I}$.

It holds that $\sigmoid(x) = 0.5\,(\tanh(0.5\,x) + 1)$ <cit.>.
We demand that derivative of $\sigmoid(x) - \approxfun(x)$ is $0$ and simplify the terms:

\begin{align*}
&  & 0             & = \frac{\mathrm{d}}{\mathrm{d} x} (\sigmoid(x) - \approxfun(x))                                                \\
\Leftrightarrow &  & 0             & = \frac{\mathrm{d}}{\mathrm{d} x}\left(0.5\,\left(\tanh\left(0.5\,x\right) + 1\right)\right) - \approxfunSlope \\
\Leftrightarrow &  & \tanh(0.5\,x) & = \pm\sqrt{1 - 4\,\approxfunSlope}                                                                             \\
\Leftrightarrow &  & x             & = \pm 2\,\arctanh\left(\sqrt{1-4 \,\approxfunSlope}\right)\text{.}\qedhere
\end{align*}

While the approach in <cit.> only works for a specific linear approximation, our approach works for any (monotonically increasing) linear approximation.
In addition, we prove that the approximation errors of our linear approximation (<ref>) are always smaller or equal to the approximation errors by <cit.> w.r.t. the area in the input-output plane (see <ref>) measuring the integrated approximation error over $\mathcal{I}$:

\begin{equation}\label{eq:img_enc_area}
A([\approxErrorL,\approxErrorU],\mathcal{I}) \coloneqq (l - u)\,(\approxErrorU - \approxErrorL)\text{.}
\end{equation}

Let $\actfun$ be an s-shaped function, and let $\mathcal{I}=[l,u]$ be an interval. Moreover, let $\approxErrorL$ and $\approxErrorU$ be the approximation errors of $\approxfun$ as defined in <ref>, and let $d_{\singhSub}$ be the approximation error by <cit.>.
It holds that

\begin{equation*}
A([\approxErrorL,\approxErrorU],\mathcal{I}) \leq A([-d_{\singhSub},d_{\singhSub}],\mathcal{I})\text{.}
\end{equation*}

See appendix.

<ref> shows an instance where the smaller approximation errors by our image enclosure enable the verification of a neural network that is not possible with the image enclosure by <cit.>.

Comparison of the output set of a neural network (nn-small trained point-based on F-MNIST with the input set $\pi_\epsilon(x)$ where $\epsilon=0.005$) computed with different image enclosures: The output set computed with our image enclosure is significantly smaller and does not intersect the unsafe region, while the output set computed with the image enclosure by <cit.> does intersect the unsafe region.
Comparison of the output set of a neural network (nn-small trained point-based on F-MNIST with the input set $\pi_\epsilon(x)$ where $\epsilon=0.005$) computed with different image enclosures: The output set computed with our image enclosure is significantly smaller and does not intersect the unsafe region, while the output set computed with the image enclosure by <cit.> does intersect the unsafe region.

§.§ Implementation

<ref> implements our image enclosure. First, we compute the interval bounds of the input set (<ref>). For each neuron, the linear approximation (<ref>) and the approximation errors (<ref>) are computed. The linear approximations are applied to the input set (<ref>), and finally the approximation errors (<ref>) are added. The time complexity of <ref> is polynomial. We use the time complexity of <ref> to later derive the time complexity of our training approach.

For an input set $\hiddenSet_{k-1}=\zonoDefault$ with $c\in\R^n$ and $G\in\R^{n\times q}$, <ref> has time complexity $\bigO(n^2\,q)$ w.r.t. the number of input dimensions $n$ and the number of generators $q$.

Finding the interval bounds of $\hiddenSet_{k-1}$ (<ref>) takes time $\bigO(n\,q)$ (<ref>). Computing the linear approximation (<ref>) and the approximation errors (<ref>) for each neuron takes constant time; hence, the loop takes time $\bigO(n)$. The linear map of $\hiddenSet_{k-1}$ (<ref>) takes time $\bigO(n^2\,q)$ (<ref>). Adding the approximation errors (<ref>) takes time $\bigO(n^2)$. Thus, in total we have $\bigO(n\,q) + \bigO(n) + \bigO(n^2\,q) + \bigO(n^2) = \bigO(n^2\,q)$.

Find bounds $\mathcal{I}_{k-1}$ of $\hiddenSet_{k-1}$ *<ref>
$i \gets 1$ $\nnNumNeurons_k$
Compute linear approx. $\approxfunSlope_{k(i)}\,x + \approxfunYint_{k(i)}$*<ref>
Compute approx. errors $\approxErrorL_{k(i)}$, $\approxErrorU_{k(i)}$*<ref>

$\widetilde{\hiddenSet}_k \gets \diag{\approxfunSlope_k}\,\hiddenSet_{k-1} + \approxfunYint_k$ *<ref>
$\hiddenSet_{k} \gets \widetilde{\hiddenSet}_{k} \oplus [\approxErrorL_k,\approxErrorU_k]$ *<ref>

Fast image enclosure of an activation layer.

The image enclosure of an s-shaped function like hyperbolic tangent or logistic sigmoid by <cit.> fits a polynomial to the activation function using polynomial regression and uses many evenly distributed samples along the activation function to bound the approximation errors (see <ref>). <ref> no longer uses a polynomial regression or requires sampling to compute the approximation errors. Moreover, each loop iteration of <ref> is independent, and the entire loop can be efficiently computed in a batch-wise fashion using matrix operations on a GPU. The results of this section obviously also benefit the set-based verification of neural networks.

§ SET-BASED TRAINING OF NEURAL NETWORKS

We present a novel set-based training procedure for neural networks. Intuitively, we replace each point-based training step with a set-based training step and make adjustments where necessary. In each training iteration, we

* compute a set of losses containing a loss for every input of an $\epsilon$-perturbance set (<ref>),

* derive a set-based backpropagation that computes sets of gradients, and

* aggregate the sets of gradients to update the values for the parameters of the neural network.

§.§ Set-Based Loss

First, we define a set-based loss function returning a set of losses for an entire set of outputs. In our work, we define a set-based loss function $\setLoss:\R^{\nnNumNeurons_\nnNumLayers}\times 2^{\R^{\nnNumNeurons_\nnNumLayers}}\to 2^{\R^{\nnNumNeurons_\nnNumLayers}}$ so that it combines

* the set-based evaluation of a point-based loss with

* the interval norm of the output set <ref>.

The set-based loss function uses a hyperparameter $\tau\in[0,1]$ to weigh the set-based evaluation of the point-based loss and the interval norm. The included interval norm minimizes the size of the output sets, thereby increasing the robustness of the trained neural network.

Given a (point-based) loss function $\pointLoss:\R^{\nnNumNeurons_\nnNumLayers}\times\R^{\nnNumNeurons_\nnNumLayers}\to\R$, we define a set-based loss function as

\begin{equation*}
\setLoss(\nntarget,\outputSet) \coloneqq (1 - \tau)\,\pointLoss(\nntarget,\outputSet) + \frac{\tau}{\epsilon}\,\norm{\outputSet}_I\text{,}
\end{equation*}

where $\pointLoss(\nntarget,\outputSet) = \left\{\pointLoss(\nntarget,\nnoutput)\;\left|\;\nnoutput\in\outputSet\right.\right\}$ is the set-based evaluation of $\pointLoss$, $\epsilon\in\R_{>0}$ is the input perturbation radius, and $\norm{\outputSet}_I$ is the interval norm of $\outputSet$ according to <ref>.

To make tuning the hyperparameter $\tau$ easier, the interval norm in <ref> is normalized with the input perturbation radius $\epsilon\in\R_{>0}$. The normalization is derived from the ratio of the interval norms of the output set and the input set, which is an $\epsilon$-perturbance set:

\begin{equation}
\frac{\norm{\outputSet}_I}{\norm{\pi_\epsilon(x)}_I} \overset{\text{\cref{def:eps_perturbed_inputs}}}{=} \frac{\norm{\outputSet}_I}{\epsilon}\text{.}
\end{equation}

Similar to point-based training, we use the gradient of the set-based loss function to update the parameters of a neural network. The gradient of a set-based loss is a set that contains a gradient for every input of the input set. Computing the set-based evaluation of the point-based loss might be hard or impossible, e.g., computing a set-based cross-entropy error is hard due to the logarithm (see <ref>). However, we only need the gradient of the set-based loss for training. If the point-based loss is the half-squared error or the cross-entropy error (<ref>), the gradient is just the difference between the output and the target (<ref>):

\begin{align}\label{eq:set_eval_point_loss}
\begin{split}
\frac{\partial \pointLoss(\nntarget,\outputSet)}{\partial \outputSet} & = \left\{\left.\frac{\partial \pointLoss(\nntarget,\nnoutput)}{\partial \nnoutput}\;\right|\;\nnoutput\in\outputSet\right\} = \left\{\nnoutput - \nntarget\;\left|\;\nnoutput\in\outputSet\right.\right\} \\
& = \zonotope{\centerZono{\outputSet} - \nntarget}{\generatorsZono{\outputSet}}\text{,}
\end{split}
\end{align}

where $\outputSet = \zonotope{\centerZono{\outputSet}}{\generatorsZono{\outputSet}}$.

The second term of the set-based loss function is the interval norm of the output set. The gradient of the interval norm is a zonotope, where the center is the derivative w.r.t. the center and the generator matrix is the derivative w.r.t. the generator matrix.

The gradient of the interval norm is

\begin{equation*}
\frac{\partial \norm{\zonoName}_{I}}{\partial \zonoName} \coloneqq \zonotope{\frac{\partial \norm{\zonoName}_{I}}{\partial c}}{\frac{\partial \norm{\zonoName}_{I}}{\partial G}}\text{\kern-\zonoZLen} = \frac{1}{n}\,\zonotope{\zeros}{\operatorname{sign}(G)}\text{,}
\end{equation*}

where $\zonoName = \zonoDefault\subset\R^n$.

The gradient of the absolute value $\abs{\cdot}$ is the $\operatorname{sign}$ function.

\begin{equation*}
\frac{\partial \norm{\zonoName}_{I}}{\partial \zonoName} = \zonotope{\frac{\partial \norm{\zonoName}_{I}}{\partial c}}{\frac{\partial \norm{\zonoName}_{I}}{\partial G}}
= \frac{1}{n}\,\zonotope{\zeros}{\operatorname{sign}(G)}\text{.}\qedhere
\end{equation*}

By combining <ref> and <ref>, we can compute the gradient of a set-based loss function:

If the point-based loss $\pointLoss$ is the half-squared error or the cross-entropy error (<ref>), then the gradient of the set-based loss function $\setLoss$ is

\begin{multline*}
\frac{\partial \setLoss(\nntarget,\outputSet)}{\partial \outputSet} = \zonotope{(1 - \tau)\,(\centerZono{\outputSet} - \nntarget)}{(1 - \tau)\,\generatorsZono{\outputSet} + \frac{\tau}{\epsilon\,\nnNumNeurons_\nnNumLayers}\,\operatorname{sign}(\generatorsZono{\outputSet})}\text{\kern-\zonoZLen,}
\end{multline*}

where $\outputSet = \zonotope{\centerZono{\outputSet}}{\generatorsZono{\outputSet}}$.

This directly follows from <ref>.

To have a end-to-end set-based training process, we extend the backpropagation (<ref>) through neural networks to sets.

§.§ Set-Based Backpropagation

In this section, we lift the point-based backpropagation to a set-based evaluation. For every layer of the neural network, the set-based backpropagation computes the gradient of the set-based loss function $\setLoss$ w.r.t. the output set $\hiddenSet_k$:

\begin{equation}\label{eq:set-backprop-grads}
\gradSet_k \coloneqq \frac{\partial \setLoss(\nntarget,\outputSet)}{\partial \hiddenSet_k} = \left\{\left.\frac{\partial \setLoss(\nntarget,\outputSet)}{\partial h_k}\;\right|\;h_k\in\hiddenSet_k\right\}\text{.}
\end{equation}

The set-based backpropagation of linear layers is straightforward as it just applies a linear map (<ref>). However, the backpropagation of activation layers requires the gradient of its nonlinear activation function (<ref>). Since zonotopes are not closed under nonlinear maps, we approximate the gradient of the activation function $\actfun_k$ with the slope $m_{k(i)}$ of its linear approximation $\approxfun_{k,i}$ (see <ref>) obtained during the set-based forward propagation. For the $i$-th neuron, we have

\begin{equation}\label{eq:act_layer_approx_set_grad}
\approxfunSlope_{k(i)} = \frac{\partial \approxfun_{k,i}(\hiddenSet_{k-1(i)})}{\partial \hiddenSet_{k-1(i)}} \approx \frac{\partial\actfun_k(\hiddenSet_{k-1(i)})}{\partial \hiddenSet_{k-1(i)}}\text{.}
\end{equation}

Using this approximation, we can formulate the set-based backpropagation:

Let $\outputSet\subset\R^{\nnNumNeurons_\nnNumLayers}$ be an output set of a neural network with target $\nntarget\in\R^{\nnNumNeurons_\nnNumLayers}$. The gradients $\gradSet_k$ are computed in reverse order as

\begin{align*}
\gradSet_\nnNumLayers & = \frac{\partial \setLoss(\nntarget,\outputSet)}{\partial \outputSet}\text{,} \\
\gradSet_{k-1}        & = \begin{cases}
W_k^\top\,\gradSet_k                 & \text{if $k$-th layer is linear,} \\
\diag{\approxfunSlope_k}\,\gradSet_k & \text{otherwise,}
\end{cases}
\end{align*}

for all $k\in\{\nnNumLayers,\dots,1\}$. If the $k$-th layer is an activation layer, then the vector $\approxfunSlope_k\in\R^{\nnNumNeurons_k}$ denotes the slopes of the linear approximations of that layer (<ref>).

See appendix.

Illustration of a set-based forward propagation (black) and set-based backpropagation (blue).
Illustration of the computation during a set-based forward propagation (black) and set-based backpropagation (blue).

<ref> illustrates the computations during a set-based forward propagation and set-based backpropagation.

§.§ Set-Based Update of Weights and Biases

We describe now how we use the set of gradients $\gradSet_k$ and the set of inputs $\hiddenSet_{k-1}$ to update the weights and biases of a linear layer.
Our main idea is to compute the outer product in <ref> in a set-based fashion using $\gradSet_k\,\hiddenSet_{k-1}^\top\subset\R^{\nnNumNeurons_k\times \nnNumNeurons_{k-1}}$. However, there are dependencies between the zonotopes, as the set of gradients $\gradSet_k$ are ultimately computed from the set of inputs $\hiddenSet_{k-1}$. We explicitly keep track of these dependencies using symbolic zonotopes <cit.>, which assign each generator a label. Let $\gradSet_k = \zonotope{c_\gradSet}{G_\gradSet}$ and $\hiddenSet_{k-1} = \zonotope{c_\hiddenSet}{G_\hiddenSet}$ with $c_\gradSet\in\R^{\nnNumNeurons_k}$, $G_\gradSet\in\R^{\nnNumNeurons_k\times q}$, $c_\hiddenSet\in\R^{\nnNumNeurons_{k-1}}$, and $G_\hiddenSet\in\R^{\nnNumNeurons_{k-1}\times r}$. We assign each column of the generator matrices $G_\gradSet$ and $G_\hiddenSet$ a label, which we denote by $G_\gradSet^{\mid l_\gradSet}$ and $G_\hiddenSet^{\mid l_\hiddenSet}$, where $l_\gradSet\in\N^q$ and $l_\hiddenSet\in\N^r$ are labels. We use the labels to compute a Cartesian product that respects the dependencies between the sets $\gradSet_k$ and $\hiddenSet_{k-1}$ <cit.>:

\begin{equation}\label{eq:cart_prod_def}
\gradSet_k\times\hiddenSet_{k-1} = \zonotope{\begin{bmatrix} c_\gradSet \\ c_\hiddenSet \end{bmatrix}}{\begin{bmatrix} \zeros & G_\gradSet^{\mid l_\gradSet\cap l_\hiddenSet} & G_\gradSet^{\mid l_\gradSet\setminus l_\hiddenSet} \\ G_\hiddenSet^{\mid l_\hiddenSet\setminus l_\gradSet} & G_\hiddenSet^{\mid l_\gradSet\cap l_\hiddenSet} & \zeros\end{bmatrix}}\text{\kern-\zonoZLen.}
\end{equation}

The generators with common labels are concatenated vertically, whereas those with unique labels are padded with zeros. Using the Cartesian product, we define a set-based outer product that respects the dependencies between $\gradSet_k$ and $\hiddenSet_{k-1}$:

\begin{equation}\label{eq:outer_prod_def}
\gradSet_k\,\hiddenSet_{k-1}^\top \coloneqq \left\{g_k\,h_{k-1}^\top\;\left|\;\begin{bmatrix} g_k^\top & h_{k-1}^\top \end{bmatrix}^\top\in\gradSet_k\times\hiddenSet_{k-1}\right.\right\}\text{.}
\end{equation}

To update the weight matrix and the bias vector, we could simply sample the set-based outer product. However, by sampling, we lose much information contained in the gradient set and the input set. While we could increase the effectiveness by taking more samples, we want to use all gradients and inputs to update the weights and biases. Hence, we aggregate the entire set-based outer product by computing its expected value, where we see the factors of the generators $\beta$ as random variables. First, we simplify the computation of the set-based outer product by exploiting the dependencies between the gradients $\gradSet_k$ and the inputs $\hiddenSet_{k-1}$:

The set-based outer product between $\gradSet_k$ and $\hiddenSet_{k-1}$ is computed as

\begin{equation*}
\gradSet_k\,\hiddenSet_{k-1}^\top = \left\{\updateWfun_k(\beta)\;\left|\;\beta\in[-1,1]^q\right.\right\}\text{,}
\end{equation*}

\begin{align*}
\updatebfun_k(\beta) & \coloneqq \begin{cases*}
c_\gradSet + G_\gradSet^{\mid l_\gradSet}\,\beta & if $\beta\in[-1,1]^q$, \\
\zeros\                                          & otherwise,
\end{cases*}                                                       \\
\updateWfun_k(\beta) & \coloneqq \begin{cases*}
\updatebfun_k(\beta)\,\left(c_\hiddenSet + \begin{bmatrix} G_\hiddenSet^{\mid l_\hiddenSet} & \zeros \end{bmatrix}\,\beta\right)^\top & if $\beta\in[-1,1]^q$, \\
\zeros                                                                                & otherwise.
\end{cases*}
\end{align*}

We make two observations:

* The image enclosure of an activation layer adds new generators for the approximation errors (<ref>);

* the ordering of the generators is not changed during a set-based forward propagation or a set-based backpropagation.

Hence, $l_\hiddenSet\setminus l_\gradSet$ is empty and $l_\gradSet\cap l_\hiddenSet = l_\hiddenSet$:

\begin{equation*}
\begin{bmatrix} \zeros & G_\gradSet^{\mid l_\gradSet\cap l_\hiddenSet} & G_\gradSet^{\mid l_\gradSet\setminus l_\hiddenSet} \\ G_\hiddenSet^{\mid l_\hiddenSet\setminus l_\gradSet} & G_\hiddenSet^{\mid l_\gradSet\cap l_\hiddenSet} & \zeros\end{bmatrix} = \begin{bmatrix} G_\gradSet^{\mid l_\hiddenSet} & G_\gradSet^{\mid l_\gradSet\setminus l_\hiddenSet} \\ G_\hiddenSet^{\mid l_\hiddenSet} & \zeros\end{bmatrix} = \begin{bmatrix} \multicolumn{2}{c}{G_\gradSet^{\mid l_\gradSet}} \\ G_\hiddenSet^{\mid l_\hiddenSet} & \zeros\end{bmatrix}\text{.}
\end{equation*}

Thus, for $\begin{bsmallmatrix} {\displaystyle g_k^\top} & {\displaystyle h_{k-1}^\top} \end{bsmallmatrix}^\top\in\gradSet_k\times\hiddenSet_{k-1}$, with some $\beta\in[-1,1]^q$:

\begin{equation*}
g_k\,h_{k-1}^\top \overset{\text{\cref{eq:cart_prod_def}}}{=} \left(c_\gradSet + G_\gradSet^{\mid l_\gradSet}\,\beta\right)\,\left(c_\hiddenSet + \begin{bmatrix} G_\hiddenSet^{\mid l_\hiddenSet} & \zeros \end{bmatrix}\,\beta\right)^\top\text{\kern-\topLen} = \updateWfun_k(\beta)\text{.}\qedhere
\end{equation*}

For a specific $\beta\in[-1,1]^q$, $\updateWfun_k(\beta)$ and $\updatebfun_k(\beta)$ are samples:

\begin{align}
\updateWfun_k(\beta) & \in\gradSet_k\,\hiddenSet_{k-1}^\top\text{,} & \updatebfun_k(\beta) & \in\gradSet_k\text{.}
\end{align}

We aggregate all elements of the set-based outer product by computing the expected value of $\updateWfun_k$ for an assumed probability distribution of the factors $\beta$; to update the bias vectors, we compute the expected value of $\updatebfun_k$:

\begin{align}\label{eq:weight_bias_update_sets}
W_k & \gets W_k - \eta\,\E\left[\updateWfun_k(\beta)\right]\text{,} & b_k & \gets b_k - \eta\,\E\left[\updatebfun_k(\beta)\right]\text{.}
\end{align}

<ref> computes the expected values of $\updateWfun_k$ and $\updatebfun_k$ based on a probability distribution of the factors $\beta$. To simplify matters, we assume that the expected value of a factor is $0$, which is reasonable as zonotopes are point-symmetric.

Let $\beta$ be a random variable with

\begin{equation}\label{prop:mean_outer_prod_zono:asm}
\E\left[\beta\right] = \zeros\text{,}
\end{equation}

the expected values of $\updateWfun_k$ and $\updatebfun_k$ are

\begin{align*}
\E\left[\updateWfun_k(\beta)\right] & = c_\gradSet\,c_\hiddenSet^\top + G_\gradSet^{\mid l_\gradSet}\,\E\left[\beta\,\beta^\top\right]\,\begin{bmatrix} G_\hiddenSet^{\mid l_\hiddenSet} & \zeros \end{bmatrix}^\top\text{\kern-\topLen,} \\
\E\left[\updatebfun_k(\beta)\right] & = c_\gradSet \text{.}
\end{align*}

Using <ref> we have

\begin{equation*}
\E\left[\updatebfun_k(\beta)_{(j)}\right] = c_{\gradSet(j)} + G_{\gradSet(j,\cdot)}^{\mid l_\gradSet}\,\E\left[\beta\right] = c_{\gradSet(j)}\text{.}
\end{equation*}

Moreover, we show,

\begin{align*}
& \E\left[\updateWfun_k(\beta)_{(i,j)}\right] \overset{\text{\cref{prop:outer_prod_simp}}}{=} \E\left[\updatebfun_k(\beta)_{(i)}\,\left(c_{\hiddenSet(j)} + \begin{bmatrix} G_{\hiddenSet(j,\cdot)}^{\mid l_\hiddenSet} & \zeros \end{bmatrix}\,\beta\right)\right] \\
& = \begin{aligned}[t]
c_{\gradSet(i)}\,c_{\hiddenSet(j)} & + \left(c_{\gradSet(i)}\,\begin{bmatrix} G_{\hiddenSet(j,\cdot)}^{\mid l_\hiddenSet} & \zeros \end{bmatrix} + c_{\hiddenSet(j)}\,G_{\gradSet(i,\cdot)}^{\mid l_\gradSet}\right)\,\E\left[\beta\right] \\
& + G_{\gradSet(i,\cdot)}^{\mid l_\gradSet}\,\E\left[\beta\,\beta^\top\right]\,\begin{bmatrix} G_{\hiddenSet(j,\cdot)}^{\mid l_\hiddenSet} & \zeros \end{bmatrix}^\top
\end{aligned}                  \\
\overset{\text{\cref{prop:mean_outer_prod_zono:asm}}} & {=} c_{\gradSet(i)}\,c_{\hiddenSet(j)} + G_{\gradSet(i,\cdot)}^{\mid l_\gradSet}\,\E\left[\beta\,\beta^\top\right]\,\begin{bmatrix} G_{\hiddenSet(j,\cdot)}^{\mid l_\hiddenSet} & \zeros \end{bmatrix}^\top\text{\kern-\topLen.}\qedhere
\end{align*}

For now, we assume an independent and uniform distribution of the factors $\beta\sim U(-1,1)^q$.

Assuming $\beta\sim U(-1,1)^q$, the expected values of $\updateWfun_k$ and $\updatebfun_k$ are

\begin{align*}
\E\left[\updateWfun_k(\beta)\right] & = c_\gradSet\,c_\hiddenSet^\top + \frac{1}{3}\,G_\gradSet^{\mid l_\gradSet}\,\begin{bmatrix} G_\hiddenSet^{\mid l_\hiddenSet} & \zeros \end{bmatrix}^\top\text{\kern-\topLen,} & \E\left[\updatebfun_k\left(\beta\right)\right] & = c_\gradSet \text{.}
\end{align*}

We use <ref>: The expected value of the uniform distribution $U(-1,1)$ is $0$, hence $\E\left[\beta\right] = \zeros$ <cit.>.
If $i\neq j$, then $\beta_i$ and $\beta_j$ are independent and hence $\E\left[\beta_i\,\beta_j\right] = \E\left[\beta_i\right]\,\E\left[\beta_j\right] = 0$.
Moreover, if $i = j$, then $\E\left[\beta_i\,\beta_j\right] = \E\left[\beta_i^2\right] = \frac{1}{3}$ <cit.>.
Thus, ultimately, we have $\E\left[\beta\,\beta^\top\right] = \frac{1}{3}\,\eye{q}$.

The uniform distribution of the factors results in every generator being weighted with $\frac{1}{3}$.
We leave research on the effect of different distributions to future research, e.g., we can give more weight to adversarial attacks by assuming a higher probability of points near the boundaries.

§.§ Implementation

<ref> implements an iteration of set-based training. First, a set-based forward propagation computes the output set $\outputSet$ for an $\epsilon$-perturbance set (line:alg_set_train:init_perturb_inputline:alg_set_train:forward_prop_end). With $\outputSet$, the gradient of the set-based loss function $\gradSet_\nnNumLayers$ is computed (<ref>). A set-based backpropagation computes the gradients $\gradSet_k$ (line:alg_set_train:back_prop_startline:alg_set_train:back_prop_end). Finally, the weights and biases of every linear layer are updated (line:alg_set_train:weight_bias_update_startline:alg_set_train:weight_bias_update_end).

Input $\nninput\in\R^{\nnNumNeurons_0}$, Target $\nntarget\in\R^{\nnNumNeurons_\nnNumLayers}$
Neural network with updated weights and biases

$\hiddenSet_0 \gets \zonotope{\nninput}{\epsilon\,\eye{\nnNumNeurons_0}}$ *<ref>
(*[f]set-based forward prop. (<ref>))$k\gets1$ $\nnNumLayers$
$k$-th layer is linear
$\hiddenSet_k \gets W_k\,\hiddenSet_{k-1} + b_k$

$\hiddenSet_k,\,\approxfunSlope_k \gets \fastEncloseAlgo\left(L_k,\hiddenSet_{k-1}\right)$

$\outputSet \gets \hiddenSet_\nnNumLayers$
$\gradSet_\nnNumLayers \gets \frac{\partial \setLoss(\nntarget,\outputSet)}{\partial \outputSet}$ *<ref>
(*[f]set-based backprop. (<ref>))$k \gets \nnNumLayers$ $1$
$k$-th layer is linear
$\gradSet_{k-1} \gets W_k^\top\,\gradSet_k$

$\gradSet_{k-1} \gets \diag{\approxfunSlope_k}\,\gradSet_k$

(*[f]update weights and biases (<ref>))$k\gets1$ $\nnNumLayers$
$k$-th layer is linear
$W_k \gets W_k - \eta\,\E\left[\updateWfun_k(\beta)\right]$
$b_k \gets b_k - \eta\,\E\left[\updatebfun_k(\beta)\right]$

Set-based training iteration. Hyperparameters: $\epsilon\in\R_{>0}$, $\tau\in[0,1]$, and $\eta\in\R_{>0}$.

Let $\nnNumNeurons_\text{max} \coloneqq \max_{k\in[\nnNumLayers]} \nnNumNeurons_k$ be the maximum number of neurons in a hidden layer of the neural network. The zonotopes used in <ref> have at most $q\in\bigO(\nnNumNeurons_0 + \nnNumNeurons_\text{max}\,\nnNumLayers)$ number of generators.
Moreover, <ref> has time complexity $\bigO(\nnNumNeurons_\text{max}^2\,q\,\nnNumLayers)$ w.r.t. $\nnNumNeurons_\text{max}$, $q$ and the number of layers $\nnNumLayers$.

The initial $\epsilon$-perturbance set has $\nnNumNeurons_0$ generators (<ref>) and every activation layer adds $\nnNumNeurons_k\in\bigO(\nnNumNeurons_\text{max})$ new generators for the approximation errors (<ref>). Moreover, there are at most $\nnNumLayers$ activation layers. Thus, in total, there are at most $\nnNumLayers\,\bigO(\nnNumNeurons_\text{max}) + \bigO(\nnNumNeurons_0) = \bigO(\nnNumNeurons_0 + \nnNumNeurons_\text{max}\,\nnNumLayers)$ generators.

Time Complexity: The $k$-th step of the set-based forward propagation takes time $\bigO(\nnNumNeurons_\text{max}^2\,q)$: The linear map (<ref>) takes time $\bigO(\nnNumNeurons_{k-1}\,\nnNumNeurons_k\,q) = \bigO(\nnNumNeurons_\text{max}^2\,q)$ (<ref>); the image enclosure (<ref>) takes time $\bigO(\nnNumNeurons_\text{max}^2\,q)$ (<ref>). Hence, the forward propagation (line:alg_set_train:forward_prop_startline:alg_set_train:forward_prop_end) takes time $\nnNumLayers\,\bigO(\nnNumNeurons_\text{max}^2\,q) = \bigO(\nnNumNeurons_\text{max}^2\,q\,\nnNumLayers)$.
Computing the gradient of the set-based loss function takes time $\bigO(\nnNumNeurons_\nnNumLayers + \nnNumNeurons_\nnNumLayers\,q) = \bigO(\nnNumNeurons_\text{max}\,q)$.
The $k$-th step of the set-based backpropagation computes a linear map (<ref> or <ref>) that takes time $\bigO(\nnNumNeurons_k\,\nnNumNeurons_{k+1}\,q) = \bigO(\nnNumNeurons_\text{max}^2\,q)$ (<ref>). Hence, the set-based backpropagation (line:alg_set_train:back_prop_startline:alg_set_train:back_prop_end) takes time $\nnNumLayers\,\bigO(\nnNumNeurons_\text{max}^2\,q) = \bigO(\nnNumNeurons_\text{max}^2\,q\,\nnNumLayers)$.
Updating a weight matrix takes time $\bigO(\nnNumNeurons_{k+1}\,\nnNumNeurons_k + \nnNumNeurons_{k+1}\,\nnNumNeurons_k\,q) = \bigO(\nnNumNeurons_\text{max}^2\,q)$ (<ref>) and updating a bias vector takes time $\bigO(\nnNumNeurons_k) = \bigO(\nnNumNeurons_\text{max})$ (<ref>). There are at most $\nnNumLayers$ linear layers; hence, updating the weights and biases of all linear layers takes time $\nnNumLayers\,(\bigO(\nnNumNeurons_\text{max}^2\,q) + \bigO(\nnNumNeurons_\text{max})) = \bigO(\nnNumLayers\,\nnNumNeurons_\text{max}^2\,q)$.
Thus, in total, an iteration of set-based training takes time $3\,\bigO(\nnNumNeurons_\text{max}^2\,q\,\nnNumLayers) = \bigO(\nnNumNeurons_\text{max}^2\,q\,\nnNumLayers)$.

The time complexity of set-based training is polynomial, and compared to point-based training, only has an additional factor $q\in\bigO(\nnNumNeurons_0 + \nnNumNeurons_\text{max}\,\nnNumLayers)$. The increased time complexity is expected because set-based training propagates entire generator matrices through the neural network. Moreover, for some linear relaxation methods, similar time complexities are reported <cit.>.

It is worth noting that set-based training only uses the operations: matrix-multiplication and matrix-addition, as well as $\min$ and $\max$. Hence, a set-based training iteration can be efficiently evaluated for an entire batch of inputs using matrix operations on a GPU.

§ EVALUATION

We use the MATLAB toolbox CORA <cit.> to implement set-based training. The efficacy of set-based training is evaluated by training neural networks of three different sizes (see <ref>) on three different datasets: MNIST <cit.>, Fashion-MNIST (F-MNIST) <cit.>, and Street View House Numbers (SVHN) <cit.>. The training parameters can be found in the appendix.

Networks and their number of parameters.

Dataset                     Model     Hidden Neurons     Parameters
3*MNIST / F-MNIST     nn-small           2x100                       89,610

nn-med             5x100                       119,910

nn-large           7x250                       575,260
2*SVHN                nn-med             5x100                       348,710

nn-large           7x250                       1,147,260

MNIST with nn-med and $\epsilon_\text{train} = 0.01$.
Training results for MNIST with nn-med and $\epsilon_\text{train} = 0.01$.

SVHN (verified accuracy / PGD accuracy) [%].

ab                                                                         3c$\mathstrut \epsilon_\text{test}$
$\mathstrut \epsilon_\text{train}$     Method     0.0                                                                0.001                               0.01

0.0                                             point               79.92                                                              73.29 / 75.89                       0.0 / 31.72
2*0.001                          PGD                 80.64                                                              75.95 / 77.78                       0.0 / 43.25

set, no approx.     80.98                                                     78.78 / 79.16     0.12 / 61.36
2*0.01                           PGD                 79.66                                                              78.1 / 78.44                        0.1 / 62.71

set, no approx.     80.06                                                     78.22 / 78.66     0.08 / 61.20

0.0                                             point               79.56                                                              61.54 / 76.21                       0.0 / 38.36
2*0.001                          PGD                 80.12                                                              66.43 / 77.01                       0.0 / 43.73

set, no approx.     84.67                                                     82.24 / 83.19     0.0 / 63.23
2*0.01                           PGD                 76.01                                                              72.99 / 74.39                       0.0 / 57.68

set, no approx.     84.39                                                     82.08 / 83.01     0.0 / 63.99

MNIST (verified accuracy / PGD accuracy) [%].

ab                                                                         3c$\mathstrut \epsilon_\text{test}$                                                           0pt1ex
$\mathstrut \epsilon_\text{train}$     Method     0.0                                                                                0.01                                0.1

0.0                                             point               97.0                                                                                42.84 / 77.0                        0.0 / 0.0
4*0.01                           PGD                 97.84                                                                                94.76 / 96.1               0.0 / 12.9

set                 95.78                                                                                93.76 / 94.04                       0.7 / 53.12

set, no approx.     97.12                                                                                95.7 / 96.06               0.04 / 61.78

set, $\tau=0$       95.4                                                                                93.26 / 93.62                       0.14 / 35.36
3*0.1                            PGD                 97.08                                                                                96.2 / 96.4       0.08 / 84.3

set                 72.24                                                                                67.98 / 69.09                       19.14 / 37.54

set, no approx.     90.54                                                                                87.62 / 88.16                       2.36 / 50.86

0.0                                             point               97.02                                                                                6.34 / 77.0                         0.0 / 0.0
3*0.01                           PGD                 97.6                                                                                89.68 / 95.72                       0.0 / 12.76

set                 95.62                                                                                93.54 / 93.84                       0.0 / 45.24

set, no approx.     97.46                                                                                96.14 / 96.58     0.0 / 60.52
3*0.1                            PGD                 97.48                                                                                96.6 / 96.84      0.0 / 86.22

set                 41.78                                                                                38.78 / 39.76                       9.42 / 21.18

set, no approx.     90.52                                                                                86.95 / 87.7                        0.68 / 46.6

0.0                                             point               97.94                                                                                0.0 / 89.28                         0.0 / 0.02
2*0.01                           PGD                 98.16                                                                                4.36 / 96.82               0.0 / 29.40

set                 96.56                                                                                95.18 / 95.54              0.0 / 54.04
3*0.1                            PGD                 98.46                                                                                91.58 / 97.94     0.0 / 87.32

set                 33.66                                                                                31.6 / 32.64                        6.18 / 19.94

set, no approx.     89.52                                                                                86.54 / 87.06                       0.02 / 48.54

F-MNIST (verified accuracy / PGD accuracy) [%].

ab                                                                         3c$\mathstrut \epsilon_\text{test}$
$\mathstrut \epsilon_\text{train}$     Method     0.0                                                                0.005                              0.05

0.0                                             point               88.88                                                              64.96 / 74.04                      0.0 / 0.86
2*0.005                          PGD                 89.02                                                     83.4 / 85.56              0.0 / 33.2

set                 88.04                                                              84.12 / 84.98             0.0 / 50.12
2*0.05                           PGD                 83.32                                                     82.32 / 82.6     8.8 / 74.54

set                 61.66                                                              60.24 / 60.84                      42.36 / 55.48

0.0                                             point               88.08                                                              19.2 / 70.66                       0.0 / 1.32
2*0.005                          PGD                 88.12                                                              72.68 / 84.78                      0.0 / 28.1

set                 88.38                                                     82.94 / 85.2     0.0 / 43.46
2*0.05                           PGD                 84.08                                                     83.1 / 83.34     0.0 / 75.28

set                 54.92                                                              53.8 / 54.56                       40.04 / 53.86

We compare set-based training (denoted by set) against point-based training (denoted by point) and training with adversarial inputs computed with PGD <cit.> (denoted by PGD (training)).
We also evaluate set-based training ignoring the approximation errors (denoted by set, no approx.), which reduces the memory load.
Moreover, we distinguish between the perturbation radius $\epsilon_\text{train}$ used during training and the perturbation radius $\epsilon_\text{test}$ used during testing[All reported perturbation radii are w.r.t. normalized inputs between 0 and 1.].
Ideally, we would like to report a neural network's adversarial accuracy for a perturbation radius. The adversarial accuracy is the minimum accuracy that can be achieved by perturbing the inputs of the test dataset. However, there is no efficient way to compute the adversarial accuracy <cit.>. Therefore, we report

* the verified accuracy as a lower bound and

* the PGD accuracy as an upper bound for the adversarial accuracy.

The verified accuracy is the percentage of test inputs for which we can formally verify the robustness of the neural network using set-based computations <cit.>. Moreover, the PGD accuracy is the accuracy of a neural network for adversarial inputs computed with PGD <cit.>. We list the findings of our experiments:

* For small training perturbation radii, the set-based trained neural networks achieve higher accuracies than the PGD-trained and point-based trained networks, e.g. for nn-med on F-MNIST with $\epsilon_\text{train} = 0.005$ (see <ref>) or for nn-large on SVHN with $\epsilon_\text{train} = 0.01$ (see <ref>).

* Set-based trained neural networks are significantly easier to verify, e.g., for nn-large on MNIST with $\epsilon_\text{train} = \epsilon_\text{test} = 0.01$, the verified accuracy of the set-based trained networks is 95.18% while the PGD trained networks and point-based trained networks achieve verified accuracies of 4.36% and 0.0% (see <ref>).

* Furthermore, set-based training with approximation errors trains neural networks with slightly lower clean accuracy ($\epsilon_\text{test} = 0$) and PGD accuracies than set-based training without approximation errors. However, set-based training with approximation errors achieves higher verified accuracies, which indicates that set-based training with approximation errors makes the trained neural networks easier to verify. <ref> visualizes the accuracies.

* We observe that set-based training with the interval norm trains more accurate neural networks than set-based training without the interval norm (denoted by set, $\tau=0$), e.g., see nn-small on MNIST with $\epsilon_\text{train} = 0.01$ (<ref>). This observation justifies the interval norm as a part of the set-based loss.

* For larger training perturbation radii, the set-based trained networks achieve lower accuracies, e.g., clean accuracy ($\epsilon_\text{test} = 0$) of 72.24% for nn-small with $\epsilon_\text{train}=0.1$ on MNIST (see <ref>). The reason for the lower accuracies is large approximation errors that build up during the set-based forward propagations. The large approximation errors distort the gradients and thereby prevent accurate training.

Set-based training on MNIST and F-MNIST with nn-small and nn-med is slower than point-based but slightly faster than PGD training (see Table <ref>). For nn-large on MNIST or SVHN, set-based training takes more time than point-based and PGD training.

Training time [s / epoch].

Dataset             Model     point     PGD     set     set, no approx.
3*MNIST       nn-small           3.87               13.5             8.91             7.81

nn-med             6.17               22.07            17.39            13.35

nn-large           8.69               31.51            65.43            29.48
2*F-MNIST     nn-small           4.54               13.11            9.42             8.01

nn-med             7.52               20.50            17.77            13.47
2*SVHN        nn-med             10.18              26.33            -                74.14

nn-large           12.78              34.23            -                141.17

Currently, the memory load and the large approximation errors limit the scalability of set-based training. The large approximation errors increase the outer approximation of the output sets, thereby increasing the number of false-positive outputs, i.e., outputs that are not true outputs. The false-positive outputs distort the gradients and prevent accurate training. Future research should explore methods to overcome both of these limitations.
Furthermore, we only evaluate set-based training for classification tasks. However, without any modifications, set-based training can be applied to train neural networks for regression tasks: The gradient of the half-squared and cross-entropy errors are the same (<ref>).

§ CONCLUSION

We introduce the first end-to-end set-based training procedure for neural networks. While other robust training approaches train neural networks using single gradients and inputs, we use entire sets of gradients and inputs to train neural networks. We use set-based computations with zonotopes to efficiently compute sets of gradients for entire input sets.
Finally, we update the parameters of neural networks by aggregating all gradients.
Our experimental results demonstrate that our set-based approach effectively trains robust neural networks while significantly simplifying the subsequent robustness verification of the trained neural networks. In many instances, our set-based training approach outperforms training with state-of-the-art adversarial attacks. Hence, set-based training represents a promising new direction for the field of robust neural network training.

The authors gratefully acknowledge partial financial support from the project SPP 2422 (No. 500936349) and the project FAI (No. 286525601), both funded by the German Research Foundation (DFG).

Missing 'biblatex' package
The bibliography requires the 'biblatex' package.

booktitleProc. of the Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH)
titleAn Introduction to CORA 2015

booktitleProc. of the Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH)
titleChecking and Establishing Reachset Conformance in CORA 2023

Technische Universität München

titleReachability analysis and its application to the safety assessment of autonomous cars

Springer New York, NY

titlePattern recognition and machine learning

journaltitleInt. Journal on Software Tools for Technology Transfer
titleFirst three years of the international verification of neural networks competition (VNN-COMP)

journaltitleAnn. of Nuclear Energy
titlePrediction of safety parameters of pressurized water reactor based on feature fusion neural network

titleZonotopes and Kalman observers: Gain optimality under distinct uncertainty paradigms and robust convergence

journaltitleInt. Journal of Control
titleA distributed Kalman filter with symbolic zonotopes and unique symbols provider for robust state estimation in CPS

Springer London

titleA modern introduction to probability and statistics

journaltitleDiscrete & Computational Geometry
titleA geometric inequality and the complexity of computing volume

booktitleProc. of the Workshop on Applied Verification for Continuous and Hybrid Systems (ARCH)
titleARCH-COMP 2022 Category Report: Falsification with Unbounded Resources

booktitleIEEE Symposium on Security and Privacy (SP)
titleAI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation

booktitleProc. of the Int. Conf. on Hybrid Systems: Computation and Control (HSCC)
titleReachability of Uncertain Linear Systems Using Zonotopes

MIT Press

titleDeep learning

booktitleProc. of the Int. Conf. on Learning Representations (ICLR)
titleExplaining and Harnessing Adversarial Examples

booktitleProc. of the IEEE/CVF Int. Conf. on Computer Vision (ICCV)
titleScalable Verified Training for Provably Robust Image Classification

journaltitleIEEE Signal Processing Magazine
titleDeep Neural Networks for Acoustic Modeling in Speech Recognition: The Shared Views of Four Research Groups

booktitleAIAA/IEEE Digital Avionics Systems Conference (DASC)
titleTowards Verification of Neural Networks for Small Unmanned Aircraft Collision Avoidance

booktitleInt. Conf. on Computer Aided Verification (CAV)
titleReluplex: An Efficient SMT Solver for Verifying Deep Neural Networks

booktitleProc. of the Int. Conf. on Learning Representations (ICLR)
titleAdam: A Method for Stochastic Optimization

booktitleNASA Formal Methods
titleOpen- and Closed-Loop Neural Network Verification Using Polynomial Zonotopes

booktitleProc. of the Int. Conf. on Learning Representations (ICLR)
titleAdversarial Machine Learning at Scale

booktitleProc. of the Int. Conf. on Hybrid Systems: Computation and Control (HSCC)
titleAutomatic Abstraction Refinement in Neural Network Verification Using Sensitivity Analysis

journaltitleATT Labs [Online]. Available: http://yann.lecun.com/exdb/mnist
titleMNIST handwritten digit database

booktitleProc. of the IEEE Conf. on Decision and Control (CDC)
titleReachability Analysis of ARMAX Models

booktitleProc. of the IEEE/CVF Conf. on Computer Vision and Pattern Recognition (CVPR)
titleTowards Evaluating and Training Verifiably Robust Neural Networks

booktitleProc. of the Int. Conf. on Learning Representations (ICLR)
titleTowards Deep Learning Models Resistant to Adversarial Attacks

booktitleProc. of the Int. Conf. on Machine Learning (ICML)
titleDifferentiable Abstract Interpretation for Provably Robust Neural Networks

journaltitleProc. of the ACM on Programming Languages
titlePRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations

booktitleProc. of the NIPS Workshop on Deep Learning and Unsupervised Feature Learning
titleReading Digits in Natural Images with Unsupervised Feature Learning

journaltitleProcedia Engineering
titleModelling using Polynomial Regression

booktitleIEEE Symposium on Security and Privacy (SP)
titleDistillation as a Defense to Adversarial Perturbations Against Deep Neural Networks

booktitleProc. of the AAAI Conf. on Artificial Intelligence (AAAI)
titleImproving the adversarial robustness and interpretability of deep neural networks by regularizing their input gradients

titleGuaranteeing Constraints of Disturbed Nonlinear Systems Using Set-Based Optimal Control in Generator Space

booktitleProc. of the Int. Conf. on Neural Information Processing Systems (NeurIPS)
titleFast and Effective Robustness Certification

booktitleProc. of the Int. Conf. on Learning Representations (ICLR)
titleBoosting Robustness Certification of Neural Networks

booktitleProc. of the Int. Conf. on Learning Representations (ICLR)
titleIntriguing properties of neural networks

booktitleProc. of the Int. Conf. on Learning Representations (ICLR)
titleRobustness May Be at Odds with Accuracy

booktitleProc. of the IEEE/CVF Conf. on Computer Vision and Pattern Recognition (CVPR)
titleYOLOv7: Trainable bag-of-freebies sets new state-of-the-art for real-time object detectors

booktitleProc. of the Int. Conf. on Machine Learning (ICML)
titleTowards Fast Computation of Certified Robustness for ReLU Networks

booktitleProc. of the Int. Conf. on Machine Learning (ICML)
titleProvable Defenses against Adversarial Examples via the Convex Outer Adversarial Polytope

titleFashion-MNIST: a Novel Image Dataset for Benchmarking Machine Learning Algorithms

journaltitleProc. of the Institution of Mechanical Engineers, Part D: Journal of Automobile Engineering
titleSteering angle prediction YOLOv5-based end-to-end adaptive neural network control for autonomous vehicles

booktitleProc. of the Int. Conf. on Learning Representations (ICLR)
titleTowards Stable and Efficient Training of Verifiably Robust Neural Networks

booktitleProc. of the Int. Conf. on Neural Information Processing Systems (NeurIPS)
titleEfficient Neural Network Robustness Certification with General Activation Functions

get arXiv to do 4 passes: Label(s) may have changed. Rerun