On Explaining Random Forests with SAT

1 Introduction

The recent successes of Machine Learning (ML), and the forecast continued growth of ML-enabled applications, including applications that impact human beings or that are even safety critical, has raised the need for identifying explanations for the predictions made by ML models. As a result, recent years witnessed the rapid growth of the field of explainable Artificial Intelligence (XAI) (see e.g. [Guidotti et al., 2019; Li et al., 2018; Montavon et al., 2018; Shih et al., 2018; Shih et al., 2019; Ribeiro et al., 2016; Ribeiro et al., 2018; Ignatiev et al., 2019; Ignatiev, 2020; Audemard et al., 2020; Ignatiev et al., 2020; Ignatiev and Marques-Silva, 2021; Marques-Silva et al., 2021]). Unfortunately, the most promising ML models, including neural networks or ensembles of classifiers, due to their size and intrinsic complexity, are generally accepted to be non-interpretable (or black-box), with the understanding that the predictions made by such black-box models cannot be understood by human decision makers.

A large body of work on XAI is based on heuristic approaches [Ribeiro et al., 2016; Lundberg and Lee, 2017; Ribeiro et al., 2018], offering no formal guarantees regarding computed explanations 1 . In contrast, recent work focused on non-heuristic approaches which offer formal guarantees with respect to computed explanations [Shih et al., 2018; Ignatiev et al., 2019; Shih et al., 2019; Ignatiev, 2020; Darwiche and Hirth, 2020; Audemard et al., 2020; MarquesSilva et al., 2020; Ignatiev et al., 2020; Ignatiev and MarquesSilva, 2021; Marques-Silva et al., 2021].

Approaches to explainability can also be characterized as being model-agnostic or model-precise 2 . Model-agnostic approaches do not require information about the ML model representation, thus allowing the explanation of any class of ML models. In contrast, in model-precise approaches, some representation of the concrete ML model is reasoned about, and so these are characterized by being model-specific. Whereas model-agnostic approaches are in general heuristic, modelprecise approaches can either be non-heuristic [Shih et al., 2018; Ignatiev et al., 2019; Shih et al., 2019; Ignatiev, 2020; Darwiche and Hirth, 2020; Audemard et al., 2020; MarquesSilva et al., 2020; Ignatiev et al., 2020; Ignatiev and MarquesSilva, 2021; Marques-Silva et al., 2021] or heuristic [Zhao et al., 2019; Petkovic et al., 2018; Mollas et al., 2020]. For model-precise non-heuristic approaches different solutions have been investigated. [Shih et al., 2018] propose an approach for explaining Bayesian network classifiers, which is based on compiling such classifiers into Ordered Decision Diagrams representing all prime implicants of the boolean function representing the target class predictions. These represent the so-called PI-explanations (which we revisit in Section 2). A different approach, based on abductive reasoning [Ignatiev et al., 2019; Ignatiev, 2020], exploits automated reasoning tools (e.g. SMT, MILP, etc.) with explanations being computed on demand. In abductive reasoning approaches, the ML model is represented as a set of constraints and, given some target instance, a prime implicant is computed, which represents a minimal set of feature-value pairs that is sufficient for the prediction. Earlier work investigated encodings of neural networks [Ignatiev et al., 2019] and of boosted trees [Ignatiev, 2020].

1 For example, an explanation E, for an input I1 resulting in prediction A, can also be consistent with input I2 resulting in prediction B ̸= A [Ignatiev, 2020]. Such loose explanations inevitably raise concerns in applications where safety is critical.

2 Orthogonal to the goals of the paper is the classification of explanations as local or global [Guidotti et al., 2019].

This paper extends earlier work on model-precise nonheuristic explainability. Concretely, the paper proposes a novel approach for computing PI (or abductive) explanations (AXps) of Random Forest classifiers [Breiman, 2001; Yang et al., 2020; Zhang et al., 2019; Gao and Zhou, 2020; Feng and Zhou, 2018; Zhou and Feng, 2017]. Random Forests (RFs) represent a widely used tree ensemble ML model, where each RF ML model is composed of a number of decision trees (DTs). (The importance of RFs is further illustrated by recent proposals for implementing deep learning (DL) with RFs [Zhou and Feng, 2017; Zhang et al., 2019; Feng and Zhou, 2018].)

In contrast with earlier work [Ignatiev, 2020], we show that in the case of RFs it is possible to devise a purely propositional encoding. In turn, this enables achieving very significant performance gains. Concretely, the experimental results show that our approach is able to compute explanations of realistically-sized RFs most often in a fraction of a second. The experiments also show that our approach is on average more than one order of magnitude faster than a state of the art model-agnostic heuristic approach [Ribeiro et al., 2018].

Recent work on model-precise non-heuristic explainability has shown that some ML models can be explained in polynomial time [Audemard et al., 2020; Marques-Silva et al., 2020]. In contrast, this paper proves that it is D P -complete to decide whether a set of literals is a PI-explanation (AXp) of an RF, thus making it unlikely that RFs can be explained in polynomial time.

The paper is organized as follows. Section 2 covers the preliminaries. Section 3 proves the complexity of deciding whether a set of literals is an explanation for an RF. Section 4 proposes a propositional encoding for computing one AXp of an RF. Section 5 presents the experimental results. Finally, Section 6 concludes the paper.

2 Preliminaries

ML Classification. We consider a machine learning classification problem, defined by a set of features F = {1, . . . ,m}, and by a set of classes K = {c1, c2, . . . , cK}. Each feature j ∈ F takes values from a domain Di. (Domains may correspond to Boolean, Categorical or Continuous data.) Thus, feature space is defined as F = D1 × D2 × . . . × Dm. To refer to an arbitrary point in feature space we use the notation x = (x1, . . . , xm), whereas to refer to a specific point in feature space we use the notation v = (v1, . . . , vm), with vi ∈ Di, i = 1, . . . ,m. An instance (or example) denotes a pair (v, c), where v ∈ F and c ∈ K. An ML classifier is characterized by a classification function τ that maps the feature space F into the set of classes K, i.e. τ : F → K. To learn a classifier, a set of instances {(v1, c1), . . . , (vk, ck)} is used as training data by a learning algorithm that returns a function with a best fit on the training data.

Decision Tree and Random Forest Classifiers. Decision trees rank among the most widely-used techniques ML models [Breiman et al., 1984; Quinlan, 1993]. Formally, a decision tree T = (VT ,ET ) is a directed acyclic graph, where the root node has no incoming edges, and every other node has exactly one incoming edge. The nodes of a tree are partitioned into terminal (VT ) and non-terminal (VNT ) nodes. Terminal nodes denote the leaf nodes, and have no outgoing edges (i.e. children). Non-terminal nodes denote the internal nodes, and have outgoing edges. Each terminal node j ∈ VT is associated with a class taken from K. We define a map κ : VT → K to represent the class associated with each terminal node. Each non-terminal node is associated with a feature taken from a set of features F. Given a feature j ∈ F associated with a non-terminal node l, each outgoing edge represents a literal of the form xj ▷◁ Sj, where either Sj ∈ Dj or Sj ⊆ Dj 3 . Each path in T is associated with a consistent conjunction of literals, denoting the values assigned to the features so as to reach the terminal node in the path. We will represent the set of literals of some tree path Rk by L(Rk).

A well-known drawback of decision trees is overfitting with respect to the training data. In contrast, tree ensembles such as Random Forests (RFs) [Breiman, 2001] combine several tree-based models, which allows for improved accuracy and ability to generalize beyond the training data. More formally, an RF F is a collection of decision trees (DTs) F = {T1, T2, . . . , TM}. Each tree Ti ∈ F is trained on a subsample of the training dataset so as the trees of the RF are not correlated. The prediction function in RF works by majority vote, that is each tree votes for a class and the most voted class is picked. (In case of ties, for simplicitly we will pick the lexicographically smallest class.)

Running Example. Let us assume a simple binary classification problem for predicting whether or not a patient has a heart disease. The class variables are: Yes and No (Yes to classify the patient as suffering from heart disease and No to classify the patient as without heart disease.) and a set of features in the following order: blocked-arteries, good-bloodcirculation, chest-pain, and weight, where features 1, 2 and 3 represent Boolean variables, and feature 4 represents an ordinal variable. Let the set of trees, shown in Figure 1, be the tree ensemble of an RF classifier F trained on the heart disease problem and τ its classification function. There are 3 trees in the forest and each tree has a maximum depth of 2. Assume we have an instance v = (1, 0, 1, 70), namely, blocked-arteries = 1, good-blood-circulation = 0, chest-pain = 1, weight = 70. Hence, Trees 1 and 3 vote for Yes and Tree 2 votes for No. As the majority votes go for Yes, then the classifier will return Yes for v, i.e. τ(v) = Yes.

Boolean satisfiability (SAT). The paper assumes the notation and definitions standard in SAT [Biere et al., 2021], i.e. the decision problem for propositional logic, which is known to be NP-complete [Cook, 1971]. A propositional formula ϕ is defined over a finite set of Boolean variables X = {x1, x2, . . . , xn}. Formulas are most often represented in conjunctive normal form (CNF). A CNF formula is a conjunction of clauses, a clause is a disjunction of literals, and a literal is a variable (xi) or its negation (¬xi). Whenever convenient, a formula is viewed as a set of sets of literals. A Boolean interpretation µ of a formula ϕ is a total mapping of X to {0, 1} (0 corresponds to False and 1 corresponds to True). Interpretations can be extended to literals, clauses and formulas with the usual semantics; hence we can refer to µ(l), µ(ω), µ(ϕ), to denote respectively the value of a literal, clause and formula given an interpretation. Given a formula ϕ, µ is a model of ϕ if it makes ϕ True, i.e. µ(φ) = 1. A formula ϕ is satisfiable (ϕ⊭ ⊥) if it admits a model, otherwise, it is unsatisfiable (ϕ⊨ ⊥). Given two formulas ϕ and ψ, we say that ϕ entails ψ (denotes ϕ⊨ψ) if all models of ϕ are also models of ψ. ϕ and ψ are equivalent (denoted ϕ ≡ ψ) if ϕ ⊨ ψ and ψ ⊨ ϕ.

3 Features are either categorical (including boolean) or real- or integer-valued ordinal, and ▷◁ ∈ {=, ∈}. (Observe that these operators allow for intervals to be represented.)

Abductive explanations. The paper uses the definition of PI-explanation [Shih et al., 2018] (also referred to as abductive explanation (AXp) in [Ignatiev et al., 2019]) 4 , based on prime implicants of some decision function (related with the predicted class). Let us consider a given ML model, computing a classification function τ on feature space F, a point v ∈ F, with prediction c = τ(v), with v = (v1, . . . , vm). A PI-explanation (AXp) is any minimal subset X ⊆ F such that:

In a similar vein, we consider contrastive explanations (CXps) [Miller, 2019]. A formal definition of contrastive explanation is proposed in recent work [Ignatiev et al., 2020].

4 Throughout the paper we will use both terms PI-explanation and abductive explanation (AXp) interchangeably.

Contrastive explanations. Contrastive explanation can be defined as a minimal subset Y ⊆ F that suffice to changing the prediction if features of Y are allowed to take some arbitrary value from their domain. Given v = (v1, . . . , vm) ∈ F with κ(v) = c, a CXp is any minimal subset Y ⊆ F such that,

Building on the results of R. Reiter in model-based diagnosis [Reiter, 1987], [Ignatiev et al., 2020] proves a minimal hitting set (MHS) duality relation between AXps and CXps, i.e. AXps are MHSes of CXps and vice-versa.

Example 1. Consider the binary classifier F of the running example. and the instance (v = (1, 0, 1, 70), Yes). If the features good-blood-circulation and weight are allowed to take any possible value from their domain, and the values of the features blocked-arteries and chest-pain are kept to their values in v, then the prediction is still Yes. This means that the features good-blood-circulation and weight can be deemed irrelevant for the prediction of Yes given the other feature values in v. Moreover, by allowing either blocked-arteries or chest-pain to take any value, prediction will change to No. Hence, {blocked-arteries, chest-pain} is a subset-minimal set of features sufficient for predicting τ(v) = Yes, that is a PI-explanation (AXp). Additionally, setting the value of blocked-arteries to 0 suffices to changing the prediction of v (i.e. τ(0, 0, 1, 70) = No), thus {blocked-arteries} is a CXp.

3 Complexity of AXps for RFs

Recent work identified classes of classifiers for which one AXp can be computed in polynomial time [Audemard et al., 2020; Marques-Silva et al., 2020]. These classes of classifiers include those respecting specific criteria of the knowledge compilation map [Audemard et al., 2020] 5 , but also Naive Bayes and linear classifiers (resp. NBCs and LCs) [MarquesSilva et al., 2020]. (In the case of NBCs and LCs, enumeration of AXps was shown to be solved with polynomial delay.) One question is thus whether there might exist a polynomial time algorithm for computing one computing AXp of an RF. This section shows that this is unlikely to be the case, by proving that deciding whether a set of features represents an AXp is D P -complete 6 .

Let F be an RF, with classification function τ , and let v ∈ F, with prediction τ(v) = c ∈ K. τ is parameterized with c, to obtain the boolean function τc, s.t. τc(x) = 1 iff τ(x) = c. A set of literals Iv is associated with each v. Let ρ be a subset of the literals associated with v, i.e. ρ ⊆ Iv. Hence,

Theorem 1. For a random forest F, given an instance v with prediction c, deciding whether a set of literals is an AXp is D P -complete.

5 The knowledge compilation map was first proposed in 2002 [Darwiche and Marquis, 2002].

6 The class D P [Papadimitriou, 1994] is the set of languages defined by the intersection of two languages, one in NP and one in coNP.

Proof. Given an instance v and predicted class c, deciding whether a set of literals ρ is an AXp of an RF F is clearly in D P . We need to prove that ρ⊨τc, which is a problem in coNP. We also need to prove that a set of literals ρ′ , obtained by the removal of any single literal from ρ (and there can be at most m of these), is such that ρ⊭τc, a problem in NP. To prove that the problem is hard for D P , we reduce the problem of computing a prime implicant of a DNF, which is known to be complete for D P [Umans et al., 2006], to the problem of computing a PI-explanation of an RF F.

Consider a DNF φ = t1 ∨ · · · ∨ tn, where each term ti is a conjunction of literals defined on a set X = {x1, . . . , xm} of boolean variables. Given φ, we construct an RF F, defined on a set F of m features, where each feature i is associated with an xi element of X, and where Di = {0, 1}. Moreover, F is such that φ(x) = 1 iff τ1(x) = 1. F is constructed as follows.

1. Associate a decision tree (DT) Ti with each term ti, such that the assignment satisfying ti yields class 1, and the other assignments yield class 0. Clearly, the size of the DT Ti is linear on the size of ti, since each literal not taking the value specified by the term will be connected to a terminal node with prediction 0.
2. Create (n-1) additional trees, each having exactly one terminal node and no non-terminal nodes. Moreover, associate class 1 with the terminal node.

Next, we prove that φ(x) = 1 iff τ1(x) = 1.

1. Let x be such that φ(x) = 1. Then, there is at least one term tj, such that tj(x) = 1. As a result, the corresponding tree Tj in the RF will predict class 1. Hence, at least n trees predict class 1, and at most n - 1 trees predict class 0. As a result, the predicted class is 1, and so τ1(x) = 1.
2. Let x be such that τ1(x) = 1. This means that at least one of the trees associated with the terms ti must predict value 1. Let such tree be Tj, associated with term tj. For this tree to predict class 1, then tj(x) = 1, and so φ(x) = 1.

Now, let ρ be a conjunction of literals defined on X. Then, we must have ρ⊨φ iff ρ⊨τ1. Every model of ρ is also a model of φ, and so it must also be a model of τ1. Conversely, every model of ρ is also a model of τ1, and so it must also be a model of φ. □

4 AXps for RandomForests

This section outlines the computation of PI-explanations (AXps) for RFs. We first present the algorithm's organization. The algorithm requires a logical encoding of RFs, which are presented next.

Computing AXps. A minimal set of features X ∈ F is an AXp if (1) holds. Clearly, this condition holds iff the following formula is unsatisfiable,

The previous formula has two components 〈H, S〉. H represents the set of hard clauses, encoding the representation of the ML model and also imposing a constraint on the predicted class, i.e. Enc(τ(x) ̸= c). S represents the unit (soft) clauses, each capturing a literal (xi = vi). Since the clauses in S are soft, they can be dropped (thus allowing xi to take any value) while searching for a minimal subset of E of S, such that,

is unsatisfiable. Our goal is to find a minimal set S such that the pair 〈H, S〉 remains unsatisfiable (where S can be viewed as the background knowledge against which the clauses in S are inconsistent). This corresponds to finding a minimal unsatisfiable subset (MUS) of 〈H, S〉, and so any off-the-shelve MUS extraction algorithm can be used for computing an AXp (as noted in earlier work [Ignatiev et al., 2019]).

Clearly, adapting the descibed procedure above of computing one AXp to one that computes a CXp is straightforward. That is, the minimal set Y of S to search is, such that,

is satisfiable. Further, hitting set duality between AXps and CXps allows to exploit any algorithm for computing MUSes/MCSes 7 to enumerate both kinds of explanations (AXps and CXps). (Recent work [Ignatiev et al., 2020; Marques-Silva et al., 2021; Ignatiev and MarquesSilva, 2021] exploits the MUS/MCS enumeration algorithm MARCO [Liffiton et al., 2016] for enumerating AXps/CXps.)

We detail next how to encode an RF, while requiring some prediction not to hold. We start with a simple encoding of an RF into an SMT formula, and then we detail a purely propositional encoding, which enables the use of SAT solvers.

SMTEncoding. Several encodings of tree ensemblemodels, such as Boosted Trees (BTs), have been proposed and they are essentially based on SMT/MILP (see e.g. [Chen et al., 2019; Einziger et al., 2019; Ignatiev, 2020], etc). Hence, it is natural to follow prior work and propose a straightforward encoding of RFs in SMT. Intuitively, the formulation of RFs into SMT formulas is as follows. We encode every single DT of an RF as a set of implication rules. That is, a DT path (classification rule) is interpreted as a rule of the form antecedent → consequent where the antecedent is a conjunction of predicates encoding the non-terminal nodes of the path and the consequent is a predicate representing the class associated with the terminal node of the path. Next, we aggregate the prediction (votes) of the DTs and count the prediction score for each class. This can be expressed by an arithmetic function that calculates the sum of trees predicting the same class. Lastly, a linear inequality checks which class has the largest score.

The implementation of the encoding above resulted in performance results comparable to those of BTs [Ignatiev, 2020]. However, in the case of RFs it is possible to devise a purely propositional encoding, as detailed below.

7 An MCS is a minimal set of clauses to remove from an unsatisfiable CNF formula to recover consistency . It is well-known that MCSes are minimal hitting sets of MUSes and vice-versa [Reiter, 1987; Birnbaum and Lozinskii, 2003].

SAT Encoding. Our goal is to represent the structure of an RF with a propositional formula. This requires abstracting away what will be shown to be information used by the RF that is unnecessary for finding an AXp. Concretely, and as shown below, the actual values of the features used as literals in the RF need not be considered when computing one AXp. We start by detailing how to encode the nodes of the decision trees in an RF. This is done such that the actual values of the features are abstracted away. Then, we present the encoding of the RF classifier itself, including how the majority voting is represented.

To encode a terminal node of a DT, we proceed as follows. Given a set of classes K = {c1, c2, . . . , cK}, a terminal node t labeled with one class of K. Then, we define for each cj ∈ K a variable lj and represent the terminal node t with its corresponding label class cj, i.e. κ(t) = cj.

Moreover, the encoding of a non-terminal node of a DT is organized as follows. Given a feature j ∈ F associated with a non-terminal node l, with a domain Dj , each outgoing edge of l is represented by a literal lj of the form xj ▷◁ Sj s.t. xj ∈ F is the variable of feature j, Sj ▷◁ Dj and ▷◁ ∈ {=, ⊆, ∈}. Hence we distinguish three cases for encoding xj ▷◁ Sj. For the first case, feature j is binary, and so the literal lj is True if xj = 1 and False if xj = 0. For the second case, feature j is categorical, and so we introduce a Boolean variable zi for each value vi ∈ Dj s.t. zi = 1 iff xj = vi. Assume Sj = {v1, . . . , vn}, then we connect lj to variables zi, i = 1, . . . , n as follows: lj ↔(z1 ∨ . . . ∨ zn) or ¬lj ↔(z1 ∨ . . . ∨ zn), depending on whether the current edge is going to left or right child-node. Finally, for the third case, feature j is real-valued. Thus, Sj is either an interval or a union of intervals. Concretely, we consider all the splitting thresholds of the feature j existing in the RF and we generate (in order) all the possible intervals. Each interval Ii ⊆ Dj is denoted by a Boolean variable zi. Let us assume Sj = I1 ∪ . . . ∪ In and z1, . . . , zn are variables associated with I1 ∪ . . . ∪ In, then we have lj ↔(z1 ∨ . . . ∨ zn) or ¬lj ↔(z1 ∨ . . .∨zn). Moreover, this encoding can be reduced into a more compact set of constraints (that also improves propagation in the SAT solver). Indeed, if the number of intervals is large the encoding will be as well. Hence, we propose to use auxiliary variables in the encoding. Assume Dj = I1 ∪ I2 ∪ I3, nodes l and l′ s.t. ¬lj ↔z1, ¬lj ↔(z1 ∨ z2 ∨ z3), ¬l′j ↔(z1 ∨ z2), l′j ↔z3, then this can be re-written as: ¬lj ↔z1, lj ↔(z2 ∨ l′j ), ¬l′j ↔(z2 ∨ ¬lj), l′j ↔z3.

The next step is to encode the RF classifier. Given an RF F formed by a set of M DTs, i.e. F = {T1, T2, . . . , TM}, and τ the classification function of F. For every DT Ti ∈ F, we encode the set of paths Ri of Ti as follows:

where lij is a literal associated with Ti in which the voted class is cj ∈ K.

For every DT Ti ∈ F, and every path Rk ∈ Ri, we enforce the condition that exactly one variable lij is True in Ti 8 . This can be expressed as 9 :

8 Only one class is returned by Ti.

Finally, for capturing the majority voting used in RFs, we need to express the constraint that the counts (of individual tree selections) for some class ck ̸= cj have to be large enough (i.e. greater than, or greater than or equal to) when compared to the counts for class cj. We start by showing how cardinality constraints can be used for expressing such constraints. The proposed solution requires the use of K - 1 cardinality constraints, each comparing the counts of cj with the counts of some other ck. Afterwards, we show how to reduce to 2 the number of cardinality constraints used.

Let cj ∈ K be the predicted class. The index j is relevant and ranges from 1 to K = |K|. Moreover, let 1 ≤ k < j ≤ K. Class ck is selected over class cj if:

Similarly, let 1 ≤ j < k ≤ K. Class ck is selected over class cj if:∑M

(A simple observation is that these constraints can be optimized for the case |K| = 2.)

It is possible to reduce the number of cardinality constraints as follows. Let us represent (5) and (6), respectively, by Cmp≺(z≺ 1 , . . . , z≺M ) andCmp≻(z≻ 1 , . . . , z≻M ). (Observe that the encodings of these constraints differ (due to the different RHSes).) Moreover, in (5) and (6) we replace (z≺ 1 , . . . , z≺M ) and (z≻ 1 , . . . , z≻M ) resp. by l1k, . . . , lMk, for some k. The idea is that we will only use two cardinality constraints, one for (5) and one for (6).

Let pk = 1 iff k is to be compared with j. In this case, Cmp▷◁(z▷◁ 1 , . . . , z ▷◁M ) (where ▷◁ is either ≺ or ≻) is comparing the class counts of cj with the class counts of some ck. Let us use the constraint pk→(z▷◁ i ↔ lik), with k ∈ {1, . . . ,K} \ {j}, and 1 ≤ i ≤ M. This serves to allow associating the (free) variables (z▷◁ 1 , . . . , z ▷◁M ) with some set of literals (l1k, . . . , lMk). Moreover, we also let p0 →(z▷◁ i ↔ 1) and pj →(z▷◁ i ↔ 1), i.e. we allow p0 and pj to pick guaranteed winners, and such that ¬p0 ∨ ¬pj . Essentially, we allow for a guaranteed winner to be picked below j or above j, but not both. Clearly, we must pick one k, either below or above j, to pick a class ck, when comparing the counts of ck and cj. We do this by picking two winners, one below j and one above j, and such that at most one is allowed to be a guaranteed winner (either 0 or j):

Observe that, by starting the sum at 0 and j, respectively, we allow the picking of one guaranteed winner in each summation, if needed be. To illustrate the described encoding above we consider again the running example.

9 We use the well-known cardinality networks [As´ın et al., 2011] for encoding all the cardinality constraints of the proposed encoding.

Example 2. Consider again the RF F of the running example and the instance v = (1, 0, 1, 70), giving the prediction Yes. Let us define the Boolean variables x1, x2 and x3 associated with the binary features blocked-arteries, goodblood-circulation, chest-pain, resp. and variables w1 and w2 representing (weight > 75) and (weight ≤ 75) resp. and an auxiliary variable w. Also, to represent the classes No and Yes, we associate variables denoting the classes for each tree: {l11, l12} for T1, {l21, l22} for T2 and {l31, l32} for T3. Hence, the corresponding set of encoding constraints is: {x1 ∧ x3→l12, x1 ∧ ¬x3→l11, ¬x1→l11, x2→l21, ¬x2 ∧ w→l22, ¬x2 ∧ ¬w→l21, x2 ∧ x1→l32, x2 ∧ ¬x1 → l31, ¬x2 ∧ x3 → l32, ¬x2 ∧ ¬x3 → l31, w ↔w1, ¬w↔w2, (l11 + l21 + l31) ≥ 2, x1, ¬x2, x3, w2}. Observe that {x1, ¬x2, x3,w2} denotes the set of the soft constraints whereas the remaining are the hard constraints.

5 Experimental Results

This section assess the performance of our approach to compute PI-explanations (AXps) for RFs and also compares the results with an heuristic explaining model Anchor [Ribeiro et al., 2018] 10 The assessment is performed on a selection of 32 publicly available datasets, which originate from UCI Machine Learning Repository [Dua and Graff, 2017] and Penn Machine Learning Benchmarks [Olson et al., 2017]. Benchmarks comprise binary and multidimensional classification datasets. The number of classes in the benchmark suite varies from 2 to 26. The number of features (resp. data samples) varies from 4 to 64 (106 to 58000, resp.) with the average being 21.9 (resp. 5131.09). When training RF classifiers for the selected datasets, we used 80% of the dataset instances (20% used for test data). For assessing explanation tools, we randomly picked fractions of the dataset, depending on the dataset size. Concretely, for datasets containing, resp., less than 200, 200-999, 1000-9999 and 10000 or more, we randomly picked, resp., 40%, 20%, 10% and 2% of the instances to analyze. The number of trees in each RF is set to 100 while tree depth varies between 3 and 8. (Note that we have tested other values for the number of trees ranging from 30 to 200, and we fixed it to 100 since with 100 trees RFs achieve the best train/test accuracies.) As a result, the accuracy of the trained models varies between 76% to 100%. We use the scikit-learn ML tool to train RF models. Note that, scikitlearn can only handle binary and ordinal features in the case of RFs. Accordingly, the experiments focus on binary and continuous data and do not include categorical features. In addition, we have overridden the implemented RF learner in sciki-learn so that it reflects the original algorithm described in [Breiman, 2001] 11 . Furthermore, PySAT [Ignatiev et al., 2018] is used to instrument incremental SAT oracle calls.

10 Anchor computes heuristic local explanations and not PIexplanations (AXp). Also, we do not consider other tools, such as LIME [Ribeiro et al., 2016] or SHAP [Lundberg and Lee, 2017], as these learn a simpler ML model as an explanation and not a set of literals.

The experiments are conducted on a MacBook Pro with a Dual-Core Intel Core i5 2.3GHz CPU with 8GByte RAM running macOS Catalina. Table 1 summarizes the results of assessing the performance of our RF explainer tool (RFxpl) on the selected datasets. (The table's caption also describes the meaning of each column.) As can be observed, and with three exceptions, the average running time of RFxpl is less than 1sec. per instance. In terms of the largest running times, there are a few outliers (this is to be expected since we are solving a D P -hard problem), and these occur when the number of classes is large. To assess the scalability of RFxpl, we compared RFxpl with the well-known heuristic explainer Anchor [Ribeiro et al., 2018]. (Clearly, the exercise does not aim to compare the explanation accuracies of Anchor and RFxpl, but only to assess how scalable it is in practice to solve a D P -complete explainability problem with a propositional encoding and a SAT oracle.) Over all datasets, RFxpl outperforms Anchor on more than 96% of the instances (i.e. 8438 out of 8746). In terms of average running time per instance, RFxpl outperforms Anchor by more than 1 order of magnitude, concretely the average run time of Anchor is 14.22 times larger than the average runtime of RFxpl.

6 Conclusion

This paper proposes a novel approach for explaining random forests. First, the paper shows that it is D P -complete to decide whether a set of literals is a PI-explanation (AXp) for a random forest. Second, the paper proposes a purely propositional encoding for computing PI-explanations (AXps) of random forests. The experimental results allow demonstrating that the proposed approach not only scales to realistically sized random forests, but it is also significantly more efficient that a state of the art model-agnostic heuristic approach. Given the practical interest in RFs [Zhou and Feng, 2017], finding AXps represents a promising new application area of SAT solvers.

11 The RF model implemented by scikit-learn uses probability estimates to predict a class, whereas in the original proposal for RFs [Breiman, 2001], the prediction is based on majority vote.

Two extensions of the work can be envisioned. One extension is to improve further the propositional encoding proposed in this paper, aiming at eliminating the very few cases where heuristic approaches are more efficient. Another extension is to exploit the proposed model (and any of its future improvements) to explain deep random forests [Zhou and Feng, 2017].

Acknowledgments

This work is supported by the AI Interdisciplinary Institute ANITI, funded by the French program "Investing for the Future - PIA3" under Grant agreement no ANR-19-PI3A-0004, and by the H2020-ICT38 project COALA "Cognitive Assisted agile manufacturing for a Labor force supported by trustworthy Artificial intelligence".