Learning logic programs by finding minimal unsatisfiable subprograms
通过寻找最小不可满足子程序学习逻辑程序
https://arxiv.org/abs/2401.16383
基础：Code：从 提出假设、验证假设、假设失败 中学习最优方案
摘要
归纳逻辑编程（ILP）的目标是搜索一个能够概括训练示例和背景知识的逻辑程序。我们介绍了一种ILP方法，该方法识别最小不可满足子程序（MUSPs）。我们展示了发现MUSPs可以让我们高效且合理地修剪搜索空间。我们在多个领域的实验，包括程序合成和游戏玩法，表明我们的方法可以将学习时间减少99%。
1 引言
归纳逻辑编程（ILP）的目标是归纳出一个逻辑程序（一组逻辑规则），它能够概括示例和背景知识（BK）。例如，假设我们有包含关系head/2、tail/2和empty/1的BK，以及以下正面（E+）和负面（E−）示例：
程序h过于具体，因为它不包含任何正面示例。因此，学习器可以修剪更具体的程序。然而，简单地解释h过于具体是相当粗糙的。程序h不能蕴含任何东西，因为空列表不能有尾部。换句话说，字面量对empty(A)和tail(A,C)是不可满足的。因此，包含这对字面量的任何规则也是不可满足的，所以我们可以从假设空间中修剪掉所有这样的规则。
我们认为，通过发现最小不可满足程序，我们可以修剪更多的程序，从而提高学习性能。这个想法受到了SAT领域寻找最小不可满足核心的工作的启发[Lynce和Silva，2004]。因此，我们使用类似的术语，并说字面量对empty(A)和tail(A,C)形成了程序h的最小不可满足子程序（MUSP），因为每个字面量单独都是可满足的。
现有的ILP方法并不识别MUSPs。一些方法对整个程序的失败进行推理，但不能精确解释为什么程序失败[Kaminski等人，2019；Cropper和Morel，2021a；Purgal等人，2022]。一些方法识别错误的规则[Shapiro，1983；Raghothaman等人，2020]或字面量[Muggleton等人，2015；Morel和Cropper，2023]，但不识别MUSPs。
为了克服这个限制，我们引入了一种识别MUSPs的方法。为了探索我们的想法，我们使用从失败中学习（LFF）的设置[Cropper和Morel，2021a]。LFF将ILP问题框架化为约束满足问题（CSP），其中CSP的每个解决方案都代表一个程序。LFF学习器的目标是积累约束以限制假设空间。我们基于LFF系统POPPER[Cropper和Morel，2021a]，它可以从无限域中学习最优和递归程序。我们使POPPER能够识别MUSPs，并从中构建约束以指导后续搜索。我们称我们的系统为MUSPER。
新颖性和贡献
本文的主要新颖之处在于识别最小不可满足子程序并从中构建约束。我们在多个领域展示了这一影响，即显著提高学习性能。此外，由于这一想法连接了人工智能的许多领域，包括机器学习、逻辑编程和约束满足，我们希望这一想法能够吸引广泛的读者。总体而言，我们做出了以下贡献：
• 我们描述了最小不可满足子程序问题，即寻找MUSPs的问题。我们展示了使用MUSPs进行修剪在最优意义上是合理的（命题1和2）以及有效的（命题3和4）。
• 我们在MUSPER中实现了我们的方法，MUSPER是一个ILP系统，它能够识别明确程序的MUSPs，包括递归程序。我们证明了MUSPER总是能够学习到一个最优解（如果存在的话）（定理1）。
• 我们在多个领域，包括程序合成和游戏玩法，通过实验展示了我们的方法可以将学习时间大幅减少99%。
2 相关工作
规则挖掘。ILP是一种规则挖掘形式。将我们的方法与规则挖掘方法进行比较是困难的。例如，AMIE+ [Gal´arraga等人，2015]，一个规则挖掘系统，使用开放世界假设，只能使用一元和二元关系，并且需要事实作为输入。相比之下，MUSPER使用封闭世界假设，可以使用任何元关系，并且以明确程序作为BK。
ILP。许多ILP系统[Muggleton，1995；Blockeel和De Raedt，1998；Srinivasan，2001；Zeng等人，2014；De Raedt等人，2015]难以学习递归程序并执行谓词发明[Cropper等人，2020a]。相比之下，MUSPER可以学习递归程序并执行谓词发明。此外，与许多ILP系统[Evans和Grefenstette，2018；Kaminski等人，2019；Si等人，2018；Dai和Muggleton，2021；Glanois等人，2022]不同，我们不要求元规则。
规则选择。许多系统将ILP问题形式化为规则选择问题[Corapi等人，2011；Law，2018；Kaminski等人，2019；Raghothaman等人，2020；Bembenek等人，2023]。这些方法预先计算假设空间中的所有可能规则，然后搜索一个子集来蕴含示例。由于它们预先计算了所有可能的规则，它们无法学习具有许多字面量的规则。相比之下，我们不预先计算每个可能的规则。此外，我们可以学习Datalog和明确程序。
理论修复和修订。理论修复方法[Bundy和Mitrovic，2016]通过应用泛化和特化运算符来修订假设。理论修订方法[Wrobel，1994；Ad´e等人，1994；Paes等人，2017]可以将字面量识别为修订点，但通常有限制，如需要用户交互[Shapiro，1983]或对训练示例的限制[Richards和Mooney，1995]。相比之下，MUSPER保证在没有这些限制的情况下找到一个最优解（如果存在）。
解释。POPPER [Cropper和Morel，2021a]从整个程序构建约束以修剪假设空间。相比之下，我们从MUSPs构建约束，这导致了更好的修剪（第3.4节）。ILASP3 [Law，2018]和PROSYNTH [Raghothaman等人，2020]从不蕴含示例的规则生成约束。
这两种方法预先计算所有可能的规则，并且只识别错误的规则。相比之下，我们不预先计算所有可能的规则，而是识别不可满足字面量的最小子集。METAGOL [Muggleton等人，2015]逐字面量构建程序并将其在示例上进行测试。如果程序不蕴含任何正面示例，METAGOL会回溯以考虑替代字面量，即它识别不可满足的字面量。METAGOL会反复重新考虑不可满足的程序，而MUSPER通过学习约束，因此永远不会这样做。HEMPEL [Morel和Cropper，2023]分析明确程序的执行路径以识别不可满足的字面量。HEMPEL使用从左到右的SLD解析来分析规则，因此只能识别明确的子程序，并且不能保证找到MUSPs。例如，给定不可满足的规则f(A,B) ← element(A,B),odd(B),even(B)，HEMPEL无法找到更小的不可满足子程序。相比之下，MUSPER识别出字面量odd(B)和even(B)构成了一个MUSP。
约束发现。子句发现方法[De Raedt和Dehaspe，1997]发现约束以包含在假设中以消除模型。相比之下，我们发现约束以修剪假设空间。DISCO [Cropper和Hocquette，2023b]作为预处理步骤从BK中发现约束。它使用预定义的约束集，如不对称性和反对称性。我们不同，因为我们（i）发现MUSPs，（ii）在学习过程中发现约束，而不是作为预处理步骤，（iii）不使用预定义的约束集，并且（iv）共同考虑BK和示例。正如我们的实验所示，这些差异极大地影响了学习性能。
3 问题设置
我们描述了我们的问题设置。我们假设熟悉逻辑编程[Lloyd，2012]，但在附录中包含了一个摘要。
3.1 从失败中学习
我们使用LFF（Learning from Failures）设置。我们学习具有最小Herbrand模型语义的明确程序。一个假设是一组明确子句。我们使用术语“程序”与“假设”同义。假设空间H是一组假设的集合。LFF使用假设约束来限制假设空间。
让L是一个定义假设的语言。一个假设约束是一个在L中表达的约束（一个无头规则）。让C是一组用语言L编写的假设约束。如果一个假设用L编写时不违反C中的任何约束，则它与C一致。我们表示为HC的是从H中与C一致的假设集合。
我们定义LFF输入：
3.2 最小不可满足子程序
我们定义了MUSP问题。我们定义了一个子程序：
请注意，子程序可以包含无头规则（目标子句），如上述第二个子程序中所示。
我们定义最小不可满足子程序：
一个最小不可满足子程序（MUSP）与最小不可满足核心[Lynce和Silva，2004]和最小不可满足子集[Alviano等人，2023]不同，这两者通常都是根据子集的最小性来定义的。相比之下，MUSP是根据基数最小性来定义的。
我们定义MUSP问题：
3.3 MUSP约束
我们希望识别MUSPs（最小不可解程序），以便从中构建约束条件，从而修剪ILP（归纳逻辑编程）学习者的假设空间。我们描述了可以从MUSP构建的约束条件。由于空间限制，所有的证明都在附录中。由于一个MUSP是完全不完整的，那么它的特化就不能是解决方案：
由于一个MUSP m 是完全不完整的，那么它的特化不能出现在最优解中，除非有一个递归规则不对m进行特化。
在第4节中，我们介绍了MUSPER，它利用这些最优合理约束来剪枝假设空间。
3.4 MUSP的优势
我们展示了使用MUSP构建约束来剪枝特化和冗余假设，从而带来了更多的剪枝。证明在附录中。
4 算法
我们现在描述我们的 MUSPER 方法。为了阐明其新颖性，我们首先描述 POPPER。
**POPPER**：POPPER 接受背景知识（bk）、正训练样例（pos）和负训练样例（neg），以及最大假设大小（max size）作为输入。POPPER 使用一个生成、测试和约束循环来寻找最优解。POPPER 从一个 CSP 程序 P（隐藏在生成函数中）开始。P的模型对应于假设（确定性程序）。在生成阶段，POPPER 搜索 P的模型。如果没有模型，POPPER 增加假设大小并重新循环。如果有模型，POPPER 将其转换为假设 h。在测试阶段，POPPER 使用 Prolog 对样例测试 h。如果h是一个解，POPPER 返回它。如果 h 失败，那么在约束阶段，POPPER 从 h 中构建假设约束（表示为 CSP 约束）。POPPER 将这些约束添加到 P中，以修剪模型并缩减假设空间。例如，如果h 是不完整的，POPPER 构建一个特化约束以修剪其特化。如果 h 是不一致的，POPPER 构建一个泛化约束以修剪其泛化。再次重申，POPPER 从整个程序中构建约束。POPPER 重复此循环，直到找到最优解或耗尽P的模型。
**MUSPER**
MUSPER（算法1）与 POPPER 类似，唯一的主要区别是：如果程序h是完全不完整的，MUSPER 在第13行调用算法2 来识别 h 的 MUSPs 并从中构建约束。再次重申，识别 MUSPs 并从中构建约束的能力是本文的主要创新点和贡献。
MUSPs
算法2从MUSP构建约束。为了找到MUSP（第2行），我们使用了Dershowitz等人[2006]所说的民间算法。我们通过从程序h中移除一个文字并检查子程序是否遵守定义4中的条件（第12行）来搜索程序h的子程序。我们还执行其他语法限制，例如规则中的文字是连接的1。我们检查每个子程序，看它是否不可满足（第13行）。如果一个子程序是不可满足的，我们递归地找到子程序本身的MUSP，并将结果添加到最小不可满足子程序集合中（第15行）。否则，我们将h添加到最小不可满足子程序集合中（第17行）。
可满足性
在我们实现算法2时，我们使用Prolog来检查子程序的可满足性（第13行）。有两种情况。如果子程序s中的所有规则都有一个头部文字，那么我们说s是可满足的，如果它至少蕴含了一个正面例子。如果子程序s包含一个没有头部文字的规则r，那么我们在r的头部添加一个is sat文字。我们说s是可满足的，如果is sat是真的。例如，给定子程序：
约束
由于一个MUSP是完全不可满足的，那么它的特化不能是解决方案（命题1）。同样，由于一个MUSP是完全不可满足的，我们可以剪枝与它相关的冗余程序（命题2）。因此，算法2为每个MUSP构建了一个特化和冗余约束（第5和6行）。
正确性
我们证明了MUSPER的正确性：
定理1（MUSPER正确性）。如果存在一个最优解，MUSPER会返回它。
5 实验
我们声称识别MUSP可以提高ILP系统（归纳逻辑编程系统）的学习性能。命题3和命题4支持这一主张，并表明识别MUSP可以改善剪枝。然而，目前尚不清楚在实践中寻找MUSP和构建约束的开销是否超过了剪枝带来的好处。因此，我们的实验旨在回答以下问题：
Q1 识别MUSP能否减少学习时间？
为了回答Q1，我们比较了MUSPER和POPPER的性能。由于MUSPER基于POPPER构建，系统之间的唯一区别在于识别MUSP的能力，因此这种比较直接衡量了我们想法的影响。
为了理解MUSPER与其他方法相比如何，我们的实验试图回答以下问题：
Q2 MUSPER与其他方法相比如何？
为了回答Q2，我们将MUSPER与ALEPH [Srinivasan, 2001]、METAGOL [Muggleton et al., 2015]、POPPER和DISCO [Cropper and Hocquette, 2023b]进行了比较。
可重复性。所有实验代码和数据都包含在补充材料中，并将在接受发表的论文时公开提供。
5.1 领域
我们简要描述我们的领域。附录包含更多细节，例如每个任务的示例解决方案和问题规模的统计数据。
火车。目标是找到一个假设，区分东西方向的火车 [Larson and Michalski, 1977]。
Zendo。Zendo是一个多人游戏，玩家必须通过构建结构来发现一个秘密规则。Zendo在认知科学中引起了兴趣 [Bramley et al., 2018]。
IMDB。我们使用一个经常使用的现实世界数据集，包含电影、演员和导演之间的关系 [Mihalkova et al., 2007; Dumanˇci´c et al., 2019]。
IGGP。归纳通用游戏玩法（IGGP）的目标是归纳出规则以解释通用游戏玩法竞赛的游戏轨迹 [Genesereth and Bj ¨ornsson, 2013]。
国际象棋。任务是学习国际象棋中车王对王（krk）残局的模式 [Hocquette and Muggleton, 2020]。
程序合成。我们使用一个程序合成数据集 [Cropper and Morel, 2021a]，并增加了5个新任务。
SQL。这个数据集[Si et al., 2018]包含了15个涉及合成SQL查询的真实世界任务。由于没有测试数据，我们报告训练准确率。
5.2 实验设置
我们对每个任务强制执行30分钟的超时限制。附录包括所有实验细节和示例解决方案。我们测量预测准确率、学习时间（包括发现MUSPs的时间）以及考虑的程序数量。我们还报告了发现MUSPs所花费的时间，即我们方法的开销。我们测量10次试验的平均值。所有表格中的误差条表示标准误差。
5.3 实验结果
Q1. 识别MUSs能否减少学习时间？
表1显示了按领域汇总的学习时间。表3显示了MUSPER和POPPER的学习时间有差异的任务的学习时间。这些结果表明，MUSPER所需的时间从不比POPPER多。配对t检验证实了差异的显著性（p < 0.01）。MUSPER可以大幅减少学习时间。例如，在sql-06任务上，POPPER在1800秒后超时，而MUSPER仅需要14秒，减少了99%。同样，在coinsg任务上，POPPER在1800秒后超时，而MUSPER仅需要6秒，减少了99%。
表2显示了按领域汇总的预测准确率。MUSPER在除了一个领域之外的所有领域上的预测准确率都等于或高于POPPER，而在那里的差异是微不足道的。这些结果表明，MUSPER可以在保持高预测准确率的同时大幅减少学习时间。
表4显示了每个系统考虑的程序总数的汇总。每个任务的完整表格在附录中。MUSPER考虑的程序数量比POPPER显著减少。例如，在sql-02任务中，POPPER考虑了25,533个程序，而MUSPER只考虑了52个，减少了99%。这一结果表明，从MUSP构建的约束可以有效地剪枝假设空间。
表5显示了在识别MUSPs上花费的学习时间比例。开销通常不超过几秒钟，最多占学习时间的23%。
为了说明我们的方法为何有效，请考虑最后一个任务，MUSPER可以生成假设：
这个程序是不满足的，因为这项任务的BK（背景知识）定义在自然数上，所以零没有前驱。
MUSPER剪枝了这个MUSP的特化和冗余，从而大幅减少了假设空间。
同样，在buttons任务中，MUSPER有时生成假设：
当MUSPER在搜索早期发现较小的MUSP时，它可以减少学习时间，但在其他情况下帮助较小。例如，在zendo任务中，MUSPER帮助不大，因为这些任务有许多几乎总是成立的背景关系，如has piece(State, Piece)，因为每个Zendo游戏状态都有一个部件，以及size(Piece, Size)，因为一个部件总是有一个大小。
总体而言，本节的结果显示，对Q1的回答是肯定的，识别MUSP可以大幅改善学习时间，同时保持高预测准确率。
Q2. MUSPER与其他方法相比如何？
表2展示了所有系统在每个领域的预测准确率汇总。MUSPER在每个领域上的预测准确率都高于METAGOL。除了两个领域——火车领域（差异可忽略不计）和krk领域——MUSPER的预测准确率等于或高于ALEPH。最具有可比性的方法是DISCO。表2的结果表明，MUSPER在所有领域上的预测准确率等于或高于DISCO。表6展示了MUSPER和DISCO在每个领域的学习时间汇总。结果表明，MUSPER在7个领域中的6个领域超过了DISCO，并且在另一个领域与之相当。配对t检验证实了差异的显著性（p < 0.01）。与DISCO相比，MUSPER可以减少高达97%的学习时间，例如在sql领域。
MUSPER与DISCO性能差异的两个主要原因是：(i) DISCO仅从背景知识（BK）中找到不满足的规则，而不考虑示例；(ii) DISCO使用预定义的属性集来找到不满足的规则。例如，在sql-02任务中，我们希望使用具有family/4事实的BK来学习out/2关系。对于此任务，DISCO没有从BK中学习到任何约束。相比之下，MUSPER迅速学习到许多MUSPs，包括：
这条规则是一个MUSP，因为在BK中的family/4事实中，没有正例out(A, B)使得A为真。因为它只考虑了BK而没有考虑示例，DISCO无法学习到这个MUSP。MUSPER也学习到了这个MUSP：
DISCO无法学习这个MUSP，因为它不是其预定义属性之一。在这个任务中，DISCO需要1005秒才能终止。相比之下，MUSPER学习到了一个最优解，并且仅在9秒内就终止了，提高了97%。
总体而言，这些结果表明，对于Q2的回答是MUSPER与现有方法相比具有优势，并且可以在预测准确率和学习时间方面大幅提高学习性能。
6 结论和局限性
我们介绍了一种识别最小不可满足子程序（MUSP）的方法。我们已经展示了使用MUSP进行剪枝在理论上是最优的（命题1和2），并且是有效的（命题3和4）。我们在MUSPER中实现了我们的方法，它可以识别包括递归程序在内的确定性程序的MUSP。我们在许多不同领域的实验结果表明，我们的方法可以大幅减少学习时间，同时保持高预测准确率，有时甚至可以将学习时间减少99%。除了显著的实证改进之外，我们认为这篇论文的一个关键贡献是展示了一个在约束满足领域中得到深入研究的想法（寻找最小不可满足核心）可以显著提高机器学习算法的性能。
局限性。为了找到MUSP，我们使用了Dershowitz等人[2006]所说的民间算法，逐个删除文字。正如Dershowitz等人[2006]所指出的，这种民间算法在大型公式中扩展性不好。尽管在我们的实验中可扩展性不是问题，但未来的工作应该解决这一局限性。
