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.

翻译：形式化XAI社区已研究了大量旨在理解决策树分类的可解释性查询。然而，对于这些传统上被视为易于解释的模型，我们究竟能回答哪些问题，目前仍缺乏更统一的理解。作为理解可解释性统一语言的初步尝试，Arenas等人（2021）提出了FOIL——一种用于解释黑盒机器学习模型的逻辑，并证明其能表达多种可解释性查询。然而，我们发现FOIL在两个方面存在局限：（i）其表达能力不足以捕获某些关键查询，（ii）其模型无关的特性导致决策树上的计算复杂度较高。本文精心构造了一阶逻辑的两个片段，用于高效解释决策树：Q-DT-FOIL及其优化变体OPT-DT-FOIL。我们提出的逻辑不仅能表达先前文献中考虑的各种可解释性查询，还能优雅地允许用户指定所求解释应优化的不同目标。利用有限模型论技术，我们证明了Q-DT-FOIL的不同组成部分对其表达能力是必要的，同时Q-DT-FOIL中的查询可通过多项式次数的SAT求解器调用进行评估，其优化版本OPT-DT-FOIL亦如此。除理论结果外，我们还提供了基于SAT的OPT-DT-FOIL评估实现，该实现在工业规模决策树上性能表现优异。