Towards Trustable Explainable AI

1 Introduction

Machine Learning (ML) models are widely used in decision making procedures in many real-world applications. The fast growth, practical achievements and the overall success of modern approaches to ML [LeCun et al., 2015; Jordan and Mitchell, 2015; Mnih et al., 2015; ACM, 2018] guarantees that machine learning will prevail as a generic computing paradigm, and will find an ever growing range of practical applications, many of which will have to do with various aspects of our lives.

Unfortunately, ML models on occasions catastrophically fail [Zhou and Sun, 2019; CACM Letters to the Editor, 2019]. They can also support poor decisions due to bias (e.g. race, gender, age) in the model [Angwin et al., 2016]. Their decisions can be confusing due to brittleness [Szegedy et al., 2014; Goodfellow et al., 2015]. As a result, there is a critical need to understand the behavior of ML models, analyze the (potential) failures of the models (or the data used to train them), debug them, and possibly repair.

This has given rise to a growing interest in validating the operation of ML models [Ruan et al., 2018; Narodytska, 2018; Narodytska et al., 2018b; Katz et al., 2017] but also motivated efforts aiming at devising approaches to explainable artificial intelligence (XAI) [Ribeiro et al., 2018; Lundberg and Lee, 2017; Ignatiev et al., 2018; Narodytska et al., 2018a; Ribeiro et al., 2016; Ignatiev et al., 2019a;

Monroe, 2018]. Unfortunately, most existing approaches to explaining ML models are of heuristic nature and are logically unsound [Ignatiev et al., 2019c] - one can find counterexamples to heuristic explanations revealing their defects. This exacerbates the problem of trust in AI, as given a misbehaving ML model and an explanation that proves to be incorrect, a user may have even less trust in the ML model.

Recent work [Shih et al., 2018; Ignatiev et al., 2019a] proposed a principled approach to computing provably correct explanations (at the expected cost of lower scalability), which is fundamentally different from the heuristic methods. The approach hinges on the use of logic and operates with efficient prime implicant computation for logical representations of the decision function associated with an ML prediction. The approach can be applied directly to the explanation computation but also to validate heuristic explanations [Ignatiev et al., 2019c]. Finally, it has been recently used to establish a rigorous relationship of global explanations and a generalization of adversarial examples, thus, making a bridge between XAI and ML model verification [Ignatiev et al., 2019b]. This paper provides a summary of ongoing efforts to develop formal reasoning approaches for explaining ML models. The reader is referred to the work referenced for further details.

2 Explainable AI and Heuristic Status Quo

Explainable AI is an emerging field, with a growing number of areas of research [Weld and Bansal, 2019]. We focus on explaining predictions of ML models and use the notation of prior work [Shih et al., 2018; Ignatiev et al., 2019a; Ignatiev et al., 2019c; Narodytska et al., 2019; Ignatiev et al., 2019b] 1 . Given an instance and its associated prediction, an explanation is a set of feature values, with a suitable set of properties. An ML model can be viewed as a function M : F → K, mapping inputs (i.e. the feature values

1 Here, a set of features F = {f1, . . . , fL} is assumed. Each feature fi is categorical (or ordinal), with values taken from some set Di. (The work can be extended to the case of Di ⊆ R.) An instance I ∈ F, F = D1 ×. . .×DL, is a vector of feature values. A classification problem is assumed, with a set of classes K = {κ1, . . . , κM}. A prediction π ∈ K is associated with each instance I ∈ F. We consider an ML model M, represented by a finite set of first-order logic (FOL) sentences M. (Where viable, alternative representations for Mcan be considered, e.g. fragments of FOL, (mixed-)integer linear programming, constraint language(s), etc.)

F) to outputs (i.e. the classes of the classification problem, K). Following [Shih et al., 2018; Ignatiev et al., 2019a], we target computing rigorous explanations of ML predictions. Given some instance I ∈ F and prediction π, a minimal rigorous (or model-precise) explanation E is a prime implicant of the Boolean function M(I) = π. We can also consider minimum explanations, in which case the goal is to compute smallest-size prime implicants.

To illustrate past work on computing explanations, we consider the well-known Zoo dataset 2 , generate the boosted tree model shown in Figure 1, and use the following example instance (adapted from [Ignatiev et al., 2019c]):

The overwhelming majority of work on computing explanations has been on exploiting heuristic approaches, which often offer guarantees of quality with respect to a given instance. Concrete examples include [Baehrens et al., 2010; Ribeiro et al., 2016; Lundberg and Lee, 2017; Ribeiro et al., 2018; Li et al., 2018] among others 3 . LIME [Ribeiro et al., 2016], Anchor [Ribeiro et al., 2018], SHAP [Lundberg and Lee, 2017] represent three alternative approaches for local exploring the feature space with respect to a given instance. As a result, computed explanations are referred to as local (or instance-dependent).

Despite the prevalence of solutions for computing local explanations heuristically, such explanations are modelagnostic and thus offer no guarantees wrt. the underlying ML model nor they provide any guarantees of minimality. For the running example shown earlier, Anchor computes the following explanation:

As Zoo is a very simple dataset, it suffices to analyze the instances in the original dataset to show that the explanation does not hold in general. Concretely, there is at least another instance (in fact, we found a large number of similar examples) for which the Anchor explanation also applies, but for which the boosted tree predicts a different class (essentially meaning that the provided explanation is incorrect):

IF (animal name = toad) ∧ ¬hair ∧ ¬feathers ∧ eggs ∧ ¬milk ∧ ¬airborne ∧ ¬aquatic ∧ ¬predator ∧ ¬toothed ∧ backbone ∧ breathes ∧ ¬venomous ∧ ¬fins ∧ (legs = 4) ∧ ¬tail ∧ ¬domestic ∧ ¬catsize THEN (class = amphibian)

Although one can argue that local explanations are meant to be local to a concrete instance, it is questionable how useful such heuristic explanations are for a human decision maker.

3 Trustable Explanations

It is not surprising that heuristic explanations may be incorrect as, being model-agnostic, they are unable to catch all the properties of the underlying ML model. As a result, it is debatable if (and to what extent) heuristic explanations can be trusted. In contrast with heuristic explanations, rigorous logic-based explanations correspond to prime implicants of the Boolean function associated with predicting the class of the target instance, and so hold for any point in feature space. In other words, rigorous explanations are provably correct for the entire feature space, which makes them trustable.

Two lines of work on computing rigorous explanations have been proposed in recent years. One is based on knowledge compilation [Shih et al., 2018] whilst the other applies abductive reasoning [Ignatiev et al., 2019a] detailed below. Knowledge compilation aims at finding canonical representations of functions, which in turn enable efficient algorithms for answering queries that would be too inefficient on the original formula. Although effective once the target representation is obtained, the compilation process itself is worst-case exponential in time and space, which may represent a significant obstacle. Also, the use of compilation for computing explanations requires developing dedicated algorithms for each ML model.

3.1 Trustable Explanations with Abduction

Rigorous explanations can be obtained by abductive reasoning [Ignatiev et al., 2016; Ignatiev et al., 2019a], without the explicit need of computing a canonical representation of the function associated with the ML model. An advantage of this approach is that the common limitations regarding the size of the representation do not apply. A drawback is that an explanation needs to be computed for each instance, whereas with compilation-based approaches explanations for any instance become available as soon as the target representation is obtained. In practice, the use of abductive reasoning requires a logic-based representation to be devised for a given ML model. Earlier work considered neural networks [Ignatiev et al., 2019a] and boosted trees [Ignatiev et al., 2019c].

Given a dataset, we can use any existing approach for computing an ML model. For the boosted tree of Figure 1, one can devise an encoding using ILP or SMT [Ignatiev et al., 2019c]. Given the running example, we can compute a prime implicant which, given the model subject to the prediction, entails the prediction. In this case, using abductive reasoning [Ignatiev et al., 2019a; Ignatiev et al., 2019c], a possible explanation is:

This rigorous explanation guarantees that, as long as the six indicated literals take the value shown, the prediction will be the same, independently of the value of any of the other features. More importantly, the use of SMT or SAT reasoners enables the generation of a proof (or proof trace) for each computed explanation, which can be independently validated. This offers another degree of trust in computed explanations. Furthermore, there is no conceptual obstacle to extracting proofs or proof traces from other types of reasoners, e.g. ILP.

Recent work [Ignatiev et al., 2019a] has shown that the use of abductive reasoning for computing explanations can analyze neural networks of modest size. In contrast, for boosted trees, abductive reasoning can be applied to trees of the sizes of practical interest [Ignatiev et al., 2019c].

4 Assessing and Repairing Heuristic Methods

The observations above raise concerns regarding the quality of heuristic explanations computed by approaches such as LIME [Ribeiro et al., 2016], SHAP [Lundberg and Lee, 2017], or Anchor [Ribeiro et al., 2018]. This section outlines recent results on assessing the quality of heuristic explanations. One validates them by abductive reasoning [Ignatiev et al., 2019c], whereas the other exploits recent work on approximate model counting [Narodytska et al., 2019].

4.1 Validating Heuristic Explanations

By applying formal reasoning about the logic-based representation of a classifier, one can check whether or not an explanation holds in the entire instance space, i.e. there exist counterexamples [Ignatiev et al., 2019c]. Such reasoning, thus, represents a principled approach for assessing validity of heuristic explanations. Furthermore, in case the explanation is invalid, one can make an attempt to repair it using a series of reasoning oracles calls. Also, as heuristic approaches like LIME, Anchor, and SHAP do not guarantee minimality of the explanation produced, one can try to reduce it further in case it is valid. A possible setup for such explanation validation procedure is shown in Figure 2. Given an explanation, its validity is checked in the entire instance space. If the explanation is invalid, it is reported to be incorrect and can be repaired. Otherwise, the explanation is proved to be valid and an attempt to reduce it is made. If the attempt succeeds, the explanation is deemed redundant. Otherwise, the explanation is proved to be correct and minimal.

Table 1 summarizes the experiment detailed in [Ignatiev et al., 2019c], which given a trained boosted tree computes a heuristic explanation for each unique instance of an input dataset, either with LIME, Anchor, or SHAP and assesses the explanation's correctness following the setup of Figure 2. Five publicly available datasets are considered in the experiment. Three of them were studied in [Ribeiro et al., 2018] to illustrate the advantage of Anchor over LIME, including adult, lending, and recidivism. Two more datasets (compas and german) were previously studied in the context of algorithmic fairness (e.g. see [Angwin et al., 2016]).

As can be observed, most explanations computed by LIME, Anchor, and SHAP are inadequate, from the global perspective. Observe that for the 4 out of 5 datasets the explanations of all three explainers are mostly incorrect. As an example, for recidivism and german more than 99% of Anchor's explanations are invalid. Similar results hold for LIME (SHAP, resp.), i.e. 94.1% and 85.3% (85.9% and 63.0%) explanations for recidivism and german are incorrect. Also note that the number of redundant explanations is usually lower, with the exception of SHAP. Overall and with the exception of lending, the number of correct explanations does not go beyond 17.9% for Anchor, 30.8% for LIME, and 19.1% for SHAP and usually constitutes just a few percent.

4.2 Evaluating Quality of Heuristic Explanations

Earlier work [Narodytska et al., 2019] proposed a generic strategy to assess the quality of heuristic explanations using approximate model counting [Soos and Meel, 2019]. Here, we overview the quality assessment results for Anchor applied to binarized neural networks [Hubara et al., 2016; Narodytska et al., 2018b]. We considered the three above datasets: adult, lending, and recidivism. Anchor's precision estimate used is defined in [Ribeiro et al., 2018], as a quality metric. To perform model counting, we used the approximate model counting solver ApproxMC3 with the standard tolerance and confidence (ε = 0.8 and δ = 0.2) [Soos and Meel, 2019]. Two sets of experiments were performed: (1) constrained and (2) unconstrained - depending on whether or not the instance space was restricted to be a local neighborhood of a given instance. We worked with instances for which Anchor's precision estimates were around 0.99. Table 2 summarizes our results. Note that the quality of Anchor's explanations can vary wildly, indicating that for some datasets Anchor's explanations are fairly accurate, but in some other cases they can be quite inaccurate. For example, observe that Anchor's estimates of the precision metric are good for the lending dataset. On average, the discrepancy between Anchor's estimates and our assessment was 0.1 for this set. In contrast, the average discrepancy was high in the adult dataset, 0.25. Note that in our experiments, ApproxMC3 had a significant theoretical error bound on the estimate we produce. Namely, we could be up to 80% off the true solution count in the worst case. Theoretically, our framework allows us to obtain an estimate with much tighter theoretical guarantees but computing these estimates is computationally expensive for the benchmarks considered. However, studies have reported that the tolerance observed in the experiments is far better than the theoretical guarantee [Soos and Meel, 2019].

The negative results summarized in this section assume that, in order to be trustable, explanations are to be meaningful over the entire feature space. This is what rigorous explanations offer. If for some reason the entire feature space is not relevant, the computation of rigorous explanations can also take this information into account.

5 Relating XAI andMLModel Verification

Adversarial examples (AE's) [Goodfellow et al., 2015] illustrate the brittleness of machine learning (ML) models, and have been the subject of growing interest in recent years. Over the last few years, a number of works realized the existence of some connection between AE's and XP's [Tao et al., 2018; Chalasani et al., 2018]. Recent work [Ignatiev et al., 2019b] exploited global rigorous explanations, introduced the concept of counterexamples, tightly related with adversarial examples, and then showed a minimal hitting set duality relationship between explanations and counterexamples, and in the process proposed approaches for computing adversarial examples from explanations and vice-versa. These recent results build on work from the 80s and 90s, first on modelbased diagnosis [Reiter, 1987], and then on computing primes of (Boolean) functions [Rymon, 1994], but also suggest that additional connections between analysis of ML models and other areas of AI can be established.

6 Conclusions

This paper overviews recent work on exploiting the logicbased approach for computing rigorous explanations to ML predictions. Moreover, the paper argues that rigorous explanations are trustable, in clear contrast to heuristic explanations, which is confirmed by the experimental results casting doubt on the quality of the heuristic explanations of [Ribeiro et al., 2016; Lundberg and Lee, 2017; Ribeiro et al., 2018]. We conjecture that potential incorrectness is intrinsic to approaches that compute model-agnostic heuristic explanations. Finally, the paper summarizes recent results relating global rigorous explanations with adversarial examples. These results build on earlier seminal work on relating conflicts and diagnoses in model-based diagnosis through subset-minimal hitting sets [Reiter, 1987], but also on finding prime implicants and implicates [Rymon, 1994].

Acknowledgements

The author thanks his colleagues Joao Marques-Silva and Nina Narodytska, who have been taking active part in the research on rigorous logic-based XAI and coauthoring the works, which this paper extensively builds on. Without them this work would be impossible.