🤖 AI

Rethinking Explanations: Formalizing Contrast in Description Logics

本文提出了一种面向用户的描述逻辑对比解释框架，该框架通过正式定义和评估如何解释为何某事实成立而非替代性对照项，从而解决了现有证成与溯因推理方法的局限性。

原作者： Yasir Mahmood, Arnab Sharma, Axel-Cyrille Ngonga Ngomo, Balram Tiwari

发布于 2026-05-06

📖 1 分钟阅读☕ 轻松阅读

原作者： Yasir Mahmood, Arnab Sharma, Axel-Cyrille Ngonga Ngomo, Balram Tiwari

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象你正漫步于一座巨大而神奇的图书馆，其中每一本书都代表着一条关于世界如何运作的规则。这座图书馆建立在一种非常严格、逻辑化的语言之上，称为描述逻辑（Description Logic, DL）。在这座图书馆中，计算机可以审视一个人（我们称她为爱丽丝）以及一组规则，然后告诉你：“是的，爱丽丝被录用了！”

旧方法：“为什么？”

通常，如果你问计算机“为什么爱丽丝被录用了？”，它会给你一个理由（Justification）。它会从图书馆中调出那些证明爱丽丝被录用的具体书页。

类比： 这就像老师向你展示数学题的确切步骤，以证明答案是 5。它很准确，但只告诉你关于“赢家”的信息。

新问题：“为什么是爱丽丝而不是鲍勃？”

本文的作者注意到人类有一种自然倾向：我们不仅想知道某事为何发生，还想知道它为何是发生了某事，而不是发生了另一件事。

想象爱丽丝得到了这份工作，但她的朋友鲍勃没有。

如果你问“为什么是爱丽丝？”，计算机列出爱丽丝的优秀技能。
如果你问“为什么不是鲍勃？”，计算机列出鲍勃缺失的技能。
但鲍勃很困惑。 他不想看两份分开的列表。他想知道：“为什么是爱丽丝而不是我？”他想看到他们之间的差异。

本文认为，给出两个分开的回答是令人不满意的。你需要一个对比解释（Contrastive Explanation, CE），它能突出两者之间的具体差距。

解决方案：“差异发现者”

研究人员提出了一种新方法，将这种“为什么是 P 而不是 Q？”的问题形式化。他们将发生的事称为事实（Fact）（爱丽丝），将未发生的事称为对照（Foil）（鲍勃）。

为了解释差异，他们考察三个方面：

爱丽丝有而鲍勃没有的：（例如，爱丽丝在人工智能领域发表了论文。）
鲍勃有而爱丽丝没有的：（例如，鲍勃在纯数学领域发表了论文。）
鲍勃缺失的、若具备本可使其被录用的：（例如，鲍勃需要在人工智能领域发表论文。）

富有创意的类比：赛跑
想象爱丽丝和鲍勃之间的一场赛跑。

事实： 爱丽丝赢了。
对照： 鲍勃输了。
旧解释： “爱丽丝跑得快。”（这是真的，但无法解释鲍勃为何输了。）
新对比解释： “爱丽丝跑得快，因为她在山丘上训练，而鲍勃在平地上训练。如果鲍勃在山丘上训练（缺失的部分），他本会赢，但他没有。”

本文通过取爱丽丝的“证明”和鲍勃的“证明”（尽管鲍勃的证明是假设性的），并找出它们的对称差，将这一过程形式化。他们剔除了两人共有的部分（例如“两人都具备资格”），只关注决定结果的那些独特因素。

“如果”情景（溯因）

有时，计算机必须猜测什么条件会使对照（Foil）成立。这被称为溯因（Abduction）。

类比： 如果鲍勃没有被录用，计算机就会问：“鲍勃要被录用，什么条件必须成立？”它可能会说：“如果鲍勃在人工智能领域发表了论文。”
本文的方法将爱丽丝的真实证明与鲍勃的“如果”情景相结合，以精确展示两条路径在何处分叉。

处理故障（不一致性）

有时，图书馆里的规则很棘手。如果规则说“你不能同时是人工智能专家和理论家”呢？

如果鲍勃是理论家，而计算机说“如果鲍勃是人工智能专家，他就会被录用”，这就产生了冲突。
本文增加了一个安全网：它识别这些冲突。它会告诉你：“如果鲍勃是人工智能专家，他本会被录用，但是这与他作为理论家的本性相矛盾。”这防止了解释破坏图书馆的逻辑。

他们实际做了什么

作者们不仅撰写了理论，还构建了一个原型（一个可运行的计算机程序）来测试它。

他们在约 40 个不同的现实世界知识库（如医学或技术数据库）上进行了测试。
他们发现，他们的方法运行迅速（大多数情况下不到一秒），并生成非常简短、易于阅读的解释（通常仅 1 到 2 句逻辑语句）。
他们在数学上证明，对于某些类型的逻辑（称为EL），该过程是高效的，不会陷入无限循环。

总结

本文旨在升级计算机解释决策的方式。他们不再仅仅说“这是 X 发生的原因”，而是说“这是 X 发生而不是 Y的原因”。他们通过数学方法比较“获胜”证据与“失败”（或假设性）证据，剔除共同部分，并精确展示造成差异的关键因素。他们构建了实现这一功能的工具，该工具能在复杂数据上快速且准确地运行。

技术摘要：重新思考解释：描述逻辑中的对比形式化

问题陈述
现有的描述逻辑（DL）知识库（KB）的解释形式化主要侧重于理由（解释为何公理 $P$ 为真）和溯因推理（解释为何缺失的公理 $P$ 可能为真）。然而，这些方法缺乏以用户为中心的视角。它们未能解决询问者的特定认知需求，而询问者往往因为预期了替代事件 $Q$ 而对事实 $P$ 感到惊讶。分别为“为何 $P$ "和“为何非 $Q$ "提供解释通常令人不满意，因为用户希望理解实际结果与预期替代方案之间的具体差异。尽管对比解释（CEs）在机器学习和论证框架中已得到充分研究，但在描述逻辑（DLs）的背景下，它们仍未得到充分探索，尽管 DLs 是本体（如 OWL）的基础，而这些本体被用于医疗保健（例如 SNOMED CT）等关键领域。

方法论
作者提出了一个在 DL KB 中生成对比解释的形式化框架，将彼得·利普顿（Peter Lipton）的对比解释哲学模型适应于 DLs 的逻辑环境。

对比问题（CQs）的形式化：
CQ 被定义为一对 $(P, Q)$ ，其中 $P$ 是一个事实（一个蕴含的 ABox 断言，例如 $C(x)$ ），而 $Q$ 是一个反事实（一个未蕴含的断言）。本文重点关注两种特定类型的反事实：
- 实体对比： $Q$ 是 $C(y)$ ，将同一概念与不同个体进行对比。
- 概念对比： $Q$ 是 $D(x)$ ，将不同概念与同一主体进行对比。
定义对比解释（CE）：
作者超越了 $P$ 的理由与 $Q$ 的溯因假设之间的简单对称差异。他们基于三个原则引入了元组定义 $E = \langle E_{fact}, E_{foil+}, E_{foil-} \rangle$ （并可选地包含冲突集 $C$ ）：
- 差异条件： 解释必须引用 $P$ 的理由与 $Q$ 缺失事实之间的差异。
- 已知与假设知识： 解释必须区分在 KB 中关于反事实为真的公理（ $E_{foil+}$ ）与蕴含反事实所需的缺失公理（ $E_{foil-}$ ）。
- 处理相似公理： 该框架引入了“重命名集差”算子（ $\ddagger$ ）。该算子移除事实与反事实之间结构相似的公理（例如 $C(x)$ 与 $C(y)$ ，或 $E \sqsubseteq C$ 与 $E \sqsubseteq D$ ），以确保解释仅突出区分因素。
处理不一致性：
如果添加反事实的缺失公理（ $E_{foil-}$ ）与现有 KB 产生冲突，该框架包含一个冲突集 $C$ 。该集表示必须移除的现有 ABox 断言的最小子集，以使反事实得以蕴含，从而有效地模拟反事实场景。
偏好标准：
为了在多个可能的 CEs 中进行选择，作者提出了一种句法发散度量（ $\sigma_{div}$ ）。该度量衡量与事实相关的公理与与反事实相关的公理之间的对称差异。首选的 CE 是使这种发散最小化的 CE，尽可能使事实和反事实的推理结构对齐，以促进比较。

主要贡献

形式化定义： 本文提供了 DL KB 对比解释的首个形式化定义，具体解决了实体对比和概念对比。
通用方案： 它提出了一个整合理由和溯因假设的 CE 通用方案，同时区分真实断言和缺失断言。
复杂度分析： 作者分析了两种 DL 中 CEs 的计算复杂度：
- $\mathcal{EL}$ ： 他们证明，对于概念对比，决定给定大小的 CE 是否存在是NP 完全的。然而，对于实体对比，具有 0 发散度的 $\sigma_{div}$ 首选 CE 可在多项式时间内计算。
- $\mathcal{ALC}$ ： 决定给定大小的 CE 是否存在的问题被证明是ExpTime 完全的。
实现与评估： 开发了一个基于 Java 的原型实现（使用 OWL API 和 ELK 推理机）。实验在约 41 个现实世界的 OWL KB 上进行。

结果
实验评估得出以下发现：

效率： 原型高效地计算 CEs，平均运行时间约为 392 毫秒。
解释大小： 生成的解释紧凑，通常最多跨越四个 ABox 公理。
共性： “公理共性比率”（事实与反事实理由之间的重叠）被发现较低（平均 13.5%），表明在许多情况下，事实和反事实依赖于不同的断言集。
一致性： 冲突率较低（4.00%），表明在大多数情况下，反事实的缺失公理不与现有 KB 矛盾。

意义与主张
本文声称通过将对比解释引入描述逻辑领域，填补了文献中的一个重大空白。作者认为，这种方法通过显式建模询问者的预期（反事实），提供了一种更直观、以用户为中心的方式来解释推理结果。

这项工作被呈现为该领域的一个初步步骤。作者谦逊地指出，虽然他们的定义扩展到任何支持溯因假设的 DL，但还需要进一步的工作来处理更具表达力的 DL（例如带有基数限制的 DL），并开发能够高效扩展到大型数据集的算法。他们还指出，需要未来的用户研究来验证这些对比解释是否确实比标准理由更受终端用户青睐。本文结论认为，其框架提供了一个严格的、形式化的机制，用于组合理由以解释事实与反事实之间的差异，为语义网应用中的更明智决策奠定了基础。