用于Horn逻辑推理的高质量嵌入

# 用于Horn逻辑推理的高质量嵌入\titletag
来源：https://arxiv.org/html/2605.20467
计算机科学与工程系113 Research DrBethlehemPA18015\\NameYasir White\\Emaily\.white005@gmail\.com \\addr洛杉矶皮尔斯学院计算机科学系6201 Winnetka AveWoodland HillsCA 91367\\NameDean Clark\\Emaildmc227@lehigh\.edu \\addr里海大学计算机科学与工程系113 Research DrBethlehemPA18015\\NameJoseph Sanchez\\Emailjrs225@lehigh\.edu \\addr里海大学计算机科学与工程系113 Research DrBethlehemPA18015\\NameJevon Lipsey\\Emailjevonlipsey1029@gmail\.com \\addr科罗拉多学院计算机科学系14 E Cache La Poudre StColorado SpringsCO 80903\\NameAshely Hirst\\Emailash320@lehigh\.edu \\addr里海大学计算机科学与工程系113 Research DrBethlehemPA18015\\NameJeff Heflin\\Emailheflin@cse\.lehigh\.edu \\addr里海大学计算机科学与工程系113 Research DrBethlehemPA18015

###### 摘要

可以训练神经网络对逻辑推理器所做出的选择进行排序，从而更有效地搜索答案。此过程的关键步骤是创建有用的嵌入，即逻辑语句的数值表示。本文介绍并评估了几种创建嵌入的方法，这些方法能带来更好的下游结果。我们使用三元组损失训练嵌入，这需要由锚点、正例和负例组成的示例。我们引入了三个想法：生成更可能包含重复项的锚点；以一种确保简单、中等和困难示例之间良好平衡的方式生成正例和负例；以及在训练过程中定期强调最困难的示例。我们进行了多项实验来评估这种方法，包括在不同知识库之间比较不同的嵌入，试图确定哪些特征使嵌入特别适合特定的推理任务。

## 1 引言

可以训练神经网络对逻辑推理器所做的选择进行排序，从而更有效地搜索答案。

几位研究人员探索了是否可以使用机器学习来改进一阶推理的性能，类似于AlphaGo使用深度学习改进AI游戏玩法。已有一些有希望的结果，但仍有许多工作要做。我们假设解决这个问题的最佳途径是解决三个子问题：表示、学习策略和控制策略。为了使问题更易于研究，我们已将初步研究限制在一阶逻辑的Horn片段。

这项工作为逻辑推理的通用神经符号方法做出了贡献，该方法包含三个关键组成部分：1) 将逻辑语句映射到向量的嵌入模型，2) 表示路径通向成功答案可能性的评分模型，以及 3) 引导推理器，其中神经模型对反向链接推理器的选择进行评分。我们之前的工作侧重于改进评分模型和引导推理器；此处，我们尝试不同的嵌入模型训练方法，以学习更有用的嵌入并提高整体性能。本文扩展了之前在研讨会上展示的工作。

具体来说，我们的贡献是 1) 对学习逻辑语句嵌入模型的过程进行了三项改进，2) 评估了嵌入使用下游评分模型提高推理效率的能力，以及 3) 调查了特定嵌入在不同知识库(KB)中有用的原因。

## 2 背景

神经符号 AI 旨在“将基于神经网络的方法与基于符号知识的方法相结合”。这涵盖了广泛的主题，从生成知识图谱的嵌入到训练神经网络预测一个逻辑语句是否蕴含另一个。早期尝试结合逻辑规则和神经网络的方法之一是 KBANN。KBANN 接受命题 Horn 规则并将其直接编码到神经网络中。Kijsirikul2016 训练了一个能够对一阶逻辑数据进行归纳学习的神经网络。然而，他们的架构只允许输入表示原子合取的数据，输出是一组类别。没有方法将公理纳入他们的推理中。rocktaschel2017 训练了一个神经网络来执行合一，并应用类似反向链接的过程来预测知识库中缺失的原子。

存在一些尝试利用大型语言模型的推理器。AlphaGeometry 生成证明来解决奥林匹克几何问题。它使用前向推理从起始前提中找出结论，然后使用语言模型生成辅助点，如果当前证明空间失败，则重试前向推理。AlphaGeometry 并非查询驱动，而是穷举地推导出新语句。ReProver 是另一个基于 LLM 的定理证明器，用于 LeanDojo，它从大型数学库中选择前提。ReProver 使用 LLM 对检索到的前提进行评分。使用这些方法固有的条件是拥有对 LLM 的无限制访问权限，并能够根据推理需求对其进行微调。

其他研究人员在自动定理证明的背景下使用了各种逻辑语句的表示方法。Jakubův 和 Urban 使用一种基于长度为三的项遍历的方法。他们解析每个逻辑语句，为其创建一个有向图，然后从图中提取每三个节点的序列并为其创建一个代码。该代码为每个可能的序列设置一个维度；因此，对于词汇表 Σ，向量必须具有 |Σ|^3 个维度。这种方法无法扩展到具有许多常量的知识库。

Crouse_Abdelaziz_Makni_Whitehead_Cornelio_Kapanipathi_Srinivas_Thost_Witbrock_Fokoue_2021 提出了一种基于链的方法，该方法从类似于 Jakubův 和 Urban 的图开始，但从子句中提取以谓词开头并以变量或常量结尾的模式。每个序列使用 MD5 进行哈希处理，然后通过模运算将该值进一步减少到 d 个维度。负子句通过连接额外的 d 个维度来表示。创建模式时，所有变量都被替换为符号“\*”。这模拟了变量可以与任何项匹配的语义，但没有模拟如果一个变量在表达式中多次出现，它在每次出现时必须匹配相同的项。此外，哈希和模运算解决了 termwalk 的可扩展性问题，但这确实意味着语句被随机放置在潜在空间中，而不是基于某种内在的相似性概念。

arnold2022 提出可以以保留变量语义的方式学习逻辑原子的嵌入。任何一阶逻辑推理算法使用的核心操作是合一，其中 Unify(α, β) 返回一个替换 σ，使得 ασ = βσ，否则失败。可以通过程序化方式找到一组可合一的原子和另一组不可合一的原子。使用优化三元组损失的神经网络，可以将这些原子映射到嵌入中，使得可合一的原子彼此接近，不可合一的原子彼此远离。我们在后续部分描述 Arnold 和 Heflin 的方法以及我们的改进。

## 3 学习改进逻辑推理

反向链接是一种用于 Horn 逻辑推理的算法，它从目标开始，系统性地通过一系列规则和已知事实向后工作，以确定实现目标所需的条件。传统的反向链接推理器通常依赖于暴力搜索来探索潜在解决方案，这随着复杂性和规模的增加可能导致效率低下。即使只有数千条语句的相对较小的知识库，也可能导致搜索数百万个节点，除非它们是由知识工程师精心设计的。我们之前的工作研究了学习评分模型以指导搜索沿着有希望的路径进行，并比较了基于链、termwalk 和合一作为解决此问题的方法。这项工作改进了先前的合一方法，以学习逻辑语句的有意义的嵌入。

从一个事实和规则的知识库开始，我们使用前向链接推理器从现有信息中推断出新事实。从这些新事实中，我们随机用变量替换常量，并将结果列表分成一百个训练查询和一百个测试查询。然后，我们使用随机化的反向链接推理器解决训练查询，探索在预定义深度限制内通向解的所有可能路径。对于路径中的每个节点，我们为结果分配 ⟨目标, 规则, 分数⟩ 元组。在此，目标指目标查询，规则表示证明中使用的逻辑语句，分数表示规则的可解性，分数为 1 表示成功规则，0 表示未导致解的规则。

首先，我们使用三元组损失学习原子的嵌入。三元组损失需要一组 ⟨锚点, 正例, 负例⟩ 元组，并学习将锚点靠近正例、远离负例的嵌入。Arnold 和 Heflin 原始的训练嵌入模型方法涉及随机生成一个原子列表，对于每个原子，从同一列表中选择一个可合一的原子作为正例，选择一个不可合一的原子作为负例。锚点、正例和负例原子使用一个最小化三元组损失的三层网络映射到 50 维嵌入空间。

其次，使用嵌入模型将 ⟨目标, 规则, 分数⟩ 元组转换为向量。最后，使用带有两层神经网络的有监督学习来训练评分模型。初始实验表明，学习到的模型通常可以显著减少反向链接搜索，有时甚至减少一个数量级或更多。然而，对于某些查询甚至某些知识库，未能实现改进。

## 4 我们的方法

在本文中，我们尝试了三种技术来改进嵌入模型及其下游性能。

首先，我们增加了生成更多带重复项原子的可能性。其次，我们定义了一种平衡的三元组生成方法，确保简单和困难训练示例的良好混合。第三，我们定期在具有最高损失的样本上训练模型。

### 4.1 生成带有重复项的原子

我们将重复项原子(RTA)定义为逻辑事实，这些事实不是由均匀分布频繁产生的，但具有嵌入模型应学习的额外语义。例如，loves(X, X) 可以与比 loves(X, Y) 少得多的原子合一。最初，在我们均匀随机生成的情况下，存在第二个项重复的概率是 1/4(1/v + 1/c)，当变量数 v 为 10 且常量数 c 为 200 时，计算出的概率为 2.6%。我们修改锚点生成过程，以固定的概率生成重复项。如果随机原子的元数 ≥ 2，则“重复机会”决定下一个项是前面项重复的可能性。例如，对于一个样本词汇表，先前的嵌入方法仅在 10,000 个原子中生成 110 个带有重复常量或变量的原子。通过创建 15% 的额外重复机会，我们能够生成 3.3 倍以上的带有重复项的原子。注意，由于此过程仅适用于元数 ≥ 2 的原子，因此生成的重复项原子少于所有锚点的 15%。实验表明，这个 15% 的值提高了我们嵌入模型和引导推理器的整体性能。

### 4.2 基于难度的平衡三元组生成

我们提出了一种生成三元组的新颖方法。首先，通过修改锚点的不同组成部分，我们创建简单和困难难度级别的正例（即可合一原子）和负例（即不可合一原子）。例如，给定一个锚点原子如 mom(X, john)，可以通

过进行微小的修改（例如，将 X 替换为一个常量，如 mary）来创建简单的正例，得到 mom(mary, john)。相反，困难的正例是通过更大的修改生成的，例如将 X 和 john 都替换为新的变量（如 Y 和 Z），得到 mom(Y, Z)。通常，要从锚点推导出正例原子，我们可以将变量替换为另一个变量或常量，反之亦然。结构变化的程度决定了难度：修改越广泛，正例就越困难。另一方面，生成负例原子时规则是相反的。大的修改，例如将谓词更改为具有不同元数的谓词，通常会产生简单的负例，因为生成的原子与锚点非常不同且无法合一。相反，小的修改——例如将一个常量替换为另一个——通常会产生困难的负例，因为修改后的原子可能在表面上与锚点相似，但仍然不可合一。这些细微的区别迫使模型学习区分表面上相似但逻辑上不相容的原子所需的细微结构线索。附录中的表 LABEL:tab:anchor_policies_map 和 6 概述了锚点原子的结构类型以及用于生成示例的转换策略。具体来说，表 LABEL:tab:anchor_policies_map 将具有一元和二元谓词的锚点原子分为七种结构类型，而表 6 详细说明了用于创建简单和困难正例/负例的转换策略。这些生成的原子构成了构建训练三元组的基础。

随后，我们通过将每个锚点与正例和负例系统地组合，构建了三种难度级别的三元组。我们定义了三个类别：简单三元组的形式为 ⟨锚点, 简单正例, 简单负例⟩：正例在结构和语义上与锚点接近，而负例明显不同。因此，锚点-正例距离小，锚点-负例距离大，两者之间的边际宽。这种强烈的对比提供了可靠的训练信号，帮助模型建立基本的判别边界，并为学习更复杂的结构区别奠定基础。中等三元组的形式为 ⟨锚点, 简单正例, 困难负例⟩ 或 ⟨锚点, 困难正例, 简单负例⟩：一个示例在结构上与锚点接近，而另一个则更远。因此，正例和负例原子之间的边际比简单三元组更窄，要求模型做出更细致的区分。最后，困难三元组的形式为 ⟨锚点, 困难正例, 困难负例⟩，对三元组损失提出了更大的挑战。困难正例在逻辑上与锚点可合一，而困难负例则不可合一。