Robustness Verification for Transformers
Authors: Zhouxing Shi
Huan Zhang
Kai-Wei Chang
Minlie Huang
Cho-Jui Hsieh
Venue:  (2020)
Keywords: Robustness
Verification
Transformers

Abstract: Robustness verification that aims to formally certify the prediction behavior of neural networks has become an important tool for understanding model behavior and obtaining safety guarantees. However, previous methods can usually only handle neural networks with relatively simple architectures. In this paper, we consider the robustness verification problem for Transformers. Transformers have complex self-attention layers that pose many challenges for verification, including cross-nonlinearity and cross-position dependency, which have not been discussed in previous works. We resolve these challenges and develop the first robustness verification algorithm for Transformers. The certified robustness bounds computed by our method are significantly tighter than those by naive Interval Bound Propagation. These bounds also shed light on interpreting Transformers as they consistently reflect the importance of different words in sentiment analysis.

Published as a conference paper at ICLR 2020
ROBUSTNESS VERIFICATION FOR TRANSFORMERS
Zhouxing Shi', Huan Zhang", Kai-Wei Chang', Minlie Huang', Cho-Jui Hsieh l 'Dept. of Computer Science & Technology. Tsinghua University, Beijing 10084, China Dept. of Computer Science, University of California, Los Angeles, CA 90095, USA @houxingghhcche@malll c com, buan@huan-zhame com kwθ kw@kwchang net, a huangggntttt singhuu edu. cn, chchsieh@cs, ucla edu
ABSTRACT
Robustness verification that aims to formally certify the prediction behavior of neural networks has become important tool for understanding model behav- ior and obtaining safety guarantees. However, previous methods can usually only handle neural networks with relatively simple architectures. In this paper, we consider the robustness verification problem for Transformers. Transformers have complex selff-atenntion layers that pose many challenges for verification, including cross- noss-nonlinearity and cross-position dependency, which have not been discussed in previous works. We resolve these challenges and develop the first robustness verification algorithm for Transformers. The certified robustness bounds com- puted by our method are significantly tighter than those by naive Interval Bound Propagation. These bounds also shed light interpreting Transformers as they consistently reflect the importance different words in sentiment analysis.
INTRODUCTION
Deep neural networks have been successfully applied to many domains. However, these black- box models are generally difficult to analyze and their behavior is not guaranteed. Moreover, has been shown that the predictions of deep networks become unreliable and unstable when tested in unseen situations, e.g., in the presence of small adversarial perturbations to the input (Szegedy al. 2013 Goodfellow
al., 2014 Lin al. 2019). Therefore, neural network verification has become an important tool for analyzing and understanding the behavior of neural networks, with applications in safety-critical applications (Katz et al., 2017: Julian al. 2019; Lin et al. 2019).
model explanation (Shih et al. 2018) and robustness analysis Tjeng et al. 2019 Wang et al. 2018c
Gehr et al. 2018 Wong Kolter [018 [Singh et al.) 2018 Weng et al. 2018 Zhang et al.,
2018).
Formally. neural network verification algorithm aims to provably characterize the prediction of network within some input space. For example, given a K K-way classification model f Rdd K
where fx(x stands for the predicted score of class i, we can verify some linear specification (defined by a vector c) as below:
min [xff((x) s.t. S
(1)
where S a predefined input space. In the robustness verification problem, S - {x }} is defined as some small ball around the original example Xo. and setting up c enables to verify whether the logit output of class Yo always greater than another class y for any input within S. This is a nonconvex optimization problem which makes computing the exact solution challenging, and thus several algorithms are recently proposed find the lower bounds of Eq. (1) in order to efficiently obtain a safety guarantee (Gehr et al., 2018 Weng et al.) 2018 Zhang al. 2018, Singh et al.) 2019). Moreover, extensions of these algorithms can be used for verifying properties beyond robustness, such rotation or shift invariant (Singh et al. 2019). conservation of energy (Qin et al. 2019) and model correctness (Yang & (
||x x 1| <
= 1gp I
However, most of existing verification methods focus on relatively simple neural network architec- tures, such as feed-forward and recurrent neural networks, while they cannot handle complex struc- tures. In this paper, we develop the first robustness verification algorithm for Transformers /Vaswani ct al., 2017) with self-attention layers. Transformers have been widely used in natural language pro- cessing (Devlin et al. 2019 Yang et al. 2019 Liu et al. 2019) and many other domains (Parmar

---

Published as a conference paper at ICLR 2020
et al. 2018: Kang & McAuley| 2018 Li et al. 2019b Su et al. 2019 Li et al. 2019a). For frames under perturbation in the imput sequence, we aim to compute a lower bound c such that when these frames are perturbed within f.p ballll centered at the original frames respectively and with radius of the model prediction is certified to be unchanged. To compute such bounds efficiently, we adopt the linear-relaxation framework (Weng et al., 2018 ZZhang et al., 2018) we recursively propagate and compute linear lower and upper bounds for each neuron w.r.t the imput within the perturbation space S. We resolve several particular challenges in verifying Transformers. First, Transformers with self- attention layers have a complicated architecture. Unlike simpler networks, they cannot be written as multiple layers of affine transformations or element-wise activation functions. Therefore, we need to propagate linear bounds differently for self-attention layers. Second, dot products, softmax, and weighted summation in self-attention layers involve multiplication or division of two variables both under perturbation, namely nons-nonlin,,rity, which not present in ferd-forward networks. Ko al. (2019) proposed gradient descent based approach to find linear bounds, however it is inefficient and poses a computational challenge for Transformer verification since self-attention is the core of Transformers. In contrast, we derive closed-form linear bounds that can be computed in ((1) complexity. Third, in the computation of self-attention, output neurons in each position depend all input neurons from different positions (namely cross-position dependency). unlike the case in recurrent neural networks where outputs depend on only the hidden features from the previous position and the current input. Previous works (Zhang et al., 2018; Weng al.. 20188] Ko et al. 2019) have to track all such dependency and thus is costly in time and memory. To tackle this, we introduce an efficient bound propagating process in a forward manner specially for self-attention layers, enabling the tighter backward bounding process for other layers to utilize bounds computed by the forward process. In this way, we avoid cross-posiin eross-position dependency in the backward process which is relatively slower but produces tighter bounds. Combined with the forward process, the complexity of the backward process reduced by ((n) for input length n, while the computed bounds remain comparably tight. Our contributions summarized below:
We propose an effective and efficient algorithm for verifying the robustness of Transformers with self-attention layers. To our best knowledge, this is the first method for verifying Transformers.
We resolve key challenges in verifying Transformers, including cross-nonlinearity and cross-position dependency. Our bounds are significantly tighter than those by adapting Interval Bound Propagation (IBP) (Mirman et al. 2018 Gowal et al.] 2018).
We quantitatively and qualitatively show that the certified bounds computed by our al- gorithm consistently reflect the importance of input words in sentiment analysis, which justifies that these bounds are meaningful in practice and they shed light on interpreting Transformers.
RELATED WORK
Robustness Verification for Neural Networks. Given input Xy and small region (x,. == (x ||x Xellp S <), the goal of robustness verification is to verify whether the prediction of the neural network unchanged within this region. This problem can be mathemat- ically formulated as Eq. (I). If Eq. (I) can be solved optimally, then we can derive the minimum adversarial perturbation of x by conducting binary search on e. Equivalently, we obtain the maxi- mum such that any perturbation within BB, c) cannot change the predicted label.
Several works focus on solving Eq. (I) exactly and optimally, using mixed integer linear program- ming (MILP) (Tjeng et al., 2019; Dutta et al. (018)), branch and bound (BaB) (Bunel et al. 2018). and satisfiability modulo theory (SMT) (Ehlers) 2017 Katz et al., 2017). Unfortunately. due to the nonconvexity of model f. solving Eq. ①I is NP-hard even for simple ReLU network (Katz cet al., 2017). Therefore, we can only expect to compute lower bound of Eq. I efficiently by using relaxations. Many algorithms can be seen as using convex relaxations for non-linear activation func-
tions (Salman et al. 2019). including using duality (Wong& & Kolter 2018: Dvijotham et al.
2018
abstract domains (Gehr al.) 2018; (Singh et al. 2018 Mirman et al. 2018
Singh et al.
2019
layer-by-layed reachability analysis (Wang et al. 2018b] Weng et al.
2018 Zhang et al.
2018
Gowal et al. 2018) and semi-definite relaxations (Raghunathan et al. 2018 Dvijotham al.
2019
2

---

Published as a conference paper at ICLR 2020
Additionally, robustness verification rely on analysis local Lipschitz constants (Hein & An- driushchenko 2017: Zhang et al. 2019). However, existing methods are mostly limited to verifying networks with relatively simple are architectures. such as feed-forward networks and RNNs (Wang et al. 2018a Akintunde et al. 2019 Ko et al. 2019), while none of them are able to handle Transformers.
Transformers and Self-Attentive Models. Transformers (Vaswani et al., 2017) based on self- aftention mechanism, further with pre-training on large-scale corpora, such BERT (Devlin al.) 2019). XL (Yang et al.) 2019), RoBERTa (Liu et al. 2019), achieved state-of-the-art performance on many NLP tasks. Sclf-attentive models are also useful beyond NLP, including VisualBERT on vision and language applications eLi al. 2019b Su et al. 2201), image transformer for image gen- eration (Parmar al. 2018), acoustic models for speech recognition (Zhou al. (0118), sequential recommendation (Kang & McAuley 2018) and graph embedding (Li et al. 2019a).
The robustness of NLP models has been studied, especially many methods have been proposed to generate adversarial examples (Papernot et al. [2016] Jia & Liang
2017: Zhao et al., 2017; Alzantot
al. 2018 Cheng al. 2018 EEbahhii et al., 2018 [Shi et al.
2019p. In particulan |Hiieh et al.
(2019) showed that Transformers are more robust than LS However, there is not much work on robustness verification for NLP models. Ko et al. (0119) verified RNN/LSTM. Jia et al. (2019);
Huang et al. (2019) used Interval Bound Propagation (IBP) for certified robustness training of CNN and LSTM. this paper, we propose the first verification method for Transformers.
3 METHODOLOGGY
We aim verify the robustness of Transformer whose input is sequence of frames X (x(1), ...).... x()] We take binary text classification
running example, where x(() is word embedding and the model outputs a score Yo (X) for each class (c E {0, 1}). Nevertheless, our method for verifying Transformers is general and can also be applied in other applications.
For clean input sequence Xo = [x]" x
(2) (),,.... x...,,x(") ((") correctly classified by the model, let P
fri, r2, rı (1 S гы I n.) be the set of perturbed positions, where is the number of perturbed positions. Thus the perturbed input belongs to S. := {X = [x()), x²)) xx("] [|x(*+)
xf" x""")) S e, < S x+) x Vi $ P}. Assuming that the gold class, the goal of robustness verification is to compute
min ye (X) (x) := XES
-
If 5. 0, the output of the correct class is always larger than the incorrect for any input within S., As mentioned previously, computing the exact values of ó, is NP-hard, and thus our goal efficiently compute a lower bound d < de.
3.1 BASE FRAMEWORK
We obtain 8 (X) by computing the bounds of each neuron when X is perturbed within S, (8 can be regarded final neuron). A Transformer layer can be decomposed into a number of sub-layers, where each sub-layer contains neurons after some operations. These operations can be categorized into three categories: 1) linear transformations, 2) unary nonlinear functions, and 3) operations in self-attention. Each sub-layer contains n positions in the sequence and each position contains a group of neurons. We assume that the Transformer
verify has sub-layers in total, and the
value of the j-th neuron at the i-th position in the I-th sub-layer (b(l.)) (X), where ((1.0)()) is
vector for the specified sub-layer and position. Specially, (00,)) x() taking I = O. We aim to
compute a global lower bound f fll..). and global upper bound (1.6).05 of क (....)) (X) for E S..
We compute bounds from the first sub-layer to the last sub-layer. For neurons in the I-th layer, we aim to represent their bounds as linear functions of neurons in a previous layer, the 1'thh layer:
(oal L. tt (x) + A U.a.r < 4 (x)
(x) S
a.r N0.0 (,,U (0, ()))) A A.S.')
(2)
k=
3

---

Published as a conference paper at ICLR 2020
are parameters of linear lower and upper bounds respectively. Using linear bounds enables us to efficiently compute bounds with a reasonable tightness. We initially have A (6.....0). A (...,..)) I and A (1.1.1).2 (l..,))UU 0. Thereby the fighthhan-side of Eq.
where A (),, A (
and A (L.. A (,
equals to Φ (1.1) (X) when = I. Generally, we use a backward process to propagate the bounds to previous sub-layers, by substituting "!f'.0) with linear functions of previous neurons. can be recursively conducted until the input layer = Since ((0.A)
x (** X (vk $ P) is constant, we can regard the bounds as linear functions of the perturbed embeddings ((0.ra) =x x((x) (1 S ks S t), and take the global bounds for x(rx) B (x(") .e):
A (l..0.
11g +
(...O.). (1)
X0 + A 1.
(3)
k=1
k=
1,000.000 =6
19
A (...0.))..
11
+
U...... (1)
X + U.i.0).U
(4)
1=1
where 1/q with p. 2 1. These steps resemble to CROWN Zhang et al. 2018) which is proposed to verify which are more complex than feed-forward networks. Moreover, unlike CROWN that conducts a fully backward process, we combine the backward process with forward process (see Sec. 3.3 to reduce the computational complexity of verifying Transformers.
networks. We further support verifying self-attentive Transformers
3.2 LINEAR TRANSFORMATIONS AND UNARY NONLINEAR FUNCTIONS
Linear transformations and unary nonlinear functions are basic operations in neural networks. We show how bounds Eq. the 1'tth sub-layer are propagated to the (!' 1) layer.
Linear Transformations If the I'-th sub-layer is connected with the (L' - 1)-th sub-layer with
linear transformation &' .k) (X) = w(') (1,)) ((()))(())A)))) (X) + b(') where w(') b(")) are parameters of the lincar transformation, we propagate the bounds to the (1' - 1) layer by substituting & .k) (X):
A (..LL
(!)), A (0..1'1)) = -A (L..)) +
Σ AA ban,
where "L/U" means that the equations hold for both lower bounds and upper bounds respectively.
Unary Nonlinear Functions
If the 1-th layer is obtained from the (?' 1)-th layer with unary
nonlinear function @0 (() ( = =x)= (0'((()) 1,8) (X)), to propagate linear bounds over the nonlinear
function, first bound o o(") "00 11.0 -10' (X)) with two linear functions of d 11A) (X):
Ar Df 1.6) (X) 81t 1l, S o (0 11,) (X)) S az (), a 11,1 (X) + 3. ,).UU
(1. ()/U). Blf L/UU are parameters such that the inequation holds true for all 4/ 1!' (1,)) (X)
where aj within its bounds computed previously. Such linear relaxations can be done for different functionns respectively. We provide detailed bounds for functions involved Transformers in Appendix
We then back propagate the bounds:
A U1.. LK) =a
at' MY./UU A MLLUU
(LALI A M.
+ +a
A
(1,1f1 -1).L/U A (.A.).I1 oft ML
L. Att
+ 2.
M.ULL
(LAY 8).
A.j.
where A (l..J..))..LL and A (...F. mean to retain positive and negative elements in vector .jst
A (1.... L/U
respectively and other elements to 0.
4

---

Published as a conference paper at ICLR 2020
3.3 SELF-ATTENTION MECHANISM
Self-attention layers are the most challenging parts for verifying Transformers. We assume that (1-11.) (X) is the input to a self-attention layer. We describe our method for computing bounds for one attention head, and bounds for different heads of the multi-head attention in Transformers can be easily concatenated. ((l-1.0 (X) is first linearly projected to queries q (L.4)) (X), keys (X),
and values v(.))(() with different linear projections, and their bounds can be obtained as described in Sec. 3.2 We also keep their linear bounds that are linear functions of the perturbed embeddings. For convenience, let x(r) = x(ra) @b x(12) ....... x(re),,,, where i indicates vector concatenation, and thereby we represent the linear bounds as linear functions of x()):
S J.
(1i0a///// (r) + e (.).///// 1 (q/k/v), (1.4) (X) S Ω j.r
(t0a////// x00) + { (iaa///
where g/k/v and q/k/v mean that the inequation holds true for queries, keys and values respec- tively. We then bound the output of the self-attention layer starting from q(,,0) kx))(X). v(l,)())))
Bounds of Multiplications and Divisions We bound multiplications and divisions in the self- attention mechanism with linear functions. We aim to bound bivariate function 2 5(u > 0) with two linear functions z6 a² + BLy + 2h and -" aa + f y + where x E U2],y E U Uy] are bounds of x, y obtained previously. For = = ay, we derive optimal parameters: a² = byy a² = -uy BL = B lax. 7 = -lghy- 70 My We provide proof in is tricky; fortunately, we can bound it indirectly by first bounding a unary function y = 1 and then bounding the multiplication 2 = zy.
or =
Appendix C However, directly bounding
A Forward Process For the self-attention mechanism, instead of using the backward process like CROWN (Zhang et al. 2018), we compute bounds with a forward process which we will show later that it can reduce the computational complexity. Attention scores are computed from q (x)) and k kl0 (X): ( = (qt.0 (X))) (X)
k=
digh (1.6)
4
(X), where dy is the dimension
of q (1.0 (X) and (1,) (X). For each multiplication q
(1.0)
(X)kk
(),, it is bounded by:
q
(1.1) (X)
(1d)
(X) 2 0k
(L.A)). (1.6)
q
(x)
k
(1..))
L
&
(1.))
(X) + 7 (L,b,).L
(.0) q
#
X < a
(.i.D).
9
(1.1)
(x)
Pk
(1...)).
(1.5)
(X) + + (1,.,)).U
We then obtain the bounds of S
2 (.1.
(r) + 0 (.:)),
< =S < 2 S. (U.), x() + 0 (10.
Ω 1.)...
(LJ)LIU akk
Ω
Σ
2 ki
R2
( 50
(aa)..0 <o
Bh
(.,..ALLUUU
Σ
BlAiSi.EUU >0
gll Al <0
L/
(.A.)LUUU -g
Σ
L.).a.LUU
Σ
(.).Ulbb k
k
1 20 a
2.6 <0 a
dyr
p
Σ
L.U)..
(J).,../L
(15).L/U
ol gll.n. 20
g a <0
In this way, linear bounds of q ((.) and k (X) are forward propagated to S. Attention scores normalized into attention probabilities with softmax, i.c. $ exp(s exp(s!))) )),
where $1)) is normalized attention probability. exp(s()) is unary nonlinear function and can
5

---

Published as a conference paper at ICLR 2020
be bounded by 0..
L/L (() L/,
S + Pijj
So we forward propagate bounds of S to bound exp(S) (S!))
with 2 e. x(r) O
L/U
where:
10 = ai (0,441
Ω 1.00000
U. = =a (,,./U
θ U.).a... + +B 1
Ouif 2 0,
(illee = 1.
2/U U.L
M.).a// = aa,
L. U.0. + 8 8.8.100 Ba.10
<0.
By summing up bounds of each exp(S linear bounds can be further propagated to (.)). With bounds of exp(s()) and Σ exp(S i.tk ready, we forward propagate
Σx=1 (x)
the bounds $0) with a division similarly bounding q (x)k(>)(X (X). The output of the
(1.0)
self-attention & (1.0) (X) is obtained with a summation of (t.j) (()))()) (x) weighted by attention probabil-
ity 5() (1.5)
(X) Σx=1 (00) (1.k) (X), which can be regarded as dot product of S and
V (1.5) (X), where v (1:5) (x) vj (X) whose bounds can be obtained from those of (t.k) (X)
with a transposing. Therefore, bounds of 5 and v((:)) (X) can be forward propagated to + (1.))
(X)
similarly to bounding S In this way, we obtain the output bounds of the self-attention:
2 0...0. O (1' s),0.L I q (0'm)) (X) S $S 0.0.0 x(1) O (),,).
(5)
Recall that x(r) is concatenation of x((m), tors with equal dimensions, Ω (2 L.1. becomes
x(12) x(rr), We can split Ω
(1 .,,0LLU
into vec-
s2 ((112.))0.110 n $.0. such that Eq.
(5)
J::
A. x (Ta) + 1 W. S (
( S
(.) x (Ta)
+ o of MAU
(6)
Backward Process to Self-Attention Layers When computing bounds for later sub-layer, the I- th sub-layer, using the backward process, we directly propagate the bounds at the the closest previous self-attention layer assumed to be the 1' layer, to the input layer, and skip other previous sub- layers. The bounds propagated the /'tth layer are as Eq. 2 We substitute &(l' .)) (X) with linear bounds in Eq. 6
(X(())))))))))))))
(.s.O.a))..UUU
(LLL of (...L//) + +A (L. MA ( A.A.A.)..UUU $K $))KS)) D8st
3:
(L....).LUUU = (Vk P),
A (/..0),LUU = -.A
MU 0d b) L.UU L) Ol' R),4U/LL
We take global bounds as Eq.
30 and Eq. to obtain the bounds of the I-th layer.
Ad Advantageous of Combining the Backward Process with a Forward Process Introducing forward process can significantly reduce the complexity of verifying Transformers. With the back- ward process only, we need to compute A (I..f',k) and A (t.i.") (I' I l). where the major cost is on A (,,. and there are Omm²n²) such matrices to compute. The O(n²) factor is from the depen- dency between all pairs of positions in the input and output respectively, which makes the algorithm inefficient especially when the input sequence is long. In contrast, the forward process represents the bounds as linear functions of the perturbed positions only instead of all positions by comput- ing (2.1 and (1,i), Imperceptible adversarial examples may not have many perturbed positions Gaa et al. 2018: Ko et al. 2019), and thus we may assume that the number of perturbed positions, f, is small. The major cost is on (2(..) while there are only ((m)) such matrices and the sizes of A (1, and (2.5)) are relatively comparable for a small t. We combine the backward process and the forward process. The number of matrices Ω in the forward process (mm). and for the backward process, since we do not propagate bounds over self-attention layers and there is no cross- position dependency in other sub-layers, we only compute A (1.i,''AA ,k) such that k, and thus the number of matrices A is reduced to O(m²n). Therefore, the total number of matrices and S2 we compute is Omm²n n) and is (nn) times smaller than O(m?n²) when only the backward process is used. Moreover, the backward process makes bounds tighter compared to solely the forward one, as explain in Appendix D

---

Published as a conference paper at ICLR 2020
4 EXPERIMENTS
To demonstrate the effectiveness of our algorithm, we compute certified bounds for several senti- ment classification models and perform an ablation study show the advantage of combining the backward and forward processes. We also demonstrate the meaningfulness of our certified bounds with an application on identifying important words.
4.1 DATASETS AND MODELS
We use two datasets: Yelp (Zhang al., 2015) and SST (Socher al. 2013). Yelp consists of 160,0000388000 examples in the training/test set and SST consists of 67,349//72/11,8 examples in the trainingdevellpmenntesst set. Each example a sentence or sentence segment (for the training data of SST only) labeled with binary sentiment polarity.
verify the robustness of Transformers trained from scratch. For the main experiments, we con- sider N N-layer models (N S 3), with 4 attention heads, hidden sizes of 256 and 512 for self-attention and feed-forward layers respectively, and we use ReLU activations for feed-forward layers. We re- move the variance related terms in layer normalization, making Transformers verification bounds tighter while the clean accuracies remain comparable (see Appendix for discussions). Although method be in principal applied Transformers with any number of layers, we do not large-scale pre-trained models such as BERT because they are too challenging to be tightly verified with the current technologies.
4.2
CERTIFIED BOUNDS
Upper
Lower (IBP)
Lower (Ours)
Ours
Upper
Datasct
N
Acc.
Ep
Min
Avg
Min
Avg
Min
Avg
Avg
f 9,085
13.917
1,4E-4
3.1E-4
1.423
1,809
16%
13%
91.5
l2 0.695
1.005
1,4E-4
3.1E-4
0.384
0.483
55%
48%
Loc
0.117
0.155
1.4E4
3.1E-4
0.034
0.043
29%
27%
11 10,228
13.452
1,4577
2.2E-7
0.389
0.512
3%
Yelp
2
91.5
82
0,773
1.103
1,4E-7
2.2F-7
0.116
0.149
15%
14%
L 0.122
0.161
1.4E-7
2.2E-7
0.010
0.013
9%
8%
E1 11.137
15.041
4.3B-10
7.1E-10
0.152
0.284
1%
2%
E2 0.826
1.090
4.3E-10
7.1E-10
0.042
0.072
7%
foc 0.136
0.187
4.3R-10
7.1E-10
0.004
0.006
3%
E 7,418
8.849
2.4E44
2.7E-4
2.503
2.689
34%
30%
83.2
E2 0.560
0.658
2.4E-4
2.7E-4
0.418
0.454
75%
69%
loc 0.091
0.111
2.4E-4
2.7E-4
0.033
0.036
32%
& 6,781
8.367
3.6E-7
3.8E-
1.919
1.969
28%
24%
SST
2
83.5
82 0.520
0.628
3.6E-7
3.8E-7
0.305
0.315
59%
50%
Eoc 0.085
0.105
3.6E-7
3.8E-7
0.024
0.024
28%
23%
E1 6.475
7.877
5.7E-10
6.7E-10
1.007
1.031
16%
13%
83.9
82 0.497
0.590
5.7E-10
6.7E-10
0.169
0.173
29%
0.084
0.101
5.7E-10
6.7E-10
0.013
0.014
16%
13%
Table Clean accuracies and computed bounds for 1-position perturbation. Bounds include upper bounds (obtained by an enumeration based method), certified lower bounds by IBP and our method respectively. also report the gap between upper bounds and our lower bounds (represented as percentage of lower bounds relative to upper bounds). We compute bounds for each possible option of perturbed positions and report the minimum ("Min") and average ("Avg") among them.
Yelp
SST
N
Lower (IBP)
Lower (Ours)
Lower (IBP)
Lower (Ours)
Min
Avg
Min
Avg
Min
Avg
Min
Avg
1
6.5E-5
1,2E-4
0.242
0.290
1.1E-4
1.1E-4
0.212
0.229
2
6.2E-8
8.6E-8
0.060
0.078
1.SE-7
1.5E-7
0.145
0.149
2.8E-10
4.4E-10
0.023
0.035
3.3E-10
4.5E-10
0.081
0.083
Table 2: Bounds IBP and method for 2-position perturbation constrained by fy-norm.

---

Published as a conference paper at ICLR 2020
We compute certified lower bounds for different models on different datasets. We include 1-position perturbation constrained by f2/22/c<-nnon -noms and 2- 2-position perturbation constrained by lz-norm. We compare our lower bounds with those computed by the Interval Bound Propagation (IBP) (Gowal eet al. 2018) baseline. For 1-position perturbation, we also compare with upper bounds computed by enumerating all the words in the vocabulary and finding the word closest the original one such that the word substitution alters the predicted label. This method has an exponential complexity with respect to the vocabulary size and can hardly be extended to perturbations thus we do not include upper bounds for 2-position perturbation. For each example, we enumerate possible options of perturbed positions (there are (:) options), and we integrate results from different options by taking the minimum or average respectively. We report the average results on 10 correctly classified random test examples with sentence lengths no more than 32 for 1-position perturbation and 16 for 2-position perturbation. Table [T and Table 2 present the results for 1-position and 2- position perturbation respectively. Our certified lower bounds are significantly larger and thus tighter than those by IBP. For I-position perturbation, the lower bounds are consistenlly smaller than the upper bounds, and the gap between the upper bounds and our lower bounds is reasonable compared with that in previous work verification of feed- forward networks, e.g., in (Weng et al., [018]] Zhang et al. 2018) the upper bounds are in the order of 10 times larger than lower bounds. This demonstrates that our proposed method can compute robustness bounds for Transformers in a similar quality to the bounds of simpler neural networks.
2 or more positions;
4.3 EPFECTIVENESS OF COMBINING THE BACKWARD PROCESS WITH A FORWARD PROCESS
Fully-Forward
Fully- Bally-Backward
Backward & Forward
Dataset
Acc.
4p
Min
Avg
Time
Min
Avg
Time
Min
Avg
Time
1 2.122
2.173
12.6
3.485
3.737
141.4
3.479
3.729
24.0
Yelp
91.3
f
0.576
0.599
12.4
0.867
0.947
140.4
0.866
0.946
26.0
foc
0.081
0.084
12.6
0.123
0.136
143.9
0.123
0.136
26.4
Ê 1.545
1.592
13.7
1.891
1.961
177.6
1.891
1.961
26.5
SST
83.3
E2 0.352
0.366
12.6
0.419
0.439
178.8
0.419
0.439
24.3
foc
0.048
0.050
14.6
0.058
0.061
181.3
0.058
0.061
24.3
Table 3: Comparison of certified lower bounds and computation time (sec) by different methods.
In the following, we show the effectiveness of combining the backward process with a forward process. We compare our proposed method (Backward & Forward) with two variations: 1) Fully- Forward propagates bounds in a forward manner for all sub-layers besides self-attention layers; 2) Fully-Backward computes bounds for all sub-layers including self-attention layers using the back- ward bound propagation and without the forward process. We compare the tightness of bounds and computation time of the three methods. We use smaller models with the hidden sizes reduced by 75%, and we use -position perturbation only, to accommodate tional cost. Experiments are conducted on an NVIDIA TITAN X GPU. Table presents the results. Bounds by Fully-Forwad are significantly looser while those by Fully- Fully-Backward and Backward & Forward are comparable. Meanwhile, the computation time of Backward & Forward is significantly shorter than that of Hally-Backward, This demonstrates that our method of combining the backward and forward processes can compute comparably tight bounds much more efficiently.
Bally-Baackwadd with large computa-
4.4 IDENTIFYING WORDS IMPORTANT TO PREDICTION
The certified lower bounds can reflect how sensitive a model is to the perturbation of each input word. Intuitively, if a word is more important to the prediction, the model is more sensitive to its perturbation. Therefore, the certified lower bounds can be used to identify important words. In the following, we conduct an experiment to verify whether important words can be identified by our certified lower bounds. We use a I-layer Transformer classifier under I-position perturbation constrained by fz-nrmm The certified lower bounds are normalized by the norm of the unperturbed word embeddings respectively, when they are used for identifying the most/least important words. We compare our method with two baselines that also estimate local vulnerability: 1) Upper uses upper bounds; 2) Gradient identifies the word whose embedding has the largest lg norm of gradients as the most important and vice versa.
8

---

Published as a conference paper at ICLR 2020
Method
Importance Score (on SST)
Words Identified from 10 Examples on the Yelp Dataset (split by "/")
Most Important Words or Symbols
Grad
0.47
terrible great /iner /est /best food/ service/ food/ perfect best terrible we /bstt / best/ / and slow / great /ti / best
Upper
0.45
Ours
0.57
terrible great / dir best /bbsst/ good/ slow/ great perfact /eest
Least Important Words Symbols
Grad
0.40
/eccadent/ 7. /had7 a
Upper
0.24
/ typicalll///c boba / dark sttrrk//saaa/tttataaesso attar//tmopphrral / l'ooba
Ours
0.01
/tte/ // / Food/
/ice
Table 4: Average importance scores of the most/least important words identified from 100 examples respectively on SST by different methods. For the most important words identified, larger important scores better, and vice 10 examples on the Yelp dataset. Boldfaced words are considered to have strong sentiment polarities, and they should appear most important words rather than least important ones.
Additionally, we show most/least important words identified from
Quantitative Analysis SST SST contains sentiment labels for all phrases on parse trees, where the labels range from very negative (0) to very positive (4), and 2 for neutral. For each word, assuming its label is I, take |x: 2/. i.e., the distance to the neutral label, as the importance score, since less neutral words tend to be more important for the sentiment polarity of the sentence. We evaluate 100 random test input sentences and compute the average importance scores of the most or least important words identified from the examples. In Table 4 compared to the baselines ("Upper" and "Grad"), the average importance score of the most important words identified by our lower bounds are the largest, while the least important words identified by our method have the smallest average score. This demonstrates that our method identifies the most and least important words more accurately compared to baseline methods.
Qualitative Analysis on Yelp We further analyze the results on larger dataset, Yelp. Since Yelp does not provide per-word sentiment labels, importance scores cannot be computed on SST. Thus, we demonstrate a qualitative analysis. We use 10 random test examples and collect the words iden- tified as the most and least important word in each example. In Table most words identified the most important by certified lower bounds are exactly the words reflecting sentiment polarities (bold- faced words), while those identified as the least important words are mostly stopwords. Baseline methods mistakenly identify more words containing no sentiment polarity as the most important. This again demonstrates that our certified lower bounds identify word importance better than base- lines and our bounds provide meaningful interpretations in practice. While gradients evaluate the sensitivity of each input word, this evaluation only holds true within a very small neighborhood (where the classifier can be approximated by first-order Taylor expansion) around the input sen- tence. Our certified method gives valid lower bounds that hold true within a large neighborhood specified by perturbation set S, and thus it provides more accurate results.
CONCLUSION
We propose the first robustness verification method for Transformers, and tackle key challenges in verifying Transformers, including cross-nonlinearity and cross-position dependency. Our method computes certified lower bounds that are significantly tighter than those by IBP. Quantitative and qualitative analyses further show that our bounds are meaningful and can reflect the importance of different words in sentiment analysis.
ACKNOWLEEDGEMENT
This work jointly supported by Tsinghua Scholarship for Undergraduate Overseas Studies, NSF I1S1719097 and I1$1927554, and NSFC key project with No. 61936010 and regular project with No. 61876096.
REFERENCES
Michael E Akintunde, Andreea Kevorchian, Alessio Lomuscio, and Edoardo Pirovano. Verification of ma--based neural agent-environment systems. In Proceedings of the 33th AAAI Conference on

---

Published as a conference paper at ICLR 2020
Artificial Intelligence (AAA119). Honolulu, HI, USA. AAAI Press., 2019.
Moustafa Alzantot, Yash Sharma, Ahmed Elgohary, Bo-Jhang Ho, Mani Srivastava, and Kai-Wei Chang. Generating natural language adversarial examples. In EMNLP, pp. 2890-2896, 2018.
Rudy R Bunel, llker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan K Mudigonda. A unified view of piecewise linear neural network verification. In Advances in Neural Information Process- ing Systems, pp- 4790-4799 2018.
Minhao Cheng, Jinfeng Yi, Huan Zhang, Pin-Yu Yu Chen, and Cho-Jui Hsieh. Seq2sick: Evaluat- ing the robustness of sequence-to-sequeee models with adversarial examples. arXiv preprint arXiv:1803.01 128, 2018.
Jacob Devlin, Ming- Wei Chang, Kenton Lee, and Kristina Toutanova. Bert: Pre-training of deep bidirectional transformers for language understanding. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume (Long and Short Papers), pp. 4171-4186, 2019.
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analy- sis for deep feedforward neural networks. In NASA Formal Methods Symposium, pp. 121-138. Springer, 2018.
Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. A dual approach to scalable verification of deep networks. UAI, 2018.
Krishnamurthy Dj Dvijotham, Robert Stanforth, Sven Gowal, Chongli Qin, Soham De, and Push- meet Kohli. Efficient neural network verification with exactness characterization. UAI, 2019.
Javid Ebrahimi, Anyi Rao, Daniel Lowd, and Dejing Dou. Hotflip: White-box adversarial exam- ples for text classification. In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), pp. 31-36, 2018.
Ruediger Ehlers. Formal verification of biece-wise linear feed-forward neural networks. In Interna- tional Symposium on Automated Technology for Verification and Analysis, pp. 269-286. Springer, 2017.
Ji Gao, Jack Lanchantin, Mary Lou Soffa, and Yanjun Qi. Black-box generation of adversarial text sequences to evade deep learning classifiers. In 2018 IEEE Security and Privacy Workshops (SPW), pp. 50-56. IEEE, 2018.
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen Petar Tsankov, Swarat Chaudhuri, and Mar- tin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpreta- pp. tion. In 2018 IEEE Symposium on Security and Privacy (SP), pp. 3-18. IEEE, 2018
Ian J Goodfellow, Jonathon Shlens. and Christian Szegedy. Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.65T 2014.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Ue- sato, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arvi 1810. 12715, 2018
Matthias Hein and Maksym Andriushchenko. Formal guarantees on the robustness of a classifier against adversarial manipulation. Advances in Neural Information Processing Systems (NIPS), pp. 2266-2276, 2017.
Yu-Lun Hsieh, Minhao Cheng, Da-Cheng Juan, Wei Wei, Wen-Lian Hsu, and Cho-Jui Hsieh. On the robustness of self-attentive models. In ACL, pp. 1520-1529, 2019.
Po-Sen Huang, Robert Stanforth, Johannes Welbl, Chris Dyer, Dani Yogatama, Sven Gowal, Krish- namurthy Dvijotham, and Pushmeet Kohli. Achieving verified robustness to symbol substitutions via interval bound propagation. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing (FMNLP--JCNIPP) pp. 4074 2019.
10

---

Published as a conference paper at ICLR 2020
Robin Jia and Percy Liang. Adversarial examples for evaluating reading comprehension systems. arXiv preprint 1.XXv:1707.07328 2017.
Robin Jia, Aditi Raghunathan, Kerem Göksel, and Percy Liang. Certified robustness to adversarial word substitutions. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference Natural Language Process- ing (EMNLP-IJCNIP), pp. 4120-4133, 4133, 2019.
Kyle D Julian, Shivam Sharma, lean-Baptiste Jeannin, and Mykel J Kochenderfer. Verifying aircraft collision avoidance neural networks through linear approximations of safe regions. arXiv preprint arXiv: arXiv:/903.000 00762, 2019.
Wang-Cheng Kang and Julian McAuley. Self-attentive sequential recommendation. In 2018 IEEE International Conference Data Mining (ICDM), pp. 197-206. IEEE, 2018.
Guy Katz, Clark Barrett, David I. Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97-117. Springer, 2017.
Ching- Bun Ko, Zhaoyang Lyu, Lily Weng, Luca Daniel, Ngai Wong, and Dahua Lin. Popqorm: Quantifying robustness of recurrent neural networks. In International Conference on Machine Learning, pp. 3468-3477, 2019.
Jia Li, Yu Rong. Hong Cheng, Helen Meng, Wenbing Huang, and Junzhou Huang. Semi-supervised graph classification: A hierarchical graph perspective. In The World Wide Web Conference, pp. 972-982. ACM, 2019a.
Liunian Harold Li, Mark Yatskar, Da Yin, Cho-Jui Hsieh, and Kai-Wei Chang. Visualbert: A simple and performant baseline for vision and language. arXiv preprint arXiv: 19050.05807.,.. 2019b.
Xuankang Lin, He Zhu, Roopsha Samanta, and Suresh Jagannathan. Art: Abstraction refinement- guided training for provably correct neural networks. arXiv preprint arXiv: 2019.
Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zettlemoyer, and Veselin Stoyanov. Roberta: A robustly optimized bert pretraining approach. arXiiv preprint arXiv: /907. 1692, 2019.
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for prov- ably robust neural networks. In International Conference on Machine Learning, pp. 3575-3583, 2018.
Nicolas Papernot, Patrick McDaniel, Ananthram Swami, and Richard Harang. Crafting adversarial input sequences for recurrent neural networks. In MILCOM 2016-2016 IEEE Military Communi- cations Conference, pp. 49-54. IEEE, 2016.
Niki Parmar, Ashish Vaswani, Jakob Uszkoreit, Lukasz Kaiser, Noam Shazeer, Alexander Ku, and Dustin Tran. Image transformer. arXiv preprint 1802.055,, 2018.
Chongli Qin, Brendan O'Donoghue, Rudy Bunel, Robert Stanforth, Sven Gowal, Jonathan Uesato, Grzegorz Swirszez, Pushmeet Kohli, et al. Verification of non-linear specifications for neural networks. arXiv preprint 102552290. 2019.
Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems, pp- 10877-10887, 2018
Hadi Salman, Greg Yang. Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. In Advances in Neural Information Processing Systems 32, pp. 0832-9842. 2019.
Zhouxing Shi, Ting Yao, Jingfang Xu, and Minlie Huang. Robustness to modification with shared words in paraphrase identification. arXiv preprint arXiv: wwt.. 2019.

---

Published as a conference paper at ICLR 2020
Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian net- work classifiers. In IJCAI, 2018.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. Advances in Neural Information Processing Systems, pp- 10825-10836, 2018.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certi- fying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):41, 2019.
Richard Socher, Alex Perelygin, Jean Wu, Jason Chuang, Christopher D Manning, Andrew Ng, and Christopher Potts. Recursive deep models for semantic compositionality over a sentiment treebank. In Proceedings of the 2013 conference on empirical methods in natural language pro- cexsing, pp. 1631-1642, 2013.
Weijie Su, Xizhou Zhu, Yue Cao, Bin Li, Lewei Lu, Furu Wei, and Jifeng Dai. VI-bert: Pre-training of generic visual- linguisic representations. arXiv preprint 10XXiv1908.08.00 2019.
Christian Szegedy, Wojeiech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 2013.
Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. ICLR, 2019.
Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in neural information processing systems, pp. 5998-6008 2017.
Qinglong Wang, Kaixuan Zhang, Xue Liu, and C Lee Giles. Verification of recurrent neural net- 2018a.
works through rule extraction. arXiv preprint
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems, pp. 6367- 6377, 2018b.
Shiqi Wang, Kexin Pei, Justin Whitchouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In 27th (USENIX) Security Symposium ((USENI)) Security 18), pp. 1614, 2018c.
Tsui- Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Bon- ing, and Inderjit Dhillon. Towards fast computation of certified robustness for relu networks. In International Conference on Machine Learning, pp. 5273-5282, 2018.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, pp. 2292, 2018.
Yichen Yang and Martin Rinard. Correctness verification of neural networks. arXiv preprint arXiv:1906.010300 2019.
Zhilin Yang, Zihang Dai, Yiming Yang, Jaime Carbonell, Ruslan Salakhutdinov, and Quoc V Le. Xlnet: Generalized autoregressive pretraining for language understanding. arXiv preprint 1rXiv:1906.0823:: 2019.
Huan Zhang, Tsui- Wei Weng. Pin- Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural net- work robustness certification with general activation functions. In Advances in neural information processing systems, pp. 4939-4948, 2018.
Huan Zhang, Pengchuan Zhang, and Cho-Jui Hsieh. Recurjac: An efficient recursive algorithm for bounding jacobian matrix of neural networks and its applications. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 33, pp. 5757-5764, 2019.
Xiang Zhang, Junbo Zhao, and Yann LeCun. Character-level convolutional networks for text clas- sification. In Advances in neural information processing systems, pp. 649-657, 2015.
12

---

Published as a conference paper at ICLR 2020
Zhengli Zhao, Dheeru Dua, and Sameer Singh. Generating natural adversarial examples. arXiv preprint arXiv:1710.11342, 2017.
Shiyu Zhou, Linhao Dong, Shuang Xu, and Bo Xu. Syllable-based sequence-fo-seqqeence speech recognition with the transformer mandarin chinese. arXiv preprint arXiv: 2018.
13

---

Published as a conference paper at ICLR 2020
A
ILLUSTRATION OF DIFFERENT BOUNDING PROCESSES
Feed- forward
Self- attention
Feed- forward
Self- attention
Feed- forward
Input
Fully-Forward
Feed- forward
Self- attention
Feed- forward
Self- attention
Feed- forward
Input
(b) Fully-Backward
Feed-
Self- attention
Feed- forward
Self- attention
Feed-
Input
forward
forward
(c) Backward & Forward
Figure 1: Illustration of three different bounding processes: Fully-Forward (a), Fulll-Backwardd (b), and Backward& divided into two kinds of blocks, FFeed-forward" and "Selffattention". "Self-attention" contains op- erations in the self-attention mechanism starting from queries, keys, and values, and "Feed-forward" contains all the other operations including linear transformations and unary nonlinear functions, Ar- rows with solid lines indicate the propagation of linear bounds in a forward manner. Each backward arrow A + B₁ with a dashed line for blocks A&. By indicates that there is a backward bound propagation to block Bş when computing bounds for block Ag- Blocks with blue rectangles have forward processes inside the blocks, while those with green rounded rectangles have backward pro- cesses inside.
(c). We show an example of 2-layer Transformer, where operations can be
Figure illustrates comparison of the Fully-Forward, Fully- Bally-Backward and Backward Forward processes, for 2-layer Transformer as an example. For Fully-Forward, there are only forward processes connecting adjacent layers and blocks. For Hally-Backward, there are only backward processes, and each layer needs backward bound propagation to all the previous layers. For our Backward Forward algorithm, we use backward processes for the feed-forward parts and forward processes for self-attention layers, and for layers after self-attention layers, they no longer need backward bound propagation to layers prior to self-attention layers. this way, we resolve the poss-position dependency in verifying Transformers while still keeping bounds comparably tight as those by using fully backward processes. Empirical comparison of the three frameworks are presented in Sec. 4.3
14

---

Published as a conference paper at ICLR 2020
B LINEAR BOUNDS OF UNARY NONLINEAR FUNCTIONS
We show in Sec. 3.2 that linear bounds can be propagated over unary nonlinear functions as long as the unary nonlinear functions can be bounded with linear functions. Such bounds are determined for each neuron respectively, according to the bounds of the input for the function. Specifically, for a unary nonlinear function (xx), with the bounds of æ obtained previously derive a linear lower bound a = 3 and a linear upper bound a x + 3 such that
E [4, uj. we aim to
a" + 3t S o(x) saxx+ 3 (
x
E [1,
where parameters a² , _.a _8 are dependent on 1, and designed for different functions (x) respectively. We introduce how the parameters are determined for different unary nonlinear func- tions involved in Transformers such that the linear bounds are valid and as tight as possible. Bounds of ReLU and tanh has been discussed by Zhang et al. (2018), and we further derive bounds of ex. 2. =², Vz. x²² and v are only used when the layer normalization is not modified for experiments to study the impact of our modification. For the following description, we define the endpoints of the function to be bounded within range (I,r) (1, (()) and (u, (u)). We describe how the lines corresponding to the linear bounds of different functions can be determined, and thereby parameters a², ,8,,, a B" can be determined accordingly.
ReLU For ReLU activation, (xx) = max 0). ReLU is inherently linear on segments (-xo, 0] and [0, oo) respectively, so we make the linear bounds exactly (22) for u S or 2 and for I < 0 < we take the line passing the two endpoints as the upper bound: and we take o (z) 0 when u < ||| and (x) = when 2 ||| as the lower bound, to minimize the gap between the lower bound and the original function.
Tanh For tanh activation, (zx) If tanh is concave for 2 O, and thus we take the line passing the two endpoints as the lower bound and take a tangent line passing (1++)/22 (((+u))/2) as the upper bound. For u < 0, tanh is convex, and thus we take the line passing the two endpoints as the upper bound and take a tangent line passing ((1 + w)/2, ((l (u)+u/2,
u)/2) as the lower bound. For
I < 0 < u, take tangent line passing the right endpoint and (d (add)) I 0) as the lower
bound, and take a tangent line passing the left endpoint and (d (dd ()(d 2 0) as the upper
bound. d and d can be found with binary search.
Exp (xx) = exp(x)> = et is convex, and thus we take the line passing the two endpoints as the upper bound and take tangent line passing (d, (d)) the lower bound. Preferably, we take
d = (1 w)/2. However, ex is always positive and used in the softmax for computing normalized attention probabilities in self-attention layers, i.e., exp
(() and Σk= erp(s Ek= (22) appears in the denominator of the softmax, and to make reciprocal function 1
exp(( (S
= finitely bounded, the range of should not pass 0. Therefore, we impose constraint force the lówer bound function to be always positive, i.e., o+(() (l) > O, since (1) is monotonously increasing. of (x) = ex ((te-d) d) +ed is the tangent line passing (d, (d)). So the constraint of (4) > 0 yields d < +++ 1. Hence we take d min((1 (1 + n1)2,11+
Aa) where Ad is small real value ensure that d < + such as
Aa = 10
Reciprocal For the reciprocal function, o(x) z' It used in the softmax and layer normaliza- tion and its input is limited to have > 0 by the lower bounds of exp(x), and Va. With / >> 0, (x) is convex. Therefore, we take the line passing the two endpoints as the upper bound. And we take the tangent line passing ((1 + w)/2, ((1 + u)/2)) as the lower bound.
Square For the square function, a (xx) = 2 It is convex and we take the line passing the two endpoints as the upper bound. And we take a tangent line passing (d, (d) e [1. u]) as the lower bound. We still prefer to take d = (1 + w)/2. z² appears in the variance term of layer normalization and is later passed to a square root function to compute a standard derivation. To make the input to the square root function valid, i.e., non-negative, we impose constraint o "x(x) 2 0(Vz E [7, ud). of (x) 2d(x= d) + d² is the tangent line passing (d, (d)). For u < 0, x² is monotonously decreasing, the constraint we impose is equivalent to of (u) = 2du - de 2 O, and with d < O, we have d > 2u. So we take d = max(( + 22/2, 2u). For 1 2 0, x2 is monotonously increasing, and
15

---

Published as a conference paper at ICLR 2020
thus the constraint impose is equivalent (!) 2dl dl 2 0. and with d 0. have < 21. So we take max((1 + w)/2, 21). And for / < < u, since of (0) = dc is negative for
d # 0 while d = 0 yields valid lower bound, we take d = 0.
Square root For the square root function, (xx) Vs. It is used the to compute standard derivation in layer normalization and its input is limited to be non-negative by the lower bounds of x², and thus 2 0. (2x) concave, and thus we take the line passing the two endpoints as the lower bound and take the tangent line passing ((1 + 2)/2, + u)/ as the upper bound.
C LINEAR BOUNDS OF MULTIPLICATIONS AND DIVISIONS
We provide a mathematical proof of optimal parameters for linear bounds of multiplications used in Sec. 3.3 We also show that linear bounds of division can be indirectly obtained from bounds of multipliaation and the reciprocal function.
For each multiplication, 3 and z" = a" x+ 3 y+7" where x and y are both variables and x E [le, unl y/ E [ly Uyl concrete bounds of x. obtained from previous layers, such that:
aim to bound zy with two linear bounding planes 2" at +
a + 7h = == xy I = z + 7p V(I, v) E Bl., unl x uy]-
Our goal is to determine optimal parameters of bounding planes, i.e., a BL, ,2t a. B q0 such that the bounds are as tight as possible.
C.1 LOWER BOUND OF MULTIPLICATIONS
We define difference function (L y) which is the difference between the original function 2 zy and the lower bound z" = aaax + 3hy + r
(r. v) = xy - (a + 3 + 7²)
To make the bound as tight as possible, we aim to minimize the integral of the difference function
FL (x, y) on our concerned area (x., y) [I., ux) x [l Uy]. which is equivalent to maximizing
vb_ - (vely
at x
8t + 7
xENloiud vEllywy)
while FL y) 2 0 (V(x,)) E Ihe uzl x By, Myl). )). For an optimal bounding plane, there must exist a point (zo. 30) E [e,, uz] x Ily uy] such that F' Mo) = 0 (otherwise we can validly increase 7- to make VL larger). To ensure that F (z, v) 2 0 within the concerned area, we need to ensure that the minimum value of F y) is non-negative. We show that we only need to check cases when (Ir, y) is any of (Lz, Ly), (lz, Ug); (uz, 12), (ux, Uy), i.e., points at the corner of the considered area. The partial derivatives of F.. are:
dFL
Or 11 -a",
OFL -3".
Oy
If there is (1), E (lz, un) x (ly, uy) such that F² (x1, 91) S F(x, v) (V(z,)) E Ul ur] x Ry uyl), OF 8m (21.11) apL (1)
should hold true. Thereby OFL ox (a,y). By (z, y) 0 v) E 11, x By, 31 )), and thus (1, (1224,)) 12) < (x) vi) and (21.91) cannot be the point with the minimum value of (1x y). On the other hand, if there is (11,81(<1 = 1,,31 (Ly, uy)), aF
OF
By
ie., on one border of the concerned area but not on any corner, By (111 = should hold true. 8FL Thereby, By (I,, y) = aF (L,,,, This property holds true for the other three borders of the concerned area. Therefore, other points within the concerned area cannot have smaller function value FL FL v), only
dy (α), y) = (V(c, v). T1 = 12), and (=1,,11)) = (o1, =
16

---

Published as a conference paper at ICLR 2020
need check the corners, and the constraints F"1x,, y) become
F ( yo)
F (he by)
2
0
FL (lar Myy
IV
IIVI
0
F (Uzr (g)
FL (Uxe Myy
0
which is equivalent to
7 TOY0 at 3
luly o (12 Ho)
B (1y Mo) Tatlo 2 0
bu a (12 σo)
3 (uy yo! To50 2 0
(8)
Unly a (ug то) 8d yo TO50
2 0
ually a (u Ho) B 360 Foll
0
We substitute 7 in Eq.
with Eq. (8) yielding
V
Vol + ug 2x0)a " + (ly + uu 200)33 + 2m00ool
where Vo
(N. L. (n.
We have shown that the minimum function value (z, y) within the concerned area cannot appear in (br, My)) (by, uy), i.e., it can only appear at the border. When (vo, yo) is point with minimum function value FL (xo. yo) = O, (ro, Uo) can also only be chosen from the border of the concerned area. At least one of Fn l- and my uu holds true.
If we take Lz:
v
Volluz -z))at + (ly + u - 2200) + 272
And from Eq.
8 we obtain
L < Uzly 12:00 - BL v0)
U1 4
L < Ug 4,300 - 3 (uy yo)
L
4, S 8b < l1 + B² = lz
Then
Vi Vollu, - 1.)aa* " L1 fly + uy]]
(uz lt < - 12y0 + min muinuuzly - -3- (ly yo). un - B yo))
-,29/0 min(mun - 11y yo), Ur 1 (uy - yo))
(uz (2) min(ly Uy)
(uz 12) Dby.
Therefore,
a < Ly To maximize VP,, since now only a is unknown in Vi and the coefficient of a Volu. -4,) 2 0, we take at = ly. and then
vit = Vo(ualy + (u
a constant.
For the other case if we take 20 =
1í2 = Vol(Oe - uz)a 1. + (ly + Uy - 2y00) + 2uzvol,
a buly uz7l0 - BL yo)
1 Ux
17

---

Published as a conference paper at ICLR 2020
at 2 11 Uz30 - (u, v0)
12 U1
Ux S S ux + g/ Ux3
V/2 Voll4z - -ux)a uz)a" + -uolly + uyy]
(12 - uz)a* S 0,30 + min(baly 3 - y00 bul - -8" - y0))
= min(l,ly U uoly boll uy
(lg Uz) max(ly; Uy)
(lx Ux My.
Therefore,
r. 2 uy-
We take a² Ml similarly in the when 3p Lz and then
V Vo + uzhy)
We notice that VL- V/2, so we can simply adopt the first one. We also notice that VL, V22 are independent yo, so we may take any Yo within [.. Uy] such as yo = ly. Thereby, we obtain the group of optimal parameters of the lower bounding plane:
aL ly
8L la
g
C.2 UPPER BOUND OF MULTIPLICATIONS
We derive the upper bound similarly. We aim to minimize
V
Vollh= ux 20o)a U (ly + uy 2y0) 2royo]
where Vo (ua (ua-la)pe -uy
we take 20 Lz:
V Volluz -2)aa " + (ly + +u - -2y0)3 + 20
v Uzly 12:00 88 (ly -y0)
U 1
1,400 8 (uy yol
U U U,
U, l
4 S 8V
S/ g8 = lz2
Then
V Volluz - 1x)aaa + Lo (ly Uy))
(ne - l 2 -l.00 + max(usly -B,11, - yu), uelly 3d (u, y0))
= max -max(ully - loly, Uy Ly)
(ur 1x) max(ly, Uy)
= (ug - 1 uyy
Therefore,
U uy
To minimize VU, we take " = uyy and then
Ve Vo uz)
18

---

Published as a conference paper at ICLR 2020
For the other case if we take 20 Ugz
V22 = Vollz ux)a + (ly + bly - 2yo)03 + 2u)
luly Uz10 BB (1y -90)
a 1
41 - Up
a 1 1g Uz30 - 188 (My 110)
4 - U2
S 38 Sux t zu =ug.
Therefore,
V2 Voll1, uz)a + urlly + &yy],
(he - uz)a 2 U, + max(luly 8 (ly yo), 8 (u, -Y0)
= max(laly - Uply, lo - uyll)
(hx Ux) (..)mmn(ly... Uy)
= (Lr Uz My.
Therefore,
a s sly.
To minimize Vi" we take a lys and then
V = Vollaty + U2 Uny)
Since V = VL, we simply adopt the first case. And VU V are independent of you so we may take any yo within [y wy] such as y/ = ly. Thereby, we obtain a group optimal parameters the upper bounding plane:
a Uy
gU = lz 70 = -ly
C.3 LINEAR BOUNDS OF DIVISIONS
We have shown that closed-form linear bounds of multiplications can be derived. However, we find that directly bounding _ is relatively more difficult. If we try to derive a lower bound C.I the difference function
y
z atx x + Bhy y + 7 for 1 as shown Appendix
F"(x,y)= - (a"x -
is possible that minimum function value of FL y) for (x. 3) within the concerned area appears at point other than the corners. For example, for 1,, = 0.05, = 0.15,,,, 0.05, My 0.15, a 10, 8- -200 22 22 the minimum function value of (L, y) for (x, y) E [0.05, 0.15) x [0.05, 0.15] appears at (0.1, 0.1) which is not corner of [0.05, 0.15) [0.05, 0.15). This makes more difficult to derive closed-form parameters such that the constraints on f- w) are satisfied. Fortunately, we can bound = indirectly by utilizing the bounds of multiplications and reciprocal functions.
We bound by first bounding unary function y y
1 and then bounding the multiplication
D TIGHTNESS OF BOUNDS BY THE BACKWARD PROCESS AND FORWARD PROCESS
We have discussed that combining the backward process with a forward process can reduce com- putational complexity, compared to the method with the backward process only. But only use the forward process for self-attention layers and do not fully use the forward process for all sub- layers, because bounds by the forward process can be looser than those by the backward process.
19

---

Published as a conference paper at ICLR 2020
We compare the tightness of bounds by the forward process and the backward process respec- tively. To illustrate the difference, for simplicity, we consider a m-layer feed-forward network S m), where x is the input vector, w and b are the weight matrix and the bias vector for the /-th layer respectively, (x) is the pre-activation vector of the 1-th layer, ((0( is the vector of neurons in the 1-th layer, and (-) is an activation function. Before taking global bounds. both the backward process and the forward process bound Φ (x) with linear functions of x. When taking global bounds as Eq. (3) and Eq. 4 only the norm of weight matrix is directly related to the in binary search for certified lower bounds. Therefore, we try to measure the tightness of the computed bounds using the differ- ence between weight matrices for lower bounds and upper bounds respectively. We show how it is computed for the forward process and the backward process respectively.
((0) = x, y(t) ((() + b(), ( (x) = (x))
D.1 THE FORWARD PROCESS
For the forward process, bound each neuron $5 (x) with linear functions:
1 x + 1 / (x)
6 (0.0
To measure the tightness of the bounds, we are interested in (1) (2(,, and also Q -0,00-20044 002 Initially.
Ω (0)2/U I, @ (0,1/U o, 1 - -2 (0)_
We can forward propagate the bounds of (x(-1)(x) (x) y (1))
U.ybk J
(1 x + D.y.k. Ijj (x) S 2 (1)
x 2 (W.e
where
Ω (...L/UU
w
2 (1-1,111
S (1-1)
3,1 2,:
<0
Ui..L/UU =
Σ w
11-1/
(1-))) + +b
With the global bounds of (1) (x) that can be obtained with Eq. activation function:
and Eq. bound the
() + 2fth2 S saly)
10 (x)) s aj
U.N y00 (x) B0U.U.
And then bounds can be propagated from a (x) to (x):
s 100,//
of
a 1// U.LLU 1/ n t.LLLL
10/1/U 20
fn,E/U <0
aj
(0.1/0 0 O..LLUU
+ M1
(0,1/ 20 10,11 <0
θ
(1,//U
a
1onU + + Nor
Therefore,
O = (a (0. -aahu -
(2 - -2
illustrates how the tightness of the bounds changed from earlier layers to later layers.
D.2 THE BACKWARD PROCESS AND DISCUSSIONS
For the backward process, we bound the neurons in the 1-th layer with linear functions of neurons in a previous layer, the -t layer:
t ((,)) = A (L))) (x) (.. < (x) S (L13,0 (1)) (x) A -
We have shown in Sec. 3.1 how such bounds be propagated to I' 0, for the case when the input is sequential. For the nonsequential case we consider here, it can be regarded as a special
case when the input length is 1. So we can adopt the method in Sec. 3.1 to propagate bounds
20

---

Published as a conference paper at ICLR 2020
for the feed-forward network consider here. We interested in A A A and also A ((L.), AI."), Weight matrices of linear bounds before taking global bounds are A (L.0),. and A (1,0).' which are obtained by propagating the bounds starting from ( A I. According to bound propagation described in Sec. 3.2
A (1--1),0 A. - 11, = (a) (")) (
(A
A 3.- 3-- (1) (A
(.1 - 0.000 J. -5--
w (10)
+J+
illustrates how the tightness bounds can be measured during the backward bound propagation until I' 0.
There is a w(') in Eq. (00) instead of |W(O)) Eq. 9 The norm of (2 22
2. in Eq.
9 can quickly grow large as increases during the forward propagation when [/0 is greater than 1, while this generally holds true for neural networks to have forward layers. While in Eq.
[ greater than feed-
(L')
10
can have both positive and negative elements and tends to
allow cancellations for different w and thus the norm of (A (A (1.--1), A (1'-11))4 tends to be smaller. Therefore, the bounds computed by the backward process tend to be tighter than those by
the forward framework, which is consistent with our experiment results in Table 3
E IMPACT OF MODIFYING THE LAYER NORMALIZATION
The original Transformers have layer normalization after the embedding layer, and two layer normalization before and after the feed-forward part respectively in each Transformer layer. We modify the layer normalization, f(x = w(x j4/aa b, where is dddimensional vector to be normalized, and are the mean and standard derivation of (x+ respectively, and w and b are
((1/d) V Ex 2=) c where C, is smoothing constant. It involves -x)² whose linear lower bound is loose and exactly when the range of the x;- μr crosses When the -n-norm of the perturbation is relatively larger, there can be many x; 3-- - with ranges crossing 0, which can cause the lower bound of a to be small and thereby the upper bound of fi(x) to be large. This can make the certified bounds loose. To tackle this, we modify the layer normalization into f(x) w(x-)u +b + by removing the standard derivation term. We use an experiment to study the impact of this modification. We compare the clean accuracies and certified bounds of the models with modified layer normalization to models with standard layer normalization and with no layer normalization respectively. Table 5 presents the results. Certified lower bounds of models with no layer normalization or modification corresponding models with the standard layer normalization. Meanwhile, the clean accuracies of the models with modification normalization (slightly lower on Yelp and slightly higher on SST). This demonstrates that it appears be worthwhile modify the layer normalization Transformers for easier verification.
gain and bias parameters respectively.
significantly tighter than those of
comparable with those of the models with the standard layer
21

---

Published as a conference paper at ICLR 2020
Upper
Lower
Ours
Upper
Dataset
N
LayerNorm
Acc.
cp
Min
Avg
Min
Avg
Min
Avg
189.934
199.265
0.010
0.022
5.3E-5
1.1E-4
Standard
91.7
&2
15.125
15.384
0.008
0.019
S.5E-4
1.3E-3
fo
2.001
3.066
0.002
0.005
8.7E-4
1.7E-3
8.044
12.948
1.360
1.844
17%
13%
None
91.4
82
0.580
0.905
0.363
0.447
63%
49%
800 0.086
0.127
0.033
0.040
38%
32%
E1 9.085
13.917
1.423
1.809
13%
Ours
91.5
82
0.695
1.005
0.384
0.483
55%
48%
Eoo
0.117
0.155
0.034
0.043
29%
27%
Yelp
E1
190.476
201.092
0.002
0.004
1.21-5
18E--
Standard
92.0
82
15.277
15.507
0.001
0.002
9.0E-5
1.6E-4
800
2.022
2,901
0.000
0.000
9.5E-5
1.3E-4
E1
8.112
15.225
0.512
0.631
6%
4%
2 None
91.5
82
0.587
1.042
0.123
0.154
21%
15%
8oo
0.081
0.140
0.010
0.013
13%
9%
E1 10.228
15.452
0.389
0.512
4%
3%
Ours
82
0.773
1.103
0.116
0.149
14%
0.122
0.161
0.010
0.013
9%
8%
E1 190.777
194.961
0.008
0.015
4,2E-5
7.8E-5
Standard
83.0
82
15.549
15.630
0.006
0.013
4.1E-4
8.2E-4
Eoo
2.241
2.504
0.001
0.003
5.2E-4
1.2E-3
E1
6,921
8,417
2,480
2.659
36%
32%
None
83.0
82
0.527
0.628
0.411
0.447
78%
71%
8
0.089
0.109
0.032
0.035
36%
32%
E1 7.418
8.849
2.503
2.689
34%
30%
Ours
83.2
82
0.560
0.658
0.418
0.454
75%
69%
8oo 0.091
0.111
0.033
0.036
36%
32%
SST
E1
191.742
196.365
0.002
0.004
9.6E-6
1.9H-
Standard
82.5
82
15.554
15.649
0.001
0.003
7.0E-5
1.7E-4
Eno
2.252
2.513
0.000
0.000
6.6E-5
1.9E-
E1 6,742
8.118
1.821
1.861
27%
23%
2
None
83.5
82
0.515
0.610
0.298
0.306
58%
50%
8oo
0.085
0.103
0.023
0.024
28%
23%
E1 6.781
8,367
1,919
1.969
28%
24%
Ours
83.5
82 0,520
0.628
0.305
0.315
59%
50%
8oo
0.085
0.105
0.024
0.024
28%
23%
Table 5: Clean accuracies, upper bounds, certified lower bounds by our method of models with different layer normalization settings.
22


Reviews:
[{"review_id": "ryxVD3SG5B", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Contributions:\nThis paper develops an algorithm for verifying the robustness of transformers with self-attention layers when the inputs for one input word embedding are perturbed. Unlike previous work the present work can deal with cross nonlinearity and cross position dependency and the lower bounds derived in the paper are much tighter than the Interval Boundary Propagation (IBP) method which uses backward propagation. The core contribution is expounded by developing bounds for multiplication (xy) and division (x/y) and using this to compute tight bounds on self-attention layer computations. Further by introducing a forward process then combining it with a backward process, they can substantially reduce computation time as compared to the IBP method (in experiments demonstrated to be over an order of magnitude). \n\nExperimental results: Very reasonable and well thought out experiments demonstrate that a) the lower bounds produced by the method are very tight (much better than IBP for instance), and the backward&forward approach is an order of magnitude faster than the fully backward approach though they are both equally tight (the fully forward method is much looser by contrast)\n\nThe experiments on using the bound to detect the word whose perturbation will cause biggest impact (ie the most important word for explaining the decision) is much less convincing. In particular in Table 3, the second example shows that the method identifiews \"a\", \"the\" \"our\" etc, which at least do not appear to be most salient to this reviewer. [Question to authors: perhaps I misunderstood something here -- if so please explain and help me understand it better]. \n\nEvaluation / Suggestions. \nOverall I liked the paper quite a bit. I may not have fully understood something about table 3 and would welcome some explanation about why the results shown there indicate that their method works better int he second example. \n\n", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper thoroughly.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "r1xpvEcpKH", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Summary:\nThis paper builds upon the CROWN framework (Zhang et al 2018) to provide robustness verification for transformers. The  CROWN framework is based upon the idea of propagating linear bounds and has been applied to architectures like MLP, CNNs and RNNs. However, in Transformers, the presence of cross-nonlinearities and cross-position dependencies makes the backward propagation of bounds in CROWN computationally intensive. A major contribution of this paper is to use forward propagation of bounds in self attention layers along with the usual back-propagation of bounds in all other layers. The proposed method provides overall reduction in computational complexity by a factor of O(n). Although the fully forward propagation leads to loose bounds, the mixed approach (forward-backward) presented in this work provides bounds which are as tight as fully backward method. \n\n\nStrength:\nUse of forward propagation to reduce computational complexity is non-trivial\nStrong results on two text classification datasets:\nLower bounds obtained are significantly tighter than IBP\nThe proposed method is an order of magnitude faster than fully backward propagation, while still maintaining the bounds tight.\n\nWeakness:\nExperiments only cover the task of text classification. Experiments on other tasks utilizing transformers would have made the results stronger.\nThe paper makes the simplifying assumption that only a single position of an input sentence will be perturbed.  They claim that generalizing to multiple positions is easy in their setup but that is not supported.   The paper needs to declare this assumption early on in the paper (abstract and intro). As far as I could tell, even during the experiments they perturb a single word at a time.\n\nThe paper is more technical than insightful.  I am not at all convinced from a practitioners viewpoint that such bounds are useful.  However, given the hotness of this topic, someone or the other got to work out the details.   If the math is correct, then this paper can be it.  \n\nThe presentation requires improvement.  Some parts, example, the Discussion section cannot be understood.\n\n\nQuestions:\nThe set-up in the paper assumes only one position in the input sequence is perturbed for simplicity. Does the analysis remain the same when multiple positions are perturbed? \n\nSuggestions:\nA diagram to describe the forward and backward process would significantly improve the understanding of the reader.\n\nIn Table 3, I am surprised that none of the sentiment bearing words were selected as the top-word by any of the methods.  Among the ‘best’ words,  the words chosen by their method does not seem better than those selected by the grad method.\nSeveral typos in the paper: spelling mistakes in “obtain a safty guarantee”, poor sentence construction in “and independent on embedding distributions”, subject verb disagreement in “Upper bounds are discrete and rely on the distribution of words in the embedding space and thus it cannot well verify”.\n\nI have not verified the math to see if they indeed compute a lower bound.  \n", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "S1elFelaKS", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Overview:\n\nThis paper is dedicated to developing robustness verification techniques. They claim their methods can deal with verification problems for Transformers which includes cross-nonlinearity and cross-position dependency. The paper solves these key challenges which are not traceable for previous methods. Moreover, the author demonstrates their certified robustness bounds are significantly higher than those by naive Interval Bound Propagation. They also point out the practice meaning through sentiment analysis.\n\nStrength Bullets:\n\n1. It is an interesting design that combines the backward process with a forward process. The author also conducts an ablation experiment to show its advantages both in the bound estimation and computation time cost.\n2. The derivation is very solid and detailed. The author not only gives the certified bounds but also further analyzes whether the bounds are reasonable.\n\nWeakness Bullets:\n\n1. For comparison experiments, especially in Table 2, the author doesn't compare with other previous state-of-the-art methods. It just an ablation among fully forward, fully backward and combine two. To be more convincing, the author needs to post not only bounds but also time costs cross several methods on one or two datasets.\n2. The experiment only uses a single-layer transformer, I don't think it contains much more nonlinear operations then MLP, CNN or RNN in the previous work. The author needs to add experiments of multi-layer transformers. \n3. The author doesn't list all famous previous verification framework, like MILP (EVALUATING ROBUSTNESS OF NEURAL NETWORKS WITH MIXED INTEGER PROGRAMMING), even doesn't give a cite. MILP is a powerful verification technique that can deal with cross-position dependency, which can be potentially applied to transformers. The author needs to compare these methods to prove the advantages of the paper's approach.\n4. The novelty of the main contribution of the paper is arguable. Although it is the first one who does robustness verification on transformers, the linear relaxation is similar to previous work just deal with different nonlinearity. The author may provide more detail and explanation about the creative modification in relaxation or other parts of the proposed verification framework.\n\nRecommendation:\n\nFor lack of necessary experiments and limit novelty, even if I like part of the approach design, this is a weak reject.", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

Meta-review: A robustness verification method for transformers is presented. While robustness verification has previously been attempted for other types of neural networks, this is the first method for transformers. 

Reviewers are generally happy with the work done, but there were complaints about not comparing with and citing previous work, and only analyzing a simple one-layer version of transformers. The authors convincingly respond to these complaints.

I think that the paper can be accepted, given that the reviewers' complaints have been addressed and the paper seems to be sufficiently novel and have practical importance for understanding transformers.
Decision: Accept (Poster)