Rigorous Explanations for Tree Ensembles

Yacine Izza; Alexey Ignatiev; Xuanxiang Huang; Peter J. Stuckey; Joao Marques-Silva

cs.AIMar 31, 2026

Rigorous Explanations for Tree Ensembles

Authors: Yacine Izza, Alexey Ignatiev, Xuanxiang Huang, Peter J. Stuckey, Joao Marques-Silva

Organizations: National University of Singapore, Singapore · Monash University, Australia · Nanyang Technological University, Singapore · ICREA & Univ. Lleida, Spain

Abstract

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

Panel of Figure 1 — 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.

Panel of Figure 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 $c_{1}$ , $c_{2}$ and $c_{3}$ , and features sepal.length , sepal.width , petal.length and petal.width are ordered, resp., as features 1–4.

Panel of Figure 3 — 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 $c_{1}$ , $c_{2}$ and $c_{3}$ , and features sepal.length , sepal.width , petal.length and petal.width are ordered, resp., as features 1–4.

Panel of Figure 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$ .

Panel of Figure 5 — Figure 5. Reducing example RFmv to RFwv.

Dataset			RFmv			SAT Enc		AXp		CXp		AEx
Dataset	( m	K )	D	#N	%A	( #var	#cl )	Len	Time	Len	Time	AEx
ann-thyroid	( 21	$3$ )	$4$	$2192$	$98$	( 17854	$29\,230$ )	$2.1$	$0.13$	$1.3$	$0.18$	0.277
appendicitis	( 7	$2$ )	$6$	$1920$	$90$	( 5181	$10\,085$ )	$4.0$	$0.03$	$2.4$	$0.06$	0.094
banknote	( 4	$2$ )	$5$	$2772$	$97$	( 8068	$16\,776$ )	$2.0$	$0.02$	$1.0$	$0.08$	0.190
biodegradation	( 41	$2$ )	$5$	$4420$	$88$	( 11007	$23\,842$ )	$16.8$	$0.29$	$4.5$	$0.19$	0.278
ecoli	( 7	$5$ )	$5$	$3860$	$90$	( 20081	$34\,335$ )	$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.

Panel of Figure 6 — Figure 6. Assessing MaxSAT and SMT encodings of BTs for computing AXps.

Panel of Figure 7 — Figure 7. Assessing MaxSAT and SMT encodings of BTs for computing CXps.

Panel of Figure 8 — Figure 8. Assessing MaxSAT and SMT encodings of RFwv for computing AXps and CXps.

Panel of Figure 9 — Figure 9. Ablation study of MaxSAT Approach for BTs.

Panel of Figure 10 — Figure 10. Assessing minimum CXps for RFmv.

Panel of Figure 11 — Figure 11. Assessing minimum CXps for RFwv.

Panel of Figure 12 — Figure 12. Assessing minimum CXps in BTs.

Panel of Figure 13 — Figure 13. Scalability of RC2 and OR-Tools oracles for computing minimum CXp.

Dataset				RFmv		SAT Enc		IF
Dataset	( m	K )	${\mathcal{P}}$	D	%A	( #var	#cl )	Time	Result
adult	( 12	$2$ )	race, gender	$6$	$78.4$	( 6374	$18\,650$ )	$0.128$	unfair
compas	( 11	$2$ )	race, gender	$5$	$58.8$	( 6169	$12\,968$ )	$0.073$	unfair
german	( 21	$2$ )	age, gender	$3$	$70.0$	( 16383	$24\,942$ )	$0.421$	fair
ricci	( 5	$2$ )	race	$3$	$100$	( 6233	$11\,382$ )	$0.052$	unfair

Table 2. Fairness verification benchmarks. Columns m and K report the number of features and classes. Column

{\mathcal{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).

Explore similar work

Leaf Values as Coordinates: Exact Contrastive Explanation for Gradient-Boosted Ensembles
Aug 19, 2026Emanuele LuzioCounterfactual Explanations Algorithmic Recourse
Independent Researcher
Optimal Counterfactual Search in Tree Ensembles: A Study Across Modeling and Solution Paradigms
May 7, 2026Awa Khouna, Youssouf Emine, Julien Ferry +1Counterfactual Explanations Mixed-Integer Linear Programming
Polytechnique Montréal · Ivey Business School
Learning Auditable Classifier Models: Source-Disjoint Tree Ensembles
Aug 16, 2026Srikumar KrishnamoorthyInterpretable ML Ensemble Learning
Information Systems Area, Indian Institute of Management Ahmedabad, India

Aug 19, 2026J/K move · Enter open · S save

Leaf Values as Coordinates: Exact Contrastive Explanation for Gradient-Boosted Ensembles

Emanuele Luzio

Independent Researcher

Counterfactual Explanations Algorithmic Recourse Gradient-Boosted Decision Trees Tabular ML

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

Leaf Values as Coordinates: Exact Contrastive Explanation for Gradient-Boosted Ensembles

Optimal Counterfactual Search in Tree Ensembles: A Study Across Modeling and Solution Paradigms

Learning Auditable Classifier Models: Source-Disjoint Tree Ensembles