这篇论文提出了一种新查询语言ExplAIner，能统一处理各种模型解释查询，还证明计算效率高，对做形式化XAI的人很有用。
论文提出ExplAIner查询语言，可统一表达溯因、对比、特征和距离等多种解释查询。它基于FOIL语言扩展，解决了FOIL无法表达最优性解释查询且决策树评估复杂的问题。ExplAIner的查询评估属于布尔层次结构，对确定性可分解布尔电路可在多项式时间内完成。引入优化片段Opt-FOIL，可通过固定次数SAT求解器调用计算最小解释。
ExplAIner: A Declarative Query Language for Explaining Classification Models
The XAI community has studied a wide range of queries and scores for explaining predictions of ML models. From a data management perspective, this proliferation of explanation notions calls for declarative query languages in which such notions can be specified, combined, and analyzed uniformly. In this paper, we develop such a framework for Boolean models. We first revisit FOIL, an interpretability query language for black-box models, and show that it has two fundamental limitations: it cannot express central optimality-based explanation queries, and its evaluation problem over decision trees is hard for every level of the polynomial hierarchy. We then introduce ExplAIner, a query language based on FOIL with an extended vocabulary and a layered structure. We show that ExplAIner can express a broad family of explanation notions, including abductive, contrastive, feature-based, and distance-based queries. We also prove that the evaluation problem for each query in ExplAIner belongs to the Boolean hierarchy over every class of Boolean models for which some basic predicates can be evaluated in polynomial time. In particular, that property holds for deterministic and decomposable Boolean circuits. Finally, we introduce Opt-FOIL, an optimization-oriented fragment of ExplAIner for computing explanations that are minimal with respect to strict partial orders, and prove that its evaluation problem is in $\mathrm{FP}^{\mathrm{NP}}$ under the same tractability assumptions. These complexity results have a direct algorithmic consequence: a fixed ExplAIner query can be evaluated with a fixed number of calls to a SAT solver, while a notion of explanation specified in Opt-FOIL can be computed with a polynomial number of such calls. This is particularly relevant in formal XAI, where SAT solvers have been successfully used to compute explanations for several classes of ML models.