Towards Verified Robustness under Text Deletion Interventions
Authors: Johannes Welbl
Po-Sen Huang
Robert Stanforth
Sven Gowal
Krishnamurthy (Dj) Dvijotham
Martin Szummer
Pushmeet Kohli
Venue:  (2020)
Keywords: natural language processing
specification
verification
model undersensitivity
adversarial
interval bound propagation

Abstract: Neural networks are widely used in Natural Language Processing, yet despite their empirical successes, their behaviour is brittle: they are both over-sensitive to small input changes, and under-sensitive to deletions of large fractions of input text. This paper aims to tackle under-sensitivity in the context of natural language inference by ensuring that models do not become more confident in their predictions as arbitrary subsets of words from the input text are deleted. We develop a novel technique for formal verification of this specification for models based on the popular decomposable attention mechanism by employing the efficient yet effective interval bound propagation (IBP) approach. Using this method we can efficiently prove, given a model, whether a particular sample is free from the under-sensitivity problem. We compare different training methods to address under-sensitivity, and compare metrics to measure it. In our experiments on the SNLI and MNLI datasets, we observe that IBP training leads to a significantly improved verified accuracy. On the SNLI test set, we can verify 18.4% of samples, a substantial improvement over only 2.8% using standard training.

Published as a conference paper at ICLR 2020
TOWARDS VERIFIED ROBUSTNESS UNDER TEXT
DELETION INTERVENTIONS
Johannes Welbl
Po-Sen Huang!
Robert Stanforth
Sven Gowal
Krishnamurthy (Dj) Dvijotham! Martin Szummer! Pushmeet Kohli
"DeepMind, London, UK University College London, UK {we (welbl, posenhuang, stanforth, sgowal, dvi j, szummer, pushmeet) @google.. com
ABSTRACT
Neural networks are widely used in Natural Language Processing, yet despite their empirical successes, their behaviour is brittle: they are both over-sensitive to small input changes, and under-sensitive to deletions of large fractions of input text. This paper aims to tackle under-sensitivity in the context of natural lan- guage inference by ensuring that models do not become more confident in their predictions as arbitrary subsets of words from the input text are deleted. We de- velop a novel technique for formal verification of this specification for models based on the popular decomposable attention mechanism by employing the effi- cient yet effective interval bound propagation (IBP) approach. Using this method we can efficiently prove, given model, whether a particular sample is free from the under-sensitivity problem. We compare different training methods to address under-sensitivity, and compare metrics to measure it. In our experiments on the SNLI and MNLI datasets, observe that IBP training leads proved verified accuracy. On the SNLI test set, we can verify 18.4% of samples, substantial improvement over only 2.8% using standard training.
significantly im-
INTRODUCTION
Natural language processing (NLP) widely relies on neural networks, a model class known to be vulnerable to adversarial input perturbations (Szegedy et al. 2013 Kurakin et al. 2016). Adversarial
samples typically expose over-sensitivity to semantically invariant text transformations (Belinkov &
Bisk
2017 Ettinger et al. 2017). e.g. character flips (Ebrahimi et al. 2018) paraphrases (Ribeiro 2018b lyyer et al. 2018).
et al.
Feng et al. (2018) exposed another type of problematic behaviour: deleting large parts of input text can cause a model's confidence to increase; Figure shows an example. That is, reduced sets of input words can suffice trigger more confident predictions. Such under-sensittiiity is problematic:
neural models can 'solve' NLP tasks without task-relevant textual comprehension skills, but instead fit spurious cues in the data that suffice to form correct predictions. Models might then achieve strong nominal test accuracy on data of the same (biased) distribution as the training set, by exploiting predictive shortcuts that are not representative of the given NLP task hand. Consequently, they fail drastically when evaluated on samples without these spurious cues (Jia & Liang 2017 Poliak al. 2018 Gururangan et al., 2018 Niven Kao, 2019).
A major issue with identifying reduced inputs is the combinatorially large space of arbitrary text deletions; this can only be searched exhaustively for short sequences. Prior work has considered heuristics like beam search (Feng et al.] (018)) or bandits (Ribeiro et al. (018a), but these are gener- ally not guaranteed to find the worst-case reductions.
In this work, we address the under-sensitivite issue by designing and formally verifying the under- sensitivity specification that a model should not become more confident as arbitrary subsets of input words are [ Under-sensitivity behaviour is not reflected in nominal accuracy, but can
Work done during an internship at DeepMind.
This specification discussed in Section Although conservative choice, we find it is rarely satisfied.

---

Published as a conference paper at ICLR 2020
Premise: little boy blue shirt holding toy. Hypothesis: A boy dressed in blue holds toy. Entailment (86.4%)
Original Sample
Reduced
Premise: litlle boy blue shirt holding toy.
Sample
Hypothesis: A boy dressed in blue holds Entailment (91.9%)
Figure Example of under-sensitive behaviour in Natural Language Inference, where deleting premise words increases model confidence. This problem was identified by Feng et al. (2018); our aim is to formally verify whether or not any such reductions exist, over the combinatorially large space of possibilities.
instead use this specification measure and evaluate the extent with which samples exhibit under- sensitivity. Instead of better, yet still imperfect search heuristics, we describe how interval bound propagation (IBP) (Gowal et 2018 Mirman et 2018 formal model verification method can be used to efficiently cover the full reduction space, and verify the under-sensitivity specification. IBP can be applied at test time arbitrary model inputs verify whether or they are under- sensitive; but it can also be used to derive new auxiliary training objective that leads to models verifiably adhering to this specification, and which we find generalises to held-out test data.
While under-sensitivee sensitivity has been demonstrated for several NLP tasks (Feng et al.. 2018), we chose to study the use case of natural language inference (NLJ) (Dagan et al. 2006 Bowman et al. 2015) in particular as a representative task: sequences are comparatively short, datasets large, and the label complexity is small. We investigate the verification the popular decomposable attention model (DAM (Parikh et al. 2016) in detail. This architecture covers many of the neural layer types of contemporary models, and we focus on a detailed description for how IBP can be leveraged to effi- ciently verify its behaviour. We then experimentally compare various training methods addressing muder--ensitivity. i) standard training ii) data augmentation iii) adversarial training iv) IBP-verified training and entropy regularisation, and evaluate their effectiveness against nominal (test) accu- racy, adversarial accuracy, Ier-verified accuracy and a verification oracle.
To summarise, the main contributions of this paper are (1) Formalisation of the problem of verifying an under-sensitivity specification, (2) Verification of the Decomposable Attention Model using Inter- val Bound Propagation, and (3) Empirical analysis of the efficacy of (i) different evaluation methods for verifying robustness; and (ii) different training methods for developing verifiably robust models.
RELATED WORK
Natural Language Inference. Natural Language Inference (Dagan et al. 2006) is the task of predicting whether a natural language premise entails a natural language hypothesis. The availibility of large-scale datasets (Bowman et al. 20155] Williams et al. 2018)) has spurred profusion of neural architecture development for this task, e.g. (Rocktäschel among many others.
2016 Parikh al. 2016 Chen al.,
2017).
Adversarial Vulnerability in NLP. There is a growing body of research into NLP adversarial examples, each using a slightly different choice of semantically invariant text transformations, or a task-specific attack. A first class of attack considers word- and character-level perturbation attacks (Ebrahimi et al. 2018 Alzantot et al. 2018) while another type of attack exploits back-translation systems to either mine rules (Ribeiro et al. 2018b) train syntactically controlled paraphrasing models (lyyer et 2018). [i et al. (2017) use syntactic and lexical transformations, whereas Be- linkov & Bisk (2017) investigate synthetic and natural noise in Machine Translation. Jia & Liang (217)) and Mudrakarta et al. (2018) introduce task-specific adversarial attacks for Reading Com- prehension/ QA, Zhao
(2018) for Machine Translation and NLI, and Thorn Vlachos (2019) for Fact Checking. In NLI in particular, MMnervini & Riedel (2018) penalise adversarially chosen
The DAM model is z 5% behind the current state-of-the-art on SNLI. We see specification verification for this model stepping stone towards verifying larger cateetion-hased NL. architectures, such BERT.
2

---

Published as a conference paper at ICLR 2020
100
Hypothesis Reduction
Words Deleted (%)
80
Premise Reduction
60
40
0
0
20
40
60
80
100
Dataset Percentile [%)
Figure 2: Under-sensitivity: This figure maps dataset percentiles against the proportion of words one can delete before DAM prediction confidence decreases, where reduced samples are found using beam search.
logical inconsistencies in NLJ predictions, Kang et al. (2018) use Miikgrround-noowledde guided adversaries, and Glockner et al. (2018) utilise lexical entailment relationships.
Ribeiro et al. (2016) and Ribeiro et al. (2018a) describe analysis tools that have uncovered model over-sensitivity and under-sensitivityy respectively. Feng al. (2018) focus on under-sensittvitty, showing that models can become more confident as large fractions of input text are deleted, whereas
Niu & Bansal (2018) address under-sensitivity in dialogue setting. JJacobsen et al. (2019) demon- strated link between excessive prediction invariance and model vulnerability in computer vision.
Formal Verification. Formal verification provides a provable guarantee that models are consistent with a formally defined specification (a mathematical relationship between the inputs and outputs of the model). Examples of specifications include robustness bounded adversarial perturbations, monotonicity of the output with respect to a subset of the inputs, and consistency with physical laws QQin et al. 2019). Literature can be categorised into complete methods that use Mixed-Integer Programming (MIP) (Bunel et al.) 2017 Cheng et al. 2017) or Satisfiability Modulo Theory (SMT) (Katz al. 2017). and incomplete methods that solve a convex relaxation of the verification problem (Weng et al. 2018 Wong & Kolter 2018 Wang al. 2018 Raghunathan et al. 2018b). Complete methods perform exhaustive enumeration to find a counter-example to the specification or rule out the existence of counter-example. (thus proving that the specification is true). Hence, complete methods are expensive and difficult to scale. Incomplete methods are conservative (i.c. they cannot
always prove that a specification is true even when it is), but are more scalable and can be used inside the training loop for training models to be consistent and verifiable (Raghunathan et al. 2018a Wong & Kolter 2018
Dvijotham al. 2018a Gowal et al. 2018 Dvijotham al.[ (018b)
While Barr & Klavans (200)) address the issue of verification in NLP, most of the recent work has focused on L. noundbounded perturbations for image classification. This paper complements work
on incomplete verification methods by extending IBP to NLI where inputs are inherently discrete (to the contrary of images which are continuous). In the NLP context in particular, |Huang et al.) (2019) Jia et al. (2019) have very recently verified CNN, and LSTM models with specifications against over-sensitivity adversaries under synonym replacement. Wang et al. (0019) study verification of output length specifications in machine translation models, showing that the outputs of machine translation and image captioning systems can be provably bounded when the inputs are perturbed within a given set. In contrast, this work examines under-sensitivity behaviour: excessive model pre- diction invariance under arbitrary word combination deletions. We highlight that the verification of neural networks is an extremely challenging task, and that scaling complete and incomplete methods to large models is an open problem.
FORMULATING A SPECIFICATION AGAINST UNDER-SENSITIVE
Neural networks are expressive models that can fit large datasets and achieve strong nominal test accuracy. At the same time however, they can fit data in way that violates our idea of how they should fit it, from an input attribution perspective. Figure 2 visualises the extent of the problem in NLI: it is, for example, for 20% of the SNLI test possible to delete 78% more of premise
3

---

Published as a conference paper at ICLR 2020
words while the prediction confidence increases remains the same. We will next formally describe a specification that checks a model's snder--snnittivity i.c. whether any such reduction exists.
The specification addresses model output probabilities when parts of the input text are deleted. To this end, we first introduce the notion of a perturbation space X (x"(xo of an original nominal input x This space contains all possible reductions, i.e. inputs where arbitrarily chosen tokens of the original nominal input x xhom are deleted. Note that this space grows exponentially in the length of the input. We would like verify whether or not there exists any reduced input x with higher probability for the (nominal) prediction than x nom has. More formally, this can be stated as a specification:
Vx
(x"om")))
P(0 S P(o
(I)
where ÿ is the (nominal) model prediction.
Determining precisely how prediction probabilities should change when input words are deleted contentious and prone to inconsistencies: removing stop words for example may lead to little relevant change, while crucial information carrying words (e.g., 'not") can significantly alter the meaning of the sentence in a task. It important to be cautious and not too restrictive in the specification design, and certain that whatever is specified is desirable. A specification to at least not increase prediction probabilities under arbitrary input deletion is a conservative choice 5 Other specifications are worth consideration, such monotonically decreasing certainty more input is deleted. We will however see that even our very conservative choice of an under-sensitivity specification is hard to positively verify for most inputs in the DAM model.
There are different approaches to establish if the Specification I is satisfied. With unlimited com- putational capacity, the property could exhaustively be evaluated for x E 2² (x"om). Statisti- cally sampling from the reduction space can give an indication of under-sensitiiitty, but has a very limited coverage rate. Search heuristics can try identify violations (and be used for "adversar- ial' training). but there is no guarantee that a stronger search procedure cannot find more or worse violations. IBP verification on the other hand offers a formal guarantee across the whole space by establishing outer bounds for Xii (xmo)) and resulting bounds on output probabilities.
4 BACKGROUND
We next give a brief introduction to the Decomposabl Attention Model (DAM) which we will later verify. The DAM architecture comprises commonly used neural NLP components, such as word embeddings, attention, and Propagation and then bring these together to verify the behaviour of the DAM, i.e. efficiently assert whether an input satisfies Specification
networks. Subsequently we introduce Interval Bound
Decomposable Attention. The NLI task takes two word sequences as input a premise and hypothesis and outputs a discrete entailment label prediction in (entailment, neutral, contra- diction). The DAM architecture (Parikh et al. 2016) assumes the input word sequences to be embedded (e.g. as d-dimensional word vectors), i.e. operates on two sequences of input vectors A = [ arr] E Rdx1, and B = [b. by] E R where [ii-] denotes concatenation, and I and J are sequence lengths. Word vectors are individually transformed with a vector-valued function F(),, and pairs thereof are then compared:
Eij = F(a.) (F.F))((())))) E IR
Note that we follow the notation of Parikh et al. (216)), and that eiy is not related to a basis vector. In the general model formulation F can be a linear transformation or MLP; this does not affect the derivations made here. Adopting matrix notation across position pairs (f,j), Equation (2) can instead be rewritten in matrix form as E F(A) F(B) E [ which is used to compute two
3 We do note that removing relativising words (c.g. 'somewhat") can present an exception to this specifica- tion, but they are very rare in the datascts used here. We will use holdface notation for vectors and matrices, and light notation for scalars and functions.
4

---

Published as a conference paper at ICLR 2020
attention masks over each sequence by normalising across i or across
p(A)
cxp (esy)
P(A) E R TxJ
(3)
Σn exp (Eks)
exp (Exj)
P =
P(B) R
(4)
Ex exp (Eix)
These two attention masks serve as coefficients in a convex combination over the original word vectors, aggregating each of the two sequences:
A A P(P(A) l RaxJ
B = B (P(BB) E RR
That is, and hold attention-aggregatee word vectors from A and B at positions j = L....,JJ and 1,... ,. respectively. These joined with the original word representations, mixed using position-wise feed-forward network G Rddd Rd and finally summed into single vector representation for each sequence:
VI [G((a,Bi) Rd
(5)
V2 E;(AAbb))) Rd
(6)
As a last step, logit vector with entries for each class computed as H(Vv,, v2l), where R2dd + RC is again a feed-forward network, and C' is the number of output classes.
Interval Bound Propagation. IBP is an incomplete but efficient verification method that can be used to verify ouput-output relationships. tracks how a part the input space (in our case: the perturbation space X (xnm))) propagates forward through the network. IBP starts with axis- aligned bounding box surrounding Xx" (x"omo) ), and uses interval arithmetic to obtain an axis-aligned bounding box for the output set. Formally, let us assume that the neural network is defined by sequence of transformations hs for each of its K layers. That is, for Za E xxi
Z hg (Zk-1)
k l,..,,,
(7)
The output Zκ E C has C logits corresponding to C' classes. IBP bounds the activation Zμ of each layer by an axis-aligned bounding box (i.e., 2 S 2 S Zς) using interval arithmetic. We have for each coordinate 2 of zg:
min
e; (z
2
15
(8)
T Th (2x-1)
Zkii Let-1 7
max
where e; is the standard 1th basis vector. Finally, at the last layer, an upper bound on the worst-case violation of the specification can be evaluated quickly from the logit lower and upper bounds ž and žg respectively, as the bounds translate directly into bounds for the softmax probabilities.
IBP can be performed in parallel while running the nominal forward pass. However in general the output bounds are loose, which is exacerbated with increasing network depth. Consequently IBP over-approximates the true extent of the image of xxin (x" in output space, and can result in false negatives. It is thus in practice important to keep the bounds as tight as possible. IBP can be used at test time for verification, but also for training, minimising loss terms derived from the logit bounds. IBP has been used on MLPs and convolutional networks with monotonic activations (Gowal et al.) 2018 Huang et al. 2019). One technical contribution of this work is apply model with an attention component (Section 5)
5 VERIFYING SEDEERSENSITIVITE GUARANTEES FOR THE DAM MODEL
To address under-sensitivity, we aim to verify Specification for the DAM model. If the upper probability bound d of the entire perturbation space X (x mlo) is smaller than the probability po)) for the predicted class, then the specification is verified. That is Vzo E zin (xnom):
P(o Z & P(g x nom)
5

---

Published as a conference paper at ICLR 2020
Using this inequality, x xmm,, i.. whether there exist any reduced samples with higher probability than x
assert whether Specification ① is verifiably satisfied for any given
Overview. We will first deseribe the model behaviour when removing single word at fixed po- sition, and then extend this to deleting single words at any position, and finally generalise this to arbitrary multi-token deletions.
One key difference to IBP bounds of other architectural components, such as CNNs or ferd-forward layers, is the need for bounds the attention normalisation, which has to take into account per-token upper and lower bounds. We will exploit the fact that each vector of B is a convex combination of the vectors that constitute B (and similarly for A). Hence, component-wise bounds on B can be obtained efficiently by maximising over those J vectors. A and B are then inputs to regular network (G followed by H), for which IBP can be used.
Deleting Single Word: Particular Position. We first describe how model variables behave when an individual token at a fixed position r is removed from one of the sequences. Without loss of generality, we delete words from the second sequence, noting that the model has symmetric chitecture and that the same can be derived for the other input sequence. We denote all resulting quantities with bar (as in B). That is, when removing single token at position
B .i.bb...bbby b, b,41,.... by] E Rd-(J-1)
(10)
whereas A A. Since F(.) is applied per-position in the sequence, the effect of word deletion remains isolated at this point; the matrix product E F(A) F(B) R(x(J-1) has identical entries as before, but the r-th column disappears.
Renormalising Attention Masks. Likewise the attention mask P(A) has identical entries com- pared P(A), but the r-th column removed. That is, for I....:I and j = l.......J........... s.t. j + r:
P(A)
cxp (eis) P(A) E (X(--1))
(11)
ΣE exp (Exz)²
The attention mask (BB) on the other hand has renormalised entries. The values retain their relative order, yet the entries are larger because the r-th normalisation summand is removed. For j * r:
P
exp (eis)
((B) E (I(((-1)
(12)
Σ Eker exp (eax)
(B) Hence compute ij in closed form
p (B) P(() En exp (cx)
(13)
Σner exp (eik)
To summarise the above: attention weights p( remain largely unchanged when deleting token r, but are rescaled to take into account missing normalisation mass.
In the next step, the model computes convex combinations and B. Concretely, A A P(A) e (J-() has unchanged elements compared to before (as remains unchanged), but the r-th column is removed. For B B (P(B))T E Raxx the dimensionality remains unchanged, but B has fewer elements and (P(B)) is renormalised accordingly. Note that all this can still be computed in closed form using Equation [3). i.e. without need for IBP thus far, and these quantities can further be fed through the remaining network layers G and H to obtain concrete probabilities.
Deleting Single Word: Arbitrary Position. We have reached the point where A, B, and B are derived in closed form, for fixed position r. These can be computed exactly without approximation, for deleted words at any position in the sequence. Extending this to arbitrary single-word deletions, we take the elementwise minimum maximum across all possible single word deletions, e.g.
B Upper
max B(r)
(14)
B Lower
min B(r)
(15)

---

Published as a conference paper at ICLR 2020
which establishes upper and lower bounds for each element, and analogously for the other matrices.
In the DAM architecture, these matrices are next fed into dense feed-forward layers G (Equations (5) and (6) and H. each with two layers D We use IBP to propagate bounds through these layers, feeding in bounds on A, B, A and B as described above. As a result, after propagating these bounds through G and H, obtain bounds output logits (and consequently probabilities) for deletions of a single token at any position.
One further simplification is possible: we compute V2 directly from V2 by subtracting the r-th summand for fixed r (see Equation (6) Generalising this to arbitrary positions r, we can bound the subtracted vector with max (G([Ar; b,))) and miny=1,..... (G([A,; br])]. and thus directly
obtain bounds for V2-
Deleting Several Words. We have described the behaviour of intermediate representations (and bounds for them) under deletions of arbitrary individual words; the case of removing several words similar. The values of remaining individual word vectors a; and by naturally remain unchanged. The previously established bounds for single word deletions can be partly re- re-used to establish bounds for arbitrary multi-word deletions, see appendix [A] for more detail. The resulting bounds for V and 22 are then input to regular feed-forward network, for which IBP can be used.
6 EXPERIMENTS
We now evaluate to which extent the DAM model verifiably satisfies the Specification against under-sensitivity, and we will furthermore compare different training approaches. Experiments are conducted two large-scale NLI datasets: SNLI (Bowman al., 2015) and multiNLI (Williams) jet al. 2018), henceforth MNLI. Whereas Ween et al. (2018) addressed deletions of hypothesis words in SNLI, we establish the phenomenon also for MNLI, and for premise reductions. In our exper- iments we use premise reductions, noting that under-sensitivity is also present for hypotheses (see standard dataset splits, tuning hyperparameters and reporting results for the test set. For MNLI we split off 2000 samples from the development set for validation purposes and use the remaining samples as test set. We use the same types of feed-forward components, layer size, dropout, and word embedding hyperparameters described by
Fig. 2. For SNLI
the development set
Parikh et al. (2066).
Evaluation Metrics We evaluate with respect to the following metries:
1. Accuracy: Standard test accuracy.
2. Verified Accuracy: This metric measures whether both i) the prediction is correct ii) it can be verified that reduction with higher probability exists, using IBP verification.
3. Beam Search Heuristic: This metric uses beam search to find specification violations in the perturbation space. following the protocol of Feng et al.) (2018). Search begins from the full sequence, gradually deleting words while keeping a beam of width 10. This metric then measures whether both i) the search heuristic found no counterexample, and ii) the prediction is correct. Note that this heuristic does not cover the full perturbation space, i.c. does not suffice to rule out counterexamples to the specification. This metric provides upper bound for verified accuracy.
Training Methods We will compare the following training methods:
1. Standard Training: log-likelihood training.
This provides baseline for under-sensitivity behaviour under standard
2. Data Augmentation: A first and comparatively simple way to address under-sensitivity is by adding training samples with random word subsets deleted, and penalising the model with a loss proportional to the specification violation.
3. Adversarial Training: Here we use a more systematic approach than random word dele- tions: search within the perturbation space for inputs with large differences between
'We use softplus activations, a continuous approximation the ReL.U used in the original model.

---

Published as a conference paper at ICLR 2020
Training Method
Accuracy
Verified Accuracy
Beam Search Heuristic
Standard Training
77.22
2.83
3.36
Data Augmentation
76.37
5.09
6.27
Adversarial Training: random
76.89
1.79
4.16
Adversarial Training: beam search
76.09
5,48
23.76
Entropy Regularisation
77.32
5.82
6.28
IBP- IBP-Training
75.51
18.36
19.26
(a) SNLI
Training Method
Accuracy
Verified Accuracy
Beam Search Heuristic
Standard Training
60.00
7.77
8.77
Data Augmentation
62.02
1.93
4.26
Adversarial Training: random
61.89
2.60
5.04
Adversarial Training: beam search
58.74
0.45
7.44
Entropy Regularisation IBP-Training
60.74
8.83
9.47
44.95
17.44
19.07
(b) MNLI
Table 1: Experimental results: accuracy verified accuracy using IBP, for different training meth- ods. All models tuned for verified accuracy, numbers in %.
nominal prediction probability and reduced probability, i.e. the strongest specification vio- lations. We compare both i) random adversarial search that samples 512 randomly reduced perturbations and picks the strongest violation, and ii) beam search with width 10, follow- ing the protocol of Feng et al. (2018). Both for data augmentation and adversarial training. altered samples are recomputed throughout training.
4. Entropy Regularisation: Feng et al. (2018) observed that entropy regularisation on predic- tion probabilities can partially mitigate the severity of under-sensitiiitty
5. IBP-Training: Here we use IBP verification described Section which provides upper bounds on the prediction probability of arbitrarily reduced inputs (Fq. (9) We penalise the model with an auxiliary hinge loss on the difference between the upper probability bound for the gold label y and the nominal probability P(y))"om). Note that the upper bound serves as a proxy for the adversarial objective, as it over-approximates the probabilities of arbitrary reduced samples, covering the full reduction space comprehensively.
Training Details The training methods described above make use of additive contribution to the training loss besides standard liglliked We tune the scale of the respective contribution in [0.01, 0.1, 1.0, 10.0, 100.0]. All experiments used learning rate of 0.001, Adam optimiser, and batch size 128. We perform early stopping with respect to verified accuracy, for a maximum of 3M training steps. For verified training, we found it useful to continuously phase in the volume of the perturbation space to its maximum size, similar to Gowal et al. 2018). Concretely, we compute the per-dimension center of upper and lower bound, and start linearly increasing its volume until it reaches the full perturbation space volume. Similarly we phase in the perturbation radius, i.c. the maximum number of words deleted from to the maximum sequence length 48. We tune phase- in intervals in [10", 103, 10a, 10 109 training steps. We also experimented with over-inflating the perturbation volume larger than real size training time, as well as randomly sampling maximum perturbation radius during training, neither of which improved verifiability results.
6.1 RESULTS AND ANALYSIS
Evaluating the Effectiveness of IBP for Verification. Tables Ta and lb show the main results. For both datasets, nonnneglig portion of data points can be verified using IBP. The gap between (standard) accuracy however striking: only small fraction of correctly predicted inputs is actually verifiably not under-sensitive. Note that IBP accuracy is naturally bounded above by the beam search heuristic, which does however not cover the full reduction space, and overestimates verification
8

---

Published as a conference paper at ICLR 2020
Metric
Time[s]
# Eval's /sample
Accuracy
2
IBP Verification
3
2
Verification Oracle
2' b L
Oracle up 200K
45674
200000
Beam Search
505
Table 2: Computational cost of verification. Left: time elapsed (1 GPU) for evaluating 300 SNLI samples, without cross-sample batching. Right: worst-case number of forward passes. L: sequence length; 6: beam width.
Training
IBP
Oracle
Beam
Standard Training
4.34
5.13
5.37
Data Augmentation
6.48
8.59
8.78
raddoo
1.87
6.88
7.03
Adversarial:bean
5.13
31.90
32.14
Entropy Regul.
8.35
8.90
9.28
IBP-Training 19.29
20.68
20.94
Table 3: Oracle on SNLI sequences up to 12 tokens. Numbers in %.
rates. IBP verification becomes particularly effective when adding the IBP-verifiability objective during training, verifying 18.36% and 17.44% of samples on SNLI and MNLI. Verifiability does however come at a cost: test accuracy is generally decreased when tuning for verifiability, compared to Parikh et al. (2016). This highlights shortcoming of test accuracy the under-sensitivity problem. Once under-sensitivity is taken into account by dedicated training objectives tuning for verification rates, nominal accuracy suffers.
metric: it does not reflect
gives a breakdown of the computational cost incurred for verification, both empirically, and the theoretical worst-case number of forward passes required per sample. IBP verification comes with small computational overhead compared to a standard forward pass, which is incurred by propagating upper and lower interval bounds through the network once. A full oracle is computationally infeasible, instead used exhaustive search oracle, but only up to a maximum budget of 200K forward passes per sample. Even when stopping soon single reduced sample is found that violates the specification, the incurred time is orders of magnitude larger than verification via IBP.
Computational Efficiency of IBP Verification. Table 2 gives
Comparing Training Methods. We next discuss the differences between training methods, and how they reflect in verified model behaviour. In absolute terms, standard training does not adhere to the under-sensitivity specification well, neither on SNLI nor MNLI. Data augmentation and ran- dom adversarial training lead to slightly different results the two datasets, albeit without major improvements. These methods have a strong random component in their choice of deletions, and this tends to lead to lower verification rates MNLI, where premises longer, and the reduction space is correspondingly larger. Beam search adversarial training leads to improved verification rates SNLI, yet not for MNLI, and it noteworthy that when also trained with beam search adversarial samples, beam search evaluation improves substantially. Entropy reg- ularisation improves verified accuracy over standard training: this in line with previous observa- tions that it mitigates under-sensitivity behaviour, made by Feng et al. (2018). Finally, the dedicated IBP-Training objective substantially raises verification rates compared all other approaches. In an ablation (Table we evaluate performance on short sequences (up to 12 tokens) in the SNLI test set: here an exhaustive search over all possible reductions is feasible. Still the absolute verification rates are low in absolute terms, but observe that shorter sequences are comparatively easier to verify, and that the incomplete IBP verification can approach the verification levels of the complete oracle (see rows 1.2,5, and 6). For adversarial training (rows 3 and 4), however, oracle verification rates are much closer to the Beam Search Heuristic. This suggests that i) for short sequences the smaller perturbation space be covered better by beam search, and ii) adversarial training can
average 6.2 tokens

---

Published as a conference paper at ICLR 2020
lead to high verifiability short sequences, but it fits model in way that results in loose IBP bounds.
7 DISCUSSION
Verification of specification offers stronger form of robustness than robustness to adversarial samples. Adversarial accuracy, as e.g. derived from beam search, might conceptually be easier to compute, yet has no guarantees find or the strongest violations. In fact, evaluating against weak adversaries under-estimates the extent of problem (Uesato et al. 2018) and may lead to false sense of confidence. IBP verification can provide guarantees on the nonexistence of reduced inputs, but it is incomplete and can have false negatives.
Observations of comparatively low verification or adversarial accuracy rates as in this work not new, and have been found to be general problem of datasets with high sample complexity (Schmidt et al. 2018). We emphasise that under-sensitivity a very challenging problem to address; even the relatively conservative specification of non-increasing probability under deletion cannot be fulfilled for the majority of test samples under the baselines tested.
We see the verification of the attention-basee based DAM model as stepping stone towards the veri- fication of larger and more performant attention-based architectures, such as BERT. Following the derivations here, token deletion bounds could similarly be propagated through BERT's self-attention layer. Towards this end, however, we see two main hurdles: i) BERT's network depth, resulting in gradually looser IBP bounds ii) BERT's word piece tokenisation, which requires special considera- tion in conjunction with token-level perturbations.
CONCLUSION
We have investigated under-sensitivity to input text deletions in III and recast the problem as one of formally verifying specification on model behaviour. We have described how Interval Bound Propagation can be used in order to verify the popular Decomposable Attention Model, and have then compared several training methods in their ability to address and be verified against under- sensitivity. We observed that only a relatively small fraction of data points can be positively verified, but that trainiigg in particular is capable of improving verified accuracy.
REFERENCES
Moustafa Alzantot, Yash Sharma, Ahmed Elgobary, Bo-Jhang Ho, Mani Srivastava, and Kai- Wei Chang.
Generating natural language adversarial examples. In Proceedings of the 2018 Conference on Empirical Methods in Natural Language Processing, pp. 2890-2896 Brussels, Belgium, October-November 2018. Association for Computational Linguistics. URL https:
7/ 7/www. aclweb. orgo hnthaooooooooooioo 1316
Valerie Barr and Judith L. Klavans. Verification and validation of language processing systems: Is it evaluation? In Proceedings of the ACL 2001 Workshop on Evaluation Methodologies for Language and Dialogue Systems, 2001. URL https: www www.wa.wwwwb...... http://www..r./tthhlo.coooo
W01 0906
Yonatan Belinkov and Yonatan Bisk. Synthetic and natural noise both break neural machine trans- lation. CoRR,
2017.
Samuel R. Bowman, Gabor Angeli, Christopher Potts, and Christopher D. Manning. A large anno- tated corpus for learning natural language inference. In Proceedings of the 2015 Conference Empirical Methods in Natural Language Processing, pp. 632-642, Association for Computational Linguisties, 2015. doi: 10. 10.18653/v/D115-1000 1075. URL http:: wwtp://wwwww.......///..oooooo.. D15-1075
Rudy Bunel, Ilker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar. Piecewise linear neural network verification: comparative study. arXiv preprint 1.1000055, 2017.
10

---

Published as a conference paper at ICLR 2020
Qian Chen, Xiaodan Zhu, Zhen-Hua Ling, Si Wei, Hui Jiang, and Diana Inkpen. for natural language inference. In Proceedings of the 55th Annual Meeting of the Associa- tion for Computational Linguistics (Volume 1: Long Papers), pp. 1657-1668. Association for Computational Linguistics, 2017. doi: 10. 10.18653/11/117-1152 URL /ttttt//://cll web. org/
Enhanced Istm
anthol.ogy/P17-1152
Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In International Symposium on Automated Technology for Verification and Analysis, pp. 251-268. Springer, 2017.
Ido Dagan, Oren Glickman, and Bernardo Magnini. The pascal recognising textual entailment chal- lenge. In Proceedings of the First International Conference on Machine Learning Challenges: Evaluating Predictive Uncertainty Visual Object Classification, and Recognizing Textual Entail- ment, MICW 05, pp. 177-190, Berlin, Heidelberg, 2006. Springer- Verlag. ISBN 3-540-33427- http://xxxcciirgg///////// URL 1t
0, 978-3-540-33427-9, doi: 10. 10.1007/117367900. 11736790_2
Krishnamurthy Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovic, Brendan O'Donoghue, Jonathan Uesato, and Pushmeet Kohli. Training verified learners with learned ver- ifiers. arXiv preprint 180. 10265, 2018a.
Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. A dual approach to scalable verification of deep networks. arXiv preprint / 2018b.
Javid Ebrahimi, Anyi Rao, Daniel Lowd, and Dejing Dou. Hotflip: White-box 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. Association for Computational Linguistics, 2018. URL pattt://aclwert org anthology/ooo -2006
Allyson Ettinger, Sudha Rao, Hal Daumé III, and Emily M. Bender. Towards linguistically gen- eralizable nip systems: A workshop and shared task. In Proceedings of the First Workshop on Building Linguistically Generalizable NLP Systems, 2017.
Shi Feng, Eric Wallace, Alvin Grissom II, Mohit lyyer, Pedro Rodriguez, and Jordan Boyd-Graber. Pathologies of neural models make interpretations difficult. In Proceedings of the 2018 Con- ference on Empirical Methods in Natural Language Processing, pp. 3719-3728. Association for Computational Linguistics, 2018. URL http::::/eallw....r///tttt...ooa
1407
Max Glockner, Vered Shwartz, and Yoav Goldberg, Breaking nli systems with sentences that require simple lexical inferences. In Proceedings of the 56th Annual Meeting of the Association for Com- putational Linguistics (Volume 2: Short Papers), pp. 650 655.655.11 Association for Computational Linguistics, 2018. http:tt////aclll
org wttp///aaooooolggg//11--------
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Ue- sato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli. On the effectiveness interval bound propagation for training verifiably robust models. CoRR, abs/18100 12715, 2018. URL htttp://axxi.org/ abs /110 12715
Suchin Gururangan, Swabha Swayamdipta, Omer Levy, Roy Schwartz, Samuel Bowman, and Noah A. Smith. Annotation artifacts natural language inference data. In Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Lin- guistics: Human Language Technologies, Volume 2 (Short Papers), pp. 107-112, New Orleans, Louisiana, June 2018. Association for Computational Linguistics. doi: 10. (0.18653/1/N118-2011
URL https:://// www. a cl web. weeeb.orr/aee httgg//nthology/// 80201
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. arXiv preprint 1rxiv:1909001490 2019.
Mohit lyyer, John Wieting, Kevin Gimpel, and Luke Zettlemoyer. Adversarial example generation with syntactically controlled paraphrase networks. In North American Association for Computa- fional Linguistics, 2018.
11

---

Published as a conference paper at ICLR 2020
Koern-Henrik Jacobsen, Jens Behrmann, Richard Zemel, and Matthias Bethge. Excessive invariance causes adversarial vulnerability. In International Conference on Learning Representations, 2019.
net.:iiwwweeeeeeeeeeee net/ Eorumn21ddBBttssscccc
Robin Jia and Percy Liang. Adversarial examples for evaluating reading comprehension systems.
In Empirical Methods in Natural Lunguage Processing (EMNLP),201) 2017.
Robin Jia, Aditi Raghunathan, Kerem Göksel, and Percy Liang. Certified robustness to adversarial 2019.
word substitutions. arXiv preprint
Dongyeop Kang, Tushar Khot, Ashish Sabharwal, and Eduard Hovy. AdvEntuRe: Adversarial training for textual entailment with knowledge-guided examples. In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pp. 2418 2418-2428, Melbourne, Australia, July 2018. Association for Computational Linguistics. URL aclweb. org/ attpaa/ooooo/.--11220
https:// www. wwtp://wwww.wwb..........o
Guy Katz, Clark Barrett, David L 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.
Alexey Kurakin, Ian Goodfellow, and Samy Bengio. Adversarial examples in the physical world. arXiv preprint 1607.0:600.2222 2016.
Yitong Li, Trevor Cohn, and Timothy Baldwin. Robust training under linguistic adversity. In Pro- ceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 2, Short Papers. pp. 11127,2017.
Pasquale Minervini and Sebastian Riedel. Adversarially regularising neural nli models to integrate logical background knowledge. In Proceedings the 22nd Conference on Computational Natural Language Learning, pp. 65 Association for Computational I Linguisties, 2018. URL http:
//acl //aclweb. org ant log./118-yy//yale/ 1007
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for prov- ably robust neural networks. In Proceedings of the 35th International Conference on Machine Learning, volume 80, pp. 3578-3586, 2018
Pramod Kaushik Mudrakarta, Ankur Taly, Mukund Sundararajan, and Kedar Dhamdhere. Did the model understand the question? In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). pp. 1896-1906, Melbourne. Australia, July 2018. Association for Computational Linguistics. URL https://wwww aclweb. org/ Mattholoyy/P1B-11
Tong Niu and Mohit Bansal. Adversarial over-sensitivity and over-stability strategies for dialogue models. In Proceedings of the 22nd Conference on Computational Natural Language Learning, pp. 486-496, Brussels, Belgium, October 2018. Association for Computational Linguistics. doi:
111/865/////1811100 URL https::///// www ac wwwwwwwwbbb......... org/ anthology//y
Timothy Niven and Hung- Yu Kao. Probing neural network comprehension of natural language arguments. In Proceedings of the 57th Annual Meeting of the Association for Computational Lin- guistics, pp. 4658-4664, Florence, Italy, July 2019. Association for Computational Linguistics. ac
URL https: http://wwwwwlllll...
www.:w.wwwebb......m www.wwbbbrr....o wwwpbb/.ggggatooooooooooooo http//aahhooooyPP11 1459
Ankur Parikh, Oscar Täckström, Dipanjan Das, and Jakob Uszkoreit. A decomposable attention model for natural language inference. In Proceedings of the 2016 Conference on Empirical Meth- ods in Natural Language Processing, pp. 2016. doi: 10. 10.18653/v1/D16 1244, URL
Association for Computational Linguistics, wtwp://wwww....e/ttoooooooo/oo// 1144
Adam Poliak, Jason Naradowsky, Aparajita Haldar, Rachel Rudinger, and Benjamin Van Durme. Hypothesis only baselines in natural language inference. In Proceedings the Seventh Joint Con- ference on Lexical and Computational Semantics, pp. 180-191. Association for Computational Linguistics, 2018. doi: 10.11853/v1/S1.. 2023. URL http: bttp::/aclweb......///// org/anthologyy S1 818- -023
12

---

Published as a conference paper at ICLR 2020
Chongli Qin, Krishnamurthy Dvijotham, Brendan O' O'Donoguue, Rudy Bunel, Robert Stanforth, Sven Gowal, Jonathan Uesato, Grzegorz Swirszez, and Pushmeet Kohli. Verification of non- linear specifications for neural networks. CoRR, abs/1902.09592, 2019.
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Certified defenses against adversarial exam- ples. arXiv preprint
2018a.
Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness adversarial examples. In Advances in Neural Information Processing Systems, pp. 10877-10887, 2018b.
Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. "Why Should Trrust You?": Explaining the predictions of any classifier. In Knowledge Discovery and Data Mining (KDD), 2016.
Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. Anchors: High- precision model-agnostee explanations. In AAAI Conference on Artificial Intelligence (AAAI), 201 8a.
Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin. Semantically equivalent adversarial rules for debugging nlp models. In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics ( (Volume 1: Long Pupers), pp. 856-865. Association for Computational Linguistics, 2018b. URL http:/ / wwwwwb.wwbbb.................... orq/ httaaaaathooooyeoooaa
Tim Rocktäschel, Edward Grefenstette, Karl Moritz Hermann, Tomas Kocisky, and Phil Blunsom. Reasoning about entailment with neural attention. In International Conference Learning Rep- resentations (ICLR), 2016.
Ludwig Schmidt, Shibani Santurkar, Dimitris Tsipras, Kunal Talwar, and Alek- sander Madry. Adversarially robust generalization requires more data. In S. Ben- gio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (eds.), Advances in Neural Information Processing Systems 31, pp. 5014-5026. Curran Associates, Inc., 2018. 7749- adversarially cetruussttgeeeraizaaeeee ion.eraaliiattooooorreerreeeee mere-rrrr-rrss--eeee---e----e mata
URL http:://aperr..nps..cco..
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. arXiv preprint 1312v9933 2013.
James Thorne and Andreas Vlachos. Adversarial attacks against fact extraction and verification. CoRR, abss/193.00543, 2019. URL httt:://aaxxii org/ wwgg/bs////..ooo.o
05543
Jonathan Uesato, Brendan O' Donoghuee Aaron van den Oord, and Pushmeet Kohli. Adversarial risk 2018.
and the dangers of evaluating against weak attacks. arXiv preprint
Chenglong Wang, Rudy Bunel, Krishnamurthy Dvijotham, Po-Sen Huang, Edward Grefenstette, and Pushmeet Kohli. Knowing when to stop: Evaluation and verification of conformity to output- size specifications. arXiv preprini arXiv::9044 12004, 2019.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. arXiv preprint arXiv: 10829, 2018
Tsui- Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsich, Duane Boning, Inderjit S Dhillon, and Luca Daniel. Towards fast computation of certified robustness for relu networks. arXiv preprint arXiv: 1804.09699, 2018
Adina Williams, Nikita Nangia, and Samuel Bowman. A broad-coverage challenge corpus for sen- tence understanding through inference. Proceedings of the 2018 Conference of the North Amer- ican Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long Papers), pp. 1112-1122, Association for Computational Linguisties, 2018. URL http:://a web. org/ antho logy /N18 1101
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, pp. 5283-5292, 2018.
Zhengli Zhao, Dheeru Dua, and Sameer Singh. Generating natural adversarial examples. In Inter- national Conference Learning Representations (ICLR), 2018.
13

---

Published as a conference paper at ICLR 2020
A APPENDIX: HULTI-WORD DELETION BOUNDS
In this section we will elaborate on how bounds for V1 and V2 are computed the case of arbitrary muldi-word deletions.
Bounds on V1: Recall from Equation 5 that
V1 = Σ G((a:BB)) R
We can compute bounds on Vi under arbitrary multi-word deletions by bounding both a, and B;, and then propagating these bounds using IBP. The values of a, remain unchanged under deletions in the second input sequence (ā, a,), and we will thus focus deriving upper and lower bounds for B,.
To this end, recall that individual columns in B are computed as convex combination of vectors in B. That is, the tth column computed as B; Σ, b, where p(B) is the entry of ((B) position (i, The (elementwise) minimum and maximum values that B; can assume, are given by the (elementwise) minimum and maximum of single vectors by: byin mins{by}, and bmae max [by}. J. The values of B, are hence bounded elementwisely from above by the values in bmaz:
B₁
Σ by P( JED
<Eb
P(
biazz
Σ P(3
-bmar Dmaz
(16)
jED
JED
where D is an arbitrary set of indices of deleted tokens. Note that whichever token set is deleted, the (renormalised) attention weights p(B) always sum 1.
The same follows analogously for Dmin as elementwise lower bound on B
Bounds Vz: Recall from Equation that
V2 = EG(AA;b,))> - E
(17)
where g, = G(A,; b,]) for notational convenience. The function G is a dense feed-forward neu- ral network with softplus nonlinearity; consequently all values in g, are strictly positive. Since each g, has positive values, their sum will monotonically decrease summands are removed, and monotonically increase summands are added.
We consider two extreme cases of deleting word combinations: i) removing all but one word ii) removing precisely one word. These will be used to bound V2 for any other number of deleted words which lie in between these extremes.
For the case that all but one words are removed (at position r), V2 gr, and the smallest values this expression can assume (elementwise) is min,,11..../ (g.)]. This is thus a lower bound on V2 for sequences with only word, and, due to the monotonicity of va in its number of summands, also for V22 under any combination of deleted words.
For the case of deleting only single word at position r, single summand is subtracted from V2: V. = V2 gr. and this expression is bounded from above by V2 min,. {gr). Again, due to the monotonicity of when deleting more symbols, this upper bound for single-word deletions is consequently also an upper bound for any combination of more deleted words.
To summarise, V2 is bounded follows:
min {gr 1 < V2 min {gr)
(18)
r=.....
14


Reviews:
[{"review_id": "ryxiFWbHcH", "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": "-- Overall --\nThis submission tackles to verify the “under-sensitivity” problem of neural network models in the natural language inference by ensuring modes do not become more confident in the predictions when arbitrary subsets of words from the input text are deleted. The authors developed new verification approaches based on decomposable attention mechanism with interval bound propagation (IBP), which can prove the under-sensitivity issue given a model and a particular sample. The experimental results on SNLI and MNLI show that the proposed approach leads to a much improved verified accuracy.\n\n-- In general, “under-sensitivity” is a very critical problem for applying neural models in natural language understanding where powerful neural networks tend to capture spurious correlations from the biased datasets. This submission formulates “under-sensitivity” as a mathematical specification and then try to verify it with IBP verification. Although the used technique IBP is not new, it would interesting to have the verification in NLI models.\n\n-- Section 5 is a bit unclear how to compute the IBP for deleting several words, and what is the output. It would be better to have a clear example for how this was computed.\n\n-- As the author mentioned, the verification of under-sensitivity can also be done by using beam-search, although it is costly and not accurate. IBP is another more efficient option, but not the optimal neigher. Maybe consider to change the title as “efficient verification”?\n\n-- Specific Questions -- \nThe entire paper builds on decomposable attention. Is the same approach also applicable to other model types, or only single layer attention-based models? \nAlso, how this methods work for other NLI or NLU tasks?\nIn experiments, how the data augumentation penalize the model with a loss for specification violation? What does the equation look like?\nCan you explain a bit more for IBP-training? How that hinge loss applies to the objective function? Is the IBP training differentiable?\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 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": "rkxuhTae5S", "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": "This paper proposes a model to verify the robustness of NLP models (change in the original probability), more specifically DAM, in the case of word removals in the input. The idea is given the lower and upper bound on the hidden state at previous layer, compute the new bound by propagating the bounding box around the hidden state at previous layer. The upper bound at the final layer is then compared with the label probability of the original input to assess if the probability increases or not. By training model with a hinge loss based on this verification method, they show that the model becomes more robust to word removals.\n\nOverall, the paper is well written and the idea of using IBP with an attentive model seems to work empirically for SNLI datasets. But, the technical contribution feels incremental over previous approaches, especially Huang (2019). I have several questions related to some parts of the paper:\n\n- Since upper and lower bounds are also propagated, do you backpropagate the gradients via these bounds or only via the original inputs?\n- How sensitive is the label in SNLI dataset to word removal? For some label types, such as entailment, it might have less of an effect that for the others.\n- How is the accuracy distributed wrt different label types?\n- Since the accuracy of the proposed model drops the most, I am wondering how the verfied accuracy and accuracy are related during training? For example, can you show what is the verified accuracy with accuracy being close to the standard training?", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "N/A", "review_assessment:_checking_correctness_of_experiments": "I carefully checked the experiments.", "review_assessment:_checking_correctness_of_derivations_and_theory": "N/A"}, "extra_text": {}}, {"review_id": "HJlme7pccr", "reviewer": "AnonReviewer4", "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": "This work is an application of interval bound propagation on evaluating the robustness of NLI model. This work is well-motivated, assuming that the confidence of a neural model should be lower when part of the sentence is missed. However, the application of vanilla IBP is quite limited in certain model architectures. In this work, the author considers specifically the decomposable attention model, which is a very shallow network, and not a state-of-the-art model anymore. It is non-trivial to adapt the proposed method to other more advanced models, such as the ones based on the Transformer model. Hence, this work does not make enough contribution to be accepted.", "extra_scores": {"experience_assessment": "I do not know much about this area.", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory.", "review_assessment:_checking_correctness_of_experiments": "I assessed the sensibility of the experiments.", "review_assessment:_thoroughness_in_paper_reading": "I read the paper at least twice and used my best judgement in assessing the paper."}, "extra_text": {}}, {"review_id": "HJefc93Z5S", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 8, "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": "This works considers the task of Natural Language Inference (NLI).\nThe question addressed is that SOTA NLI models tend to lead to\nhigher confidence when some parts are deleted from the \"premise\".\nIt is a problem known as under-sensitivity.\nA method based on IBP is proposed to address this issue.\nThe idea of Interval Bound Propagation (IBP) is to use interval arithmetic to propagate\nintervals and bound the variation of the target based\non variation of the input. In other words, one propagates\nupper and lower interval bounds through the network.\nThe DAM model from (Parikh et al., 2016)\nis studied in particular.\n\nThe paper is well written and easy to follow.\n\nMy only concern is about the relevance of approach based on DAM when\nthere are now more accurate models for this task. The paper is however\ninteresting and addressed a relevant topic.\n\nMisc:\n- transpose should be written with $^\\top$ (not $^T$).\n\n", "extra_scores": {"experience_assessment": "I do not know much about 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": "N/A"}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper deals with the under-sensitivity problem in natural language inference tasks.  An interval bound propagation (IBP) approach is applied to predict the confidence of the model when a subsets of words from the input text are deleted.  The paper is well written and easy to follow.  The authors give detailed rebuttal and 3 of the 4 reviewers lean to accept the paper.
Decision: Accept (Poster)