Tree ensembles (TEs) find a multitude of practical applications. They represent one of the most general and accurate classes of machine learning methods. While they are typically quite concise in representation, their operation remains inscrutable to human decision makers. One solution to build trust in the operation of TEs is to automatically identify explanations for the predictions made. Evidently, we can only achieve trust using explanations, if those explanations are rigorous, that is truly reflect properties of the underlying predictor they explain This paper investigates the computation of rigorously-defined, logically-sound explanations for the concrete case of two well-known examples of tree ensembles, namely random forests and boosted trees.
Figures & tables
Figure 1. Example of a simple boosted tree model ( Chen and Guestrin, 2016 ) generated by XGBoost on the well-known Iris classification dataset. Here, the tree ensemble has 2 trees for each of the 3 classes with the depth of each tree being at most 2.
Figure 2. Example of a simple RFmv trained using Scikit-learn with 3 trees, on Iris dataset. Here, the tree ensemble has 3 trees with the depth of each tree being at most 2. In the running examples, classes “Setosa”, “Versicolor” and “Virginica” are denoted, resp. class c1 , c2 and c3 , and features sepal.length , sepal.width , petal.length and petal.width are ordered, resp., as features 1–4.
Figure 3. Example of a simple RFwv trained using Scikit-learn with 3 trees, on Iris dataset. Here, the tree ensemble has 3 trees with the depth of each tree being at most 2. In the running examples, classes “Setosa”, “Versicolor” and “Virginica” are denoted, resp. class c1 , c2 and c3 , and features sepal.length , sepal.width , petal.length and petal.width are ordered, resp., as features 1–4.
Figure 4. Reducing example RFmv to BT. Note that splitting nodes yielding to a score 0 , in its leaf nodes, are pruned and replaced with labeled leaf node 0 .
Figure 5. Reducing example RFmv to RFwv.
Dataset
RFmv
SAT Enc
AXp
CXp
AEx
( m
K )
D
#N
%A
( #var
#cl )
Len
Time
Len
Time
ann-thyroid
( 21
3 )
4
2192
98
( 17854
29230 )
2.1
0.13
1.3
0.18
0.277
appendicitis
( 7
2 )
6
1920
90
( 5181
10085 )
4.0
0.03
2.4
0.06
0.094
banknote
( 4
2 )
5
2772
97
( 8068
16776 )
2.0
0.02
1.0
0.08
0.190
biodegradation
( 41
2 )
5
4420
88
( 11007
23842 )
16.8
0.29
4.5
0.19
0.278
ecoli
( 7
5 )
5
3860
90
( 20081
34335 )
4.0
0.10
1.2
0.20
0.384
Table 1. Detailed performance evaluation of the SAT encoding for computing AXp’s and CXp’s for RFmv. The table shows results for 31 datasets, i.e. those for which test data accuracy is no less than 76%. Columns m and K report, respectively, the number of features and classes in the dataset. Columns D , #N and %A show, respectively, each tree’s max. depth, total number of nodes and test accuracy of an RF classifier. Columns #var and #cl show the number of variables and clauses of a CNF formula encoding an RFmv classifier along with any instance to analyze. Column Time shows the average runtime for extracting an explanation. Column Len reports the average explanation length (i.e. average number of features contained in the explanations). AEx reports the average runtime for robustness verification to adversarial examples.
Figure 6. Assessing MaxSAT and SMT encodings of BTs for computing AXps.
Figure 7. Assessing MaxSAT and SMT encodings of BTs for computing CXps.
Figure 8. Assessing MaxSAT and SMT encodings of RFwv for computing AXps and CXps.
Figure 9. Ablation study of MaxSAT Approach for BTs.
Figure 10. Assessing minimum CXps for RFmv.
Figure 11. Assessing minimum CXps for RFwv.
Figure 12. Assessing minimum CXps in BTs.
Figure 13. Scalability of RC2 and OR-Tools oracles for computing minimum CXp.
Dataset
RFmv
SAT Enc
IF
( m
K )
P
D
%A
( #var
#cl )
Time
Result
adult
( 12
2 )
race, gender
6
78.4
( 6374
18650 )
0.128
unfair
compas
( 11
2 )
race, gender
5
58.8
( 6169
12968 )
0.073
unfair
german
( 21
2 )
age, gender
3
70.0
( 16383
24942 )
0.421
fair
ricci
( 5
2 )
race
3
100
( 6233
11382 )
0.052
unfair
Table 2. Fairness verification benchmarks. Columns m and K report the number of features and classes. Column P lists the protected attributes considered for individual fairness. Columns #var and #cl show the size of the CNF encoding. Column Time reports total runtime (encoding and verification). Column Result indicates whether the classifier satisfies individual fairness (IF).
A gradient-boosted ensemble predicts by summing one leaf value per tree. Read those values as coordinates rather than as intermediate results, and every instance becomes a point in R^M on which the model acts linearly: the score is the sum of the coordinates. This small change of view makes contrastive explanation exact. The difference between two instances is a vector that is identically zero wherever they share a leaf, so the gap between a rejected applicant and an accepted one is carried by a handful of coordinates, each traceable to a real split in a real tree. Nothing is fitted, sampled, or assumed additive in features -- the additivity is already there, in the right space. We build a recourse method on this representation and evaluate it on five tabular datasets under repeated cross-validation. Its recommendation reconstructs the model's own decision to 6.2 x 10^-15, so an auditor can re-check the arithmetic without the model. On the credit datasets it is Pareto-non-dominated on effort against realism. And when recommendations are restricted to changes the subject could actually make -- not their age, not a settled delinquency -- it retains 58% of its validity where the strongest baseline retains 41%, a distinction the standard evaluation cannot see because it never asks whether a recommendation can be carried out.
Trust in counterfactual explanations depends critically on whether their recommended changes are truly minimal: suboptimal explanations may vastly overshoot the actual changes needed to alter a decision, and heuristic errors can affect individuals unevenly, giving some users relevant recourse while assigning others unnecessarily costly recommendations. Consequently, we study the problem of computing optimal counterfactual explanations for tree ensembles under plausibility and actionability constraints. This is a combinatorial problem: for a fixed model, counterfactual search boils down to selecting consistent branching decisions and threshold-defined regions under a distance objective. We exploit this structure through CPCF, a constraint programming (CP) formulation in which numerical features are encoded as interval domains induced by split thresholds, while discrete features retain native finite-domain representations. This yields a compact finite-domain formulation that supports multiple distance objectives without continuous split-boundary search. We then place CPCF in a broader comparison across mathematical programming paradigms: we extend a maximum Boolean satisfiability (MaxSAT) formulation, originally designed for hard-voting random forests, to soft-voting ensembles, and compare against the current state-of-the-art mixed-integer linear programming (MILP) optimal approach. Across ten datasets and three types of tree ensembles, we analyze scalability, anytime performance, and sensitivity to distance metrics. We observe that CP achieves the best overall performance. More importantly, our results identify regimes in which the specific strengths of each paradigm make it best suited: CP is most versatile overall, MaxSAT handles hard-voting ensembles particularly well, and MILP remains competitive in amortized inference settings with a moderate number of split levels.
Predictive models in clinical and regulated settings must be accurate and fully auditable. Tree ensembles deliver strong accuracy on tabular data, but their sequential boosting couples structure discovery with coefficient estimation, making compact per-prediction auditing difficult. Interpretable alternatives impose structural constraints that limit expressiveness: generalized additive models typically restrict interactions to pairwise terms and post-hoc rule extractors produce overlapping rules that hinder compact interpretation. We introduce Residual Pattern Tree Ensemble (RPTE), a three-stage learning approach, that is built on three key principles: bounded feature budget, source disjointness, and separate coefficient estimation. Stage1 builds a supervised symbolic feature vocabulary. Stage2 grows shallow trees under a source-disjointness constraint, where each raw variable is allocated to at most one tree, and retains only the discovered tree structures. Stage~3 solves a single ℓ1-regularized logistic regression over leaf-region indicators, yielding jointly optimal sparse coefficients. This learning approach ensures that every prediction decomposes into an algebraic sum of named, non-overlapping rule contributions, enabling full auditability by design. Empirical evaluation on twelve clinical-domain binary classification benchmarks using repeated stratified 5-fold cross-validation shows that RPTE performs competitively against tuned opaque ensembles and interpretable baselines. RPTE reduces model inspection units by 9× to 87× relative to XGBoost and maintains lower audit complexity than EBM on all 12 datasets. RuleFit requires comparable or fewer inspection units on three datasets where its rule count is small, but without source-disjointness guarantees. The source code is available at this https URL.
Srikumar Krishnamoorthy
Information Systems Area, Indian Institute of Management Ahmedabad, India