ExplAIner：解释分类模型的声明性查询语言

背景

可解释人工智能（XAI）社区已针对机器学习模型预测的解释问题，提出了大量查询类型和评分方法。从数据管理的视角来看，这些层出不穷的解释概念迫切需要一种声明式查询语言，使得各类解释概念能够被统一地定义、组合和分析。然而，现有框架在表达能力与计算可行性上存在根本性局限：例如 FOIL 语言虽旨在为黑盒模型提供可解释性查询，但它无法表达基于最优性（optimality）的核心解释查询，且其在决策树上的评估问题对多项式层级的每一层都是困难的。为了解决这一问题，本文引入 ExplAIner，一种基于 FOIL 扩展词汇与分层结构的声明式查询语言，用于布尔分类模型的解释。

核心内容

本文首先回顾了 FOIL（一种面向黑盒模型的可解释性查询语言），并指出其两大局限：第一，无法表达基于最优性的解释查询（例如需要最小化代价或最大化保真度的查询）；第二，在决策树模型上，FOIL 查询的评估问题对于多项式层级（polynomial hierarchy）的每一层都是困难的，这意味着其计算复杂性极高。

为此，作者提出了 ExplAIner。ExplAIner 在 FOIL 的基础上扩展了词汇表，并采用分层结构。它能够表达广泛的解释概念，包括：

• 溯因解释（abductive explanations）：寻找使模型输出特定决策的最小特征子集；
• 对比解释（contrastive explanations）：解释为何输出为 A 而非 B；
• 基于特征的解释（feature-based explanations）：衡量每个特征对预测的贡献；
• 基于距离的解释（distance-based explanations）：寻找与给定实例最近的反事实。

论文证明了 ExplAIner 中每个查询的评估问题属于 Boolean 层级（Boolean hierarchy），只要基础谓词（basic predicates）能在多项式时间内计算。该性质对于确定性和可分解的布尔电路（deterministic and decomposable Boolean circuits）成立——这类电路涵盖了许多常用的机器学习模型结构。

此外，论文引入了 Opt-FOIL，它是 ExplAIner 的一个面向优化的片段，用于计算关于严格偏序（strict partial orders）最小的解释。Opt-FOIL 的评估问题在同样的可处理性假设下属于 $\mathrm{FP}^{\mathrm{NP}}$ 类。这些复杂性结果具有直接的算法意义：固定一个 ExplAIner 查询可以用固定次数的 SAT 求解器调用来评估，而 Opt-FOIL 中指定的解释概念可以用多项式次数的 SAT 求解器调用来计算。在形式化 XAI 领域，SAT 求解器已成功用于多种机器学习模型类的解释计算，因此该结果极具实践价值。

关键要点

• FOIL 的两大缺陷：无法表达最优性解释查询；在决策树上的评估问题对多项式层级的每一层都是困难的。
• ExplAIner 的设计：以 FOIL 为基础，扩展词汇并引入分层结构，支持溯因、对比、基于特征和基于距离四类主要解释查询。
• 评估复杂性：每个 ExplAIner 查询的评估问题属于 Boolean 层级（等价于多项式层级中的有限层），前提是基础谓词可多项式时间计算；该条件在确定性和可分解布尔电路下成立。
• Opt-FOIL 片段：专为计算最小化严格偏序的解释而设计，其评估问题属于 $\mathrm{FP}^{\mathrm{NP}}$（多项式次数的 NP 预言机调用）。
• 算法后果：固定 ExplAIner 查询可通过常数次 SAT 调用完成评估；固定 Opt-FOIL 解释概念可通过多项式次 SAT 调用计算出最优解释。
• 适用性：结果直接适用于形式化 XAI 中常用的模型类，为 SAT 求解器在解释计算中的系统化使用提供了理论保证。

意义与影响

该工作为 XAI 领域提供了一个统一、声明式的查询语言框架，填补了现有语言在表达最优性查询和计算复杂性方面的空白。通过将多种解释概念纳入同一语言并严格刻画其评估复杂度，ExplAIner 使得研究人员和实践者能够以声明式方式指定和比较不同解释方法，而无需为每种解释单独设计算法。Opt-FOIL 则将优化目标与解释计算结合，支持形式化地寻找“最小”解释（例如最简特征集或最近反事实）。论文的复杂性结果不仅证明了 ExplAIner 在多种重要模型类上的可计算性，还直接给出了基于 SAT 求解器的具体算法策略——这对于实际系统中的可解释性引擎设计具有重要的指导意义。未来，该语言有望扩展到更一般的模型类（如回归模型、概率模型），并集成到现有的机器学习工作流中。