A Uniform Language to Explain Decision Trees

TL;DR

This work introduces a uniform language for explaining decisions in decision trees by refining the FOIL framework into the tree-specific DT-FOIL family. It identifies FOIL’s expressiveness and tractability gaps and addresses them with guarded quantification in $\textsc{DT-FOIL}$, plus two practical extensions, $\textsc{Q-DT-FOIL}$ and $\textsc{Opt-DT-FOIL}$, which support unbounded quantification without triggering intractable evaluation and enable optimization over explanations. The authors provide theoretical analyses of expressiveness and complexity, showing polynomial-time evaluability for guarded formulas and bounded NP oracle usage for the extended queries, with BH classifications for the evaluation problems. They also implement a SAT-based prototype, including a simplifier and encoder, and demonstrate scalability to industry-size trees, validating the approach’s practicality for complex interpretability tasks. Collectively, the work yields a principled, scalable framework for expressive, user-guided explanations of decision trees, bridging formal logic and practical XAI tooling."

Abstract

The formal XAI community has studied a plethora of interpretability queries aiming to understand the classifications made by decision trees. However, a more uniform understanding of what questions we can hope to answer about these models, traditionally deemed to be easily interpretable, has remained elusive. In an initial attempt to understand uniform languages for interpretability, Arenas et al. (2021) proposed FOIL, a logic for explaining black-box ML models, and showed that it can express a variety of interpretability queries. However, we show that FOIL is limited in two important senses: (i) it is not expressive enough to capture some crucial queries, and (ii) its model agnostic nature results in a high computational complexity for decision trees. In this paper, we carefully craft two fragments of first-order logic that allow for efficiently interpreting decision trees: Q-DT-FOIL and its optimization variant OPT-DT-FOIL. We show that our proposed logics can express not only a variety of interpretability queries considered by previous literature, but also elegantly allows users to specify different objectives the sought explanations should optimize for. Using finite model-theoretic techniques, we show that the different ingredients of Q-DT-FOIL are necessary for its expressiveness, and yet that queries in Q-DT-FOIL can be evaluated with a polynomial number of queries to a SAT solver, as well as their optimization versions in OPT-DT-FOIL. Besides our theoretical results, we provide a SAT-based implementation of the evaluation for OPT-DT-FOIL that is performant on industry-size decision trees.

Figures (4)

• Figure 1: Illustration of different explanations for decision trees of $500$ leaves over the binarized MNIST dataset deng2012mnist. The explanations are obtained using our implementation over the Opt-DT-FOIL queries described in \ref{['sec:opt-dt-foil']}. \ref{['sub@subfig:msr']} displays a minimum sufficient reason for an image classified as 1, where the white pixels of the original image that are part of the explanation are highlighted in perfect white, and the black pixels that are part of the explanation are highlighted in red. Arguably, this explanation reveals that the model, trained to recognize digit 1, has learned to detect a slanted vertical stripe of white pixels, sorrounded by black pixels. \ref{['sub@subfig:mcr']} shows that adding a single white pixel to the image of a 3 is enough to change its classification (cf. one-pixel attacksSu_2019). Interestingly, \ref{['sub@subfig:mca']} shows that one can simultaneously flip all pixels on an image of digit 8 while retaining its classification, showing the model is somewhat invariant to the roles of white and black pixels in the original image. Finally, \ref{['sub@subfig:dfs']} shows that a subset of the pixels, around the center of MNIST images (colored in yellow), is enough to determine the veredicts of a model trained to detect digit 1. As an application, one could leverage this knowledge to reduce the dimensionality of the dataset by cropping the borders.
• Figure 2: Example of a decision tree of dimension $4$.
• Figure 3: Empirical evaluation of different Opt-DT-FOIL queries over random synthetic data.
• Figure :

Theorems & Definitions (30)

• Theorem 1
• Theorem 2
• Theorem 3
• Proposition 4
• Corollary 5
• Theorem 6
• Theorem 7
• Proposition 8
• Proposition 9
• Theorem 10