Towards Rigorous Explainability by Feature Attribution Olivier Létoffé1[0009−0001−0035−0444] , Xuanxiang Huang2[0000−0002−3722−7191] , and Joao Marques-Silva3[0000−0002−6632−3086] IRIT, University of Toulouse France [email protected] 2 Nanyang Technological University, Singapore [email protected] 3 ICREA & Univ. Lleida, Spain [email protected]
arXiv:2604.15898v1 [cs.AI] 17 Apr 2026
1
Abstract. For around a decade, non-symbolic methods have been the option of choice when explaining complex machine learning (ML) models. Unfortunately, such methods lack rigor and can mislead human decisionmakers. In high-stakes uses of ML, the lack of rigor is especially problematic. One prime example of provable lack of rigor is the adoption of Shapley values in explainable artificial intelligence (XAI), with the tool SHAP being a ubiquitous example. This paper overviews the ongoing efforts towards using rigorous symbolic methods of XAI as an alternative to non-rigorous non-symbolic approaches, concretely for assigning relative feature importance. Keywords: Formal Methods · Explainable AI · Shapley values.
1
Overview
The remarkable advances in machine learning (ML) are not without shortcomings. Among these, lack of interpretability is paramount. Motivated by the complexity of ML models, human decision makers are often unable to understand the rationale for the predictions made. Thus, one key goal of eXplainable Artificial Intelligence (XAI) is to help human decision makers in fathoming the predictions of ML models. The explanation of ML models can be broadly organized into explanations by feature selection and those by feature attribution [54]. Explanations by feature selection can be interpreted as answering a Why? question, i.e. if the selected features take their assigned values, then the prediction is the one we want to explain. In contrast, feature attribution aims to assign a value to each feature, representing the relative importance of the feature for the prediction. The best-known method of explainability by feature attribution is the tool SHAP [43], which finds ubiquitous uses in ML. SHAP is based on the well-known Shapley values from game theory [62], and computes the so-called SHAP scores. A cooperative game is a pair G = (N, υ), where N is a set of players, e.g. the
2
O. Létoffé et al.
players in a game, the voters in an election, or the features in an ML model, and υ is a characteristic function that maps sets of features to the real values, υ : 2N → R. Given a characteristic function, the Shapley values are unique. Furthermore, for each characteristic function a different set of Shapley values is obtained. This paper provides a brief overview of the recent efforts that demonstrated critical flaws in the most often used definition of Shapley values for XAI, i.e. the definition used in SHAP [49,29]. As detailed in more recent work, the SHAP scores can produce misleading information because of the characteristic function that has been used in XAI [64,65,43]. In addition, this paper outlines more recent work on finding alternatives to the widely used (but flawed) SHAP scores [40,50]. This recent work involves proposing a new characteristic function, and devising novel algorithms aiming at the efficient computation of corrected SHAP scores. The novel characteristic function is based on a logic definition of explanation by feature selection [44], and so it establishes a link between two well-known kinds of explanation, i.e. feature selection and feature attribution, but also between Shapley values and logic-based definitions of explanations. At a more abstract level, this work also uncovers new links between formal methods and game theory. The paper is organized as follows. Section 2 introduces the notation and definitions used in the remainder of the paper, and Section 3 completes the preliminaries by providing a brief glimpse of logic-based XAI. Afterwards, Section 4 overviews the known flaws of SHAP scores. The remainder of the paper summarizes our recent work towards developing a trustable alternative to SHAP scores. Section 5 surveys a recent proposal of SHAP scores that corrects the known flaws of past definitions. These will be referred to as corrected SHAP scores. Then, Section 6 details practical methods for computing the corrected SHAP scores. Section 7 provides a glimpse of existing experimental results, and Section 8 concludes the paper.
2
Preliminaries
Machine learning (ML) models. An ML model is defined on a set F = {1, . . . , m} of features. Each feature i ∈ F takes values from a domain Di . Domains can be categorical, integer- or real-valued. The feature space F is defined as the cartesian product (in order) of the domains of the features, i.e. F = D1 × · · · × Dm . Given a set V of values, the ML model computes a nonconstant prediction function π : F → V. An ML model M is defined as a tuple M = (F, F, V, π). Observe that the definition of ML model applies both to classification and regression models. For classification problems, V is a finite set of values, which may be categorical. For regression problems, V may be infinite, and there are no restriction on the values of V. An instance I is a pair I = (v, p) where v ∈ F and p = π(v).
Rigorous Explainability by Feature Attribution
3
row # x1 x2 x3 π1 (x) 1 2 3 4 5 6 7 8 9 10 11 12
0 0 0 0 0 0 1 1 1 1 1 1
0 0 0 1 1 1 0 0 0 1 1 1
0 1 2 0 1 2 0 1 2 0 1 2
0 4 0 0 7 0 1 1 1 1 1 1
(a) Tabular representation
x1 1
∈ {0}
∈ {1}
x3
1
S 3 2
∈ {1}
∈ {0, 2}
x2
0 5
4
∈ {0}
∈ {1}
4
7
6
7
(b) Decision tree
rows(S)
υe (S)
∅ 1..12 {1} 7..12 {2} 4..6, 10..12 {3} 3, 6, 9, 12 {1, 2} 10..12 {1, 3} 9, 12 {2, 3} 6, 12 {1, 2, 3} 12
17/12
1 10/6 1/2
1 1 1/2 1
(c) Expected values
Fig. 1: Classification model M1 represented as a decision tree. x1 1
row # x1 x2 π2 (x) 1 2 3 4
0 0 1 1
0 1 0 1
−1/2 3/2
1 1
(a) Tabular representation
∈ {0}
∈ {1}
x2
1 3
2
∈ {0}
∈ {1}
−1/2
3/2
4
5
(b) Regression tree (RT)
S
rows(S) υe (S)
∅ 1, 2, 3, 4 {1} 3, 4 {2} 2, 4 {1, 2} 4
3/4
1 5/4
1
(c) Expected values
Fig. 2: Regression model M2 represented as a regression tree. An explanation problem is a tuple E = (M, I), where M can either be a classification or a regression model, and I = (v, p) is a given instance, with v ∈ F. (Observe that p = π(v), with p ∈ V.) Running examples. Figure 1 shows one of the running examples used throughout the paper. This example was first studied in [49]. Example 1. For the ML model shown in Figure 1, we have F1 = {1, 2, 3}, D1,1 = D1,2 = {0, 1}, D1,3 = {0, 1, 2}, F1 = D1,1 × D1,2 × D1,3 , and V1 = {0, 1, 4, 7}. The ML model M1 is represented by the tuple M1 = (F1 , F1 , V1 , π1 ), where π1 is shown in Figures 1a and 1b, respectively as a tabular representation (TR) and as a decision tree (DT). The target instance is I1 = ((1, 1, 2), 1) as shown. The explanation problem is thus E1 = (M1 , I1 ). Figure 2 shows the second running example that is used throughout the paper. This example was first studied in [40], and represents a regression model with discrete domains and discrete predicted values. Example 2. For the ML model shown in Figure 2, we have F2 = {1, 2}, D2,1 = D2,2 = {0, 1}, F2 = D2,1 × D2,2 , and V1 = {1, −1/2, 3/2}. The ML model M2 is represented by the tuple M2 = (F2 , F2 , V1 , π2 ), where π2 is shown in Figures 2a
4
O. Létoffé et al.
and 2b, respectively as a tabular representation (TR) and as a regression tree (DT). The target instance is I2 = ((1, 1), 1) as shown. The explanation problem is thus E2 = (M2 , I2 ). The expected values shown in both Figures 1c and 2c are discussed later in the paper. The definition of expected values is standard, e.g. [40]. Lipschitz continuity. Let (F, dF ) and (V, dV ) denote metric spaces.4 A regression function π : F → V is Lipschitz-continuous [57] if there exists a constant C ≥ 0 such that, ∀(x1 , x2 ∈ F).dV (π(x1 ), π(x2 )) ≤ CdF (x1 , x2 ),
(1)
where C is referred to as the Lipschitz constant. It is well-known that any Lipschitz-continuous function is also continuous. The relationship between Lipschitz continuity and adversarial robustness has been acknowledged for more than a decade [66], i.e. since the brittleness of ML models was recognized as a significant limitation of neural networks (NNs). Additional notation. fined by,
Given an instance (v, p), the notation xS = vS is de:=
xS = vS
^ i∈S
xi = vi
(2)
Thus, given S ∈ F , Υ (S)
:=
{x ∈ F | xS = vS }
denotes the set of points x in feature space such that the features represented by S take the values specified by the instance (v, p). Shapley values. Following [9], we define a game G as a pair (N, ν), where N is a finite non-empty set and ν : 2N → R is a characteristic function. The elements of N are referred to as the players, the voters, but also as the features. The characteristic function assigns a value to each coalition, i.e. subset of the players. In the context of XAI, N corresponds to the set of features F . The Shapley value represents one way of dividing the worth of a game (i.e. υ(N )) by its players, one that respects a number of important properties. For each element i ∈ N , given a characteristic function υt , its Shapley value is defined by: X Svt (i) = ς(S) × ∆i (S) (3) S⊆N \{i}
4
dF : F × F → R and dV : V × V → R denote distance functions between two points, which we refer to as d. A distance function d respects the well-known axioms: (i) d(x, x) = 0; (ii) if x ̸= y, then d(x, y) > 0; (iii) d(x, y) = d(y, x); and (iv) d(x, z) ≤ d(x, y) + d(y, z). Examples of distance functions include Hamming, Manhattan, Euclidean and other distance defined by norm lp , p ≥ 1, where Pm p 1/p ∥x∥p := . i=1 |xi |
Rigorous Explainability by Feature Attribution
5
where, ∆i (S) = (υt (S ∪ {i}) − υt (S)) ς(S) = |S|!(|N |−|S|−1)!/|N |! The complexity of computing the Shapley values is unwieldy. For example, for weighted voting games [9, Chapter 4], it is known that decision problem of computing the Shapley values is #P-complete [16, Theorem 9]. As a result, approximation algorithms have often been proposed [8]. Furthermore, alternatives to the Shapley value include the Banzhaf index [3], among many others. These alternatives are often studied in the context of measuring a priori voting power [19], one example being weighted voting games. SHAP scores. The original work on SHAP [43] adopted a concrete game for XAI and an algorithm for approximating the computation of the Shapley value for that game. The game for XAI builds on earlier work [64,65], where N denotes the set of features F , and the characteristic function is given by, υe (S) = E[π(x) | xS = vS ]
(4)
i.e. for the XAI game, the characteristic function is defined as the expected value of the classifier when the features in S are fixed to the values dictated by v. For each feature i ∈ F, the SHAP score for i obtained with (4) is denoted by Sve (i).5 Furthermore, given the game adopted for XAI, the tool SHAP uses a dedicated method to estimate the expected value for a given set S [43]. Example 3. The computation of the SHAP scores for the explanations problems in Figures 1 and 2 are shown in Figures 3 and 4, respectively. Computing Shapley values & SHAP scores. Motivated by the complexity of their exact computation, Shapley values are usually approximated. This is the case with the tool SHAP, but there exist well-known alternatives [8]. For the case of SHAP scores, exact algorithms have been studied [2]. Finally, for the special case of weighted voting games, there exist pseudo-polynomial time algorithms based on dynamic programming, e.g. [52]. The similarity predicate. With the purpose of enabling a unified treatment of logic-based XAI, we can abstract away some details of ML models [45]. Given an ML model and some input x, the computed prediction is distinguishable with respect to the sample (v, q) if the observed change in the model’s output is deemed sufficient; otherwise it is similar (or indistinguishable). This is represented by a similarity predicate (which can be viewed as a boolean function) σ : F → {⊥, ⊤} (where ⊥ signifies false, and ⊤ signifies true). Concretely, σ(x; E) holds true iff the change in the ML model output is deemed insufficient and so 5
The computation of expected values depends on the type of features used. The definitions proposed in [40] are assumed.
6
O. Létoffé et al. i=1 S
υe (S)
∅ {2} {3} {2, 3}
17/12 10/12 1/2 1/2
υe (S ∪ {1})
∆1 (S)
ς(S)
ς(S) × ∆1 (S)
1 1 1 1
−5/12
1/3
−2/3 1/2 1/2
1/6
−5/36 −2/18 1/12 1/6
1/6 1/3
Sve (1) =
0
i=2 S
υe (S)
υe (S ∪ {2})
∆2 (S)
ς(S)
ς(S) × ∆2 (S)
∅ {1} {3} {1, 3}
17/12
5/3
1/4
1/3
1/12
1 1/2 1
1 1/2 1
0 0 0
1/6
0 0 0
1/6 1/3
Sve (2) =
0.08(3)
i=3 S
υe (S)
υe (S ∪ {3})
∆3 (S)
ς(S)
ς(S) × ∆3 (S)
∅ {1} {2} {1, 2}
17/12
1/2
−11/12
1/3
1 5/3 1
1 1/2 1
0 −7/6 0
1/6 1/3
−11/36 0 −7/36 0
Sve (3) =
−0.5
1/6
Fig. 3: Computation of SHAP scores for E1 . i=1 S
υe (S)
υe (S ∪ {1})
∆1 (S)
ς(S)
ς(S) × ∆1 (S)
∅ {2}
3/4
1 1
1/4
1/2
−1/4
1/2
1/8 −1/8
5/4
Sve (1) =
0
i=2 S
υe (S)
υe (S ∪ {2})
∆2 (S)
ς(S)
ς(S) × ∆2 (S)
∅ {1}
3/4
5/4
1/2
1/2
1/4
1
1
0
1/2
0
Sve (2) =
0.25
Fig. 4: Computation of SHAP scores for E2 . no observable difference exists between the ML model’s output for x and v.6 For regression problems, we write instead σ as the instantiation of a template 6
Throughout the paper, parameterization are shown after the separator ’;’, and will be elided when clear from the context.
Rigorous Explainability by Feature Attribution
7
predicate, i.e. σ(x; E) = Tσ(x; E, δ), where δ is an optional measure of output change, which can be set to 0.7 For regression problems, we represent relevant changes to the output by a parameter δ. Given a change in the input from v to x, a change in the output is indistinguishable (i.e. the outputs are similar) if, σ(x; E) := Tσ(x; E, δ) := [|π(x) − π(v)| ≤ δ]
(5)
otherwise, it is distinguishable. For classification problems, similarity is defined to equate with not changing the predicted class. Given a change in the input from v to x, a change in the output is indistinguishable (i.e. the outputs are similar) if, σ(x; E) := [π(x) = π(v)]
(6)
otherwise, it is distinguishable. Example 4. For the two running examples (see Figures 1 and 2), it suffices to use Equation (6) as the similarity predicate, i.e. it suffices to test equality of prediction.
3
Logic-Based Explainability
In this paper, we study both logic-based explanations obtained from some logic representation of the ML model, but also from some sample of the ML model’s behavior. The former are referred to as model-aware explanations, whereas the latter are referred to as model-agnostic explanations. Model-agnostic explanations represent a rigorous alternative to the explanations obtained with tools such as Anchors [61]. Throughout, it is assumed an explanation problem E = (M, I), where M = (F, F, V, π) is an ML model, and I = (v, p) is an instance. 3.1
Model-Aware Explanations
Two types of logic-based explanations have been studied: abductive [33] and contrastive [32]. The following paragraphs provide brief overviews of their definitions. Abductive explanations. Given an instance (v, p), a weak abductive explanation (WAXp) is a set X ⊆ F such that, WAXp(X ; E)
:=
∀(x ∈ F). [xX = vX ] → [σ(x; E)]
(7)
Thus, if the features in X are fixed to the values dictated by v, then the prediction is guaranteed to be π(v) = p. A WAXp X ⊆ F is an abductive explanation 7
Exploiting a threshold to decide whether there exists an observable change has been used in the context of adversarial robustness [69]. Furthermore, the relationship between adversarial examples and explanations is well-known [34,69,49].
8
O. Létoffé et al.
(AXp) if it is subset-minimal, i.e. none of its subsets is a WAXp. A predicate AXp is associated with the condition of a set of features being an AXp. Although the relationship between the definition of AXp and logic-based abduction [17] might seem straightforward, it has been the subject of emergent controversy [37]. Appendix A provides a simple argument detailing the connection between AXps and logic-based abduction. Example 5. For E1 = (M1 , I1 ) (see Figure 1), inspection of the DT confirms that X1 = {1} is a WAXp, i.e. fixing the value of feature 1 suffices for guaranteeing that the prediction is 1. In this case, it is also plain that X1 is an AXp, since ∅ cannot be an AXp (as we assume non-constant ML models). For E2 = (M2 , I2 ) (see Figure 2), inspection of the RT confirms that X2 = {1} is a WAXp, for the same reasons as above. Also, it is the case that X2 is an AXp. Contrastive explanations. Given an instance (v, p), a weak contrastive explanation (WCXp) is a set Y ⊆ F such that, (8) WCXp(Y; E) := ∃(x ∈ F). xF \Y = vF \Y ∧ [¬σ(x; E)] Thus, when the features in Y are allowed to take some value from their domains (and the remaining features are fixed to the values dictated by v), it is the case that the prediction can be made different from π(v) = p. A WCXp Y ⊆ F is a contrastive explanation (CXp) if it is subset-minimal, i.e. none of its subsets is a WCXp. A predicate CXp is associated with the condition of a set of features being a CXp. Contrastive explanations are tightly related with adversarial examples [21] (AExs), namely when the measure of distance is l0 , i.e. the Hamming distance, and the target are subset-minimal and not cardinality-minimal sets of features [34,69,49]. Thus, any (W)CXp represents an AEx, since it denotes an example of the features to change so that the prediction also changes. Moreover, it is well-known that AXps are minimal hitting sets (MHSes) of the CXps and vice-versa [32]. MHS duality builds on Reiter’s seminal work on model-based diagnosis in the 1980s [59], and plays a key role in the enumeration of explanations [32,44]. Example 6. For E1 = (M1 , I1 ) (see Figure 1), inspection of the DT confirms that Y1 = {1} is a WCXp, i.e. allowing the value of feature 1 to change allows changing the prediction to a value other than 1. In this case, it is also plain that Y1 is a CXp, since ∅ cannot be an CXp (i.e. if all features are fixed, the prediction cannot change). For E2 = (M2 , I2 ) (see Figure 2), inspection of the RT confirms that Y2 = {1} is a WCXp, for the same reasons as above. Also, it is the case that Y2 is a CXp. Furthermore, one can compute all the CXps for the running examples using the polynomial-time algorithm proposed in earlier work [25]. In contrast, the set of AXps is obtained by hitting set dualization [20,42]. (Observe that, since all the CXps are computed in polynomial time, there is no need to exploit implicit hitting set dualization [41].) For the two running examples, the set of CXps is
Rigorous Explainability by Feature Attribution
9
{{1}} and the set of AXps is {{1}}. For both E1 and E2 , the sole adversarial example requires changing the value of feature 1; there is no other way to change the prediction of 1 other than changing the value of feature 1. Finally, a feature is said to be relevant if it occurs in some AXp. Otherwise, the feature is irrelevant. A relevant feature also occurs in some CXp, whereas an irrelevant feature does not [44, Proposition 8]. If one computes all the AXps (or all the CXps), then feature relevancy is decided in linear time on the set of AXps (or CXps). Example 7. For E1 = (M1 , I1 ) (see Figure 1), it is simple to conclude that feature 1 is relevant and that the features 2 and 3 are irrelevant [49]. Progress, status & assessment. Logic-based explainability has been the subject of significant progress since the initial works in 2018/19 [63,33]. Recent overviews provide a detailed account of this progress [44,14,45]. For several families of classifiers, it has been shown that there exist polynomial-time algorithms for computing a single AXp/CXp [46,47,25,12,24,13,7,4]. For other families of classifiers, it has been shown that finding one AXp/CXp is computationally hard, and different logic encodings have been devised [33,31,35,30]. Appendix A outlines the method that is used in practice when the computation of AXps/CXps involves logic encodings. Alternative methods based on compilation to a canonical representation have also been studied in the past [14,55].
3.2
Model-Agnostic Explanations
In contrast to the model-aware case, model-agnostic explanations are defined with respect to a given sample of the ML model’s behavior. Different methods can be envisioned to crease such a sample, including those used by tools such as LIME [60], SHAP [43] and Anchors [61], but also the dataset used for training the ML model. A sample S is a tuple (D, pT ), where D is a n × m matrix, such that each row j denotes a point dj of F. In addition, p = (p1 , . . . , pn ), such that pj ∈ V, j = 1, . . . , n, and such that π(dj ) = pj , j = 1, . . . , n. The definition of model-agnostic explanations mimic those of the modelaware case, but now quantification is restricted to the points in the sample. Thus, WAXp(X ; E)
∀(x ∈ D). [xX = vX ] → [σ(x; E)]
(9)
∃(x ∈ D). xF \Y = vF \Y ∧ [¬σ(x; E)]
(10)
:=
and, WCXp(Y; E)
:=
(W)AXps/(W)CXps for model-aware and model-agnostic are referred to using the same predicate names; the difference will be clear from the context. Recent works have studied rigorous model-agnostic explanations [11,1,51].
10
O. Létoffé et al.
Table 1: Theoretical SHAP scores vs. feature relevancy for the running examples (see Figures 1 and 2). E1 = (M1 , I1 )
4
E2 = (M2 , I2 )
Feature i
Sve (i)
Relevant?
Feature i
Sve (i)
Relevant?
1 2 3
0 0.08(3) −0.5
Yes No No
1 2 —
0 0.25 —
Yes No —
The Flaws of SHAP Scores
Several flaws in the theory underlying SHAP scores have been reported since 2023 [26,27,28,48]. Since then, further results confirmed the flaws of theoretical SHAP scores [49,29,39]. Concretely, it has been shown that there arbitrarily many ML models for which the theoretical scores will mislead human decision makers. This section briefly overviews the known flaws of theoretical SHAP scores. Throughout this section, we focus on cases where the computed SHAP score is clearly misleading, i.e. importance is given to features that are manifestly unimportant, and no importance is given to features that are guaranteed to be important. Classification & regression models. For the two running examples (see Figures 1 and 2), feature 1 is relevant and the remaining features are irrelevant. However, as shown in Figures 3 and 4, the SHAP score for the relevant feature 1 is 0, which signifies [64,65] no importance for the prediction. In contrast, the SHAP score for the remaining features is not 0, which signifies some importance for the prediction. Therefore, for the two running examples, the relative importance of features obtained using SHAP scores is evidently misleading for a human decision maker. Table 1 summarizes the comparison between computed theoretical SHAP scores and feature relevancy. Continuous & differentiable models. A possible criticism regarding classification models and regression models with discrete domains and discrete predicted values is that these may not represent all the possible ranges of uses of ML. However, one can create examples where both the features and the predicted values take (uncountable) real values. The following example, first discussed in [39], confirms that the flaws of SHAP scores also exist in the case of real-valued ML models. In this case, the definition of the similarity predicate is from (5), and so a value of δ must be chosen. We will pick some δ < 1/4. Example 8. (Regression model M3 .) We consider a regression problem defined over two real-valued features, taking values from interval [−1/2, 3/2]. Thus, we have F3 = {1, 2}, D3,1 = D3,2 = D3 = [−1/2, 3/2], F3 = D3 × D3 . (We also let − + 1 3 D+ 3 = [ /2, /2] and D3 = D3 \ D3 .) In addition, the regression model maps to
Rigorous Explainability by Feature Attribution
11
Table 2: Expected values of π3 , for each possible set S of fixed features, and given the sample ((1, 1), 1). These expected values also apply in the case of π4 (see Figure 5). S
∅
{1}
{2}
{1, 2}
E[π3 (x) | xS = vS ]
1/2
1
3/2
1
real values, i.e. V3 = R, and is defined as follows: if x1 ∈ D+ x1 3 + π3 (x1 , x2 ) = x2 − 2 if x1 ̸∈ D+ 3 ∧ x2 ̸∈ D3 + x2 + 1 if x1 ̸∈ D3 ∧ x2 ∈ D+ 3 As a result, the regression model is represented by M3 = (F3 , F, V3 , π3 ). Moreover, we assume the target instance to be I3 = (v3 , p3 ) = ((1, 1), 1), and so the explanation problem becomes E3 = (M3 , (v3 , p3 )). Example 9. (AXps, CXps and AExs for E3 .) Given the regression model M3 , we define the similarity predicate by picking a suitably small value δ, e.g. δ < 1/4 as suggested above. This suffices to ensure that the similarity predicate σ only takes value ⊤ when feature 1 takes value 1. Given the above, the similarity predicate takes value ⊤ only when feature 1 takes value 1, and independently of the value assigned to feature 2. Thus, fixing feature 1 ensures that the similarity predicate always takes value ⊤. Otherwise, if feature 1 is allowed to take a value other than 1, then the similarity predicate can take value ⊥, and so the WAXp condition does not hold. As a result, {1} is one (and the only) AXp, and {1} is also one (and the only) CXp. A similar analysis allow concluding that a l0 -minimal AEx exists iff feature 1 is allowed to take any value from its domain. Example 10. (SHAP scores for E3 .) The expected values of π3 for all possible sets S of fixed features is shown in Table 2.8 Hence, the computation of SHAP scores is also the one shown in Figure 4, given the expected values. As a result, Sve (1) = 0 and Sve (2) = 1/2. Given the example above, we have constructed a regression example over uncountable domains and predicted values, such that the SHAP scores mislead. Nevertheless, one possible criticism of the example above is that the ML model is not continuous, and one may argue that often used ML models are continuous. We now present a family of continuous ML models, that also produce misleading SHAP scores. The family of models is parameterized on α. We will then argue that the proposed family of ML models also ensures Lipschitz continuity. 8
The computation of these expected values is fairly straightforward, and is summarized in the supplemental materials.
12
O. Létoffé et al.
x1 (1 + 4|α|)x1 − 4|α| π4 (x1 , x2 ) = 28|α|x x + (1 − 28|α|)x − 28|α|x + 28|α| 1 2 1 2 −4|α|x1 x2 + (1 + 8|α|)x1 + 4|α|x2 − 8|α|
if x2 ≤ 1 ∧ αx1 ≤ α if x2 ≤ 1 ∧ αx1 ≥ α if x2 ≥ 1 ∧ αx1 ≤ α if x2 ≥ 1 ∧ αx1 ≥ α
Fig. 5: Example of regression model that is Lipschitz continuous. Example 11. We consider a regression problem defined over two real-valued features, taking values from interval [0, 2]. Thus, we have F = {1, 2}, D4,1 = D4,2 = D4 = [0, 2], F4 = D4 × D4 . In addition, the regression model maps to real values, i.e. V4 = R, and is defined as shown in Figure 5. The value of α is such that α ∈ R \ {0}. We will pick α = 1/4. As a result, the regression model is represented by M4 = (F4 , F4 , V4 , π4 ). Moreover, we assume the target sample to be I4 = (v4 , p4 ) = ((1, 1), 1), and so the explanation problem becomes E4 = (M4 , I4 ). By inspection, it is plain that π4 is continuous; this is further discussed below. Example 12. (AXps, CXps and AExs for E4 .) As before, it is plain to reach the conclusion that the set of AXps is {{1}}, and this is also the set of CXps. Moreover, and as before, there is a l0 -minimal AEx containing feature 1. Example 13. (SHAP scores for E4 .) The regression model M4 is devised such that the expected values of π4 for each possible set S of fixed features are exactly the ones shown in Table 2. As a result, the computed SHAP scores are the same as before, and so they are again misleading. As shown in [39], π4 is Lipschitz-continuous. Thus, the continuity of π4 , which is claimed above, is implied by the fact that π4 Lipschitz-continuous. Finally, recent work also argues that the flaws of SHAP scores can also exist in arbitrarily differentiable ML models [39]. Significance of SHAP’s flaws. As summarized above, earlier work provided extensive evidence regarding the flaws of SHAP scores [26,27,28,48,49,29,39], that cover classification, regression, but also (Lipschitz-)continuous and differentiable ML models. The majority of cases relate with assigning importance to irrelevant features, not assigning importance to relevant features, and also allowing the relative importance of relevant and irrelevant features to be reversed [49]. In turn, this can serve to mislead human decision makers. The fact that the tool SHAP approximates Shapley values only makes matters worse. This is further discussed in Section 7. Despite the mounting evidence regarding the flaws of SHAP scores, the growing popularity of the tool SHAP [43] is evident and underlined by its impact. For example, and quoting from recent work [22,23]: “... we note that certain studies have pointed out the limitations of SHAP (...). However, it has been used extensively in the literature due to its demonstrated effectiveness and has contributed to significant discoveries in science, engineering, and business, which were discussed in publications in leading journals such
Rigorous Explainability by Feature Attribution
13
as Science, Nature Machine Intelligence, Nature Communications, and Management Science (see ...), just to name a few (the paper by Lundberg and Lee (2017) has been cited more than 34,000 times as of May 2025).” Unfortunately, rigor cannot be established by popularity. The flaws of SHAP scores have been demonstrated with a vast number of case studies (and supporting theory), included in this and in earlier papers [26,27,28,48,49,29,39]. Some researchers have recently suggested the assessment of results by domain experts or additional interpretation to confirm the quality of SHAP’s results [36,18,67,6]. Clearly, for complex ML models, this is error-prone. Given the above, and in light of the identified flaws, we contend that the most significant conclusions drawn in the many publications that build on the tool SHAP [43] ought to be reassessed.
5
Corrected SHAP Scores – Theory
Given the theoretical flaws of SHAP scores, a natural question is whether such flaws can be fixed. This section proposes a game for explainability which is guaranteed not to exhibit the limitations of the SHAP scores used in the tool SHAP. 5.1
Properties of Characteristic Functions for XAI
Recent work [38,40] proposed several properties that characteristic functions for XAI games should respect so that the identified flaws of SHAP scores are eliminated. Strong value independence. Let M1 = (F, F, T1 , τ1 ) be an ML model, with domain Di for each feature i ∈ F . Moreover, let M2 = (F , F, T2 , τ2 ) be another classifier, with the same domains. In addition, let µ : K1 → K2 be a mapping from T1 to T2 , such that for q ∈ T1 , and such that, ∀(b ∈ T1 ).[(b ̸= q) →(µ(b) ̸= µ(q))] Finally, let the target samples be (v, p), for M1 , and (v, µ(p)) for M2 , thus defining the explanation problems E1 = (M1 , (v, p)) and E2 = (M2 , (v, µ(p))). A characteristic function υt is strongly value-independent if, given µ, ∀(i ∈ F).[Svt (i; E1 ) = Svt (i; E2 )] Given the above, the following result holds Compliance with feature (ir)relevancy. Characteristic functions should respect feature (ir)relevancy, i.e. a feature is irrelevant iff its (corrected) SHAP score is 0. Formally, a characteristic function υt is compliant with feature (ir)relevancy if, ∀(i ∈ F ).Irrelevant(i) ↔ (Svt (i) = 0) (11) In previous work [26,29,49], SHAP scores are said to be misleading when compliance with feature (ir)relevancy is not respected. In the remainder of the paper, we assign the same meaning to the term misleading. Numerical neutrality. Existing definitions of SHAP scores are based on expected values and so require V to be ordinal. However, classification problems often contemplate categorical classes. A characteristic function respects numerical neutrality if it can be used with both numerical and non-numerical V.
14
5.2
O. Létoffé et al.
A Logic-Based Game for XAI
Instead of defining the XAI game using a characteristic function defined in terms of the expected value of the ML model, as has been done in the past [64,65,43], we have proposed instead the following characteristic function [38,40]: ( 1 if WAXp(S; E) υa (S; E) := (12) 0 otherwise (Clearly, the game is still defined on the set of features, with the difference to earlier definitions being the characteristic function.) As noted in earlier work [40], the relationship with the characteristic functions used in a priori voting power are apparent. It is also important to underline the connection between the proposed game for XAI and logic-based explainability by feature selection. Finally, the proposed characteristic function ensures that the resulting game is a simple game [9], i.e. the characteristic function is monotonically increasing, and takes values from the set {0, 1}. Earlier work proved that the logic-based characteristic function proposed above respects the properties listed in Section 5.1 that characteristic functions for XAI should respect.
6
Corrected SHAP Scores – Practice
This section details the organization of nuSHAP [50], a recently proposed alternative to the tool SHAP [43]. Whereas the tool SHAP approximates the well-known SHAP scores, which correspond to a game where the characteristic function is given by (4), nuSHAP uses the logic-based characteristic function shown in (12). Computing Shapley values. Although polynomial-time algorithms have been proposed for computing SHAP scores for restricted families of ML models [2], those results do not apply in the case of corrected SHAP scores, because the characteristic function tests whether the given set is a WAXp and does not compute expected values. At present, no polynomial-time algorithms have been devised for computing corrected SHAP scores. The solution that has been proposed in recent work [50] is to adopt the well-known approximation algorithm of Castro, Gómez and Tejada (CGT) [8], which provides strong theoretical guarantees. Thus, nuSHAP implements the CGT algorithm on the XAI game Ga = (F, υa ). The rest of this section discusses how the predicate WAXp is decided in practice. Model-aware corrected SHAP scores. Assuming that we are equipped with an explainer capable of deciding whether a set of features is a WAXp, then we can simply run the CGT algorithm, at each step computing the characteristic function by checking the predicate WAXp. For several families of classifiers, this can be attained in polynomial-time [44].
Rigorous Explainability by Feature Attribution
15
Model-agnostic corrected SHAP scores. For complex ML models, checking the predicate WAXp cannot be achieved in polynomial-time. For these cases, nuSHAP proposes the computation of rigorous model-agnostic explanations, where the sample is either obtained from the ML model, or alternatively by adopting the dataset used for training the ML model. One advantage of rigorous model agnostic explanations is that the predicate WAXp can be checked in polynomial-time [11,51]. Open research topics. As noted above, the exact computation of corrected SHAP scores is currently an open topic of research. While the CGT algorithm [8] provides strong theoretical guarantees, it is open whether alternatives might exist, for either computing the SHAP scores approximately or exactly.
7
Experiments
This section summarizes the experiments comparing the tools SHAP [43] and nuSHAP [50], a recently proposed alternative. The tool nuSHAP approximates the Sva SHAP scores, using the CGT algorithm [8]. In contrast, the tool SHAP approximates the Sve SHAP scores using its own approximation algorithm. The goal of the experiments is to assess the quality of the SHAP tool [43] at ranking features in terms of their relative importance for a given prediction. To ensure a fair comparison, the sampling performed by the tool SHAP was recorded. This sampling was then used by nuSHAP. The tools SHAP9 and nuSHAP were assessed on several well-known classifiers [70], namely: logistic regression (LR), decision tree (DT), k-nearest neighbors (kNN) classifier, boosted trees (BT), and Convolutional Neural Network (CNN). LR, DT, and kNN models are trained using scikit-learn [58], BT models are trained using the XGBoost algorithm [10], while CNN models are trained using TensorFlow10 . The comparison was conducted across a range of widely used tabular classification datasets selected from the PMLB benchmark [56], as well as the MNIST dataset [15] of handwritten digits (0–9). The classifiers and datasets used in the experiments are briefly summarized in Table 3. (Additional detail is included in [50].) For each tabular dataset, we randomly picked 50 tested instances for computing nuSHAP and SHAP scores. For the MNIST dataset, we randomly selected 20 test instances to compute these scores. Moreover, we chose different model-agnostic SHAP explainers when computing SHAP scores. ExactExplainer was used for the first and second sets, PermutationExplainer was used for the third set, and SamplingExplainer was used for the fourth and last set. All explainers are provided with the entire training data so that the SHAP tool can draw samples from it. However, for MNIST a reduced training data was used, to curb the size of sampling. For the nuSHAP tool, the parameters of the CGT algorithm used were ϵ = 0.0015 and α = 0.015, for all the tested instances. 9 10
Available from https://github.com/slundberg/shap. https://www.tensorflow.org/.
16
O. Létoffé et al.
Table 3: Summary of RBO values for all the tested instances, including the minimum, maximum, and mean RBO values.
Min
nuSHAP vs SHAP nuSHAP vs |SHAP|
0.08 0.05
0.17 0.31 0.12 0.27
0.32 0.32
0.0 0.0
0.01 0.05
0.0 0.0
0.0 0.0
0.0 0.0 0.0 0.03
0.0 0.0
Mean Max
LR DT kNN BT CNN adult corral iris mux6 conn..4 spamb. spectf clean1 coil..0 dna MNIST
nuSHAP vs SHAP 0.96 nuSHAP vs. |SHAP| 0.88
0.96 0.94 0.97 0.94
0.97 0.95
0.9 0.77
0.94 0.94
0.91 0.91
0.69 0.88
0.69 0.88 0.69 0.88
0.06 0.06
nuSHAP vs SHAP 0.37 nuSHAP vs. |SHAP| 0.31
0.53 0.84 0.5 0.84
0.7 0.69
0.21 0.19
0.41 0.42
0.2 0.19
0.12 0.17
0.05 0.17 0.08 0.43
0.0 0.0
Table 4: Average runtime (in seconds) for computing SHAP and nuSHAP scores. adult corral iris mux6 conn..4 spamb. spectf clean1 coil..0 dna MNIST SHAP nuSHAP
3.4 1.9
0.1 0.0 1.5 1.5
0.0 1.5
21.7 4.5
0.5 2.7
0.7 2.9
6.8 2.7
28.2 23.0 1.7 4.5
281.3 48.9
SHAP and nuSHAP were compared using two metrics: i) the ranking of feature importance imposed by different scores; and ii) the runtime for computing these scores. Specifically, for each tested instance, we first compute its nuSHAP and SHAP scores. We then determined the order of feature importance based on these scores. For SHAP, we considered two orders: one based on the original SHAP scores and the other based on the absolute values of the SHAP scores. Next, we compare the order imposed by nuSHAP scores with the order imposed by original SHAP scores, and separately compare the order imposed by nuSHAP scores with the order imposed by the absolute values of SHAP scores. To compare the rankings of feature importance, we used the metric rankbiased overlap (RBO) [68] for each pair of scores. RBO is a metric used to measure the similarity between two ranked lists, and it ranges between 0 and 1. A higher RBO value indicates a greater degree of similarity between the two rankings, with 1 denoting a perfect match for the top-ranked elements considered. A publicly available implementation11 of RBO was used in our experiments. Given the fact that human decision makers are able to grasp a reduced number of features [53], we set persistence to 0.5 and depth to 5 in our setting. This means that we focused on the top-5 features while placing greater emphasis on the top-3 features. Table 3 summarizes the RBO values for all the tested instances, including the minimum, maximum, and mean RBO values. As can be observed, there is essentially no correlation between the results of the tools nuSHAP and SHAP. Finally, Table 4 presents the average running times for computing the different scores, confirming that nuSHAP performs similarly to SHAP. 11
https://github.com/changyaochen/rbo.
Rigorous Explainability by Feature Attribution
8
17
Conclusions
This paper provides a brief account of the ongoing efforts to develop a rigorous alternative to the tool SHAP [43], which is used ubiquitously as a method of feature attribution in XAI. The paper revisits the limitations of the theory underlying SHAP, and proposes a rigorous alternative, i.e. the so-called corrected SHAP scores. Furthermore, the paper outlines possible methods for computing corrected SHAP scores. The experiments provide additional evidence regarding the limitations of the tool SHAP. Future work will target the exact computation of corrected SHAP scores.
References 1. Leila Amgoud, Martin C. Cooper, and Salim Debbaoui. Axiomatic characterisations of sample-based explainers. In ECAI, pages 770–777, 2024. 2. Marcelo Arenas, Pablo Barceló, Leopoldo E. Bertossi, and Mikaël Monet. On the complexity of SHAP-score-based explanations: Tractability via knowledge compilation and non-approximability results. J. Mach. Learn. Res., 24:63:1–63:58, 2023. 3. John F Banzhaf III. Weighted voting doesn’t work: A mathematical analysis. Rutgers L. Rev., 19:317, 1965. 4. Pablo Barceló, Alexander Kozachinskiy, Miguel Romero, Bernardo Subercaseaux, and José Verschae. Explaining k -nearest neighbors: Abductive and counterfactual explanations. Proc. ACM Manag. Data, 3(2):97:1–97:26, 2025. 5. Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2021. 6. Sebastian Bordt, Eric Raidl, and Ulrike von Luxburg. Position: Rethinking explainable machine learning as applied statistics. In ICML, 2025. 7. Clément Carbonnel, Martin C. Cooper, and João Marques-Silva. Tractable explaining of multivariate decision trees. In KR, pages 127–135, 2023. 8. Javier Castro, Daniel Gómez, and Juan Tejada. Polynomial calculation of the shapley value based on sampling. Comput. Oper. Res., 36(5):1726–1730, 2009. 9. Georgios Chalkiadakis, Edith Elkind, and Michael J. Wooldridge. Computational Aspects of Cooperative Game Theory. Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2012. 10. Tianqi Chen and Carlos Guestrin. XGBoost: A scalable tree boosting system. In KDD, pages 785–794, 2016. 11. Martin C. Cooper and Leila Amgoud. Abductive explanations of classifiers under constraints: Complexity and properties. In ECAI, pages 469–476, 2023. 12. Martin C. Cooper and João Marques-Silva. On the tractability of explaining decisions of classifiers. In CP, pages 21:1–21:18, 2021. 13. Martin C. Cooper and João Marques-Silva. Tractability of explaining classifier decisions. Artif. Intell., 316:103841, 2023. 14. Adnan Darwiche. Logic for explainable AI. In LICS, pages 1–11, 2023. 15. Li Deng. The MNIST database of handwritten digit images for machine learning research [best of the web]. IEEE signal processing magazine, 29(6):141–142, 2012. 16. Xiaotie Deng and Christos H Papadimitriou. On the complexity of cooperative solution concepts. Mathematics of operations research, 19(2):257–266, 1994.
18
O. Létoffé et al.
17. Thomas Eiter and Georg Gottlob. The complexity of logic-based abduction. J. ACM, 42(1):3–42, 1995. 18. Gillian England-Mason, Sarah J MacEachern, Kimberly Amador, Munawar Hussain Soomro, Anthony JF Reardon, Amy M MacDonald, David W Kinniburgh, Nicole Letourneau, Gerald F Giesbrecht, Jonathan W Martin, et al. Using machine learning to investigate the influence of the prenatal chemical exposome on neurodevelopment of young children. NeuroToxicology, 108:218–230, 2025. 19. Dan S Felsenthal and Moshé Machover. The measurement of a priori voting power. In Jac C. Heckelman and Nicholas R. Miller, editors, Handbook of Social Choice and Voting, chapter 08, pages 117–139. Edward Elgar Publishing, 2015. 20. Michael L. Fredman and Leonid Khachiyan. On the complexity of dualization of monotone disjunctive normal forms. J. Algorithms, 21(3):618–628, 1996. 21. Ian J. Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In ICLR, 2015. 22. Zezhen He. The Role of Explainable Artificial Intelligence in Model Selection, Adoption, and Wait Time Communication. PhD thesis, University of Rochester, 2025. 23. Zezhen Dawn He and Yaron Shaposhnik. Explaining model behavior across space and time: Differential and intertemporal explanations. SSRN, (5277675), 2025. 24. Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, Martin C. Cooper, Nicholas Asher, and João Marques-Silva. Tractable explanations for d-DNNF classifiers. In AAAI, pages 5719–5728, 2022. 25. Xuanxiang Huang, Yacine Izza, Alexey Ignatiev, and João Marques-Silva. On efficiently explaining graph-based classifiers. In KR, pages 356–367, 2021. 26. Xuanxiang Huang and Joao Marques-Silva. The inadequacy of Shapley values for explainability. CoRR, abs/2302.08160, 2023. 27. Xuanxiang Huang and João Marques-Silva. A refutation of Shapley values for explainability. CoRR, abs/2309.03041, 2023. 28. Xuanxiang Huang and Joao Marques-Silva. Refutation of Shapley values for XAI – additional evidence. CoRR, abs/2310.00416, 2023. 29. Xuanxiang Huang and João Marques-Silva. On the failings of shapley values for explainability. Int. J. Approx. Reason., 171:109112, 2024. 30. Alexey Ignatiev, Yacine Izza, Peter J. Stuckey, and João Marques-Silva. Using maxsat for efficient explanations of tree ensembles. In AAAI, pages 3776–3785, 2022. 31. Alexey Ignatiev and Joao Marques-Silva. SAT-based rigorous explanations for decision lists. In SAT, pages 251–269, 2021. 32. Alexey Ignatiev, Nina Narodytska, Nicholas Asher, and Joao Marques-Silva. From contrastive to abductive explanations and back again. In AIxIA, pages 335–355, 2020. 33. Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. Abduction-based explanations for machine learning models. In AAAI, pages 1511–1519, 2019. 34. Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva. On relating explanations and adversarial examples. In NeurIPS, pages 15857–15867, 2019. 35. Yacine Izza and Joao Marques-Silva. On explaining random forests with SAT. In IJCAI, pages 2584–2591, 2021. 36. Gabriel Kallah-Dagadu, Mohanad Mohammed, Justine B Nasejje, Nobuhle Nokubonga Mchunu, Halima S Twabi, Jesca Mercy Batidzirai, Geoffrey Chiyuzga Singini, Portia Nevhungoni, and Innocent Maposa. Breast cancer prediction based on gene expression data using interpretable machine learning techniques. Scientific Reports, 15(1):7594, 2025.
Rigorous Explainability by Feature Attribution
19
37. Faezeh Labbaf, Tomás Kolárik, Martin Blicha, Grigory Fedyukovich, Michael Wand, and Natasha Sharygina. Space explanations of neural network classification. In CAV, pages 287–303, 2025. 38. Olivier Létoffé, Xuanxiang Huang, and Joao Marques-Silva. On correcting SHAP scores. CoRR, abs/2405.00076, 2024. 39. Olivier Létoffé, Xuanxiang Huang, and João Marques-Silva. SHAP scores fail pervasively even when Lipschitz succeeds. CoRR, abs/2412.13866, 2024. 40. Olivier Létoffé, Xuanxiang Huang, and João Marques-Silva. Towards trustable SHAP scores. In AAAI, pages 18198–18208, 2025. 41. Mark H. Liffiton, Alessandro Previti, Ammar Malik, and João Marques-Silva. Fast, flexible MUS enumeration. Constraints An Int. J., 21(2):223–250, 2016. 42. Mark H. Liffiton and Karem A. Sakallah. Algorithms for computing minimal unsatisfiable subsets of constraints. J. Autom. Reason., 40(1):1–33, 2008. 43. Scott M. Lundberg and Su-In Lee. A unified approach to interpreting model predictions. In NeurIPS, pages 4765–4774, 2017. 44. João Marques-Silva. Logic-based explainability in machine learning. In Reasoning Web, pages 24–104, 2022. 45. Joao Marques-Silva. Logic-based explainability: Past, present and future. In ISoLA, pages 181–204, 2024. 46. Joao Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, and Nina Narodytska. Explaining naive bayes and other linear classifiers with polynomial time and delay. In NeurIPS, 2020. 47. João Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, and Nina Narodytska. Explanations for monotonic classifiers. In ICML, pages 7469– 7479, 2021. 48. João Marques-Silva and Xuanxiang Huang. Explainability is NOT a game – preliminary report. CoRR, abs/2307.07514, 2023. 49. João Marques-Silva and Xuanxiang Huang. Explainability is Not a game. Commun. ACM, 67(7):66–75, 2024. 50. João Marques-Silva, Xuanxiang Huang, and Olivier Létoffé. The explanation game - rekindled (extended version). CoRR, abs/2501.11429, 2025. 51. João Marques-Silva, Jairo A. Lefebre-Lobaina, and Maria Vanina Martinez. Efficient and rigorous model-agnostic explanations. In IJCAI, pages 2637–2646, 2025. 52. Tomomi Matsui and Yasuko Matsui. A survey of algorithms for calculating power indices of weighted majority games. Journal of the Operations Research Society of Japan, 43(1):71–86, 2000. 53. George A Miller. The magical number seven, plus or minus two: Some limits on our capacity for processing information. Psychological review, 63(2):81–97, 1956. 54. Christoph Molnar. Interpretable machine learning. Lulu.com, 2020. 55. Alnis Murtovi, Maximilian Schlüter, and Bernhard Steffen. Computing inflated explanations for boosted trees: A compilation-based approach. In Mike Hinchey and Bernhard Steffen, editors, The Combined Power of Research, Education, and Dissemination, pages 183–201, 2025. 56. Randal S. Olson, William La Cava, Patryk Orzechowski, Ryan J. Urbanowicz, and Jason H. Moore. PMLB: a large benchmark suite for machine learning evaluation and comparison. BioData Mining, 10(36):1–13, Dec 2017. 57. Mícheál O’Searcoid. Metric spaces. Springer Science & Business Media, 2006. 58. Fabian Pedregosa, Gaël Varoquaux, Alexandre Gramfort, Vincent Michel, Bertrand Thirion, Olivier Grisel, Mathieu Blondel, Peter Prettenhofer, Ron Weiss, Vincent Dubourg, et al. Scikit-learn: Machine learning in python. the Journal of machine Learning research, 12:2825–2830, 2011.
20
O. Létoffé et al.
59. Raymond Reiter. A theory of diagnosis from first principles. Artif. Intell., 32(1):57– 95, 1987. 60. Marco Túlio Ribeiro, Sameer Singh, and Carlos Guestrin. "why should I trust you?": Explaining the predictions of any classifier. In KDD, pages 1135–1144, 2016. 61. Marco Túlio Ribeiro, Sameer Singh, and Carlos Guestrin. Anchors: High-precision model-agnostic explanations. In AAAI, pages 1527–1535, 2018. 62. Lloyd S. Shapley. A value for n-person games. Contributions to the Theory of Games, 2(28):307–317, 1953. 63. Andy Shih, Arthur Choi, and Adnan Darwiche. A symbolic approach to explaining bayesian network classifiers. In IJCAI, pages 5103–5111, 2018. 64. Erik Strumbelj and Igor Kononenko. An efficient explanation of individual classifications using game theory. J. Mach. Learn. Res., 11:1–18, 2010. 65. Erik Strumbelj and Igor Kononenko. Explaining prediction models and individual predictions with feature contributions. Knowl. Inf. Syst., 41(3):647–665, 2014. 66. Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. Intriguing properties of neural networks. In ICLR, 2014. 67. Ting-Ting Wang, Kun-Yu Liu, Hong-Jie Peng, and Xinyan Liu. Interpretable machine learning for battery prognosis: Retrospect and prospect. Advanced Energy Materials, page e03067, 2025. 68. William Webber, Alistair Moffat, and Justin Zobel. A similarity measure for indefinite rankings. ACM Transactions on Information Systems (TOIS), 28(4):1–38, 2010. 69. Min Wu, Haoze Wu, and Clark W. Barrett. VeriX: Towards verified explainability of deep neural networks. In NeurIPS, 2023. 70. Zhi-Hua Zhou. Machine Learning. Springer, 2021.
A
Abductive Explanations & Logic-Based Abduction
Throughout this section, we adopt the definition of (subset-minimal) logic-based abduction from earlier work [17]. Furthermore, and for simplicity, we assume an ML model with boolean features and boolean prediction function, such that it has a propositional logic representation. Nevertheless, more expressive logics, e.g. (fragments of) first order logic, could be considered. Let T denote a logic theory representing a given ML model, that is defined on two sets of propositional variables, vars(T ) = {x1 , . . . , xm } ∪ {y1 , . . . , yM }. Clearly, {x1 , . . . , xm } are associated with the ML model’s features. Furthermore, define propositional variables hi ↔ (xi ↔ vi ), i = 1, . . . , m, and also m ↔ (π(x) ↔ π(v)). Thus, let H = {h1 , . . . , hm } and M = {o}. Finally, let the set of propositional variables be V = vars(T ) ∪ H ∪ M . Given the above, the logicbased abduction problem is thus a tuple P = ⟨V, H, M, T ⟩ and an explanation (or solution) for the abduction problem is a set S ⊆ H such that: 1. T ∪ S is consistent; and 2. T ∪ S ⊨ M . Clearly, for any set S ⊆ H, it is the case that T ∪ S is consistent, since it suffices to assign to the other xi variables the values dictated by v. Furthermore, it is also plain that T ∪ S ⊨ M corresponds to the set S being sufficient
Rigorous Explainability by Feature Attribution
21
for the prediction. Therefore, abductive explanations are indeed an instantiation of logic-based abduction, when explanations (for the logic-based abduction problem) are restricted to be subset-minimal. The use of abduction as outlined above is also exploited in practice when using logic encodings for either computing AXps or CXps. The set S can be viewed as a set of soft clauses such that T ∪ {¬o} ∪ S ⊨ ⊥. (This is equivalent to T ∪S ⊨ M , with the single clause in M complemented.) The goal is then to find a minimal subset of S of H, such that inconsistency is preserved. This corresponds to finding a minimal unsatisfiable subset (MUS) of an inconsistent propositional formula [5].