# Certifying Robustness of Convolutional Neural Networks with Tight Linear
Approximation

Yuan Xiao  Nanjing UniversityJiangsuChina<EMAIL_ADDRESS>,
Tongtong Bai  Southwest University of Science and TechnologySichuanChina
<EMAIL_ADDRESS>,  Mingzheng Gu  Nanjing UniversityJiangsuChina
<EMAIL_ADDRESS>,  Chunrong Fang  Nanjing UniversityJiangsuChina
<EMAIL_ADDRESS>and  Zhenyu Chen  Nanjing UniversityJiangsuChina
<EMAIL_ADDRESS>
###### Abstract.

The robustness of neural network classifiers is becoming important in the
safety-critical domain and can be quantified by robustness verification.
However, at present, efficient and scalable verification techniques are always
sound but incomplete. Therefore, the improvement of certified robustness
bounds is the key criterion to evaluate the superiority of robustness
verification approaches. In this paper, we present a Tight Linear
approximation approach for robustness verification of Convolutional Neural
Networks(Ti-Lin). For general CNNs, we first provide a new linear constraints
for S-shaped activation functions, which is better than both existing _Neuron-
wise Tightest_ and _Network-wise Tightest_ tools. We then propose _Neuron-wise
Tightest linear bounds_ for Maxpool function. We implement Ti-Lin, the
resulting verification method. We evaluate it with 48 different CNNs trained
on MNIST, CIFAR-10, and Tiny ImageNet datasets. Experimental results show that
Ti-Lin significantly outperforms other five state-of-the-art methods(CNN-Cert
(boopathy2019cnn, ), DeepPoly (singh2019abstract, ), DeepCert
(wu2021tightening, ), VeriNet (henriksen2020efficient, ), Newise
(zhang2022provably, )). Concretely, Ti-Lin certifies much more precise
robustness bounds on pure CNNs with Sigmoid/Tanh/Arctan functions and CNNs
with Maxpooling function with at most 63.70% and 253.54% improvement,
respectively.

##  1\. Introduction

Although neural networks achieve remarkable success in many complex
classification tasks, such as speech and image recognition, researchers
discover that non-robust neural networks are vulnerable to the perturbation
from environment and adversarial attacks (moosavi2017universal, ;
szegedy2013intriguing, ; DBLP:conf/issta/00020LJMZ22, ;
DBLP:conf/issta/ZhaoCWYS021, ). In some safety-critical and security-sensitive
domain, such as self-driving (gopinath2018deepsafe, ) and face recognition
(goswami2018unravelling, ), some subtle adversarial perturbation is extremely
imperceptible and harmful, and may cause disastrous consequences. Therefore,
there is a great need to certify model robustness guarantees against
adversarial attacks, which can provide certified defense against any possible
attack (singh2018fast, ; boopathy2019cnn, ; du2021cert, ; muller2021prima, ).

The methodology of neural network robustness verification could be divided
into two categories: _complete verifier_ and _incomplete verifier_ (ji2022, ).
_Complete verifier_ (katz2017reluplex, ; ehlers2017formal, ; huang2017safety,
; tjeng2018evaluating, ) which can get accurate robustness bounds, is time-
consuming and only applies to ReLU-based networks. In contrast, _incomplete
verifier_ (weng2019proven, ; fazlyab2019probabilistic, ; jia2020certified, )
risks verification precision loss due to over-approximation but is more
scalable and efficient. Thus, to evaluate the robustness of other types of
CNNs, acceleration techniques, such as linear approximation
(zhang2018efficient, ; lyu2020fastened, ; wu2021tightening, ) or abstract
interpretation (gehr2018ai2, ; singh2018fast, ) is necessary. As approximation
technique inevitably introduces overestimation, certified lower bound is the
key criterion to evaluate robustness verification methods’ performances.

Regarding the tightness of the linear approximation technique, there is a
plenty of works focusing on narrowing the input-output zone of non-linear
functions in the network to gain larger certified robustness bounds
(zhang2018efficient, ; wu2021tightening, ; lyu2020fastened, ; ko2019popqorn, ;
boopathy2019cnn, ; singh2019abstract, ). Some works propose tight linear
bounds of non-linear functions by producing the minimal over-approximation
zone, resulting in much more precise certified robustness bounds. Zhang et al.
(zhang2022provably, ) define the linear bounds producing the minimal over-
approximation area as _Neuron-wise Tightest_ linear bounds. Concretely,
POPQORN (ko2019popqorn, ), CNN-Cert (boopathy2019cnn, ), and VeriNet
(henriksen2020efficient, ) propose _Neuron-wise Tightest_ robustness bounds of
$\sigma(x)tanh(y),x\cdot\sigma(y)$ functions, ReLU function, and
Sigmoid/Tanh/Arctan function, respectively. Recently, Zhang et al.
(zhang2022provably, ) introduce the notion of _Network-wise Tightest_ and
propose _Network-wise Tightest_ linear bounds for monotonous CNNs with
Sigmoid/Tanh/Arctan function. Unfortunately, regarding the approximation
methods’ performances on CNNs with Sigmoid/Tanh/Arctan function, _Neuron-wise
Tightest_ technique(VeriNet) is limited in precision while _Network-wise
Tightest_ technique(Newise (zhang2022provably, )) is limited in scalability.
Moreover, Maxpooling function is far more complex to verified as it is a
multivariate function. Some attempts have been made to verify Maxpooling
function but result in loose certified robustness bounds (boopathy2019cnn, ;
singh2019abstract, ).

To address the above challenges, in this work, we propose a Tight Linear
approximation method called Ti-Lin for general CNNs. By introducing the notion
of _Neuron-wise Tightest_ , we discover that _Neuron-wise Tightest_ is
equivalent to _Layer-wise Tightest_ , which can explain the reason why
minimizing the area/volume between upper and lower constraints of non-linear
functions can get a tighter robustness bound. We then analyze the limitations
of the _Neuron-wise Tightest_ and _Network-wise Tightest_ techniques(VeriNet,
Newise). To overcome these limitations, we make our first contribution by
proposing the Tightest linear bounds for Sigmoid/Tanh/Arctan function among
three state-of-the-art baseline methods. Regarding our second contribution, as
mentioned above, Maxpooling is a complex function to verified. To the best of
our knowledge, we are the first to propose _Neuron-wise Tightest_ linear
constraints for Maxpooling function.

We implement Ti-Lin atop the state-of-the-art robustness veriﬁcation framework
CNN-Cert (boopathy2019cnn, ). We evaluate it with neural networks trained on
MNIST, CIFAR-10, and Tiny ImageNet datasets. For CNNs with Sigmoid/Tanh/Arctan
functions, experimental results reveal that VeriNet (henriksen2020efficient, )
is superior to DeepCert (wu2021tightening, ) in 78.33% cases and Ti-Lin
outperforms these two state-of-the-art techniques in 96.67% cases.
Furthermore, Ti-Lin outperforms Newise, which is _Network-wise Tightest_
approach with up to 63.70% improvement to certified robustness bounds. For
CNNs with Maxpooling function, Ti-Lin outperforms CNN-Cert (boopathy2019cnn, )
and DeepPoly (singh2019abstract, ) with up to 235.54%, 43.14% improvement to
certified robustness bounds, respectively. Finally, we conduct Wilcoxon rank-
sum test (Capitani2011OnSO, ) and the results confirm that Ti-Lin
significantly outperform the five state-of-the-art baseline methods in
precision with the same time consumption.

Compared to other related works, Ti-Lin has four significant advantages: (i)
effective, it provides much tighter robustness bounds than state-of-the-art
approaches,(ii) efficient, it has almost the same time consumption as other
state-of-the-art techniques, (iii) versatile, it applies to general CNNs,
(iv)detailed analysis and proof, it provides proofs to all theorems mentioned
in this work.

In summary, our work makes the following contributions:

  * •

We propose a Tight Linear approximation technique(Ti-Lin), which applies to
general CNNs with ReLU, Sigmoid, Tanh, Arctan, and Maxpooling functions.

  * •

We identity the limitations of existing _Neuron-wise Tightest_ and _Network-
wise Tightest_ methods. We then propose novel linear constraints for
Sigmoid/Tanh/Arctan function, which stands for the Tightest among the existing
_Neuron-wise Tightest_ and _Network-wise Tightest_ tools.

  * •

We first propose provably _Neuron-wise Tightest_ linear constraints for
Maxpool function, which significantly outperforms prior works in precision.

  * •

We evaluate our methods on 35 different CNNs with Sigmoid/Tanh/Arctan
functions and 13 types of CNNs with Maxpooling, which are both trained on
MNIST, CIFAR-10 and Tiny ImageNet. The results confirm that Ti-Lin certifies
more precise robustness bounds in an efficient manner than other five state-
of-the-art baseline methods. We make our implementation and appendix available
at https://github.com/Ti-Lin/Ti-Lin

The rest of this paper is organized as follows. In Section 2, we introduce
some necessary preliminaries of our approach, including notations of Ti-Lin,
some notions of linear approximation technique and notions of the tightness of
the linear approximation technique. In Section 3, we present a technical
description of Ti-Lin. We first introduce the limitationd of the existing
_Neuron-wise Tightest_ and _Network-wise Tightest_ technique which motivates
us to find a tighter constraints for Sigmoid/Tanh/Arctan function. Then, we
propose Neuron-wise Tightest linear bounds for Maxpool function and finally we
present the whole computing process of our approach. In Section 4, we first
introduce our experiment settings, including datasets, models and research
questions and then we analyse our experimental results. Section 5 and 6 are
threats to validity and related works. Section 7 is the summary of this paper.

##  2\. Preliminaries

This section briefly introduces some related concepts and notations to
understand our approach. Specially, we present the linear upper and lower
bounds of convolutional and fully-connected layers, which is fundamental to
our approach.

###  2.1. Notations

Let $F(x):\mathbb{R}^{n_{0}}\to\mathbb{R}^{n_{K}}$ be a neural network
classifier function with (K+1) layers and $x_{0}$ be an input data point. We
use $\sigma(\cdot)$ to denote all non-linear functions in $F(x)$. In our work,
non-linear functions can be
Tanh:$\sigma(x)=\frac{e^{x}-e^{-x}}{e^{x}+e^{-x}}$,
Arctan:$\sigma(x)=tan^{-1}(x)$, Sigmoid: $\sigma(x)=\frac{1}{1+e^{-x}}$,
ReLU:$\sigma(x)=max(0,x)$, Maxpool:
$\sigma(x_{1},\cdots,x_{n})=max\\{x_{1},\cdots,x_{n}\\}$. We use superscripts
$k$ to denote the index of layers, subscripts $u,l$ to denote upper and lower
and subscripts $j$($i,q$,respectively) denotes the
$j^{th}$($i^{th},q^{th}$,respectively) Neuron of current layer. The symbols
$u_{j}(\cdot),l_{j}(\cdot)$ denote the linear approximation bounding
lines/planes of the $j^{th}$ Neuron at current layer and $a,b$ denotes the
slope and intercept of linear approximation function, for example,
$u_{j}(x)=a_{u,j}x+b_{u,j},l_{j}(x)=a_{l,j}x+b_{l,j}$. We use superscripts
$+$,$-$ to denote the positive and negative values, for example,
$a^{+}=max(a,0),a^{-}=min(a,0)$. In our approach, the global linear bounds of
$F^{k}(x)$ are the final linear bounds to compute $l^{k},u^{k}$. Other
notations are in Table 1.

Notation | Definition
---|---
$F:\mathbb{R}^{n_{0}}\to\mathbb{R}^{n_{K}}$ | network classifier
$n_{k}$ | number of Neurons in the $k^{th}$ layer
$[K]$ | the set $\\{1,\cdots,K\\}$
$F_{j}^{k}(x):\mathbb{R}^{n_{0}}\to\mathbb{R}$ | the $j^{th}$ output of the $k^{th}$ layer
$L_{j}(x):\mathbb{R}^{n_{0}}\to\mathbb{R}$ | linear lower bound of $F_{j}^{K}(x)$
$U_{j}(x):\mathbb{R}^{n_{0}}\to\mathbb{R}$ | linear upper bound of $F_{j}^{K}(x)$
$L_{j}^{k}(x):\mathbb{R}^{n_{0}}\to\mathbb{R}$ | linear lower bound of $F_{j}^{k}(x)$
$U_{j}^{k}(x):\mathbb{R}^{n_{0}}\to\mathbb{R}$ | linear upper bound of $F_{j}^{k}(x)$
$a_{u,i}^{k}$ | the slope of linear upper bound
$b_{u}^{k}$ | the intercept of linear upper bound
$A_{U,i}^{k}$ | the slope of $U^{k}(X)$
$B_{U}^{k}$ | the intercept of $U^{k}(X)$
$l_{j}^{k}$ | lower bound of $F_{j}^{k}(x)$
$u_{j}^{k}$ | upper bound of $F_{j}^{k}(x)$
$x^{k}\in[l^{k-1},u^{k-1}]$ | values of neurons at the $k^{th}$ layer
$f^{k}(x^{k-1}):R^{n_{k-1}}\to R^{n_{k}}$ | the function of the $k^{th}$ layer
$\gamma_{L,j}$ | global lower bound of $F_{j}^{K}(x)$
$\gamma_{U,j}$ | global upper bound of $F_{j}^{K}(x)$
Table 1. Notations

Let $\mathbb{B}_{p}(x_{0},\epsilon)$ denotes $x_{0}$ perturbed within an
$l_{p}$-normed ball with radius $\epsilon$, that is
$\mathbb{B}_{p}(x_{0},\epsilon)=\\{x|\|x-x_{0}\|_{p}\leq\epsilon\\}$. $t$
denotes the true label of $x_{0}$ in $F$, that is $t=argmax_{i}F_{i}(x_{0})$

###### Definition 2.1 (Local robustness bound).

if $\epsilon_{r}(\epsilon_{r}\geq 0)$ is the local robustness bound of an
input $x_{0}$ in neural network, if and only if these two conditions (i)
$argmax_{i}F_{i}(x)=t,\forall x\in\mathbb{B}_{p}(x_{0},\epsilon_{r})$ and (ii)
$\forall\delta>0,\exists
x_{a}\in\mathbb{B}_{p}(x_{0},\epsilon+\delta)s.t.argmax_{i}F_{i}(x_{a})\neq c$
are satisfied.

###### Definition 2.2 (Certified lower bound).

if $\epsilon_{cert}$ is a certified lower bound of input $x_{0}$ in a neural
network, if and only if these two conditions (i)
$\epsilon_{cert}\leq\epsilon_{r}$ and (ii) $argmax_{i}F_{i}(x)=t,\forall
x\in\mathbb{B}_{p}(x_{0},\epsilon_{r})$.

That is to say, the local robustness bound of input $x_{0}$ is the maximum
absolute safe radius of $x_{0}$, while the certified lower bound of $x_{0}$ is
the absolute safe radius of $x_{0}$.

###  2.2. Linear approximation

The key idea of the linear approximation technique is to give constrains
$l(x)\leq f(x)\leq u(x),x\in[l,u]$ of every layer’s function $f(x)$, including
non-linear, fully-connected and convolutional layers. Through propagation, the
linear constraints must ensure the value of output will not exceed the upper
and lower bounds, which is the key to keeping the soundness of the linear
approximation technique. In our work, we fully exploit the CNNs with Maxpool
and Sigmoid/Tanh/Arctan functions to give the Tightest linear constraints and
make use of the general framework in CNN-Cert (boopathy2019cnn, )

The procedure of computing robustness bounds is a layer-by-layer process
computing from the first hidden layer to the last output layer. To compute
global robustness bounds, we need to compute the linear bounds of every layer
in CNNs. For details of the whole computing procedure, readers can refer to
the work (singh2019abstract, ).

###### Definition 2.3 (Upper/Lower linear bounds).

Let $f^{k}_{i}(x)$ be the function of the $i^{th}$ Neuron in the $k^{th}$
layer of neural network $F$, with
$x\in[l,u]\subset\mathbb{R}^{n},a_{u},a_{l},b_{u},b_{l}\in\mathbb{R}^{n}$ and

$u_{i}(x)=a_{u}x+b_{u},l_{i}(x)=a_{l}x+b_{l}$

$u_{i}(x)$ and $l_{i}(x)$ are called linear upper and lower bounds of
$f^{k}_{i}(x)$ if $l_{i}(x)\leq f^{k}_{i}(x)\leq u_{i}(x),\forall x\in[l,u]$

It is worth mentioning that $n$ is determined by the type of $f^{k}_{i}(x)$.
When $f^{k}_{i}(x)$ is Maxpool function, $n$ is equal to the size of the input
to be pooled. When $f^{k}_{i}(x)$ is ReLU/Sigmoid/Tanh/Arctan function, $n=1$.
When the $k^{th}$ layer is a convolutional layer, $n$ corresponds to the size
of the weight filter, and the linear constraints are

$u_{i}(x)=w*x+b,l_{i}(x)=w*x+b.$

When the $k^{th}$ layer is a fully-connected layer, $n=n_{k-1}$ and the linear
constraints are

$u(x)=wx+b,l(x)=wx+b.$

###  2.3. Tightness of linear approximation techniques

Linear approximation techniques offer an over-approximation zone of every
layer’s function in essence. DeepPoly (singh2019abstract, ) first discovers
that minimizing the over-approximation zone can give rise to a more precise
certified robustness bound. However, empirical analysis in Newise
(zhang2022provably, ) shows that the linear constraints that producing the
minimal over-approximation zone could not lead to the most precise robustness
result all the time, which motivates us to find the relation between
minimizing the over-approximation zone and Tightest robustness bound.
Therefore, we introduce the notion of _Neuron-wise Tightest Linear Bounds_
from Newise.

###### Definition 2.4 (Neuron-wise Tightest).

upper linear approximation
$u_{i}^{k}:\times_{q\in[n_{k-1}]}[l_{q}^{k-1},u_{q}^{k-1}]\to\mathbb{R}$,
lower linear approximation
$l_{i}^{k}:\times_{q\in[n_{k-1}]}[l_{q}^{k-1},u_{q}^{k-1}]\to\mathbb{R}$ is
Neuron-wise Tightest iff
$D^{k-1}=\times_{q\in[n_{k-1}]}[l_{q}^{k-1},u_{q}^{k-1}],\forall
j\in[n_{k+1}]$,$\iint_{D^{k-1}}u_{i}^{k}(x)dx$ and
$\iint_{D^{k-1}}-l_{i}^{k}(x)dx$ are minimal

We discover _Neuron-wise Tightest_ linear bounds can keep the Tightest through
one-layer propagation(proved in appendix). Therefore, _Neuron-wise Tightest_
can explain why narrowing the over-approximation zone can increase certified
robustness bounds. Furthermore, Newise defines the notion of _Network-wise
Tightest_ , that is, _Network-wise Tightest_ linear bounds can keep the
Tightest through the whole network propagation. Furthermore, Newise provides
the _Network-wise Tightest_ linear bounds for monotonous networks, such as
non-negative networks (zhang2022provably, ).

###### Definition 2.5 (Network-wise Tightest).

global upper linear approximation
$U_{i}^{K}:\times_{q\in[n_{0}]}[x_{0,q}-\epsilon,x_{0,q}+\epsilon]\to\mathbb{R}$,
global lower linear approximation
$L_{i}:\times_{q\in[n_{0}]}[x_{0,q}-\epsilon,x_{0,q}+\epsilon]\to\mathbb{R}$
is network-wise Tightest iff for any different global linear constraints
$\hat{U}_{i}^{K},\hat{L}_{i}^{K}$,

$maxU_{i}^{K}(x)\leq max\hat{U}_{i}^{K}(x),\,\,minL_{i}^{K}(x)\geq
min\hat{L}_{i}^{K}(x),x\in\mathbb{B}_{p}(x_{0},\epsilon)$

##  3\. Methodology

In this section, we present a technical description of our approach.
Concretely, we first introduce our tight linear bounds for S-shaped activation
function, which is tighter than both _Neuron-wise Tightest_ and _Network-wise
Tightest_ techniques. Then, we propose _Neuron-wise Tightest_ linear bounds
for Maxpool function. Finally, we describe the process of computing certified
robustness bounds in our approach.

###  3.1. Tighter Linear Bounds for S-shaped activation Functions

As approximation technique inevitably introduces imprecision, giving tighter
approximation is crucial to obtaining more precise verification results.
Previous works mainly provide tighter certified robustness bounds by gradually
narrowing the input-output zone between the bound and linear constraint of
non-linear function. Henriksen et al. (henriksen2020efficient, ) propose
VeriNet and gives linear constraints for Sigmoid/Arctan/Tanh function by
producing the minimal input-output zone. By Definition 2.4, VeriNet is the
_Neuron-wise Tightest_ technique for robustness verification of CNNs with
Sigmoid/Arctan/Tanh function and stands for the highest precision in the
sequel of narrowing the zone. As shown in Figure1, VeriNet produces smaller
over-approximation zone than DeepCert, which is the most recent work.

To explain the reason why narrowing over-approximation zone can give rise to
certified robustness bounds, we define _Layer-wise Tightest_ linear bounds:

###### Theorem 3.1 (Layer-wise Tightest).

$\forall k\in[K],i\in[n_{k}],m=\frac{l^{k-1}+u^{k-1}}{2}$, if both
$u_{i}^{k}(m)$ and $-l_{i}^{k}(m)$ reach the minimum, then the linear upper
and lower linear approximations of every non-linear function are the layer-
wise Tightest.

We discover that _Layer-wise Tightest_ is equivalent to _Neuron-wise Tightest_
and we prove this in the Appendix. This means that _Neuron-wise Tightest_ can
be preserved through one-layer propagation, which can explain the reason why
VeriNet outperforms most previous works(such as DeepPoly (singh2018fast, ),
Neurify (Wang2018EfficientFS, )). Zhang et al. (zhang2022provably, ) discover
that VeriNet is sometimes inferior to DeepCert and we also compare these two
state-of-the-art methods(results shown in Table 2). To tackle this, they
define the notion of _Network-wise Tightest_ and propose Newise, the resulting
method, which can preserve the tightest through the whole network propagation.
However, Newise only has the best performance on monotonous neural
network(such as non-negative networks), which is not the mainstream.

To solve the above problems, we propose the Tightest linear constraints for
Sigmoid/Tanh/Arctan functions among these three state-of-the-art
methods(Newise, VeriNet and DeepCert). Different from Newise, our approach
performs well on general CNNs, without limiting conditions for the weights of
CNNs. Because Sigmoid, Arctan and Tanh functions satisfy when
$x<0,f^{\prime\prime}(x)>0$; when $x>0,f^{\prime\prime}(x)<0$; when
$x=0,f^{\prime\prime}(x)=0$ and are twice differentiable and centrosymmetry.
Therefore, these functions are with a characteristic S shape. Due to this
characteristic, these three activation functions’ linear constraints are
versatile in essence. We propose our linear bounds for Sigmoid/Tanh/Arctan
functions:

Figure 1. Linear approximation of S-shaped activation function in different $[l,u]$. |  | DeepCert | VeriNet
---|---|---|---
| $l_{p}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$
MINST, | Sig | 0.03587 | 0.24017 | 0.55843 | 0.03594 | 0.24094 | 0.56010
CNN5_3, | Tanh | 0.01015 | 0.08234 | 0.20855 | 0.01010 | 0.08240 | 0.20970
4 layers | Atan | 0.01204 | 0.09324 | 0.23936 | 0.01197 | 0.09333 | 0.23964
MINST, | Sig | 0.03482 | 0.20465 | 0.44958 | 0.03485 | 0.20515 | 0.45075
CNN5_3, | Tanh | 0.01258 | 0.09006 | 0.23889 | 0.01257 | 0.09014 | 0.23912
5 layers | Atan | 0.00984 | 0.06896 | 0.16568 | 0.00983 | 0.06902 | 0.16579
MINST, | Sig | 0.03602 | 0.17939 | 0.35227 | 0.03024 | 0.15513 | 0.32903
CNN5_3, | Tanh | 0.00896 | 0.06245 | 0.16180 | 0.00822 | 0.05748 | 0.13810
6 layers | Atan | 0.01202 | 0.07923 | 0.20257 | 0.01007 | 0.07339 | 0.18638
Table 2. Certified Robustness Bounds for $l_{1},l_{2},l_{\infty}$-norm
perturbation by DeepCert vs. VeriNet on FNNs and CNNs, CNN5_3 denotes CNN with
5 layers and 5 filters of size $3\times 3$

###### Theorem 3.2 (Sigmoid/Tanh/Arctan Linear Bounds).

Supposing the $k^{th}$ layer’s function $f(x)$ is the S-shaped activation
function, we define $m=F^{k-1}(x_{0})$. Given $f(x),x\in[l,u]$, the linear
bounds are:

case 1: If $m\geq 0$,

$l(x)=\left\\{\begin{aligned} &k(x-u)+f(u),k<f^{\prime}(l)\\\
&f^{\prime}(x^{**})(x-u)+f(u),k\geq f^{\prime}(l)\\\ \end{aligned}\right.$

$u(x)=\left\\{\begin{aligned} &f^{\prime}(m)(x-m)+f(m),k_{ml}>f^{\prime}(m)\\\
&f^{\prime}(x^{*})(x-l)+f(l_{x}),k_{ml}\leq f^{\prime}(m)\text{ and
}k>f^{\prime}(u)\\\ &k(x-l)+f(l),k_{ml}\leq f^{\prime}(m)\text{ and }k\leq
f^{\prime}(u)\\\ \end{aligned}\right.$

case 2: If $m<0$

$l(x)=\left\\{\begin{aligned} &f^{\prime}(m)(x-m)+f(m),k_{mu}\geq
f^{\prime}(m)\\\ &f^{\prime}(x^{**})(x-u)+f(u),k_{mu}<f^{\prime}(m)\text{ and
}k>f^{\prime}(l)\\\ &k(x-l)f(l),k_{mu}<f^{\prime}(m)\text{ and }k\leq
f^{\prime}(l)\end{aligned}\right.$

$u(x)=\left\\{\begin{aligned} &k(x-u)+f(u),k\leq f^{\prime}(u)\\\
&f^{\prime}(x^{*})(x-l)+f(l),k>f^{\prime}(u)\\\ \end{aligned}\right.$

where
$k=\frac{f(u)-f(l)}{u-l}$,$k_{ml}=\frac{f(m)-f(l)}{m-l}$,$k_{mu}=\frac{f(m)-f(u)}{m-u}$,$x^{*},x^{**}$
are tangent points, which are the solutions of these two equations:
$f^{\prime}(x^{*})=\frac{f(x^{*})-f(l)}{x^{*}-l},f^{\prime}(x^{**})=\frac{f(x^{**})-f(u)}{x^{**}-u}$.

Due to the space limitation, the proof of Theorem 3.2 is deferred to Appendix.
Based on Theorem 3.2, we can both efficiently and effectively obtain tight
upper and lower linear bounds for Sigmoid/Tanh/Arctan function.

###  3.2. Neuron-wise Tightest Linear Bounds for Maxpool Function

Because Maxpool function is a multivariate function, it is far more complex to
be verified compared to Sigmoid/Tanh/Arctan function. DeepPoly
(singh2019abstract, ) gives non-trivial linear bounds to Maxpooling function
and its parallel work, CNN-Cert (boopathy2019cnn, ) leverages a hyperplane
containing n different particular points to give the upper and lower bound.
Both these two state-of-the-art techniques fail to capture the characteristic
of Maxpooling function and fail to give its _Neuron-wise Tightest_ Linear
Bounds, resulting in loose robustness bounds. To address this problem, we
first leverage the notion of _Neuron-wise Tightest_ and discover the _Neuron-
wise Tightest_ Linear Bounds:

###### Theorem 3.3 (Neuron-wise Tightest Linear Bounds).

$\forall k\in[K],i\in[n_{k}],m=\frac{l^{k-1}+u^{k-1}}{2}$, if both
$u_{i}^{k}(m)$ and $-l_{i}^{k}(m)$ reach the minimum, then the linear upper
and lower linear approximations of every non-linear function are the Neuron-
wise Tightest.

Due to the space limitation, the proof of Theorem 3.3 is deferred to Appendix.
By Theorem 3.3, we further propose Theorem 3.4 to help us find _Neuron-wise
Tightest Linear Bounds_ of Maxpooling function.

###### Theorem 3.4 (Finding Neuron-wise Tightest Linear Bounds).

Given that $f(x)$ is a continuous function, then

(1) if $f^{\prime}(m)(x-m)+f(m)$ is an upper(lower) bound, then
$u(m)$($-l(m)$) reaches its minimum.

(2)considering two points $(d_{1},f(d_{1})),(d_{2},f(d_{2}))$ where
$d_{1},d_{2}\in\times_{i=1}^{n}[l_{i},u_{i}]$. When $m=\lambda
d_{1}+(1-\lambda)d_{2},\lambda\in[0,1]$, if the upper(lower) bounding
line/plane passes through $(d_{1},f(d_{1})),(d_{2},f(d_{2}))$, then

$u(m)$($-l(m)$) reaches its minimum.

Because Maxpooling function has a characteristic of piece-wise linearity, we
find two particular input points of Maxpooling function which satisfy Theorem
3.4(2). These two points help us to find _Neuron-wise Tightest_ upper bound.
We then leverage Theorem 3.4(1) and find _Neuron-wise Tightest_ lower bound.
The _Neuron-wise Tightest_ upper and lower bounds are presented as follows:

###### Theorem 3.5 (MaxPool Linear Bounds).

Given
$f(x_{1},\cdots,x_{n})=max\\{x_{1},\cdots,x_{n}\\},x_{i}\in[l_{i},u_{i}]$, we
first sort the elements of $\\{l_{i},u_{i}\\},i=1,\cdots,n$ from largest to
smallest and gain the sequence $q$. Then the linear bounds are:

upper bound: $u(x_{1},\cdots,x_{n})=\sum_{i}a_{i}(x_{i}-l_{i})+b$.
Specifically, there are three different cases:

case1: If $q:u_{i}\geq l_{i}\geq\cdots,\forall i$, then
$a_{i}=1;b=l_{i};a_{j}=0,j\neq i$.

case2: If $q:u_{i}\geq u_{j}\geq l_{j}\geq\cdots,\forall i,j$ or $q:u_{j}\geq
u_{i}\geq l_{j}\geq\cdots,\forall i,j$, then
$a_{i}=\frac{u_{i}-l_{j}}{u_{i}-l_{i}};a_{j}=1;b=l_{j};a_{j}=0,j\neq i,j$.

case3: If $q:u_{i}\geq u_{j}\geq u_{k}\geq\cdots,\forall i,j,k$, then
$a_{i}=\frac{u_{i}-u_{k}}{u_{i}-l_{i}};a_{j}=\frac{u_{j}-u_{k}}{u_{j}-l_{j}};b=u_{k};a_{j}=0,j\neq
i,j$.

lower bound: $l(x_{1},\cdots,x_{n})=x_{j},j=argmax_{i}(m_{i})$

Due to the space limitation, the proofs of Theorem 3.3 and 3.5 are deferred to
Appendix. In the Appendix, we also prove that the linear bounds in Theorem 3.5
is the _Neuron-wise Tightest_ Linear Bound for Maxpooling function.

Figure 2. A toy example of how Ti-Lin computing global bounds of a FNN with
one hidden-layer. For simplicity, activation function is ReLU.

###  3.3. Computing Certified Robustness Bounds

It consists of two parts to compute certified robustness bounds, i.e.
computing global bounds for all inputs under a perturbation threshold, and
computing certified robustness bounds such that all perturbed inputs have the
same output classification result as the original input point.

####  3.3.1. Computing global bounds $\gamma_{U,j},\gamma_{L,j}$ of network
output $F_{j}^{K}(x)$

Given a K-layer CNN or FNN $F$, an input data point $x_{0}$, and a
perturbation threshold $\epsilon$ with $l_{p}$ norm, we first compute linear
bounds of each layer $f^{k}(x),k=1,2,\cdots,K$ from the first hidden layer to
the last output layer. We then compute the global bounds of each layer by the
inequation, which are deduced by Holder’s inequality:

(1) $\displaystyle F(x)$
$\displaystyle\leq\epsilon\|A_{U}\|_{q}+A_{U}x_{0}+B_{U}$ (2) $\displaystyle
F(x)$ $\displaystyle\geq-\epsilon\|A_{L}\|_{q}+A_{L}x_{0}+B_{L}$

where $\frac{1}{q}+\frac{1}{p}=1$. Readers can refer to the work
(wu2021tightening, ) for the detailed deduction of the inequality. Note that
in this paper, $p=1,2,\infty$.

According to the perturbation range $x\in[x_{0}-\epsilon,x_{0}+\epsilon]$ of
input layer, we compute the linear bounds of the first hidden layer. Then, by
backsubstitution (singh2019abstract, )from current layer to the input layer
and leveraging eq(1),(2) we compute the bounds $[l^{1},u^{1}]$ of $F^{1}(x)$.
Next, based on $[l^{1},u^{1}]$, we can compute linear bounds of the second
hidden layer and then compute the bounds $[l^{2},u^{2}]$ by backsubstitution.
This process is repeated until the global bounds $[l^{K},u^{K}]$(a.k.a
$[\gamma_{L},\gamma_{U}]$) of output layer is produced. To better illustrate
the workflow of computing the global bounds, we cite a toy example from
DeepPoly (boopathy2019cnn, ) of how it works on a simple FNN with one hidden-
layer, two nodes of every layer and the bias set as zero(Figure 2). In Figure
2, $x^{k}_{i}$ represents the $i^{th}$ Neuron at the $k^{th}$ layer. We use
$u^{k}_{i},l^{k}_{i}$ to denote the upper and lower bounds of $x^{k}_{i}$, and
$u^{k}_{i}(\cdot),l^{k}_{i}(\cdot)$ to denote the upper and lower linear
bounds, for example,
$u^{2}_{2}(x^{1}_{1},x^{1}_{2})=0.5x^{1}_{2}+1,l^{2}_{2}(x^{1}_{1},x^{1}_{2})=0$.

####  3.3.2. Computing certified lower bound $\epsilon_{cert}$

We use a binary search algorithm to find the maximal certified robustness
bound against all perturbed input, as shown in Algorithm 1. Concretely, we
first initialize the perturbation range $\epsilon=0.05$. To keep $\epsilon\geq
0$, we focus on the logarithm of $\epsilon$(line 7,10). We decide whether the
perturbation range is an absolute safe radius by checking whether the lower
bound of $F_{t}(x)$ is larger than the upper bounds of $F_{j}(x),\forall
j,j\neq t$(line 5). If $\epsilon$ is an absolute safe radius, we increase the
perturbation range(line 7); otherwise, we decrease the perturbation range(line
10). The repeat times of the binary search procedure is 15 and the difference
between $\epsilon_{max}$ and $\epsilon_{min}$ is sufficiently small enough
when the algorithm terminates.

Algorithm 1 Computing the robustness bound

0: model F, input $x$, true label $t$;

0: $\epsilon_{cert}$;

1: $\epsilon\leftarrow 0.05$.

2: Let $\epsilon_{l}\leftarrow
log(\epsilon),\epsilon_{min}\leftarrow-\infty,\epsilon_{max}\leftarrow\infty$.

3: for i=0 to 14 do

4: Compute $\gamma_{L},\gamma_{U}$ of $F(x)$ with
$x\in\mathbb{B}_{p}(x_{0},exp(\epsilon_{l}))$

5: if $\gamma^{L}_{t}\geq max_{j\neq t}(\gamma^{U}_{j})$ then

6: $\epsilon_{min}=\epsilon_{l}$

7: $\epsilon_{l}=min(\epsilon_{l}+1,\frac{\epsilon_{max}+\epsilon_{min}}{2})$;

8: else

9: $\epsilon_{max}=\epsilon_{l}$

10:
$\epsilon_{l}=max(\epsilon_{l}-1,\frac{\epsilon_{max}+\epsilon_{min}}{2})$;

11: end if

12: end for

13: $\epsilon_{cert}=exp(\epsilon_{l})$

14: return $\epsilon_{cert}$

##  4\. Experiments

We conduct extensive experiments by comparing Ti-Lin with five state-of-the-
art tools (DeepCert (wu2021tightening, ), VeriNet (henriksen2020efficient, ),
Newise (zhang2022provably, ),CNN-Cert (boopathy2019cnn, ), DeepPoly
(singh2019abstract, )). The experiments run on a server running an 8 core
Intel(R) Xeon(R), Silver 4114 CPU, and 15 GB of RAM with Python 3.6.13(numpy
1.19.5 with numba 0.53.1). We use the Tensorflow 1.12.0 deep learning platform
to train and test CNNs.

Network | Certified Bounds | Average Computation Time(sec)
---|---|---
|  | DeepCert | VeriNet | Ti-Lin | DeepCert | VeriNet | Ti-Lin
| $l_{p}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$
MNIST | Sig | 0.03587 | 0.24017 | 0.55843 | 0.03594 | 0.24094 | 0.5601 | 0.03606 | 0.24209 | 0.56207 | 6.85 | 6.69 | 6.7 | 6.78 | 6.7 | 6.74 | 7.63 | 6.77 | 6.62
CNN5_3 | Tanh | 0.01015 | 0.08234 | 0.20855 | 0.0101 | 0.0824 | 0.2097 | 0.0101 | 0.08243 | 0.20976 | 6.82 | 6.84 | 6.82 | 6.83 | 6.74 | 6.74 | 6.89 | 6.72 | 6.71
4 layer | Atan | 0.01204 | 0.09324 | 0.23936 | 0.01197 | 0.09333 | 0.23964 | 0.01198 | 0.09338 | 0.23976 | 6.55 | 6.44 | 6.61 | 6.68 | 6.69 | 6.79 | 6.87 | 6.68 | 6.7
MNIST | Sig | 0.03482 | 0.20465 | 0.44958 | 0.03485 | 0.20515 | 0.45075 | 0.03502 | 0.20672 | 0.45423 | 16.42 | 16.37 | 18.75 | 16.17 | 16.42 | 17.95 | 16.83 | 16.02 | 17.45
CNN5_3 | Tanh | 0.01258 | 0.09006 | 0.23889 | 0.01257 | 0.09014 | 0.23912 | 0.01259 | 0.09034 | 0.23967 | 16.49 | 17.5 | 18.29 | 16.06 | 16.41 | 18.17 | 16.28 | 16.14 | 18.15
5layer | Atan | 0.00984 | 0.06896 | 0.16568 | 0.00983 | 0.06902 | 0.16579 | 0.00985 | 0.06913 | 0.16598 | 16 | 18.13 | 18.17 | 15.95 | 17.85 | 18.12 | 16.21 | 16.36 | 17.79
MNIST | Sig | 0.03602 | 0.17939 | 0.35227 | 0.03024 | 0.15513 | 0.32903 | 0.03645 | 0.18177 | 0.35641 | 31.98 | 32.89 | 31.96 | 32.30 |  33.33 | 32.72 | 32.8 | 34.17 | 32.27
CNN5_3 | Tanh | 0.00896 | 0.06245 | 0.1618 | 0.00822 | 0.05748 | 0.1381 | 0.00901 | 0.06278 | 0.16269 | 32.35 | 32.24 | 32.21 | 32.25 | 32.48 |  32.87 | 32.53 | 32.22 | 33.14
6layer | Atan | 0.01202 | 0.07923 | 0.20257 | 0.01007 | 0.07339 | 0.18638 | 0.01207 | 0.07956 | 0.2032 | 32.44 | 33.45 | 33.39 | 32.57 | 32.42 |  32.65 | 32.53 | 32.32 | 32.12
MNIST | Sig | 0.06192 | 0.23208 | 0.41802 | 0.06263 | 0.23518 | 0.42313 | 0.06317 | 0.23764 | 0.42798 | 55.81 | 55.67 | 53.77 | 59.19 | 55.75 | 62.80 | 54.4 | 56.03 | 54.5
CNN5_3 | Tanh | 0.00899 | 0.06489 | 0.17935 | 0.00904 | 0.06508 | 0.17953 | 0.00907 | 0.06531 | 0.18016 | 54.23 | 54.39 | 55.69 | 55.11 | 55.09 | 55.61 | 54.63 | 54.78 | 54.92
7layer | Atan | 0.01124 | 0.07608 | 0.18589 | 0.01128 | 0.07637 | 0.1864 | 0.01131 | 0.07655 | 0.1869 | 55.2 | 54.96 | 55.08 | 55.34 | 58.65 | 55.61 | 54.51 | 54.45 | 54.69
MNIST | Sig | 0.04335 | 0.1833 | 0.3564 | 0.04387 | 0.18567 | 0.3608 | 0.04433 | 0.18774 | 0.3648 | 84.3 | 82.28 | 81.01 | 83.63 | 82.65 | 83.20 | 85.13 | 88.17 | 82.53
CNN5_3 | Tanh | 0.00961 | 0.06128 | 0.14527 | 0.00965 | 0.06149 | 0.14567 | 0.0097 | 0.06181 | 0.14644 | 81.81 | 84.24 | 83.91 | 83.62 | 83.71 | 84.56 | 82.86 | 82.8 | 83.14
8 layer | Atan | 0.01001 | 0.06736 | 0.17055 | 0.01004 | 0.06764 | 0.17122 | 0.01007 | 0.06784 | 0.17177 | 83.25 | 83.02 | 80.2 | 83.67 | 83.83 | 84.10 | 82.54 | 82.8 | 82.47
MNIST | Sig | 0.03149 | 0.15305 | 0.31889 | 0.03163 | 0.15385 | 0.32056 | 0.03184 | 0.15492 | 0.32251 | 158.9 | 159.99 | 169.07 | 161.60 |  160.56 | 159.25 | 163.1 | 158.97 | 158.93
CNN10_3 | Tanh | 0.00739 | 0.04488 | 0.10848 | 0.00744 | 0.04524 | 0.10934 | 0.00746 | 0.04535 | 0.10964 | 159.68 | 160.31 | 169.27 |  160.18 | 160.01 | 160.15 | 159.08 | 159.6 | 159.12
8 layer | Atan | 0.00581 | 0.03499 | 0.08051 | 0.00588 | 0.03543 | 0.08148 | 0.00589 | 0.0355 | 0.08163 | 159.09 | 165.78 | 166.73 | 160.60 | 160.84 | 160.59 | 158.92 | 163.08 | 158.61
MNIST | Sig | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | -
CNN20_3 | Tanh | 0.00507 | 0.02932 | 0.06925 | 0.00512 | 0.02966 | 0.07009 | 0.00513 | 0.0297 | 0.07018 | 427.14 | 427.65 | 423.69 | 423.27 | 424.76 | 408.56 | 401.54 | 408.79 | 404.25
8 layer | Atan | 0.00581 | 0.03315 | 0.07906 | 0.00592 | 0.03376 | 0.08042 | 0.00593 | 0.03381 | 0.08057 | 419.33 | 420.43 | 414.76 | 413.13 | 414.5 | 408.8 | 404.26 | 409.78 | 409.43

Table 3. Averaged certified robusntess bounds and runtime on pure CNNs tested
on MNIST by DeepCert, VeriNet and Ti-Lin

Network | Certified Bounds | Average Computation Time(sec)
---|---|---
|  | DeepCert | VeriNet | Ti-Lin | DeepCert | VeriNet | Ti-Lin
| $l_{p}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$
CIFAR | Sig | 0.0048 | 0.07464 | 0.29181 | 0.00479 | 0.07456 | 0.29177 | 0.0048 | 0.07487 | 0.29242 | 27.27 | 27.19 | 27.35 | 29.12 | 28.86 | 29.64 | 27.97 | 27.51 | 27.99
CNN5_3 | Tanh | 0.0021 | 0.03887 | 0.13322 | 0.0021 | 0.03886 | 0.13323 | 0.0021 | 0.03887 | 0.13325 | 27.47 | 27.42 | 27.47 | 30.01 | 28.95 | 29.04 | 27.46 | 27.69 | 27.81
5 layer | Atan | 0.00232 | 0.04134 | 0.14716 | 0.00232 | 0.04135 | 0.14734 | 0.00232 | 0.04135 | 0.14734 | 26.81 | 26.97 | 27.11 | 28.85 | 29.04 | 29.4 | 28.3 | 27.61 | 28.03
CIFAR | Sig | 0.00778 | 0.10585 | 0.38266 | 0.00778 | 0.10589 | 0.3829 | 0.00777 | 0.10539 | 0.38016 | 102.03 | 113.12 | 108.31 | 99.03 | 105.53 | 96.09 | 111.07 | 120.69 | 114.31
CNN5_3 | Tanh | 0.00081 | 0.02575 | 0.12023 | 0.00081 | 0.02575 | 0.12041 | 0.00081 | 0.02575 | 0.12041 | 123.38 | 114.89 | 105.78 | 94.17 | 90.55 | 88.37 | 104.48 | 119.65 | 104.61
6 layer | Atan | 0.00094 | 0.02812 | 0.12944 | 0.00094 | 0.02813 | 0.12964 | 0.00094 | 0.02813 | 0.12964 | 103.85 | 113.59 | 106.33 | 94 .22 | 99.01 | 97.13 | 99.16 | 106.91 | 106.49
CIFAR | Sig | 0.02036 | 0.16852 | 0.52567 | 0.02046 | 0.1693 | 0.52814 | 0.02081 | 0.17176 | 0.53537 | 151.43 | 160.8 | 133.69 | 125.68 | 124.27 | 129.50 | 145.4 | 147.03 | 145.07
CNN5_3 | Tanh | 0.00078 | 0.02222 | 0.10962 | 0.00078 | 0.02222 | 0.10982 | 0.00078 | 0.02222 | 0.10982 | 139.93 | 146.92 | 127.9 |  124.18 | 125.57 | 123.87 | 134.31 | 145.56 | 140.34
7 layer | Atan | 0.00116 | 0.02897 | 0.12481 | 0.00116 | 0.02897 | 0.12494 | 0.00116 | 0.02898 | 0.12494 | 145.71 | 145.62 | 129.86 | 123.64 | 124.82 | 123.9 | 149.02 | 149.44 | 144.26
CIFAR | Sig | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | -
CNN5_3 | Tanh | 0.00156 | 0.02907 | 0.09497 | 0.00156 | 0.02908 | 0.09505 | 0.00156 | 0.02908 | 0.09506 | 187 | 179.6 | 171.34 | 172.47 |  174.26 | 171.19 | 185.86 | 181.71 | 177.3
8 layer | Atan | 0.001 | 0.02564 | 0.11059 | 0.001 | 0.02564 | 0.1107 | 0.001 | 0.02564 | 0.1107 | 178.97 | 175.3 | 175.13 | 170.41 | 170.97 | 173.10 | 181.46 | 176.01 | 177.86
CIFAR | Sig | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | -
CNN5_3 | Tanh | 0.001 | 0.02078 | 0.08589 | 0.001 | 0.02078 | 0.08591 | 0.001 | 0.02078 | 0.08592 | 183.02 | 182.47 | 182.65 | 180.85 | 180.57 | 180.79 | 194.67 | 188.13 | 191.04
9 layer | Atan | 0.00119 | 0.02175 | 0.08199 | 0.00119 | 0.02175 | 0.082 | 0.00119 | 0.02176 | 0.08202 | 181.3 | 181.41 | 181.45 |  180.56 | 181.11 | 181.39 | 191.16 | 190.61 | 188.62
CIFAR | Sig | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | - | -
CNN10_3 | Tanh | 0.00096 | 0.02518 | 0.11476 | 0.00096 | 0.02518 | 0.11476 | 0.00096 | 0.02519 | 0.1149 | 581.81 | 586.82 | 586.2 | 531 | 572.75 | 570.55 | 585.05 | 592.39 | 588.48
8 layer | Atan | 0.00074 | 0.02172 | 0.11343 | 0.00074 | 0.02172 | 0.11343 | 0.00074 | 0.02173 | 0.11366 | 546.31 | 579.98 | 507.19 | 528.93 | 497.72 | 575.7 | 552.37 | 466.9 | 550.25

Table 4. Averaged certified robusntess bounds and runtime on pure CNNs tested
on CIFAR-10 by DeepCert, VeriNet and Ti-Lin

Network | Certified Bounds | Ti-Lin Impr.(%) | Average Computation Time(second)
---|---|---|---
|  | Newise | Ti-Lin | vs. Newise | VeriNet | Ti-Lin
| $l_{p}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$
MNIST | Sig | 0.03715 | 0.2165 | 0.48434 | 0.0361 | 0.2421 | 0.5621 | -2.93 $\downarrow$ | 11.82 $\uparrow$ | 16.05 $\uparrow$ | 6.61 | 6.66 | 6.58 | 7.63 | 6.77 | 6.62
CNN5_3 | Tanh | 0.00901 | 0.05944 | 0.1417 | 0.0101 | 0.0824 | 0.2098 | 12.10 $\uparrow$ | 38.68 $\uparrow$ | 48.03 $\uparrow$ | 6.57 | 6.72 | 6.68 | 6.89 | 6.72 | 6.71
4 layer | Atan | 0.01079 | 0.06836 | 0.16643 | 0.0120 | 0.0934 | 0.2398 | 11.03 $\uparrow$ | 36.60 $\uparrow$ | 44.06 $\uparrow$ | 6.52 | 6.6 | 6.58 | 6.87 | 6.68 | 6.7
MNIST | Sig | 0.03593 | 0.18297 | 0.38635 | 0.0350 | 0.2067 | 0.4542 | -2.53 $\downarrow$ | 12.98 $\uparrow$ | 17.57 $\uparrow$ | 15.85 | 16.1 | 15.8 | 16.83 | 16.02 | 17.45
CNN5_3 | Tanh | 0.01115 | 0.06868 | 0.173 | 0.0126 | 0.0903 | 0.2397 | 12.91 $\uparrow$ | 31.54 $\uparrow$ | 38.54 $\uparrow$ | 16.5 | 15.98 | 15.78 | 16.28 | 16.14 | 18.15
5layer | Atan | 0.0085 | 0.05174 | 0.11899 | 0.0099 | 0.0691 | 0.1660 | 15.88 $\uparrow$ | 33.61 $\uparrow$ | 39.49 $\uparrow$ | 15.95 | 15.88 | 15.67 | 16.21 | 16.36 | 17.79
MNIST | Sig | 0.02898 | 0.13453 | 0.27428 | 0.0365 | 0.1818 | 0.3564 | 25.78 $\uparrow$ | 35.11 $\uparrow$ | 29.94 $\uparrow$ | 31.84 | 31.78 | 32.46 | 32.8 | 34.17 | 32.27
CNN5_3 | Tanh | 0.00701 | 0.04351 | 0.09938 | 0.0090 | 0.0628 | 0.1627 | 28.53 $\uparrow$ | 44.29 $\uparrow$ | 63.70 $\uparrow$ | 31.9 | 32.51 | 31.9 | 32.53 | 32.22 | 33.14
6layer | Atan | 0.00862 | 0.05596 | 0.13531 | 0.0121 | 0.0796 | 0.2032 | 40.02 $\uparrow$ | 42.17 $\uparrow$ | 50.17 $\uparrow$ | 31.95 | 31.9 | 32.02 | 32.53 | 32.32 | 32.12
MNIST | Sig | 0.06872 | 0.22792 | 0.38977 | 0.0632 | 0.2376 | 0.4280 | -8.08 $\downarrow$ | 4.26 $\uparrow$ | 9.80 $\uparrow$ | 53.69 | 54.51 | 54.42 | 54.4 | 56.03 | 54.5
CNN5_3 | Tanh | 0.00765 | 0.04997 | 0.13122 | 0.0091 | 0.0653 | 0.1802 | 18.56 $\uparrow$ | 30.70 $\uparrow$ | 37.30 $\uparrow$ | 53.83 | 53.94 | 54.13 | 54.63 | 54.78 | 54.92
7layer | Atan | 0.00948 | 0.05808 | 0.13547 | 0.0113 | 0.0766 | 0.1869 | 19.30 $\uparrow$ | 31.80 $\uparrow$ | 37.96 $\uparrow$ | 54.01 | 54.34 | 53.76 | 54.51 | 54.45 | 54.69
MNIST | Sig | 0.04683 | 0.17735 | 0.33256 | 0.0443 | 0.1877 | 0.3648 | -5.34 $\downarrow$ | 5.86 $\uparrow$ | 9.69 $\uparrow$ | 81.45 | 88.06 | 81.83 | 85.13 | 88.17 | 82.53
CNN5_3 | Tanh | 0.00797 | 0.04658 | 0.10542 | 0.0097 | 0.0618 | 0.1464 | 21.71 $\uparrow$ | 32.70 $\uparrow$ | 38.91 $\uparrow$ | 81.69 | 81.52 | 82.36 | 82.86 | 82.8 | 83.14
8 layer | Atan | 0.00823 | 0.05105 | 0.12405 | 0.0101 | 0.0678 | 0.1718 | 22.36 $\uparrow$ | 32.89 $\uparrow$ | 38.47 $\uparrow$ | 86.48 | 81.7 | 81.72 | 82.54 | 82.8 | 82.47
MNIST | Sig | 0.03095 | 0.13464 | 0.26974 | 0.0318 | 0.1549 | 0.3225 | 2.88 $\uparrow$ | 15.06 $\uparrow$ | 19.56 $\uparrow$ | 161.2 | 162.11 | 161.68 | 163.1 | 158.97 | 158.93
CNN10_3 | Tanh | 0.00584 | 0.03324 | 0.07814 | 0.0075 | 0.0454 | 0.1096 | 27.74 $\uparrow$ | 36.43 | 40.31 | 163.16 | 161.57 | 162.99 | 159.08 | 159.6 | 159.12
8 layer | Atan | 0.00441 | 0.02512 | 0.0564 | 0.0059 | 0.0355 | 0.0816 | 33.56 $\uparrow$ | 41.32 | 44.73 $\uparrow$ | 161.03 | 161.69 | 162.98 | 158.92 | 163.08 | 158.61
MNIST | Sig | - | - | - | - | - | - | - | - | - | - | - | - | - | - | -
CNN20_3 | Tanh | 0.00372 | 0.02066 | 0.04802 | 0.0051 | 0.0297 | 0.0702 | 37.90 $\uparrow$ | 43.76 $\uparrow$ | 46.15 $\uparrow$ | 432.55 | 417.85 | 415.31 | 401.54 | 408.79 | 404.25
8 layer | Atan | 0.00445 | 0.02424 | 0.05654 | 0.0059 | 0.0338 | 0.0806 | 33.26 $\uparrow$ | 39.48 $\uparrow$ | 42.50 $\uparrow$ | 425.37 | 413.34 | 413.98 | 404.26 | 409.78 | 409.43

Table 5. Averaged certified robustness bounds and runtime on pure CNNs tested
on MNIST by Newise and Ti-Lin

Network | Certified Bounds | Ti-Lin Impr.(%) | Average Computation Time(second)
---|---|---|---
|  | Newise | Ti-Lin | vs. Newise | VeriNet | Ti-Lin
| $l_{p}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$ | $l_{\infty}$ | $l_{2}$ | $l_{1}$
CIFAR | Sig | 0.00473 | 0.06054 | 0.21678 | 0.0048 | 0.07487 | 0.29242 | 1.48 $\uparrow$ | 23.67 $\uparrow$ | 34.89 $\uparrow$ | 29.12 | 28.86 | 29.64 | 27.97 | 27.51 | 27.99
CNN5_3 | Tanh | 0.00197 | 0.02957 | 0.09394 | 0.0021 | 0.03887 | 0.13325 | 6.60 $\uparrow$ | 31.45 $\uparrow$ | 41.85 $\uparrow$ | 30.01 | 28.95 | 29.04 | 27.46 | 27.69 | 27.81
5 layer | Atan | 0.00216 | 0.03078 | 0.10256 | 0.00232 | 0.04135 | 0.14734 | 7.41 $\uparrow$ | 34.34 $\uparrow$ | 43.66 $\uparrow$ | 28.85 | 29.04 | 29.40 | 28.30 | 27.61 | 28.03
CIFAR | Sig | 0.00793 | 0.08821 | 0.29653 | 0.00777 | 0.10539 | 0.38016 | -2.02 $\downarrow$ | 19.48 $\uparrow$ | 28.20 $\uparrow$ | 104.25 | 121.23 | 104.56 | 111.07 | 120.69 | 114.31
CNN5_3 | Tanh | 0.0008 | 0.0222 | 0.08789 | 0.00081 | 0.02575 | 0.12041 | 1.25 $\uparrow$ | 15.99 $\uparrow$ | 37.00 $\uparrow$ | 120.08 | 105.66 | 106.15 | 104.48 | 119.65 | 104.61
6 layer | Atan | 0.00093 | 0.0237 | 0.09422 | 0.00094 | 0.02813 | 0.12964 | 1.08 $\uparrow$ | 18.69 $\uparrow$ | 37.59 $\uparrow$ | 119.15 | 118.06 | 114.62 | 99.16 | 106.91 | 106.49
CIFAR | Sig | 0.02172 | 0.16076 | 0.47508 | 0.02081 | 0.17176 | 0.53537 | -4.19 $\downarrow$ | 6.84 $\uparrow$ | 12.69 $\uparrow$ | 145.41 | 149.28 | 136.21 | 145.4 | 147.03 | 145.07
CNN5_3 | Tanh | 0.00077 | 0.0185 | 0.07987 | 0.00078 | 0.02222 | 0.10982 | 1.30 $\uparrow$ | 20.11 $\uparrow$ | 37.50 $\uparrow$ | 149.42 | 136.88 | 134.65 | 134.31 | 145.56 | 140.34
7 layer | Atan | 0.00113 | 0.02334 | 0.09015 | 0.00116 | 0.02898 | 0.12494 | 2.65 $\uparrow$ | 24.16 $\uparrow$ | 38.59 $\uparrow$ | 149.67 | 126.95 | 139.84 | 149.02 | 149.44 | 144.26
CIFAR | Sig | - | - | - | - | - | - | - | - | - | 216.77 | 204.66 | 193.63 | 97.62 | 91.6 | 88.71
CNN5_3 | Tanh | 0.00147 | 0.02218 | 0.06738 | 0.00156 | 0.02908 | 0.09506 | 6.12 $\uparrow$ | 31.11 $\uparrow$ | 41.08 $\uparrow$ | 177.03 | 173.17 | 171.51 | 185.86 | 181.71 | 177.3
8 layer | Atan | 0.00098 | 0.02146 | 0.0814 | 0.001 | 0.02564 | 0.1107 | 2.04 $\uparrow$ | 19.48 $\uparrow$ | 36.00 $\uparrow$ | 173.27 | 174.95 | 171.16 | 181.46 | 176.01 | 177.86
CIFAR | Sig | - | - | - | - | - | - | - | - | - | - | - | - | - | - | -
CNN5_3 | Tanh | 0.00093 | 0.01631 | 0.06166 | 0.001 | 0.02078 | 0.08592 | 7.53 $\uparrow$ | 27.41 $\uparrow$ | 39.34 $\uparrow$ | 179.14 | 182.18 | 180.04 | 194.67 | 188.13 | 191.04
9 layer | Atan | 0.0011 | 0.01663 | 0.05847 | 0.00119 | 0.02176 | 0.08202 | 8.18 $\uparrow$ | 30.85 $\uparrow$ | 40.28 $\uparrow$ | 179.71 | 180.24 | 179.85 | 191.16 | 190.61 | 188.62
CIFAR | Sig | - | - | - | - | - | - | - | - | - | - | - | - | - | - | -
CNN10_3 | Tanh | 0.00094 | 0.02083 | 0.08419 | 0.00096 | 0.02519 | 0.1149 | 2.13$\uparrow$ | 20.93 $\uparrow$ | 36.48 $\uparrow$ | 578.9 | 558.31 | 563.76 | 585.05 | 592.39 | 588.48
8 layer | Atan | 0.00073 | 0.01897 | 0.08388 | 0.00074 | 0.02173 | 0.11366 | 1.37$\uparrow$ | 14.55 $\uparrow$ | 35.50 $\uparrow$ | 534.42 | 496.85 | 490.54 | 552.37 | 466.9 | 550.25

Table 6. Averaged certified robustness bounds and runtime on pure CNNs tested
on CIFAR-10 by Newise and Ti-Lin

Network |  | Certified Bounds | Ti-Lin Impr.(%) | Average Runtime(second)
---|---|---|---|---
| $l_{p}$ | CNN-Cert | DeepPoly | Ti-Lin | vs. CNN-Cert | vs. DeepPoly | CNN-Cert | DeepPoly | Ti-Lin
MNIST | $l_{\infty}$ | 0.01318 | 0.02277 | 0.02569 | 94.92$\uparrow$ | 12.82$\uparrow$ | 105.75 | 99.62 | 104.42
CNN | $l_{2}$ | 0.04427 | 0.08888 | 0.10647 | 140.50$\uparrow$ | 19.79$\uparrow$ | 83.45 | 81.06 | 84.84
4 layer | $l_{1}$ | 0.08544 | 0.17689 | 0.21507 | 151.72$\uparrow$ | 21.58 $\uparrow$ | 83.03 | 81.73 | 85.58
MNIST | $l_{\infty}$ | 0.01288 | 0.02057 | 0.02382 | 84.94$\uparrow$ | 15.80$\uparrow$ | 506.17 | 528.11 | 508.01
CNN | $l_{2}$ | 0.05164 | 0.08445 | 0.09867 | 91.07 $\uparrow$ | 16.84 $\uparrow$ | 713.8 | 486 | 825.79
5 layer | $l_{1}$ | 0.10147 | 0.16244 | 0.18877 | 86.04 $\uparrow$ | 16.21 $\uparrow$ | 646.46 | 486 | 505.46
MNIST | $l_{\infty}$ | 0.01025 | 0.0163 | 0.01848 | 80.29 $\uparrow$ | 13.37 $\uparrow$ | 227.7 | 230.53 | 226.69
CNN | $l_{2}$ | 0.03954 | 0.06473 | 0.0729 | 84.37 $\uparrow$ | 12.62$\uparrow$ | 233.77 | 230.62 | 234.5
6 layer | $l_{1}$ | 0.07708 | 0.12361 | 0.13894 | 80.25 $\uparrow$ | 12.40 $\uparrow$ | 235.9 | 230.76 | 234.91
MNIST | $l_{\infty}$ | 0.00647 | 0.01241 | 0.01383 | 113.76$\uparrow$ | 11.44 $\uparrow$ | 274.17 | 260.64 | 264.99
CNN | $l_{2}$ | 0.02733 | 0.05875 | 0.06572 | 140.47$\uparrow$ | 11.86$\uparrow$ | 274.86 | 261.3 | 274.53
7layer | $l_{1}$ | 0.05443 | 0.11925 | 0.1331 | 144.53$\uparrow$ | 11.61 $\uparrow$ | 271.96 | 262.35 | 273.25
MNIST | $l_{\infty}$ | 0.00847 | 0.01312 | 0.01655 | 95.40 $\uparrow$ | 26.14$\uparrow$ | 289.08 | 298.85 | 293.12
CNN | $l_{2}$ | 0.03751 | 0.05789 | 0.07124 | 89.92 $\uparrow$ | 23.06 $\uparrow$ | 291.67 | 325.52 | 292.86
8 layer | $l_{1}$ | 0.07515 | 0.11376 | 0.1383 | 84.03 $\uparrow$ | 21.57$\uparrow$ | 292.05 | 340.22 | 291.42

Table 7. Averaged certified robustness bounds and runtime on CNNs(ReLU) with
Maxpooling tested on MNIST by CNN-Cert, DeepPoly and Ti-Lin

Network |  | Certified Bounds | Ti-Lin Impr.(%) | Average Runtime(second)
---|---|---|---|---
| $l_{p}$ | CNN-Cert | DeepPoly | Ti-Lin | vs. CNN-Cert | vs. DeepPoly | CNN-Cert | DeepPoly | Ti-Lin
CIFAR | $l_{\infty}$ | 0.00108 | 0.00162 | 0.0019 | 75.93 $\uparrow$ | 17.28$\uparrow$ | 151.98 | 158.63 | 162.54
CNN | $l_{2}$ | 0.00751 | 0.01655 | 0.02332 | 210.52$\uparrow$ | 40.91$\uparrow$ | 153.19 | 160.23 | 163.34
4 layer | $l_{1}$ | 0.02127 | 0.04986 | 0.07137 | 235.54 $\uparrow$ | 43.14 $\uparrow$ | 152.16 | 156.71 | 163.34
CIFAR | $l_{\infty}$ | 0.00115 | 0.00175 | 0.00211 | 83.48 $\uparrow$ | 20.57$\uparrow$ | 817.49 | 775.74 | 796.36
CNN | $l_{2}$ | 0.00953 | 0.0176 | 0.0236 | 147.64 $\uparrow$ | 34.09$\uparrow$ | 780.93 | 761.15 | 791.13
5 layer | $l_{1}$ | 0.0285 | 0.05459 | 0.0732 | 156.84 $\uparrow$ | 34.09 $\uparrow$ | 783.2 | 774.19 | 805.72
CIFAR | $l_{\infty}$ | 0.00099 | 0.00144 | 0.0017 | 71.72 $\uparrow$ | 18.06 $\uparrow$ | 353.38 | 374.11 | 366.72
CNN | $l_{2}$ | 0.0083 | 0.01301 | 0.0163 | 96.39 $\uparrow$ | 25.29 $\uparrow$ | 356.44 | 363.89 | 355.38
6 layer | $l_{1}$ | 0.02387 | 0.03794 | 0.04797 | 100.96 $\uparrow$ | 26.44 $\uparrow$ | 356.91 | 369.94 | 352.09
CIFAR | $l_{\infty}$ | 0.00066 | 0.00082 | 0.001 | 51.52$\uparrow$ | 21.95 $\uparrow$ | 395.46 | 416.51 | 408.75
CNN | $l_{2}$ | 0.00573 | 0.00761 | 0.00995 | 73.65 $\uparrow$ | 30.75 $\uparrow$ | 401.45 | 418.47 | 410.17
7layer | $l_{1}$ | 0.01673 | 0.02271 | 0.02975 | 77.82$\uparrow$ | 31.00$\uparrow$ | 393.44 | 417.33 | 395.37
CIFAR | $l_{\infty}$ | 0.00056 | 0.0009 | 0.00106 | 89.29 $\uparrow$ | 17.78 $\uparrow$ | 511.38 | 465.3 | 507.67
CNN | $l_{2}$ | 0.00536 | 0.00863 | 0.01099 | 105.04$\uparrow$ | 27.35 $\uparrow$ | 447.3 | 450.49 | 449.19
8 layer | $l_{1}$ | 0.01609 | 0.02574 | 0.03354 | 108.45$\uparrow$ | 30.30 $\uparrow$ | 443.38 | 448.39 | 445.2

Table 8. Averaged certified robustness bounds and runtime on CNNs(ReLU) with
Maxpooling tested on CIFAR-10 by CNN-Cert, DeepPoly and Ti-Lin

Network |  | Certified Bounds | Ti-Lin Impr.(%) | Average Runtime(second)
---|---|---|---|---
| $l_{p}$ | CNN-Cert | DeepPoly | Ti-Lin | vs. CNN-Cert | vs. DeepPoly | CNN-Cert | DeepPoly | Ti-Lin
Tiny ImageNet | $l_{\infty}$ | 0.00051 | 0.00065 | 0.0007 | 37.25 $\uparrow$ | 7.69 $\uparrow$ | 1459.47 | 1445.06 | 1242.36
CNN | $l_{2}$ | 0.00484 | 0.01067 | 0.01504 | 210.74 $\uparrow$ | 40.96 $\uparrow$ | 1247.22 | 1208.68 | 1237.03
4 layer | $l_{1}$ | 0.01393 | 0.03273 | 0.04647 | 233.60 $\uparrow$ | 41.98 $\uparrow$ | 1242.38 | 1210.06 | 1239.86
Tiny ImageNet | $l_{\infty}$ | 0.00062 | 0.00084 | 0.00094 | 51.61 $\uparrow$ | 11.90 $\uparrow$ | 5304.63 | 5072.55 | 5489.77
CNN | $l_{2}$ | 0.00578 | 0.01036 | 0.01369 | 136.85 $\uparrow$ | 32.14 $\uparrow$ | 5176.38 | 5242.1 | 5155.05
5 layer | $l_{1}$ | 0.01504 | 0.02726 | 0.03616 | 140.43 $\uparrow$ | 32.65 $\uparrow$ | 5155.55 | 4945.58 | 5147.84
Tiny ImageNet | $l_{\infty}$ | 0.00047 | 0.00058 | 0.00065 | 38.30 $\uparrow$ | 12.07 $\uparrow$ | 12459.81 | 11982.54 | 12385.09
CNN | $l_{2}$ | 0.00515 | 0.00756 | 0.00942 | 82.91 $\uparrow$ | 24.60 $\uparrow$ | 12845.13 | 12030 | 12833.63
6 layer | $l_{1}$ | 0.01499 | 0.02213 | 0.02808 | 87.32 $\uparrow$ | 26.89 $\uparrow$ | 12331.93 | 11896.23 | 12218.5

Table 9. Averaged certified robustness bounds and runtime on CNNs(ReLU) with
Maxpooling tested on Tiny ImageNet by CNN-Cert, DeepPoly and Ti-Lin

###  4.1. Experiment Setups

Experiment Framework. Since the computation time of six methods may vary due
to various robustness verification platform, for a fair comparison, we conduct
the whole experiments and implement these six methods atop state-of-the-art
robustness verification framework CNN-Cert.

Datasets. MNIST, CIFAR-10, and Tiny ImageNet are used in experiments. The
MNIST(lecun1998mnist, ) is a dataset of $28\times 28$ handwritten digital
images(from 0 to 9) in 10 classes. CIFAR-10 is a dataset of 60,000 $32\times
32\times 3$ images in 10 classes, e.g., airplane, bird, and ship. Tiny
ImageNet consists of 100000 $64\times 64\times 3$ images in 200 classes. The
value of each pixel is normalized into [0,1] and thus the perturbation is in
[0,1].

Models. We evaluate the performance of Ti-Lin on two classes of networks: (I)
pure CNNs whose activation function is Sigmoid, Tanh, or Arctan function
without Maxpooling; (II)general CNNs whose activation function is ReLU
function with Maxpooling and Batch Normalization. We train all CNNs on the
MNIST, CIFAR-10, and Tiny ImageNet by Adam optimizer (Kingma2015AdamAM, )(50
epochs of batch size 128). Most pure CNNs(Sigmoid/Tanh/Atan) without
Maxpooling use 3$\times$3 convolutions and have five filters, while other pure
CNNs use 3$\times$3 convolutions and have 10 or 20 filters. The convolutional
networks(ReLU) with Maxpooling use 32 and 64 filters for two convolution
layers each.

Metrics. We refer to the metrics in CNN-Cert (boopathy2019cnn, ). Concretely,
we evaluate Ti-Lin and other methods on 10 random test images. As for
effectiveness, we use
$\frac{100(\epsilon_{cert}^{\prime}-\epsilon_{cert})}{\epsilon_{cert}}\%$ to
quantify the percentage of improvement, where $\epsilon_{cert}^{\prime}$ and
$\epsilon_{cert}$ represent the robustness bounds certified by Ti-Lin and
other comparative tools, respectively. We color result tables’ cells in orange
from light to dark by checking whether the value of improvement(%) is in
$[0,20),[20,40),[40,60),$ or $[60,+\infty)$. As for efficiency, we record the
average computation time over the correctly-classified images.

###  4.2. Research Questions

To check whether Ti-Lin is the Tightest linear approximation technique for
Sigmoid/Tanh/Arctan function among existing _Neuron-wise Tightest_ linear
approximation approach(VeriNet) and _Network-wise Tightest_ approach(Newise),
we propose two research questions which are listed as follows:

  * •

RQ1(vs. Neuron-wise Tightest Approach) : Whether Ti-Lin outperforms Neuron-
wise Tightest technique on various networks in different datasets perturbed in
$l_{1},l_{2},l_{\infty}$ norm and overcomes the aforementioned limitation of
Neuron-wise Tightest technique?

  * •

RQ2(vs. Network-wise Tightest Approach): Whether Ti-Lin outperforms Network-
wise Tightest technique on various networks in different datasets perturbed in
$l_{1},l_{2},l_{\infty}$ norm?

To check whether Ti-Lin, the _Neuron-wise Tightest_ method for Maxpooling
function, stands for the highest precision of certifying robustness bounds
among DeepPoly and CNN-Cert, we propose the following research question:

  * •

RQ3(vs. State-of-the-art) :Whether Ti-Lin outperforms State-of-the-art
techniques on various networks in different datasets perturbed in
$l_{1},l_{2},l_{\infty}$ norm?

Finally, we propose the following research question:

  * •

RQ4(Significant Improvement):Is the improvement of Ti-Lin statistically
significant compared to all baseline methods?

###  4.3. RQ1(vs. Neuron-wise Tightest Approach)

We answers RQ1 by comparing our approach with VeriNet(_Neuron-wise Tightest_
technique) and DeepCert, which are the two most recent methods.

Table 3 and Table 4 show the results of certified lower bounds computed by
these three methods for pure convolutional networks with three different
activation functions on the MNIST and CIFAR-10 datasets, respectively. The
best one’ cell is colored in orange.

Compared to the results in Table 2, Table 3 shows that Ti-Lin has overcome the
limitation of _Neuron-wise Tightest_ Approach(VeriNet). Concretely, in Table 3
and 4 Ti-Lin outperforms both VeriNet and DeepCert in 96.67% and 93.33% cases,
respectively, while VeriNet outperforms DeepCert in 78.33% cases on MNIST
dataset. The only five bad results in Table 3 happen in CNNs with four layers
and Sigmoid network with 6 layers. However, when the number of layers
increases, the superiority of Ti-Lin plays a more and more important role in
tightening certified robustness bound and thus the bounds certified by Ti-Lin
become larger than other two baseline methods. Some sigmoid networks’ results
are omitted due to poor test set accuracy. As for time efficiency, these three
methods cost almost the same time for the same network architectures.

###  4.4. RQ2(vs. Network-wise Tightest Approach)

We answers RQ2 by comparing our approach with Newise(_Network-wise Tightest_
technique), which stands for the highest precision for monotonous networks.

Table 5 and 6 show the results of certified lower bounds for 36 different pure
convolutional networks with three types of activation functions on the MNIST
and CIFAR-10 dataset respectively. As shown in Table 5 and 6, in 94.29% cases,
Ti-Lin can compute much larger robustness bounds with up to 63.70% and 43.66%
improvement than Newise. Ti-Lin is inferior to Newise in some sigmoid networks
against $l_{\infty}$-norm perturbation. The reason is that Sigmoid function’s
value is non-negative, which is different from Tanh and Arctan functions and
this makes the weights of the network prone to be non-negative. Moreover,
Newise is the Tightest approximation technique for non-negative networks and
therefore has better performance than Ti-Lin. However, the proportion of bad
results is only 5.71%. Regarding time efficiency, Ti-Lin costs almost the same
time as Newise. In conclusion, Ti-Lin is the best linear approximation
approach for general CNNs among DeepCert, VeriNet and Newise.

###  4.5. RQ3(vs. State-of-the-art)

We answers RQ3 by comparing our approach with the two promising methods(CNN-
Cert, DeepPoly) as baselines.

Table 7, 8 and 9 show the results of certified lower bounds for general
convolutional networks(ReLU) with Maxpooling on MNIST, CIFAR-10 dataset, and
Tiny ImageNet respectively. Ti-Lin can compute much larger robustness bounds
with up to 235.54% improvement than CNN-Cert and 43.14% improvement than
DeepPoly, which further confirms that _Neuron-wise Tightest_ technique can
give rise to tighter robustness bounds. As for time efficiency, Ti-Lin costs
almost the same time as DeepPoly and CNN-Cert for the same network
architecture due to their common framework CNN-Cert.

###  4.6. RQ4(Significant Improvement)

We answers RQ4 by applying Wilconxon Rank-sum Test(a.k.a Mann–Whitney U test)
(Capitani2011OnSO, ) at the significance level of 0.05. We suppose $Y,T$ are
continuous random variables and represent the robustness bound certified by
baseline method and Ti-Lin, respectively. To check whether the improvement of
Ti-Lin in the above results is significant compared to the five state-of-the-
art baseline methods, we consider the statistic:

$W=\\#\\{(T_{i},Y_{i}):T_{i}>Y_{i};i=1,\cdots,n\\}$

where $n$ is the number of samples. Therefore, we define $B$ as a continuous
random variable representing the difference between Ti-Lin and the baseline
method $T-Y$. We define $Z$ as another random variable and $P(Z=0)=1$. The
null hypothesis is that $B$ and $Z$ are equal in distribution and alternative
hypothesis is that $B$ is stochastically strictly greater than $Z$:

$H_{0}:B\overset{\text{d}}{=}Z\,\,\,versus\,\,\,H_{1}:B>_{st}Z$

Table 10 contains the results of Wilconxon Rank-sum Test, which reject $H_{0}$
and confirm that Ti-Lin significantly performs better than any one of the five
state-of-the-art baseline methods across different network architectures on
various datasets.

Dataset | Baseline Methods | p-value
---|---|---
MNIST | DeepCert | $1.17\times 10^{-18}$
VeriNet | $1.54\times 10^{-20}$
Newise | $2.66\times 10^{-16}$
CIFAR-10 | DeepCert | $1.37\times 10^{-4}$
VeriNet | $1.10\times 10^{-2}$
Newise | $9.75\times 10^{-14}$

Dataset | Baseline Methods | p-value
---|---|---
MNIST | CNN-Cert | $3.06\times 10^{-6}$
DeepPoly | $3.06\times 10^{-6}$
CIFAR-10 | CNN-Cert | $3.06\times 10^{-6}$
DeepPoly | $3.06\times 10^{-6}$
Tiny | CNN-Cert | $3.48\times 10^{-4}$
ImageNet | DeepPoly | $3.48\times 10^{-4}$

Table 10. Wilconxon Rank-sum Test Results

##  5\. Threats to validity

We discuss potential threats to the validity of this paper in terms of its
application domains.

Neural networks with ReLU functions Despite the focus on Sigmoid, Arctan, Tanh
and Maxpooling functions, our approach is applicable to ReLU-based network,
and the linear constraints is deffered in Appendix due to space limitation.
The ReLU constraints provided is also the _Neuron-wise Tightest_. However,
approximation technique is not necessary for ReLU-based networks as there are
other verification methods which can get accurate robustness bounds by using
Satisfiability Modulo Theories (katz2017reluplex, ) and Mixed Integer Linear
Programming (tjeng2018evaluating, ).

Neural networks with non-negative weights For such networks, Newise is the
best verification techniques, which can efficiently obtain accurate certified
robustness bounds. The training dataset and the number of fully-connected
layers can influence the weights. When the number of fully-connected layer is
only one, the variety of the weights decrease and may be prone to non-
negative. However, we believe that most network are mix-weight. The reasons
are listed as follows:(i) To tackle various complex tasks, the number of the
fully-connected layers in networks is often more than one; (ii) Neural network
are widely used in various domains, weights of the network can be quite
different.

##  6\. Related work

There is plenty of ongoing works using linear approximation to verify the
robustness of convolutional neural networks against adversarial attacks, and
the main challenge to verify robustness is the non-linear property of
networks, that is, ReLU, Maxpool, Sigmoid/Arctan/Tanh. Moreover, abstract
interpretation is also a robustness verification method, which is similar to
linear approximation. We briefly introduce the similarity and difference
between these two verification methods in this section. A survey on formal
robustness verification with linear approximation is proposed in the work
(meng2022adversarial, ).

ReLU. Linear approximation of the ReLU function is firstly proposed in the
work (meyer2019soundness, ) by offering a pair of bounds to ReLU function
instead of its piecewise feature. Fast-Lin (weng2018towards, ) gives parallel
linear bounds to ReLU function. State-of-the-art linear approximation of ReLU
function is proposed in DeepPoly (singh2019abstract, ), which has the highest
precision among all relevant works by producing the smallest over-
approximation region of ReLU function.

Sigmoid, Arctan and Tanh. Other notable non-linear functions are Sigmoid,
Arctan and Tanh functions. As these functions’ shapes are similar(S-shaped),
their linear constraints are the same in essence. Recent techniques for
Sigmoid and Tanh functions are proposed in DeepZ (singh2018fast, ) and
DeepPoly (singh2019abstract, ). CROWN (zhang2018efficient, ) proposes a more
general method that can offer non-trivial linear bounds to Sigmoid, Arctan,
and Tanh functions and is extended to FROWN (lyu2020fastened, ) with tighter
approximation by using a gradient-based method to find the bounding lines.
State-of-the-art linear approximation of Sigmoid, Arctan, and Tanh functions
are proposed in VeriNet (henriksen2020efficient, ) and DeepCert
(wu2021tightening, ), DeepCert can compute much tighter robustness bounds
compared with CROWN and FROWN, while VeriNet produces a minimum over-
approximation region of Sigmoid, Arctan and Tanh functions and stands for the
highest precision for general CNNs. Recently, network-wise Tightest approach
is proposed in Newise (zhang2022provably, ) and is the most precise method for
monotonous CNNs(such as non-negative CNNs).

Maxpool. Besides ReLU, Sigmoid, Arctan, and Tanh functions, Maxpool is a non-
linear function commonly used in CNNs. However, as it is a multivariate
function, Maxpool is far more complex to be verified. DeepPoly
(singh2019abstract, ) gives a loose linear bound to Maxpool and its parallel
work, CNN-Cert (boopathy2019cnn, ) gives non-trivial bounds by leveraging a
hyperplane containing n different particular points. 3DCertify
(lorenz2021robustness, ) gives tighter bounds than DeepPoly by double
description method and is appliable for point cloud models. However,
3DCertify’s perturbation form is rotation and is not suitable for image data,
which is perturbed in a $l_{p}$-norm ball.

Abstract Interpretation In the survey (ji2022, ), linear approximation
technique is contained in abstract interpretation domain (gehr2018ai2, ;
singh2018fast, ; mirman2018differentiable, ). The over-appriximation zone is
called as abstract domain in this field. In the survey (meng2022adversarial,
), these two technique are divided. The similarity between abstract
interpretation and linear approximation is that they both need to give a pair
of upper and lower linear constraints of a non-linear function $f(x)$ in a
given interval $[l,u]$. When the abstract domain of abstract interpretation is
polyhedra (singh2019abstract, ), there is no essential difference between
these two techniques. However, when the abstract domain is zonotope
(gehr2018ai2, ; mirman2018differentiable, ), abstract interpretation can
abandon the backsubstitution process (singh2019abstract, ) and computes faster
than the linear approximation method. However, abstract interpretation has
some precision loss due to its parallel linear constraints compared to linear
approximation.

##  7\. Conclusion

In this paper, we propose Ti-Lin, providing tight linear bounds for certifying
the robustness of general CNNs. Ti-Lin applies to CNNs with
Sigmoid/Tanh/Arctan/ReLU/Maxpool functions and gains tighter non-trivial
certified robustness bounds with almost the same computational complexity.
Concretely, Ti-Lin certifies much more precise robustness bounds on pure CNNs
with Sigmoid/Tanh/Arctan functions and CNNs with Maxpooling function with at
most 63.70% and 253.54% improvement, respectively. Furthermore, we illustrate
the relation of tighter certified bounds and minimizing the over-approximation
zone of non-linear function by introducing the notion of _Neuron-wise
Tightest_. We implemented Ti-Lin in various networks on MNIST, CIFAR-10, and
Tiny ImageNet datasets, including pure CNNs without any Maxpooling layer, and
CNNs with Maxpooling layers. The experimental results have shown Ti-Lin’s
efficiency and effectiveness.

## References

  * (1) Y. Wu and M. Zhang, “Tightening robustness verification of convolutional neural networks with fine-grained linear approximation,” in _Proceedings of the AAAI Conference on Artificial Intelligence_ , vol. 35, no. 13, 2021, pp. 11 674–11 681.
  * (2) A. Boopathy, T.-W. Weng, P.-Y. Chen, S. Liu, and L. Daniel, “Cnn-cert: An efficient framework for certifying robustness of convolutional neural networks,” in _Proceedings of the AAAI Conference on Artificial Intelligence_ , vol. 33, no. 01, 2019, pp. 3240–3247.
  * (3) C.-Y. Ko, Z. Lyu, L. Weng, L. Daniel, N. Wong, and D. Lin, “Popqorn: Quantifying robustness of recurrent neural networks,” in _International Conference on Machine Learning_. PMLR, 2019, pp. 3468–3477.
  * (4) G. Singh, T. Gehr, M. Püschel, and M. Vechev, “An abstract domain for certifying neural networks,” _Proceedings of the ACM on Programming Languages_ , vol. 3, no. POPL, pp. 1–30, 2019.
  * (5) H. Zhang, T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel, “Efficient neural network robustness certification with general activation functions,” _Advances in neural information processing systems_ , vol. 31, 2018.
  * (6) M. N. Müller, G. Makarchuk, G. Singh, M. Püschel, and M. Vechev, “Prima: Precise and general neural network certification via multi-neuron convex relaxations,” _arXiv preprint arXiv:2103.03638_ , 2021.
  * (7) T. Du, S. Ji, L. Shen, Y. Zhang, J. Li, J. Shi, C. Fang, J. Yin, R. Beyah, and T. Wang, “Cert-rnn: Towards certifying the robustness of recurrent neural networks.” in _CCS_ , 2021, pp. 516–534.
  * (8) G. Singh, T. Gehr, M. Mirman, M. Püschel, and M. Vechev, “Fast and effective robustness certification,” _Advances in neural information processing systems_ , vol. 31, 2018.
  * (9) Z. Lyu, C.-Y. Ko, Z. Kong, N. Wong, D. Lin, and L. Daniel, “Fastened crown: Tightened neural network robustness certificates,” in _Proceedings of the AAAI Conference on Artificial Intelligence_ , vol. 34, no. 04, 2020, pp. 5037–5044.
  * (10) S.-M. Moosavi-Dezfooli, A. Fawzi, O. Fawzi, and P. Frossard, “Universal adversarial perturbations,” in _Proceedings of the IEEE conference on computer vision and pattern recognition_ , 2017, pp. 1765–1773.
  * (11) C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, and R. Fergus, “Intriguing properties of neural networks,” _arXiv preprint arXiv:1312.6199_ , 2013.
  * (12) D. Gopinath, G. Katz, C. S. Păsăreanu, and C. Barrett, “Deepsafe: A data-driven approach for assessing robustness of neural networks,” in _International symposium on automated technology for verification and analysis_. Springer, 2018, pp. 3–19.
  * (13) G. Goswami, N. Ratha, A. Agarwal, R. Singh, and M. Vatsa, “Unravelling robustness of deep learning based face recognition against adversarial attacks,” in _Proceedings of the AAAI Conference on Artificial Intelligence_ , vol. 32, no. 1, 2018.
  * (14) T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, “Ai2: Safety and robustness certification of neural networks with abstract interpretation,” in _2018 IEEE symposium on security and privacy (SP)_. IEEE, 2018, pp. 3–18.
  * (15) P. Henriksen and A. Lomuscio, “Efficient neural network verification via adaptive refinement and adversarial search,” in _ECAI 2020_. IOS Press, 2020, pp. 2513–2520.
  * (16) B. Meyer, “Soundness and completeness: With precision,” _Retrieved May_ , vol. 28, p. 2020, 2019.
  * (17) L. Weng, H. Zhang, H. Chen, Z. Song, C.-J. Hsieh, L. Daniel, D. Boning, and I. Dhillon, “Towards fast computation of certified robustness for relu networks,” in _International Conference on Machine Learning_. PMLR, 2018, pp. 5276–5285.
  * (18) M. H. Meng, G. Bai, S. G. Teo, Z. Hou, Y. Xiao, Y. Lin, and J. S. Dong, “Adversarial robustness of deep neural networks: A survey from a formal verification perspective,” _IEEE Transactions on Dependable and Secure Computing_ , 2022.
  * (19) T. Lorenz, A. Ruoss, M. Balunović, G. Singh, and M. Vechev, “Robustness certification for point cloud models,” in _Proceedings of the IEEE/CVF International Conference on Computer Vision_ , 2021, pp. 7608–7618.
  * (20) P. Huang, Y. Yang, M. Liu, F. Jia, F. Ma, and J. Zhang, “$\epsilon$-weakened robustness of deep neural networks,” in _ISSTA ’22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18 - 22, 2022_ , S. Ryu and Y. Smaragdakis, Eds. ACM, 2022, pp. 126–138. [Online]. Available: https://doi.org/10.1145/3533767.3534373
  * (21) Z. Zhao, G. Chen, J. Wang, Y. Yang, F. Song, and J. Sun, “Attack as defense: characterizing adversarial examples using robustness,” in _ISSTA ’21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, Denmark, July 11-17, 2021_ , C. Cadar and X. Zhang, Eds. ACM, 2021, pp. 42–55. [Online]. Available: https://doi.org/10.1145/3460319.3464822
  * (22) Z. Zhang, Y. Wu, S. Liu, J. Liu, and M. Zhang, “Provably tightest linear approximation for robustness verification of sigmoid-like neural networks,” _arXiv preprint arXiv:2208.09872_ , 2022.
  * (23) Y. LeCun, “The mnist database of handwritten digits,” _http://yann. lecun. com/exdb/mnist/_ , 1998.
  * (24) L. D. Capitani and D. D. Martini, “On stochastic orderings of the wilcoxon rank sum test statistic with applications to reproducibility probability estimation testing,” _Statistics & Probability Letters_, vol. 81, pp. 937–946, 2011.
  * (25) D. P. Kingma and J. Ba, “Adam: A method for stochastic optimization,” _CoRR_ , vol. abs/1412.6980, 2015.
  * (26) S. L. Ji, T. Y. Du, S. G. Deng, P. Cheng, J. Shi, M. Yang, and B. Li, “Robustness certification research on deep learning models: A survey,” _Jisuanji Xuebao/Chinese Journal of Computers_ , vol. 45, no. 1, pp. 190–206, 2022.
  * (27) M. Mirman, T. Gehr, and M. Vechev, “Differentiable abstract interpretation for provably robust neural networks,” in _International Conference on Machine Learning_. PMLR, 2018, pp. 3578–3586.
  * (28) G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient smt solver for verifying deep neural networks,” in _International conference on computer aided verification_. Springer, 2017, pp. 97–117.
  * (29) R. Ehlers, “Formal verification of piece-wise linear feed-forward neural networks,” in _International Symposium on Automated Technology for Verification and Analysis_. Springer, 2017, pp. 269–286.
  * (30) X. Huang, M. Kwiatkowska, S. Wang, and M. Wu, “Safety verification of deep neural networks,” in _International conference on computer aided verification_. Springer, 2017, pp. 3–29.
  * (31) V. Tjeng, K. Y. Xiao, and R. Tedrake, “Evaluating robustness of neural networks with mixed integer programming,” in _International Conference on Learning Representations_ , 2018.
  * (32) J. Jia, B. Wang, X. Cao, and N. Z. Gong, “Certified robustness of community detection against adversarial structural perturbation via randomized smoothing,” in _Proceedings of The Web Conference 2020_ , 2020, pp. 2718–2724.
  * (33) M. Fazlyab, M. Morari, and G. J. Pappas, “Probabilistic verification and reachability analysis of neural networks via semidefinite programming,” in _2019 IEEE 58th Conference on Decision and Control (CDC)_. IEEE, 2019, pp. 2726–2731.
  * (34) L. Weng, P.-Y. Chen, L. Nguyen, M. Squillante, A. Boopathy, I. Oseledets, and L. Daniel, “Proven: Verifying robustness of neural networks with a probabilistic approach,” in _International Conference on Machine Learning_. PMLR, 2019, pp. 6727–6736.
  * (35) S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. S. Jana, “Efficient formal safety analysis of neural networks,” in _NeurIPS_ , 2018.

##  8\. Appendix

###### Theorem 8.1 (ReLU Linear Bounds).

Given $f(x)=max(0,x),x\in[l,u]$. Then the linear bounds are:

$\left\\{\begin{aligned} &u(x)=\frac{f(u)-f(l)}{u-l}(x-l)+f(l),l(x)=0,m\leq
0\\\ &u(x)=\frac{f(u)-f(l)}{u-l}(x-l)+f(l),l(x)=x,m>0\\\ \end{aligned}\right.$

Define $[n_{k}^{+}]=\\{i|w^{k}_{i}>0\\}$ and $[n_{k}^{-}]=\\{i|w^{k}_{i}<0\\}$

###### Proof:Neuron-wise Tightest is equivalent to Layer-wise Tightest.

We define linear bounds are _Layer-wise Tightest_ is when

$\iint_{x\in\times_{q\in[n_{k-1}]}[l^{k-1}_{q},u^{k-1}_{q}]}(\sum_{i\in[n_{k}^{+}]}W_{ji}^{+,k+1}u^{k}_{i}(x)-\sum_{i\in[n_{k}^{-}]}W_{ji}^{-,k+1}l^{k}_{i}(x))dx$
is minimal.

As $l^{k-1}_{q},u^{k-1}_{q},W_{i}^{+,k+1},W_{i}^{-,k+1}$ are constant and
$[n_{k}^{+}]\cap[n_{k}^{-}]=\emptyset$, thus we need to minimize
$\iint_{x\in\times_{q\in[n_{k-1}]}[l^{k-1}_{q},u^{k-1}_{q}]}u^{k}_{i}(x)dx,i\in[n_{k}^{+}]$
and
$\iint_{x\in\times_{q\in[n_{k-1}]}[l^{k-1}_{q},u^{k-1}_{q}]}(-l^{k}_{i}(x))dx,i\in[n_{k}^{-}]$
respectively. ∎

###### Proof:Neuron-wise Tightest Linear Bounds.

Because $u^{k}_{i}(x)$ is a linear combination of $x$. Without loss of
generality, we assume
$u^{k}_{i}(x)=u^{k}_{i}(x_{1},\cdots,x_{n_{k-1}})=\sum_{q\in[n_{k-1}]}a_{u,iq}^{k}x_{q}+b^{k}_{u,i}$.
Then,

$\displaystyle\iint_{x\in\times_{q\in[n_{k-1}]}[l^{k-1}_{q},u^{k-1}_{q}]}u^{k}_{i}(x)dx$
$\displaystyle=$
$\displaystyle\iint_{x\in\times_{q\in[n_{k-1}]}[l^{k-1}_{q},u^{k-1}_{q}]}(\sum_{q\in[n_{k-1}]}a_{u,iq}^{k}x_{q}+b^{k}_{u,i})dx$
$\displaystyle=$
$\displaystyle\sum_{q\in[n_{k-1}]}\frac{a_{u,iq}^{k}}{2}((u^{k-1}_{q})^{2}-(l^{k-1}_{q})^{2})+b^{k}_{u,i}(u^{k-1}_{q}-l^{k-1}_{q})$
$\displaystyle=$
$\displaystyle(u^{k-1}_{q}-l^{k-1}_{q})(\sum_{q\in[n_{k-1}]}a_{u,iq}^{k}\frac{u^{k-1}_{q}+l^{k-1}_{q}}{2}+b^{k}_{u,i})$
$\displaystyle=$ $\displaystyle(u^{k-1}_{q}-l^{k-1}_{q})u_{i}^{k}(m)$

where
$m=(\frac{u^{k-1}_{1}+l^{k-1}_{1}}{2},\cdots,\frac{u^{k-1}_{n_{k-1}}+l^{k-1}_{n_{k-1}}}{2})$,
because $u^{k-1}_{q},l^{k-1}_{q},q\in[n_{k-1}]$ are constant, and the minimize
target has been transformed into minimizing $u_{i}^{k}(m),i\in[n_{k}^{+}]$.

Symmetric to the proof of minimizing
$\iint_{x\in\times_{q\in[n_{k-1}]}[l^{k-1}_{q},u^{k-1}_{q}]}u^{k}_{i}(x)dx$,
minimizing
$-\iint_{x\in\times_{q\in[n_{k-1}]}[l^{k-1}_{q},u^{k-1}_{q}]}(l^{k}_{i}(x))dx,i\in[n_{k}^{-}]$
is equivalent to minimize $-l_{i}^{k}(m),i\in[n_{k}^{-}]$.

And symmetric to the above proof, minimizing
$-\iint_{x\in\times_{q\in[n_{k-1}]}[l^{k-1}_{q},u^{k-1}_{q}]}(\sum_{i\in[n_{k}^{+}]}W_{ji}^{+,k+1}l^{k}_{i}(x)-\sum_{i\in[n_{k}^{-}]}W_{ji}^{-,k+1}u^{k}_{i}(x))dx$,
is equivalent to
$-l_{i}^{k}(m),i\in[n_{k}^{+}]$,$u_{i}^{k}(m),i\in[n_{k}^{-}]$.

This completes the proof. ∎

Here, we provide a way to find Neuron-wise Tightest linear bounds of non-
linear function $f(x)$.

In essence, the theorem ”Finding Neuron-wise Tightest Linear Bounds” shows
that if the tangent line/plane at $m$ is the upper/lower bound of $f(x)$, then
the tangent line/plane at $x=m$ is obviously the Neuron-wise Tightest linear
upper/lower bound of $f(x)$. Otherwise, we try to find two points that satisfy
$m=\lambda d_{1}+(1-\lambda)d_{2},\lambda\in[0,1]$, so that if a line/plane
passing through $(d_{1},f(d_{1})),(d_{2},f(d_{2}))$ is the linear bound of
$f(x)$, then this line/plane is the Neuron-wise Tightest bounding constraints.

###### Proof:Finding Neuron-wise Tightest Linear Bounds.

Obviously, (1) is right.

And we prove (2) by contradiction. Without loss of generality, we suppose the
line/plane to be proved is an upper bound $u(x)$ and
$u(d_{1})=f(d_{1}),u(d_{2})=f(d_{2}),m=\lambda
d_{1}+(1-\lambda)d_{2},\lambda\in[0,1]$. We assume there is another bounding
line/plane $u^{\prime}(x)$ and $u^{\prime}(m)<u(m)$. Because
$u(x),u^{\prime}(x)$ are linear combinations of $x$ and $m=\lambda
d_{1}+(1-\lambda)d_{2},\lambda\in[0,1]$,then $u(m)=\lambda
u(d_{1})+(1-\lambda)u(d_{2}),u^{\prime}(m)=\lambda
u^{\prime}(d_{1})+(1-\lambda)u^{\prime}(d_{2}),\lambda\in[0,1]$. Therefore,
$\lambda u^{\prime}(d_{1})+(1-\lambda)u^{\prime}(d_{2})<\lambda
u(d_{1})+(1-\lambda)u(d_{2})=\lambda f(d_{1})+(1-\lambda)f(d_{2})$ which
contradicts $u^{\prime}(d_{1})\geq f(d_{1}),u^{\prime}(d_{2})\geq f(d_{2})$.

This completes the proof. ∎

###### Proof:Sigmoid/Tanh/Arctan Linear Bounds.

$m=F^{k}(x_{0})\in[l,u]\in\mathbb{R}$, and if $d_{1}\leq m\leq d_{2}$, then
there exists $\lambda=\frac{d_{2}-m}{d_{2}-d_{1}}$, s.t. $\lambda
d_{1}+(1-\lambda)d_{2}=m$

case 1: $m\geq 0$

upper bound:

(1) when $k_{ml}>f^{\prime}(m)$:

As $m\geq 0$, we have $u\geq 0$, and when $x\geq 0$, $f(x)$ is concave.
Therefore, $f(x)\leq f^{\prime}(m)(x-m)+f(m),x\in[m,u]$.

Considering $x<0$, because $k_{ml}>f^{\prime}(m)$, we have
$f^{\prime}(m)(l-m)+f(m)>k_{ml}(l-m)+f(m)=f(l)$ and
$f^{\prime}(m)(l-m)+f(m)\geq f(0)$. Thus, as $f(x),x<0$ is convex, then
$f^{\prime}(m)(l-m)+f(m)\geq f(x)$

Thus, $f^{\prime}(m)(x-m)+f(m)$ is the upper bounding line and $u(m)$ is
minimum obviously, by theorem 3.4(1).

(2) when $k_{ml}<f^{\prime}(m)$ and $k>f^{\prime}(u)$:

$k>f^{\prime}(u)$, means the tangent point $x^{*}$ exists. Because $f(x)$ is
continuous, $f^{\prime}(0)>\frac{f(0)-f(l)}{0-l}$ and
$f^{\prime}(u)<\frac{f(u)-f(l)}{u-l}$, thus there exists a solution
$x^{*}\in[0,u]$ for equation
$f^{\prime}(x^{*})=\frac{f(x^{*})-f(l)}{x^{*}-l}$.

$k_{ml}<f^{\prime}(m)$, means $m\in[l,x^{*}]$. Because $k_{ml}<f^{\prime}(m)$
and $f^{\prime}(u)<\frac{f(u)-f(l)}{u-l}$, thus $m<x^{*}<u$. Because
$f(x),x\geq 0$ is concave, $f(x)\leq f^{\prime}(x^{*})(x-x^{*})+f(x^{*}),x\geq
0$. Because $f^{\prime}(x^{*})(0-x^{*})+f(x^{*})\geq f(0)$,
$f^{\prime}(x^{*})(l-x^{*})+f(x^{*})=f(l)$ and $f(x),x<0$ is convex, thus
$f^{\prime}(x^{*})(x-x^{*})+f(x^{*})\geq f(x),x<0$

Therefore, $f^{\prime}(x^{*})(x-x^{*})+f(x^{*})$ is the upper bound, and as
$l\leq m<x^{*}$, by theorem 3.4(2), $u(m)$ reaches minimum.

(3) when $k_{ml}<f^{\prime}(m)$ and $k\leq f^{\prime}(u)$:

$k\leq f^{\prime}(u)$, which means $k(x-l)+f(l)\geq f(x)$. Because when $x>0$,
we have $k(x-l)+f(l)=k(x-u)+f(u)>f^{\prime}(u)(x-u)+f(u)$ and $f(x),x>0$ is
concave, thus $k(x-l)+f(l)\geq f(x),x>0$. When $x\leq 0$, we have $k\leq
f^{\prime}(u)<\frac{f(0)-f(u)}{0-u}$, thus
$k(0-u)+f(u)>\frac{f(0)-f(u)}{0-u}(0-u)+f(u)=f(0)$. As $f(x)$ is convex when
$x\leq 0$. Thus $k(x-l)+f(l)$ is the upper bound and as $m\in[l,u]$, $u(m)$
reaches minimum by Theorem 3.4(2).

lower bound:

(4) when $k\geq f^{\prime}(l)$,

As proved above, $k\geq f^{\prime}(l)$ means the tangent point $x^{**}$ exists
and the $f^{\prime}(x^{**})(x-u)+f(u)$ is the lower bound. As $u\geq
m>0>x^{*}*$, $l(m)$ reaches its minimum by Theorem 3.4(2).

(5) when $k<f^{\prime}(l)$,

As proved above, $k(x-l)+f(l)$ is the lower bound and as $l\leq m\leq u$,
$l(m)$ achieves it minimum by theorem 3.4(2).

case 2: $m<0$ The proof of case 2 is symmetric to the proof of case 1, for the
reason that $f(x)$ is centrosymmetry about the origin.

∎

Similar to proof ” Sigmoid/Tanh/Arctan Linear Bounds” , when
$m=\frac{u+l}{2}$, the linear bounds of theorem 3.1 is Neuron-wise Tightest
according to theorem 3.4 and theorem 3.2. Although the Neuron-wise Tightest
technique (henriksen2020efficient, ) can compute a larger robustness bounds
than other state-of-the-art works and stands for the highest precision among
related work, experimental results have shown that Ti-Lin is better than the
Neuron-wise Tightest linear bounds of Sigmoid/Tanh/Arctan function.

###### Proof:Maxpool Linear Bounds.

$m=(m_{1},\cdots,m_{n})\in\mathbb{R}^{n}$.

upper bound:

case 1: When $u_{i}\geq l_{i}\geq\cdots$,
$f(x_{1},\cdots,x_{n})=x_{i},\forall(x_{1},\cdots,x_{n})$, then we set
$u(x_{1},\cdots,x_{n})=x_{i}$, then $u(m)=f(m)$ which is the Neuron-wise
Tightest upper bounding plane by Theorem 3.4(1).

case 2:When $u_{i}\geq u_{j}\geq l_{j}\geq\cdots$,
$f(x_{1},\cdots,x_{n})=max(x_{i},x_{j}),\forall(x_{1},\cdots,x_{n})$.

If $f(x_{1},\cdots,x_{n})=x_{i}$,

$\displaystyle u(x_{1},\cdots,x_{n})-x_{i}$
$\displaystyle=\frac{u_{i}-l_{j}}{u_{i}-l_{i}}(x_{i}-l_{i})+(x_{j}-l_{j})+l_{j}-x_{i}$
$\displaystyle=\frac{u_{i}-l_{j}}{u_{i}-l_{i}}(x_{i}-l_{i})+(x_{j}-l_{j})+l_{j}-l_{i}+l_{i}-x_{i}$
$\displaystyle=(x_{i}-l_{i})(\frac{u_{i}-l_{j}}{u_{i}-l_{i}}-1)+(x_{j}-l_{j})+l_{j}-l_{i}$
$\displaystyle=(x_{i}-l_{i})\frac{l_{i}-l_{j}}{u_{i}-l_{i}}+(x_{j}-l_{j})+l_{j}-l_{i}$
$\displaystyle=(l_{j}-l_{i})(1-\frac{x_{i}-l_{i}}{u_{i}-l_{i}})+(x_{j}-l_{j})$
$\displaystyle=(l_{j}-l_{i})\frac{u_{i}-x_{i}}{u_{i}-l_{i}}+(x_{j}-l_{j})$
$\displaystyle\geq 0$

If $f(x_{1},\cdots,x_{n})=x_{j}$,

$\displaystyle u(x_{1},\cdots,x_{n})-x_{j}$
$\displaystyle=\frac{u_{i}-l_{j}}{u_{i}-l_{i}}(x_{i}-l_{i})+(x_{j}-l_{j})+l_{j}-x_{j}$
$\displaystyle=\frac{u_{i}-l_{j}}{u_{i}-l_{i}}(x_{i}-l_{i})$
$\displaystyle\geq 0$

Because

$\displaystyle
u(u_{1},\cdots,u_{i-1},u_{i},u_{i+1},\cdots,u_{j-1},l_{j},u_{j+1},\cdots,u_{n})$
$\displaystyle=\frac{u_{i}-l_{j}}{u_{i}-l_{i}}(u_{i}-l_{i})+(l_{j}-l_{j})+l_{j}$
$\displaystyle=u_{i}-l_{j}+l_{j}$
$\displaystyle=f(u_{1},\cdots,u_{i-1},u_{i},u_{i+1},\cdots,u_{j-1},l_{j},u_{j+1},\cdots,u_{n})$

and

$\displaystyle
u(l_{1},\cdots,l_{i-1},l_{i},l_{i+1},\cdots,l_{j-1},u_{j},l_{j+1},\cdots,l_{n})$
$\displaystyle=\frac{u_{i}-l_{j}}{u_{i}-l_{i}}(l_{i}-l_{i})+(u_{j}-l_{j})+l_{j}$
$\displaystyle=u_{j}-l_{j}+l_{j}$
$\displaystyle=f(l_{1},\cdots,l_{i-1},l_{i},l_{i+1},\cdots,l_{j-1},u_{j},l_{j+1},\cdots,l_{n})$

we notice that
$(u_{1},\cdots,u_{i-1},u_{i},u_{i+1},\cdots,u_{j-1},l_{j},u_{j+1},\cdots,u_{n})$
and
$(l_{1},\cdots,l_{i-1},l_{i},l_{i+1},\cdots,l_{j-1},u_{j},l_{j+1},\cdots,l_{n})$
are the space diagonal of $\times_{i=1}^{n}[l_{i},u_{i}]$, and
$m=\frac{1}{2}(u_{1},\cdots,u_{i-1},u_{i},u_{i+1},\cdots,u_{j-1},l_{j},u_{j+1},\cdots,u_{n})+\frac{1}{2}(l_{1},\cdots,l_{i-1},l_{i},l_{i+1},\cdots,l_{j-1},u_{j},l_{j+1},\cdots,l_{n})$,
thus the plane is the Neuron-wise Tightest linear upper plane by Theorem
3.4(2).

case 3:When $u_{i}\geq u_{j}\geq u_{k}\geq\cdots$,
$f(x_{1},\cdots,x_{n})=max(x_{1},\cdots,x_{n}),\forall(x_{1},\cdots,x_{n})$.
If $f(x_{1},\cdots,x_{n})=x_{i}$,

$\displaystyle u(x_{1},\cdots,x_{n})-x_{i}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(x_{i}-l_{i})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+u_{k}-x_{i}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-u_{k}}(x_{i}-l_{i})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+u_{k}-l_{i}+l_{i}-x_{i}$
$\displaystyle=(x_{i}-l_{i})(\frac{u_{i}-u_{k}}{u_{i}-l_{i}}-1)+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+u_{k}-l_{i}$
$\displaystyle=(x_{i}-l_{i})\frac{l_{i}-u_{k}}{u_{i}-l_{i}}+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+u_{k}-l_{i}$
$\displaystyle=(u_{k}-l_{i})(1-\frac{x_{i}-l_{i}}{u_{i}-l_{i}})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})$
$\displaystyle=(u_{k}-l_{i})\frac{u_{i}-x_{i}}{u_{i}-l_{i}}+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})$
$\displaystyle\geq 0$

If $f(x_{1},\cdots,x_{n})=x_{j}$, the proof is the same as above.

$\displaystyle u(x_{1},\cdots,x_{n})-x_{j}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(x_{i}-l_{i})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+u_{k}-x_{j}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-u_{k}}(x_{i}-l_{i})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+u_{k}-l_{j}+l_{j}-x_{j}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(x_{i}-l_{i})+(\frac{u_{j}-u_{k}}{u_{j}-l_{j}}-1)(x_{j}-l_{j})+u_{k}-l_{j}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(x_{i}-l_{i})+\frac{l_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+u_{k}-l_{i}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(x_{i}-l_{i})+(1-\frac{x_{j}-l_{j}}{u_{j}-l_{j}})(u_{k}-l_{j})$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(x_{i}-l_{i})+\frac{u_{j}-x_{j}}{u_{j}-l_{j}}(u_{k}-l_{j})$
$\displaystyle\geq 0$

If $f(x_{1},\cdots,x_{n})=x_{k}$,

$\displaystyle u(x_{1},\cdots,x_{n})-x_{j}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(x_{i}-l_{i})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+(u_{k}-x_{k})$
$\displaystyle\geq 0$

If $f(x_{1},\cdots,x_{n})=x_{l},l\neq i,j,k$,

$\displaystyle u(x_{1},\cdots,x_{n})-x_{l}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(x_{i}-l_{i})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+u_{k}-x_{l}$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(x_{i}-l_{i})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(x_{j}-l_{j})+(u_{k}-u_{l})+(u_{l}-x_{l})$
$\displaystyle\geq 0$

Because

$\displaystyle
u(u_{1},\cdots,u_{i-1},u_{i},u_{i+1},\cdots,u_{j-1},l_{j},u_{j+1},\cdots,u_{n})$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(u_{i}-l_{i})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(l_{j}-l_{j})+u_{k}$
$\displaystyle=u_{i}-u_{k}+u_{k}$
$\displaystyle=f(u_{1},\cdots,u_{i-1},u_{i},u_{i+1},\cdots,u_{j-1},l_{j},u_{j+1},\cdots,u_{n})$

and

$\displaystyle
u(l_{1},\cdots,l_{i-1},l_{i},l_{i+1},\cdots,l_{j-1},u_{j},l_{j+1},\cdots,l_{n})$
$\displaystyle=\frac{u_{i}-u_{k}}{u_{i}-l_{i}}(l_{i}-l_{i})+\frac{u_{j}-u_{k}}{u_{j}-l_{j}}(u_{j}-l_{j})+u_{k}$
$\displaystyle=u_{j}-u_{k}+u_{k}$
$\displaystyle=f(l_{1},\cdots,l_{i-1},l_{i},l_{i+1},\cdots,l_{j-1},u_{j},l_{j+1},\cdots,l_{n})$

$m=\frac{1}{2}(u_{1},\cdots,u_{i-1},u_{i},u_{i+1},\cdots,u_{j-1},l_{j},u_{j+1},\cdots,u_{n})+\frac{1}{2}(l_{1},\cdots,l_{i-1},l_{i},l_{i+1},\cdots,l_{j-1},u_{j},l_{j+1},\cdots,l_{n})$,
by Theorem 3.4(2), the upper bound is the Neuron-wise Tightest bounding plane.

lower bound:

$l(x_{1},\cdots,x_{n})=x_{j}=argmax_{i}m_{i}$, and
$\forall(x_{1},\cdots,x_{n})\in\times_{i=1}^{n}[l_{i},u_{i}]$,

$\displaystyle f(x_{1},\cdots,x_{n})$ $\displaystyle=max(x_{1},\cdots,x_{n})$
$\displaystyle\geq x_{j}$ $\displaystyle=l(x_{1},\cdots,x_{n})$

Furthermore, $l(m)=f(m_{1},\cdots,m_{n})$, hence, $l(x_{1},\cdots,x_{n})$ is
the Neuron-wise Tightest lower bounding plane by Theorem 3.4(1).

This completes the proof. ∎