Learning higher-order logic programs from failures
从失败中学习高阶逻辑程序
基础：
**摘要**
通过归纳逻辑编程（ILP）学习复杂程序仍然是一个巨大的挑战。现有的启用高阶定义的 ILP 系统在准确性和学习性能上有所改善，但仍然受到基础学习机制的限制。实验结果表明，我们通过高阶定义扩展的多功能失败学习范式显著提高了学习性能，而不需要现有系统所需的繁琐人工指导。我们的理论框架捕捉了一类高阶定义，并保持了现有基于包含关系的剪枝方法的健全性。
**1 介绍**
归纳逻辑编程（ILP）[Mug91, NdW97] 是一种符号机器学习方法，通过背景知识（BK）谓词和一组正负例来学习逻辑程序。乍一看，学习一个接受正整数 n 并返回形式为 [[1], [1, 2], ···, [1, ···, n]] 的列表的逻辑程序似乎不是一个艰巨的学习任务。使用传统的高阶（HO）定义很容易构建出这样的逻辑程序。
第一个迭代产生列表[1, ···, N]，而map对[1, ···, N]中的每个成员应用功能上等效的迭代，从而产生所需的结果。然而，这个看似无害的函数在写成无函数的第一阶（FO）逻辑程序时需要25个文字分散在五个子句中，这对大多数现有FO ILP方法来说是一项艰巨的任务[CDEM21]。
过大的BK在许多情况下可能导致性能损失[Cro20, SKB03]。相比之下，添加HO定义会增加搜索空间的整体大小，但可能导致存在显著简单的解决方案（见图1）。使学习者能够使用HO定义，并且强烈倾向于短解决方案，可以提高性能。我们开发了HO启用的Popper [CM21a]（Hopper），这是一个新颖的ILP系统，旨在学习最优短解决方案。实验表明，在与Popper和表现最好的HO启用ILP系统MetagolHO [CMM20]相比时，硬任务的性能显著更好。见第4节。
现有的HO启用ILP系统基于元解释学习（MiL）[MLPT14]。基于MiL的系统的效率和性能在很大程度上依赖于人类指导的形式，即元规则（HO horn子句的受限形式）。选择这些规则在所有但最简单的情况下都是一种艺术。例如，迭代是三元的（关于FO参数），这对某些系统构成挑战，在HEXMILHO [CMM20]的情况下，这个定义不能考虑，因为只允许二元定义（关于FO参数）。
在微调搜索空间时限制人为参与是实现强符号机器学习的重要一步。通过Popper实现的新颖的从失败中学习（LFF）范式[CM21a]，作为学习过程的一部分修剪搜索空间。这不仅减少了人为指导，还去除了对HO定义结构的限制，使我们能够进一步利用上述好处。
将HO概念集成到基于MiL的系统中非常无缝，因为HO定义本质上是一种特殊类型的元规则。因此，使MiL学习者启用HO只需要对理论基础进行最小的更改。在像Popper这样的LFF学习者的情况下，修剪机制影响可以使用的HO定义（见[CM21a]的第813页）。
我们通过间接添加HO定义来避免这些健全性问题。Hopper使用HO定义的FO实例，每个实例都与一组独特的谓词符号相关联，这些符号表示定义的HO参数。这些谓词符号出现在候选程序中子句的头部文字中，当且仅当其关联的FO实例出现在候选程序中时。因此，只有结构匹配的程序才可能被修剪。我们在第3节进一步检查这个问题，并提供了一个封装接受的HO定义类别的构造。
简洁地说，我们工作在与子sumption和entailment单调的HO定义类别中；p1 ≤θ (|=) p2 ⇒ H(p1) ≤θ (|=) H(p2)，其中p1和p2是逻辑程序，H(·)是合并了p1和p2部分的HO定义。与文献中考虑的类别类似，我们的类别排除了HO否定的大多数情况（见第3.4节）。然而，我们的框架为在实践中发明HO谓词（一个重要的开放问题）提供了机会，尽管这在实践中仍然效率低下，留给未来的工作。
2 相关工作
[CMM20]（第2节）的作者提供了有关高阶（HO）程序合成的文献综述，特别是现有的ILP系统如何处理HO结构。我们提供这项调查的简要总结，并重点介绍最先进系统，即Metagol的HO扩展[CM16]和HEXMIL的HO扩展[KEI18]。此外，我们介绍了Popper[CM21a]，这是Hopper基于的系统。对于感兴趣的读者，最近已经发表了关于ILP研究现状的详细调查[CDEM21]。
2.1 谓词发明和HO合成
有效使用HO谓词与辅助谓词发明（PI）密切相关。以下示例说明了如何结合使用fold/4和PI来提供一个简洁的程序来反转列表：
将p包含在背景知识中是不直观的。可以合理地期望综合器产生它。许多众所周知的非MiL基础ILP框架不支持谓词发明，例如Foil [Qui90]、Progol [Mug95]、Tilde [Blo99] 和 Aleph [Sri01]。尽管在整个ILP的长期历史中，人们对PI一直非常感兴趣，但它仍然是“ILP 20岁”[MRP+12]中讨论的开放问题。从那时起，已经有一些成功的途径。ILASP [Law18]和δILP [EG18]都可以在受限的意义上引入发明的谓词，然而，两者都不处理无限域，也不适合我们正在研究的任务，即树和列表的操作。
在上述任务方面表现最好的系统是Metagol [CM16]和HEXMIL [KEI18]；两者都基于元解释学习（MiL）[MLPT14]，在程序构造的每一步都考虑PI。然而，为了有效的搜索过程，需要强烈的语言偏见。这种语言偏见以元规则[CM14]的形式出现，元规则是HO horn子句的受限形式。
进一步讨论见第2.2节。Popper [CM21a]并不直接支持PI，尽管可以通过语言偏见强制执行PI（Poppi是支持PI的扩展[CM21b]）。Popper的语言偏见虽然部分固定，但本质上是任意的ASP程序。[CM21a]的作者通过提供模拟链元规则的ASP代码来说明这一点（见[CM21a]的附录A）。我们利用这一特性扩展Popper，允许它构建包含HO定义实例的程序。我们的扩展Hopper与Popper相比，在性能上有显著提升。Hopper还超越了通过HO定义扩展的最新MiL基础ILP系统。有关Popper的进一步讨论见第2.3节，有关Hopper的讨论见第3节。
2.2 Metagol和HEXMIL
我们简要总结由A. Cropper等人[CMM20]介绍的现有的能够处理高阶（HO）的ILP系统。
高阶Metagol
简而言之，Metagol是一个使用Prolog元解释器实现的元解释学习器。作为输入，Metagol接收一组形式为body pred(P/n)的谓词声明PD，正例集合E+和负例集合E-，编译后的背景知识BKc，以及一组元规则M。这些示例提供了目标谓词的参数和名称。最初，Metagol尝试使用BKc满足E+。如果失败，则Metagol尝试将当前目标原子与m ∈ M中的元规则统一。此时，Metagol尝试证明元规则m的主体。如果成功，推导提供了一个可以在E-上测试的Prolog程序。如果程序蕴含了E-中的一些内容，Metagol会回溯并尝试找到另一个程序。在证明元规则的主体时，当BKc不足以构建程序时，会引入发明的谓词。
Metagol和MetagolHO之间的区别在于包含了解释性背景知识BKin。例如，map/3作为BKin的形式是：
高阶谓词 `caselist(p[], p[H|T], A, B)` 会在 A 为空时调用 `p[]`，否则调用 `p[H|T]`。我们的 `halflst(A, B)` 定义无法通过标准的搜索过程找到，因为每次调用 `caselist` 都会导致对元解释器证明过程的调用。下划线标记的 `caselist` 调用导致 `p[H|T]` 的 PI 无限循环。同样，除非明确指定，否则初始目标无法被替换。
就像 `halflst(A, B)` 一样，下面定义的 `issubtree(A, B)` 程序计算 B 是否是 A 的子树，需要通过 `any` 递归调用 `issubtree`。
这可以通过使用元类型（参见第4节）来解决，但这不是标准方法，结果会产生强语言偏差，并且并不总是有效。Hopper 成功地学习了这些谓词，没有显著的缺点。
据我们所知，MetagolHO 并未完全支持对发明谓词（BK_in 定义的高阶参数）的否定（参见 [CMM20] 第4.2节）。Hopper 也存在类似的问题，这在第3.4节中进行了讨论。
**高阶 HEXMIL**
HEXMIL 是 Meta-interpretive Learning 的 ASP 编码 [KEI18]。鉴于 ASP 可能比较限制性，HEXMIL 利用 HEX 形式来编码 MiL。HEX 允许 ASP 求解器与外部资源进行接口 [ERS16]。HEXMIL 限于前向链式元规则。
因此，仅可以处理二元学习任务。此外，许多有用的元规则并不符合这种形式，即 `P(A, B) :- Q(A, B), R(A, B)`。HEXMILHO 将高阶定义纳入了定义2的前向链式结构。有关编码的详细信息，请参见 [CMM20] 第4.4节。[CMM20] 的作者展示了 HEXMILHO 在列表操作任务上的较差表现，其局限性使得在感兴趣的任务上应用变得困难。因此，我们在第4节中专注于 MetagolHO。
**2.3 Popper: 从失败中学习 (LFF)**
LFF范式和 Popper 提供了一种基于反例引导的归纳合成 (CEGIS) [SL08] 的归纳逻辑编程新方法。LFF 和实现该方法的系统由 A. Cropper 和 R. Morel [CM21a] 引入。作为输入，Popper 接受一组谓词声明 PD、正例集 E+ 和负例集 E− 以及背景知识 BK，这些是基于推理的 ILP 学习的典型设置 [Rae08]。
在生成阶段，候选程序从可行的假设空间中选择，即尚未被生成约束排除的程序空间。然后，选定的程序在测试阶段与 E+ 和 E− 进行测试。如果候选假设仅对部分 E+ 和/或部分 E− 进行推理，Popper 会构建约束（约束阶段），进一步限制生成阶段搜索的可行假设空间。当候选程序仅对 E+ 进行推理时，Popper 终止。
Popper 在有限的假设空间中进行搜索，该空间由语言偏差的特征（即体谓词的数量、变量等）进行参数化。重要的是，如果在这个参数化的假设空间中存在最优解，Popper 将找到它（定理 1l [CM21a]）。最优解被定义为包含最少文字的解 [CM21a]。
这一生成、测试、约束循环的关键方面是约束的选择。根据候选程序在测试阶段的表现，Popper 引入约束，修剪候选程序的特殊化和/或概化。特殊化/概化通过 Θ-包含 [Plo70, Rey70] 定义。Popper 还可能引入消除约束，修剪可分离的子句集。
有关这种方法的好处的详细信息见 [CM21a]。本质上，Popper 精炼的是假设空间，而不是程序 [Sri01, Mug95, QCJ93]。
除了在搜索过程中引入的约束外，与大多数 ILP 系统一样，Popper 还包含一种形式的语言偏差 [NCWSC97]，即假设空间的预定义语法和/或语义限制。Popper 最基本的要求是谓词声明，即谓词是否可以在子句的头部或体部使用，以及谓词可以出现的参数个数。Popper 还接受类似模式声明的假设约束 [Mug95]，这些声明为给定谓词的每个参数定义了类型和方向。额外的假设约束可以被表述为 ASP 程序（参见第2.1节）。
Popper 实现了生成、测试、约束循环，使用了多次解算框架 [GKKS19] 和将确定性逻辑程序及约束编码到 ASP [Lif19] 范式中的方法。语言偏差以及生成的约束被编码为 ASP 程序。ASP 解算器在此程序上运行，得到的模型（如果存在的话）即为候选程序的编码。
**3 理论框架**
我们简要概述了逻辑编程。我们的阐述远非全面。有关详细信息，请参见更为详细的资料 [Llo87]。
3.1 基础知识
**3.2 可解释理论与实例化**
我们的假设空间由一种特定类型的理论组成，我们称之为可解释理论（interpretable theories）。从这些理论中，可以推导出所谓的“主要程序”（principal programs），即一阶（FO）子句理论，这些理论编码了某些字面（literals）和子句之间的关系以及一组高阶定义。Hopper 生成和测试主要程序。这种编码保留了 [CM21a] 中提出的修剪机制的有效性。直观上，这种有效性来源于每个主要程序编码了一个唯一的高阶程序。这个方法的一个结果是，每个高阶程序可能由多个主要程序编码，其中一些可能互不包含在一个包含关系中，即它们不是相互可修剪的。这导致了一个更大但更具表达力的假设空间。
**3.3 可解释理论与约束**
第2.3节中的约束基于 Θ-子集关系 (Θ-subsumption)。
给定一个库 L 和一个 L 兼容理论的空间，我们可以使用 Θ-子集关系来比较 L-归约，并根据测试阶段的结果来修剪泛化（特化）。
**归约与消除约束**
在生成阶段，消除约束用于修剪可分离的程序（参见脚注 5）。虽然 L-归约是非分离的，因此在存在消除约束的情况下避免修剪，但查询 ASP 求解器的 L-归约效率低下。ASP 求解器必须了解库及其如何包含定义。此外，库必须以适合 ASP 的形式编写 [CM21a]。
因此，我们查询 ASP 求解器以获取主程序。库 L 中的定义被视为背景知识（BK）。考虑示例 3，在生成阶段，ASP 求解器可能返回以下子句的编码：
在测试阶段，L-归一化的其余部分被重新引入。虽然这消除了低效性，但上述程序现在可以被分离，并且可能会被剪枝。为了有效地实现高阶合成，我们在有库的情况下放宽了消除约束。相反，我们引入了所谓的调用图约束，定义了高阶文字和辅助子句之间的关系。这与[CM21b]中引入的依赖图类似。
**3.4 否定、泛化和特化**
在经典语义下，高阶文字的否定可能会干扰Popper约束。考虑ILP任务和候选程序：
最优解是 `progs`，而 `progf` 是一个不正确的假设，Hopper 可以在 `progs` 之前生成 `progf`，并且 `progf ≤θ progs`。注意，`progf |= ¬f(b) ∧ ¬f(a) ∧ f(c)`，它不能涵盖所有正例 `E+`。我们应该对 `progf` 进行泛化，以找到一个解决方案，即向 `p1` 中添加文字。引入的约束 [CM21a] 修剪了扩展 `p1` 的程序，即 `progs`。特化情况也是如此。考虑 ILP 任务和候选程序：
最优解是 `progs`，而 `progf` 是一个不正确的假设，Hopper 可以在 `progs` 之前生成 `progf`，并且 `progs ≤θ progf`。注意，`progf |= f(a) ∧ f(b) ∧ f(c)`，它涵盖了部分负例 `E−`。我们应该特化 `p1` 以找到一个解决方案，即向 `progf` 中添加子句。引入的约束 [CM21a] 修剪了添加子句的程序，即 `progs`。
处理发明的谓词的否定是可行的，但并非简单，因为这需要对约束构建过程进行重大修改。我们将此问题留待未来研究。
**4 实验**
一个可能的，尽管非常弱的，程序综合器是一个枚举过程，它按大小顺序排列所有可能从背景知识（BK）构建的程序，测试每个程序直到找到解决方案。在[CM21a]中，这个过程被称为Enumerate。Popper通过根据先前测试过的程序的性能来剪枝假设空间，从而扩展了Enumerate。
剪枝机制永远不会剪枝最短的解决方案。因此，评估Popper和Hopper时重要的问题不是Popper是否会找到解决方案，也不是它是否是高质量的解决方案，而是Popper找到解决方案需要多长时间。[CM21a]中提出了一系列广泛的实验，说明了Popper显著优于Enumerate和现有的ILP系统。
提高基于LFF的ILP系统（如Popper）性能的一种方法是引入缩短或简化解决方案的技术。[CMM20]的作者除了引入MetagolHO和HEXMILHO外，还提供了一套全面的实验，说明了添加HO谓词可以提高准确性，最重要的是减少学习时间。学习时间的减少是由于HO谓词减少了解决方案的复杂性/大小。
[CM21a]中的实验全面涵盖了简单列表转换任务的可扩展性和学习性能问题，但没有涵盖具有大型解决方案的复杂任务的性能。[CMM20]中的实验说明了使用HO库解决许多简单任务时的性能提升，以及添加HO谓词如何允许合成相对复杂的谓词，如dropLast。当解决方案很大时，Popper的性能显著下降。当解决方案需要谓词和子句之间复杂的交互时，找到一组不过于描述性或不遭受长时间学习之苦的MetagolHO的元规则变得非常困难。
我们的实验说明了将Popper与HO谓词[CMM20]结合起来显著提高了Popper学习复杂程序的性能。与[CM21a]一样，我们使用谓词声明，即body pred(head,2)，类型声明，即type(head,(list,element))，方向声明，即direction(head,(in,out))，以及Popper的搜索机制所需的参数，max var, max body, 和 max clauses。
我们重新评估了[CM21a]中提出的7个任务和[CMM20]中提出的2个任务。此外，我们增加了8个列表操作任务，3个树操作任务和2个算术任务（按类型在表1中分开）。我们额外的任务比之前工作中评估的任务要困难得多。
对于每个任务，我们保证最优解在假设空间中，并记录Popper和Hopper找到它所需的时间。我们使用最优设置和最小BK运行Popper。在某些情况下，没有谓词发明（参见表1的PI?列），Popper无法解决任务，即任何既准确又精确的解释性假设都需要BK中没有的辅助概念。
我们以两种模式运行Hopper，Hopper列关注使用与Popper相同的设置和Popper使用的BK的超集（减去用于强制发明的构造），而Hopper (Opt)列关注使用最优设置和最小BK运行Hopper。对于Popper和Hopper，max var和max body等设置显著影响性能。两个系统都搜索当前约束下最短的程序（按文字计数）。注意，与先前生成的程序相比，假设一个额外子句的程序需要至少增加两个文字计数。因此，当前的搜索过程避免这样的假设，直到所有更短的程序都被剪枝或测试过。参数max var和max body对单个子句假设空间的大小有显著影响。鉴于使用HO定义始终需要辅助子句，对于上述参数使用大值将妨碍它们的使用。这就是为什么Hopper在优化后性能显著更好。使用较大的BK相比使用不合直觉的大型参数设置（参见[CM21a]第14页的命题1）对性能影响不大。
表1的HO-Predicate列列出了特定任务使用的谓词。当需要大型子句或多个变量时，Popper和Hopper超时（300秒已过）。超时意味着在300秒内未找到最优解。鉴于我们知道每个任务的解决方案，#Literals列提供了已知解决方案的大小，而不是系统在超时情况下找到的非最优解决方案的大小。
关于优化，这些Hopper的运行紧密模拟了这样的系统将如何被使用，因为假设较小的子句和较少的变量足够是实用的，并根据需要扩展空间。Popper和Hopper的性能仅通过假设解决方案可能是复杂的就会下降。对于findDup，Hopper找到了FO解决方案。
总的来说，这个优化问题提出了一个关于Popper和Hopper当前使用的搜索机制的问题。虽然HO解决方案通常比相应的FO解决方案短，但这种简洁性是以复杂的程序结构为代价的。当前的LFF范式实现没有考虑这种权衡。计划未来的工作是研究替代的搜索机制和最优性条件（除了文字计数）。
我们尝试使用MetagolHO解决每个任务。使用MetagolHO成功学习高度依赖于元规则的选择。为了简化问题，我们选择了模仿解决方案中子句的元规则。在某些情况下，这需要通过在元规则的主体中添加声明，即metagol:type(Q,2,head pred)，来明确限制某些变量的实例化方式（在表1中用metatype表示）。这相当于大量的人为指导，因此，我们限制自己只表明成功或失败。
在这些实验设置下，每个成功的任务都比使用最佳设置的Hopper更快地被MetagolHO解决。放宽对元规则集的限制会引入一个新的变量到实验中。选择一个通用的元规则集，涵盖每个任务，可能会导致大多数任务失败。有些任务需要像P(A, B):- Q(A, B), R(A, B)这样的拆分规则，这显著增加了假设空间的大小。按任务选择元规则，但不为成功优化，留下了一个问题，哪些元规则对给定任务是适当/可接受的？虽然这是一个有趣的问题[CT20]，但存在一套通用元规则，使得MetagolHO的性能可与Hopper相比，甚至更好，这进一步加强了我们关于所选实验设置的论点，因为人们将不得不推断/设计这套规则。
**5 结论和未来工作**
我们将基于LFF的ILP系统Popper扩展为在学习期间有效使用用户提供的HO定义。我们的实验表明，当优化后，Hopper能够在大多数任务上超越Popper，特别是在本工作中引入的更难任务（第4节）。与表现最好的基于MiL的ILP系统MetagolHO相比，Hopper需要最少的指导。我们的实验测试了在大量指导下MetagolHO找到解决方案的理论可能性。然而，鉴于对元规则选择的敏感性，以及许多任务具有三元甚至四元谓词，很难恰当地比较这些方法。
我们提供了一个理论框架，封装了接受的HO定义，这些定义在子sumption和entailment上是单调的，讨论了这个框架的限制。第3节提供了详细说明。
这个框架的主要限制涉及HO否定，我们将其留作未来的工作。我们的框架还允许在通过形式为的构造学习期间发明HO谓词。我们可以验证Hopper原则上可以找到解决方案，但我们还没有成功地在学习期间发明HO谓词。我们计划进一步调查这个问题。
如前所述，由于系统参数对其性能的重大影响，Hopper在实验期间被测试了两次。这可以看作是当前LFF实现的副作用，它偏向于具有较少但较长子句的程序，而不是具有许多短子句的程序。考虑到这种偏见以及其他偏见的替代LFF实现，留作未来的调查。
http://cl-informatik.uibk.ac.at/cek/docs/22/spdcck-ijcai22.pdf
