ExplAIner：一种用于解释分类模型的声明式查询语言

# ExplAIner：一种用于解释分类模型的声明式查询语言

来源：https://arxiv.org/html/2607.06407  
Pablo Barceló，智利天主教大学，智利圣地亚哥  
Diego Bustamante，智利天主教大学，智利圣地亚哥  
Jose Caraball，智利天主教大学，智利圣地亚哥  
María Alejandra Schild，智利天主教大学，智利圣地亚哥  
以及 Bernardo Subercaseaux，卡内基梅隆大学，美国宾夕法尼亚州匹兹堡  

###### 摘要。可解释人工智能（XAI）社区已经研究了大量用于解释机器学习模型预测的查询和评分。从数据管理的角度来看，这种解释概念的激增呼唤一种声明式查询语言，使得这些概念可以被统一地指定、组合和分析。在本文中，我们为布尔模型开发了这样一个框架。我们首先重新审视 FOIL，一种用于黑盒模型的可解释性查询语言，并证明它有两个根本性局限：它无法表达基于最优性的核心解释查询，并且它在决策树上的评估问题对于多项式层次结构的每一层都是困难的。然后，我们引入 ExplAIner，一种基于 FOIL 并具有扩展词汇和分层结构的查询语言。我们证明 ExplAIner 能够表达广泛的解释概念，包括溯因查询、对比查询、基于特征的查询和基于距离的查询。我们还证明，对于任何一类布尔模型，只要其基本谓词可以在多项式时间内求值，ExplAIner 中每个查询的评估问题都属于布尔层次结构。特别地，该性质适用于确定性和可分解的布尔电路。最后，我们引入 Opt-FOIL，这是 ExplAIner 的一个面向优化的片段，用于计算关于严格偏序最小的解释，并证明在相同的可处理性假设下，其评估问题属于 $\mathrm{FP}^{\mathrm{NP}}$。这些复杂性结果有一个直接的算法推论：一个固定的 ExplAIner 查询可以通过固定次数的 SAT 求解器调用来求值，而 Opt-FOIL 中指定的一种解释概念则可以通过多项式次数的此类调用来计算。这对于形式化 XAI 尤其重要，因为 SAT 求解器已成功用于计算多类机器学习模型的解释。

## 1. 引言

#### 可解释性作为查询语言问题。机器学习模型在决策系统中的日益广泛使用，催生了对理解这些模型预测结果的基本原则性方法的迫切需求。这种需求引发了可解释人工智能（XAI）领域的大量工作（Gunning and Aha, 2019；Guidotti et al., 2019；Arrieta et al., 2020；Molnar, 2022），尤其是产生了各种旨在识别模型为何以特定方式对给定输入进行分类的查询、评分和解释概念（Marques-Silva, 2023, 2024；Darwiche, 2023）。例如，溯因解释、对比解释、反事实风格查询，以及特征必要性或特征相关性概念（Ignatiev et al., 2019；Darwiche and Hirth, 2020；Ribeiro et al., 2018；Huang et al., 2023）。从数据管理的角度来看，这种解释概念的激增提出了一个自然的问题：与其为每个解释任务设计单独的算法或形式体系，能否开发一种声明式语言，让用户通过它指定他们正在寻找什么样的解释？这与数据库领域的悠久传统是一致的：复杂的计算任务通过具有良好定义语法和语义的查询语言来呈现，而对它们表达能力与评估复杂性的研究则提供了关于可以问什么以及回答有多困难的原则性理解（Abiteboul et al., 1995；Kanellakis, 1990；Vardi, 1982；Papadimitriou and Yannakakis, 1999）。在这种观点下，模型成为对其提出查询的对象，而解释概念则成为在该对象上求值的固定查询（Arenas et al., 2021a；Arenas, 2024）。这种视角有几个优点。首先，它提供了一个统一框架来比较和组合解释概念。这一点很重要，因为并不存在一种最适合所有用户、所有模型或所有应用场景的单一解释概念；在许多情况下，最具信息量的解释是通过组合多个标准获得的（Doshi-Velez and Kim, 2017；Marques-Silva and Ignatiev, 2023）。其次，它使得可以通过标准数据库理论视角（如表达能力和评估复杂性）来研究可解释性（Abiteboul et al., 1995；Vardi, 1982；Libkin, 2004）。第三，它为开发面向可解释性查询语言操作符的通用优化技术打开了大门。这类技术可以同时降低多个可解释性查询的评估时间，而不是孤立地处理每个查询。

在这种框架中，一个核心问题是如何衡量查询评估的复杂性。由于一个解释概念应由语言的固定公式指定，因此适当的衡量标准是数据复杂性：查询是固定的，而输入由模型表示和待解释的实例组成（Vardi, 1982）。从这个角度来看，多项式时间的数据复杂性是理想的，但它并非唯一有意义的可处理性目标。许多解释任务本质上是计算密集型的（Barceló et al., 2020；Wäldchen et al., 2021），因此一个有用的可解释性语言还应当允许受控形式的非多项式复杂性。特别是，$\mathrm{P}^{\mathrm{NP}}$ 层次的数据复杂性仍然是一个合理且有用的目标：它对应于通过多项式次数的 NP 预言机调用进行的计算，并且与使用 SAT 求解器作为评估引擎兼容。这种复杂性水平在我们的设定中尤为合适，因为输入是模型表示，而不是传统意义上的数据库实例。与大型关系数据库不同，形式化可解释性中通常考虑的基于树的模型往往规模适中，并且基于 SAT 的方法已成功用于计算此类模型的解释（Ignatiev and Silva, 2021；Izza and Marques-Silva, 2021；Yu et al., 2020）。因此，在本文中，我们将多项式时间和 $\mathrm{P}^{\mathrm{NP}}$ 视为可解释性查询语言理想的数据复杂性界限。

#### 迈向模型可解释性的声明式语言。Arenas 等人（2021a）迈出了第一步，他们引入了 FOIL，一种用于查询机器学习模型的一阶可解释性逻辑。FOIL 是模型无关的：它将模型视为黑盒，并提供对其正实例以及部分实例上的自然包含关系的访问。这种简单的设计使 FOIL 成为一种有吸引力的基础语言，并且它足够表达，能够捕捉若干基本解释概念。然而，模型无关性也有局限性。如果语言太弱，它将无法表达实践中核心的解释概念；如果它过于无约束，其评估问题可能变得过于复杂，无法支持数据库导向框架所期望的查询评估。因此，挑战在于设计一种能平衡两个要求的语言：一方面，它应有足够的表达力来捕获广泛的解释查询，包括基于最优性的概念，如最小或最大解释；另一方面，对于相关类别的布尔模型，它应具有良好的评估和计算问题表现。

在本文中，我们通过开发一个用于解释布尔模型的声明式框架来应对这一挑战。我们的设定并不局限于决策树。相反，我们将模型抽象地视为布尔函数，同时也研究具体的表示类别，如确定性和可分解的布尔电路以及决策树。这使得我们可以将解释查询的逻辑规范与评估它们时依赖于表示的复杂性分离开来。从数据库角度来看，这种分离特别自然，因为在数据库中，查询规范与在不同表示类别上的查询评估被当作不同但相关的问题来处理。

#### FOIL 的局限性。我们首先从查询语言设计的角度重新审视 FOIL。我们证明，尽管 FOIL 具有基础性作用，但它并不满足上述要求。首先，FOIL 缺乏表达一些基于最优性的自然解释概念所需的表达能力。特别地，我们证明最小溯因解释不能在 FOIL 中表达，即使底层模型被限制为决策树。这表明该局限并非由复杂模型类别造成，而是语言本身的表达资源不足。其次，FOIL 具有很高的评估复杂性。我们证明，对于多项式层次结构的每一层，都存在一个固定的 FOIL 公式，其在决策树上的评估问题对于该层次是困难的。因此，即使在传统上被视为可解释的模型类别上，不受限制的 FOIL 也无法提供人们从实用的声明式解释语言中期望的那种受控数据复杂性。这补充了早期关于模型可解释性的复杂性理论方法，这些方法研究了在不同模型类别上回答解释查询的难度（Barceló et al., 2020；Wäldchen et al., 2021）。

#### ExplAIner：一种用于解释查询的可处理逻辑。受这些局限性的启发，我们引入了 ExplAIner，一种旨在表达布尔模型上的解释查询，同时保持受控评估复杂性的的一阶逻辑。该语言扩展了 FOIL 的基本词汇，增加了一个根据已定义特征数量比较部分实例的关系。这一扩展对于表达基于基数的最优性条件至关重要，例如最小溯因解释（Barceló et al., 2020；Darwiche and Hirth, 2020）和最大对比解释（Ignatiev et al., 2019；Huang et al., 2023）。ExplAIner 按层次组织。其原子层捕获部分实例的结构性质；其量化层允许公式通过组合原子层的公式与谓词 $\mathsf{AllPos}$ 和 $\mathsf{AllNeg}$ 来引用模型的行为，这两个谓词表达了部分实例的所有完成是否被分类为正或负；其最顶层允许解释属性的布尔组合。这种组织旨在为解释任务提供足够的表达能力，同时保持评估的可控性。我们证明 ExplAIner 能够表达本文中研究的解释概念，包括弱溯因解释、溯因解释和最小溯因解释（Ignatiev et al., 2019；Darwiche and Hirth, 2020；Barceló et al., 2020；Audemard et al., 2022a）；弱对比解释、对比解释和最大对比解释（Ignatiev et al., 2019；Barceló et al., 2020；Darwiche, 2023）；最小所需变更和最大允许变更（Barceló et al., 2020）；以及必要特征和相关特征（Izza et al., 2021；Huang et al., 2023）。同时，我们证明 ExplAIner 的评估问题属于布尔层次结构，适用于所有那些基本 $\mathsf{AllPos}$ 和 $\mathsf{AllNeg}$ 检查是可处理的模型类别。这包括决策树，以及具有适当可处理性性质的更丰富表示类别，例如确定性和可分解的布尔电路（Darwiche and Marquis, 2011；Arenas et al., 2021b）。

#### Opt-FOIL：计算解释。评估只是问题的一部分。一个用于可解释性的语言还应支持解释的计算。为此，我们引入了 Opt-FOIL，这是一个面向优化的片段，由 ExplAIner 的量化层以及一个针对可定义严格偏序的最小化操作符构成。Opt-FOIL 捕获这样的解释任务：寻找一个满足逻辑规范并在用户定义的偏好顺序下最小的对象。这包括标准的子集最小解释、基数最小解释，以及基于距离的概念，如最小所需变更。通过改变顺序，同一形式体系还能够表达基于最大性的概念，例如最大对比解释和最大允许变更。我们对 Opt-FOIL 的主要计算结果是：对于所有 $\mathsf{AllPos}$ 和 $\mathsf{AllNeg}$ 可以在多项式时间内求值的模型类别，其计算问题属于 $\mathrm{FP}^{\mathrm{NP}}$，其中 $\mathrm{FP}$ 是可以在多项式时间内计算的函数类。用上面的术语来说，这意味着计算 Opt-FOIL 中指定的解释具有受控的数据复杂性：公式是固定的，代价是作为模型表示和输入实例的函数来衡量的。这将 Opt-FOIL 置于前面确定为适用于声明式可解释性语言的复杂性体制内，同时允许该语言捕获那些不太可能在完全一般性下承认多项式时间算法的、基于优化的解释任务。

#### 技术贡献。以下是本文的技术贡献。
- 我们证明了 FOIL 在决策树上的评估问题对于多项式层次结构的每一层都是困难的。
- 我们证明了 FOIL 无法表达最小溯因解释，即使是在决策树上。
- 我们引入了 ExplAIner，一种基于 FOIL 但具有额外基数量词的分层逻辑，并且证明了它能够表达广泛的解释概念。
- 我们证明了在决策树和确定性与可分解布尔电路上，ExplAIner 的评估问题属于布尔层次结构。
- 我们引入了 Opt-FOIL，并证明了在相同模型类别上，其计算问题属于 $\mathrm{FP}^{\mathrm{NP}}$。