A Uniform Language to Explain Decision Trees

The formal XAI community has studied a plethora of interpretability queriesaiming to understand the classifications made by decision trees. However, amore uniform understanding of what questions we can hope to answer about thesemodels, 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 expressiveenough to capture some crucial queries, and (ii) its model agnostic natureresults in a high computational complexity for decision trees. In this paper,we carefully craft two fragments of first-order logic that allow forefficiently interpreting decision trees: Q-DT-FOIL and its optimization variantOPT-DT-FOIL. We show that our proposed logics can express not only a variety ofinterpretability queries considered by previous literature, but also elegantlyallows users to specify different objectives the sought explanations shouldoptimize for. Using finite model-theoretic techniques, we show that thedifferent ingredients of Q-DT-FOIL are necessary for its expressiveness, andyet that queries in Q-DT-FOIL can be evaluated with a polynomial number ofqueries 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 theevaluation for OPT-DT-FOIL that is performant on industry-size decision trees.