On Guaranteed Optimal Robust Explanations for NLP Models

1 Introduction

The increasing prevalence of deep learning models in realworld decision-making systems has made AI explainability a central problem, as we seek to complement such highlyaccurate but opaque models with comprehensible explanations as to why the model produced a particular prediction [Samek et al., 2017; Ribeiro et al., 2016; Zhang et al., 2019; Liu et al., 2018; Letham et al., 2015]. Amongst existing techniques, local explanations explain the individual prediction in terms of a subset of the input features that justify the prediction. State-of-the-art explainers such as LIME and Anchors [Ribeiro et al., 2016; Ribeiro et al., 2018] use heuristics to obtain short explanations, which may generalise better beyond the given input and are more easily interpretable to human experts, but lack robustness to adversarial perturbations. The abduction-based method of [Ignatiev et al., 2019b], on the other hand, ensures minimality and robustness of the prediction by requiring its invariance w.r.t. any perturbation of the left-out features, meaning that the explanation is sufficient to imply the prediction. However, since perturbations are potentially unbounded, this notion of robustness may not be appropriate for certain applications.

∗ First Author, contact at emanuele.la.malfa@cs.ox.ac.uk

1 Code available at https://github.com/EmanueleLM/OREs

In this paper, we focus on natural language processing (NLP) neural network models and, working in the embedding space with words as features, introduce optimal robust explanations (OREs). OREs are provably guaranteed to be both robust, in the sense that the prediction is invariant for any (reasonable) replacement of the features outside the explanation, and minimal for a given user defined cost function, such as the length of the explanation. Our core idea shares similarities with abduction-based explanations (ABE) of [Ignatiev et al., 2019b], but is better suited to NLP models, where the unbounded nature of ABE perturbations may result in trivial explanations equal to the entire input. We show that OREs can be formulated as a particular kind of ABE or, equivalently, minimal satisfying assignment (MSA). We develop two methods to compute OREs by extending existing algorithms for ABEs and MSAs [Ignatiev et al., 2019b; Dillig et al., 2012]. In particular, we incorporate state-ofthe-art robustness verification methods [Katz et al., 2019; Wang et al., 2018] to solve entailment/robustness queries and improve convergence by including sparse adversarial attacks and search tree reductions. By adding suitable constraints, we show that our approach allows one to detect biased decisions [Darwiche and Hirth, 2020] and enhance heuristic explainers with robustness guarantees [Ignatiev et al., 2019d].

To the best of our knowledge, this is the first method to derive local explanations for NLP models with provable robustness and optimality guarantees. We empirically demonstrate that our approach can provide useful explanations for nontrivial fully-connected and convolutional networks on three widely used sentiment analysis benchmarks (SST, Twitter and IMDB). We compare OREs with the popular Anchors method, showing that Anchors often lack prediction robustness in our benchmarks, and demonstrate the usefulness of our framework on model debugging, bias evaluation, and repair of non-formal explainers like Anchors.

2 RelatedWork

Interpretability of machine learning models is receiving increasing attention [Chakraborty et al., 2017]. Existing methods broadly fall in two categories: explanations via globally interpretable models (e.g. [Wang and Rudin, 2015; Zhang et al., 2018]), and local explanations for a given input and prediction (to which our work belongs). Two prominent examples of the latter category are LIME [Ribeiro et al., 2016], which learns a linear model around the neighbourhood of an input using random local perturbations, and Anchors [Ribeiro et al., 2018] (introduced in Section 3). These methods, however, do not consider robustness, making them fragile to adversarial attacks and thus insufficient to imply the prediction. Repair of non-formal explainers has been studied in [Ignatiev et al., 2019d] but only for boosted trees predictors. [Narodytska et al., 2019] assesses the quality of Anchors' explanations by encoding the model and explanation as a propositional formula. The explanation quality is then determined using model counting, but for binarised neural networks only. Other works that focus on binarised neural networks, Boolean classifiers or similar representations include [Shi et al., 2020; Darwiche and Hirth, 2020; Darwiche, 2020]. Methods tailored to (locally) explaining NLP model decisions for a given input include [Li et al., 2015; Singh et al., 2018]. These identify input features, or clusters of input features, that most contribute to the prediction, using saliency and agglomerative contextual decomposition respectively. Layer-wise relevance propagation [Bach et al., 2015] is also popular for NLP explanations, and is used in [Arras et al., 2016; Arras et al., 2017; Ding et al., 2017]. Similarly to the above, these methods do not consider robustness. Robustness of neural network NLP models to adversarial examples has been studied in [Huang et al., 2019; Jia et al., 2019; La Malfa et al., 2020]. We note that robustness verification is a different (and arguably simpler) problem from deriving a robust explanation, as the latter requires performing multiple robustness verification queries (see Section 4). Existing neural network verification approaches include symbolic (SMT) [Katz et al., 2019], relaxation [Ko et al., 2019; Wang et al., 2018], and global optimisation [Ruan et al., 2018]. Research utilising hitting sets can be seen in [Ignatiev et al., 2019c], which relates explanations and adversarial examples through a generalised form of hitting set duality, and [Ignatiev et al., 2019a], which works on improving modelbased diagnoses by using an algorithm based on hitting sets to filter out non-subset-minimal sets of diagnoses.

3 Optimal Robust Explanations for NLP

Preliminaries. We consider a standard NLP classification task where we classify some given input text t into a plausible class y from a finite set Y. We assume that t is a fixed length sequence of words (i.e., features) l, t = (w1, . . . ,wl), where wi ∈ W with W being a finite vocabulary (possibly including padding). Text inputs are encoded using a continuous word embedding E : W → Rd , where d is the size of the embedding [Mikolov et al., 2013]. Thus, given a text t = (w1, . . . ,wl), we define the embedding E(t) of t as the sequence x = (xw1 , . . . , xwl ) ∈ Rl·d , where xwi = E(wi). We denote with WE ⊆ W the vocabulary used to train E. We consider embedding vectors trained from scratch on the sentiment task, a technique that enforces words that are positively correlated to each of the output classes to be gathered closer in the embedding space [Baroni et al., 2014], which is considered a good proxy for semantic similarity with respect to the target task compared to count-based embeddings [Alzantot et al., 2018]. For classification we consider a neural network M : Rl·d → Y that operates on the text embedding.

Robust Explanations. In this paper, we seek to provide local explanations for the predictions of a neural network NLP model. For a text embedding x = E(t) and a prediction M(x), a local explanation E is a subset of the features of t, i.e., E ⊆ F where F = {w1, . . . , wl}, that is sufficient to imply the prediction. We focus on deriving robust explanations, i.e., on extracting a subset E of the text features F which ensure that the neural network prediction remains invariant for any perturbation of the other features F \ E. Thus, the features in a robust explanation are sufficient to imply the prediction that we aim to explain, a clearly desirable feature for a local explanation. In particular, we focus on explanations that are robust w.r.t. bounded perturbations in the embedding space of the input text. We extract word-level explanations by means of word embeddings: we note that OREs work, without further extensions, with diverse representations (e.g., sentence-level, characters-level, etc.). For a word w ∈ W, with embedding xw = E(w) we denote with B(w) ⊆ Rd a generic set of word-level perturbations. We consider the following kinds of perturbation sets, depicted also in Fig. 1.

ϵ-ball: B(w) = {x ∈ Rd | ‖x - xw‖p ≤ ϵ}, for some ϵ > 0 and p > 0. This is a standard measure of local robustness in computer vision, where ϵ-variations are interpreted as manipulations of the pixel intensity of an image. It has also been adopted in early NLP robustness works [Miyato et al., 2016], but then replaced with better representations based on actual word replacements and their embeddings, see below.

k-NN box closure: B(w) = BB(E(NNk(w))), where BB(X) is the minimum bounding box for set X; for a set W ′ ⊆ W, E(W ′ ) = ⋃w′∈W ′{E(w′ )}; and NNk(w) is the set of the k closest words to w in the embedding space, i.e., words w′ with smallest d(xw, E(w′ )), where d is a valid notion of distance between embedded vectors, such as p-norms or cosine similarity, even though the box closure can be calculated for any set of embedded words. This provides an over-approximation of the k-NN convex closure, for which constraint propagation (and thus robustness checking) is more efficient [Jia et al., 2019; Huang et al., 2019].

For some word-level perturbation B, set of features E ⊆ F, and input text t with embedding (x1, . . . , xl), we denote with BE(t) the set of text-level perturbations obtained from t by keeping constant the features in E and perturbing the others according to B:

A robust explanation E ⊆ F ensures prediction invariance for any point in BE(t), i.e., any perturbation (within B) of the features in F \ E.

Def. 1 (Robust Explanation). For a text t = (w1, . . . ,wl) with embedding x = E(t), word-level perturbation B, and classifier M, a subset E ⊆ F of the features of t is a robust explanation iff

We denote (2) with predicate RobM,x(E).

Optimal Robust Explanations (OREs). While robustness is a desirable property, it is not enough alone to produce useful explanations. Indeed, we can see that an explanation E including all the features, i.e., E = F, trivially satisfies Definition 1. Typically, one seeks short explanations, because these can generalise to several instances beyond the input x and are easier for human decision makers to interpret. We thus introduce optimal robust explanations (OREs), that is, explanations that are both robust and optimal w.r.t. an arbitrary cost function that assign a penalty to each word.

Def. 2 (Optimal Robust Explanation). Given a cost function C : W → R+, and for t = (w1, . . . ,wl), x, B, and M as in Def. 1, a subset E∗ ⊆ F of the features of t is an ORE iff

Note that (3) is always feasible, because its feasible set always includes at least the trivial explanation E = F. A special case of our OREs is when C is uniform (it assigns the same cost to all words in t), in which case E∗ is (one of) the robust explanations of smallest size, i.e., with the least number of words.

Relation with Abductive Explanations. Our OREs have similarities with the abduction-based explanations (ABEs) of [Ignatiev et al., 2019b] in that they also derive minimalcost explanations with robustness guarantees. For an input text t = (w1, . . . ,wl), let C = ∧li=1 χi = xwi be the cube representing the embedding of t, where χi is a variable denoting the i-th feature of x. Let N represent the logical encoding of the classifier M, and ˆ y be the formula representing the output of N given χ1, . . . , χl.

Def. 3 ([Ignatiev et al., 2019b]). An abduction-based explanation (ABE) is a minimal cost subset C ∗ of C such that C ∗ ∧N |= ˆ y.

Note that the above entailment is equivalently expressed as C ∗ |= (N → ˆ y). Let B = ∧li=1 χi ∈ B(wi) be the constraints encoding our perturbation space. Then, the following proposition shows that OREs can be defined in a similar abductive fashion and also in terms of minimum satisfying assignments (MSAs) [Dillig et al., 2012]. In this way, we can derive OREs via analogous algorithms to those used for ABEs [2019b] and MSAs [Dillig et al., 2012], as explained in Section 4. Moreover, we find that every ORE can be formulated as a prime implicant [Ignatiev et al., 2019b], a property that connects our OREs with the notion of sufficient reason introduced in [Darwiche and Hirth, 2020].

Prop. 1. Let E∗ be an ORE and C ∗ its constraint encoding. Define φ ≡ (B ∧ N ) → ˆ y. Then, all the following definitions apply to C ∗ :

1. C ∗ is a minimal cost subset of C such that C ∗ |= φ.
2. C ∗ is a minimum satisfying assignment for φ.
3. C ∗ is a prime implicant of φ.

The key difference with ABEs is that our OREs are robust to bounded perturbations of the excluded features, while ABEs must be robust to any possible perturbation. This is an important difference because it is hard (often impossible) to guarantee prediction invariance w.r.t. the entire input space when this space is continuous and high-dimensional, like in our NLP embeddings. In other words, if for our NLP tasks we allowed any word-level perturbation as in ABEs, in most cases the resulting OREs will be of the trivial kind, E∗ = F (or C ∗ = C), and thus of little use. For example, if we consider ϵ-ball perturbations and the review "the gorgeously elaborate continuation of the lord of the rings", the resulting smallest-size explanation is of the trivial kind (it contains the whole review) already at ϵ = 0.1.

Exclude and include constraints. We further consider OREs E∗ derived under constraints that enforce specific features F ′ to be included/excluded from the explanation:

where φ(E) is one of F ′ ∩ E = ∅ (exclude) and F ′ ⊆ E (include). Note that adding include constraints doesn't affect the feasibility of our problem, because the feasible region of (4) always contains at least the explanation E∗ ∪F ′ , where E∗ is a solution of (3) and F ′ are the features to include. See Def. 1. Conversely, exclude constraints might make the problem infeasible when the features in F ′ don't admit perturbations, i.e., they are necessary for the prediction, and thus cannot be excluded. Such constraints can be easily accommodated by any solution algorithm for non-constrained OREs: for include ones, it is sufficient to restrict the feasible set of explanations to the supersets of F ′ ; for exclude constraints, we can manipulate the cost function so as to make any explanation with features in F ′ strictly sub-optimal w.r.t. explanations without, that is, we use cost C ′ such that ∀w∈F\F ′C ′ (w) = C(w) and ∀w′∈F ′C ′ (w′ ) > ∑w∈F\F ′ C(w). The ORE obtained under cost C ′ might still include features from F ′ , which implies that (4) is infeasible (i.e., no robust explanation without elements of F ′ exists).

2 For this and any subsequent reference to the supplement/appendix, please refer to the full version of the paper on the arXiv.

Constrained OREs enable two crucial use cases: detecting biased decisions, and enhancing non-formal explainability frameworks.

Detecting bias. Following [Darwiche and Hirth, 2020], we deem a classifier decision biased if it depends on protected features, i.e., a set of input words that should not affect the decision (e.g., a movie review affected by the director's name). In particular, a decision M(x) is biased if we can find, within a given set of text-level perturbations, an input x′ that agrees with x on all but protected features and such that M(x) ̸= M(x′ ).

Def. 4. For classifierM, text t with features F, protected features F ′ and embedding x = E(t), decision M(x) is biased w.r.t. some word-level perturbation B, if

The proposition below allows us to use exclude constraints to detect bias.

Prop. 2. For M, t, F, F ′ , x and B as per Def. 4, decision M(x) is biased iff (4) is infeasible under F ′ ∩E = ∅.

Enhancing non-formal explainers. The local explanations produced by heuristic approaches like LIME or Anchors do not enjoy the same robustness/invariance guarantees of our OREs. We can use our approach to minimally extend (w.r.t. the chosen cost function) any non-robust local explanation F ′ in order to make it robust, by solving (4) under the include constraint F ′ ⊆ E. In particular, with a uniform C, our approach would identify the smallest set of extra words that make F ′ robust. Being minimal/smallest, such an extension retains to a large extent the original explainability properties.

Relation with Anchors. Anchors [Ribeiro et al., 2018] are a state-of-the-art method for ML explanations. Given a perturbation distribution D, classifier M and input x, an anchor A is a predicate over the input features such that A(x) holds and A has high precision and coverage, defined next.

In other words, prec(A) is the probability that the prediction is invariant for any perturbation x′ to which explanation A applies. In this sense, precision can be intended as a robustness probability. cov(A) is the probability that explanation A applies to a perturbation. To discuss the relation between Anchors and OREs, for an input text t, consider an arbitrary distribution D with support in B∅(t) (the set of all possible text-level perturbations), see (1); and consider anchors A defined as subsets E of the input features F, i.e., AE(x) = ∧w∈E xw = E(w). Then, our OREs enjoy the following properties.

Prop. 3. If E is a robust explanation, then prec(AE) = 1.

Note that when D is continuous, cov(AE) is always zero unless E = ∅, in which case cov(A∅) = 1 (as A∅ = true). Indeed, for E ̸= ∅, the set {x′ | AE(x′ )} has |E| fewer degrees of freedom than the support of D, and thus has both measure and coverage equal to zero. We thus illustrate the next property assuming that D is discrete (when D is continuous, the following still applies to any empirical approximation of D).

The above proposition suggests that using a uniform C, i.e., minimizing the explanation's length, is a sensible strategy to obtain high-coverage OREs.

4 Solution Algorithms

We present two solution algorithms to derive OREs, respectively based on the hitting-set (HS) paradigm of [Ignatiev et al., 2019b] and the MSA algorithm of [Dillig et al., 2012]. Albeit different, both algorithms rely on repeated entailment/robustness checks B∧E∧N |= ˆ y for a candidate explanation E ⊂ C. For this check, we employ two state-ofthe-art neural network verification tools, Marabou [Katz et al., 2019] and Neurify [Wang et al., 2018]: they both give provably correct answers and, when the entailment is not satisfied, produce a counter-example x′ ∈ BE(t), i.e., a perturbation that agrees with E and such that B ∧ C ′ ∧ N ̸|= ˆ y, where C ′ is the cube representing x′ . We now briefly outline the two algorithms. A more detailed discussion (including the pseudo-code) is available in the supplement.

Minimum Hitting Set. For a counterexample C ′ , let I ′ be the set of feature variables where C ′ does not agree with C (the cube representing the input). Then, every explanation E that satisfies the entailment must hit all such sets I ′ built for any counter-examples C ′ [Ignatiev et al., 2016]. Thus, the HS paradigm iteratively checks candidates E built by selecting the subset of C whose variables form a minimum HS (w.r.t. cost C) of said I ′ s. However, we found that this method often struggles to converge for our NLP models, especially with large perturbations spaces (i.e., large ϵ or k). We solved this problem by extending the HS approach with a sub-routine that generates batches of sparse adversarial attacks for the input C. This has a two-fold benefit: 1) we reduce the number of entailment queries required to produce counter-examples, and 2) sparsity results in small I ′ sets, which further improves convergence.

Minimum Satisfying Assignment. This algorithm exploits the duality between MSAs and maximum universal subsets (MUSs): for cost C and formula φ ≡ (B ∧N) → ˆ y, an MUS X is a set of variables with maximum C such that ∀X.φ, which implies that C \ X is an MSA for φ [Dillig et al., 2012] and, in turn, an ORE. Thus, the algorithm of [Dillig et al., 2012] focuses on deriving an MUS, and it does so in a recursive branch-and-bound manner, where each branch adds a feature to the candidate MUS. Such an algorithm is exponential in the worst-case, but we mitigated this by selecting a good ordering for feature exploration and performing entailment checks to rule out features that cannot be in the MUS (thus reducing the search tree).

5 Experimental Results

Settings. We have trained fully connected (FC) and convolutional neural networks (CNN) models on sentiment analysis datasets that differ in the input length and difficulty of the learning task 3 . We considered 3 well-established benchmarks for sentiment analysis, namely SST [Socher et al., 2013], Twitter [Go et al., 2009] and IMDB [Maas et al., 2011] datasets. From these, we have chosen 40 representative input texts, balancing positive and negative examples. Embeddings are pre-trained on the same datasets used for classification [Chollet and others, 2018]. Both the HS and MSA algorithms have been implemented in Python and use Marabou [Katz et al., 2019] and Neurify [Wang et al., 2018] to answer robustness queries. Marabou is fast at verifying ReLU FC networks, but it becomes memory intensive with CNNs. On the other hand, the symbolic interval analysis of Neurify is more efficient for CNNs. A downside of Neurify is that it is less flexible in the constraint definition (inputs have to be represented as squared bi-dimensional grids, thus posing problems for NLP inputs which are usually specified as 3-d tensors). In the experiments below, we opted for the kNNbox perturbation space, as we found that the k parameter was easier to interpret and tune than the ϵ parameter for the ϵ-ball space, and improved verification time. Further details on the experimental settings, including a selection of ϵ-ball results, are given in the supplement.

3 Experiments were parallelized on a server with two 24-core Intel Xenon 6252 processors and 256GB of RAM, but each instance is single-threaded and can be executed on a low-end laptop.

Effect of classifier's accuracy and robustness. We find that our approach generally results in meaningful and compact explanations for NLP. In Figure 2, we show a few OREs extracted for negative and positive texts, where the returned OREs are both concise and semantically consistent with the predicted sentiment. However, the quality of our OREs depends on that of the underlying classifier. Indeed, enhanced models with better accuracy and/or trained on longer inputs tend to produce higher quality OREs. We show this in Figures 4, 3 and 5, where we observe that enhanced models tend to result in more semantically consistent explanations. For lower-quality models, some OREs include seemingly irrelevant terms (e.g., "film", "and"), thus exhibiting shortcomings of the classifier.

Detecting biases. As per Prop. 2, we applied exclude constraints to detect biased decisions. In Figure 6, we provide a few example instances exhibiting such a bias, i.e., where any robust explanation contains at least one protected feature. These OREs include proper names that shouldn't constitute a sufficient reason for the model's classification. When we try to exclude proper names, no robust explanation exists, indicating that a decision bias exists.

Debugging prediction errors. An important use-case for OREs is when a model commits a misclassification. Misclassifications in sentiment analysis tasks usually depend on over-sensitivity of the model to polarized terms. In this sense, knowing a minimal, sufficient reason behind the model's prediction can be useful to debug it. As shown in the first example in Figure 7, the model cannot recognize the double negation constituted by the terms not and dreadful as a syntax construct, hence it exploits the negation term not to classify the review as negative.

Comparison to Anchors. We evaluate the robustness of Anchors for FC and CNN models on the SST and Twitter datasets: accuracies are 0.89 for FC+SST, 0.82 for FC+Twitter, 0.89 for CNN+SST, and 0.77 for CNN+Twitter. To compute robustness, we assume a kNN-box perturbation space B with k = 15 for FC and k = 25 for CNN models. To extract Anchors, we set D to the standard perturbation distribution of [Ribeiro et al., 2018], defined by a set of contextwise perturbations generated by a powerful language model. Thus defined Bs are small compared to the support of D, and so one would expect high-precision Anchors to be relatively robust w.r.t. said Bs. On the contrary, the Anchors extracted for the FC models attain an average precision of 0.996 on SST and 0.975 on Twitter, but only 12.5% of them are robust for the SST case and 7.5% for Twitter. With CNN models, high-quality Anchors are even more brittle: 0% of Anchors are robust on SST reviews and 5.4% on Twitter, despite an average precision of 0.995 and 0.971, respectively.

We remark, however, that Anchors are not designed to provide such robustness guarantees. Our approach becomes useful in this context, because it can minimally extend any local explanation to make it robust, by using include constraints as explained in Section 3. In Figure 8 we show a few examples of how, starting from non-robust Anchors explanations, our algorithm can find the minimum number of words to make them provably robust.

6 Conclusions

We have introduced optimal robust explanations (OREs) and applied them to enhance interpretability of NLP models. OREs provide concise and sufficient reasons for a particular prediction, as they are guaranteed to be both minimal w.r.t. a given cost function and robust, in that the prediction is invariant for any bounded replacement of the left-out features. We have presented two solution algorithms that build on the relation between our OREs, abduction-based explanations and minimum satisfying assignments. We have demonstrated the usefulness of our approach on widely-adopted sentiment analysis tasks, providing explanations for neural network models beyond reach for existing formal explainers. Detecting biased decisions, debugging misclassifications, and repairing non-robust explanations are some of key use cases that our OREs enable. Future research plans include exploring more general classes of perturbations beyond the embedding space.

Acknowledgements

This project has received funding from the European Research Council (ERC) under the European Union's Horizon 2020 research and innovation programme (FUN2MODEL, grant agreement No. 834115) and the EPSRC Programme Grant on Mobile Autonomy (EP/M019918/1).