神经符号编程在 Scallop 中的原理与实践（上,1-4章）

神经符号编程在 Scallop 中的原理与实践

https://www.nowpublishers.com/article/DownloadSummary/PGL-059

https://www.cis.upenn.edu/~jianih/res/papers/scallop_principles_practice.pdf

Neurosymbolic Programming inScallop: Principles and Practice

摘要

神经符号编程结合了深度学习和符号推理这两个互补的领域，从而为人工智能任务提供了更准确、可解释且具有领域感知能力的解决方案。我们介绍了 Scallop，这是一种用于开发神经符号应用程序的通用语言和编译器工具链。Scallop 程序将人工智能任务的计算分解为独立的学习和推理模块。学习模块使用现有的机器学习框架构建，涵盖从自定义神经模型到用于语言、视觉和多模态数据的基础模型。推理模块则通过基于 Datalog 的声明性逻辑编程语言指定，支持递归、聚合、否定以及对结构化关系的概率编程等表达性特性。

Scallop 的编译器能够使用端到端可微推理框架，以数据和计算高效的方式自动训练神经符号程序。Scallop 还支持对构建实际应用有用的功能，例如用户定义的数据类型和外部接口。

我们展示了在 Scallop 中编程的应用，这些应用涵盖了图像和视频处理、自然语言处理、规划和信息检索等领域，并涉及多种学习设置，例如监督学习、强化学习、规则学习、对比学习和上下文学习。

1 引言

1.1 神经符号编程

经典算法和深度学习体现了现代编程的两种主流范式。经典算法非常适合定义明确的任务，例如对数字列表进行排序或在图中找到最短路径。而深度学习则非常适合那些无法通过过程化方法有效或可行完成的任务，例如检测图像中的对象或解析自然语言文本。这些任务通常通过一组输入-输出训练数据来指定，解决这些任务涉及通过基于梯度的方法学习深度神经网络的参数以拟合数据。

这两种范式本质上是互补的。例如，图 1.1a 中所示的逻辑程序 λ 这样的经典算法是可解释的，但只能处理有限的、结构化的输入 r。另一方面，图 1.1b 中所示的深度神经网络 Mθ 可以处理丰富的、非结构化的输入 x，但缺乏可解释性。现代应用需要这两种范式的能力。例如，问答系统（Rajpurkar 等，2016）、代码补全（Chen 等，2021）和数学问题求解（Lewkowycz 等，2022）等。以代码补全为例，它需要深度学习来从代码上下文中理解程序员的意图，同时需要经典算法来确保生成的代码是正确的。

一个自然而根本的问题是：如何通过整合这两种范式来编写此类应用程序。

神经符号编程是一种新兴的范式，旨在实现这一目标（Chaudhuri 等，2021）。它试图将符号知识和推理与神经架构相结合，以实现比单独的神经或符号方法更高的效率、可解释性和泛化能力。以手写公式评估任务为例（Li 等，2020），该任务将公式图像作为输入，并输出一个对应于公式计算结果的数字。该任务的输入-输出示例为。针对此任务的神经符号程序（如图 1.1c 所示）可能首先将卷积神经网络 Mθ 应用于输入图像，以获得结构化的中间形式 r，即符号序列 [‘1’, ‘+’, ‘3’, ‘/’, ‘5’]，然后通过经典算法 λ 解析该序列，评估解析后的公式，并输出最终结果 1.6。

尽管在个别神经符号应用中取得了显著进展（Yi 等，2018；Mao 等，2019；Chen 等，2020；Li 等，2020；Minervini 等，2020a；Wang 等，2019），但缺乏一种具有编译器支持的语言来使神经符号范式的优势更广泛地普及。我们着手开发这样一种语言，并确定了它应满足的五个关键标准，以使其具有实用性。这些标准（通过图 1.1c 中神经符号程序的组件进行注释）如下：

1.2 Scallop：是什么以及为什么

1. 支持多种数据的符号数据表示：用于表示 r 的符号数据表示应支持图像、视频、自然语言文本、表格数据及其组合等多种数据类型。

2. 表达常见推理模式的符号推理语言：用于 λ 的符号推理语言应能够表达递归、否定和聚合等常见推理模式。

3. 自动且高效的可微推理引擎：用于在算法监督下学习（∂y/∂r），即在可观察的输入-输出数据（x, y）而非 r 上进行监督学习。

4. 针对应用特性定制学习的能力：由于符号程序的非连续损失函数特性，使用一刀切的方法会阻碍学习，因此需要针对不同应用的特点定制学习（∂y/∂r）。

5. 利用并集成现有训练流程的机制：能够与现有的训练流程（∂θ/∂r）、神经架构和模型 Mθ 的实现以及硬件（如 GPU）优化进行集成。

1.2 Scallop：是什么以及为什么

我们开发了 Scallop，这是一种满足上述所有标准的编程语言。Scallop 的核心设计理念基于三个相互依赖的设计决策：用于符号数据表示的关系模型、用于符号推理的声明性语言，以及用于可微推理的溯源框架。

我们的设计选择受到以下关键观察的启发：

首先，世界上大部分数据都存储在关系数据库中。关系模型足够灵活，能够表示从高级视觉和语言特征到形式化程序再到分子结构等多种类型的数据。其次，用于符号推理的声明性语言允许通过高级规则简洁地表达计算，从而减轻程序员的负担。最后，关系范式为神经符号编程所需的各种高级功能（如查询规划、硬件加速以及概率和可微推理）提供了合适的抽象。

Scallop 的目标是提供一个统一的语言和框架，用于整合神经和符号组件。通过这种方式，我们希望使程序员能够构建更高效、可泛化且可解释的神经符号解决方案。

1.3 神经符号解决方案的构建模块

一种整合神经和符号组件的语言可用于构建多样化且适应性强的解决方案。广义上讲，任何任务的神经符号解决方案都涉及神经和符号组件的灵活交互，每个组件在问题解决中扮演着不同但互补的角色。从现有文献中，几个构建模块已成为有效神经符号解决方案的关键，如图 1.2 所示。接下来，我们将详细讨论这些核心构建模块。

特征提取 特征提取过程涉及通过符号组件（此处表示为 λ）从输入 x 中提取符号特征，然后将这些特征传递给神经模型 Mθ 进行训练。尽管特征提取是机器学习中的一种常见做法，通常不被归类为神经符号方法，但它仍然体现了符号和神经元素的功能性整合。在这种方法中，学习仅限于神经组件，而符号组件则用于对输入数据进行预处理。

值得注意的是，高级特征提取不仅限于简单的表格数据，通常还结合复杂的推理机制来构建复杂的数据结构。例如，在程序分析中，源代码可以被预处理为抽象语法树（AST）、数据流图、符号约束或关系数据库等复杂结构（Dinella 等，2020；Li 等，2021；Zhu 等，2024）。因此，神经网络可以从更全面、结构化的信息中受益，以支持下游任务，例如提出错误修复、检测漏洞以及分析二进制代码中的类型信息。

符号推理 符号推理涉及使用程序员提供的符号组件 λ 对神经网络 Mθ 的输出进行后验分析。这种分析可以用于多种目的，例如过滤无意义的输出、验证输出完整性，或通过符号方式结合多个信息源以推导出额外的见解。尽管概念上简单，但高级符号推理组件 λ 可以处理概率信息，推导出分布而不仅仅是最可能的输出。

例如，在手写公式识别任务 ⟨x =, y = 1.6⟩ 中，神经网络为各个符号生成概率分布后，概率符号推理引擎可以合成可能的有理数分布。另一个例子是 RNA 二级结构预测，其中神经网络预测每个核苷酸的结构，然后概率 RNA 折叠算法解析该概率序列以生成前 k 个最可能的结构解析。在第 5 节中，我们将介绍许多符号推理解决方案，其中 Mθ 为基础模型。

算法监督 算法监督通过使符号组件 λ 能够将学习信号传播到神经网络 Mθ，从而扩展了符号推理的功能。如前所述，我们假设 λ 由程序员提供。虽然图 1.1 展示了通过 λ 的可微性实现算法监督的一个示例，但通常只要 λ 能够传播学习信号就足够了。通过这种方式，符号“算法” λ 充当神经网络 Mθ 的指导监督者。

算法监督也作为一种弱监督形式，因为它不需要对 Mθ 进行直接的、完全监督的标签；只需要最终标签 y。这减少了对大量数据标注或特征工程的需求，简化了训练过程。Scallop 中的许多应用都利用了这种方法，包括前面提到的学习评估手写公式的任务（Li 等，2020；Li 等，2023）。本教程在第 6 节中探讨了更多算法弱监督的高级示例。

神经符号程序合成 神经符号程序合成涉及在神经网络的支持下学习符号程序 λ。这种范式类似于经典的语法引导合成任务（Alur 等，2013），但用神经网络 Mθ 取代了传统的算法合成过程。在这里，符号程序 λ 负责生成预期的输出，并且可以迭代优化以更好地与数据集对齐。

这种方法具有可解释性的优势，因为学习到的符号组件是一个白盒程序，可以由人类检查和验证（Ellis 等，2022）。传统上，合成 λ 需要定义一个有限的领域特定语言（Ellis 等，2020），因为通用语言会使合成在计算上变得不可行。然而，随着最近能够生成通用语言（如 Python）程序的大型语言模型（LLMs）的发展，λ 的合成现在可以更高效地实现（Ma 等，2024）。

神经松弛 神经松弛通过将确定性且离散的符号推理组件 λ 中的某些部分替换为神经网络 Mθ，从而实现对其的松弛。这使得原本符号化的部分能够通过神经网络进行近似，从而提高了对未见场景的适应能力。

例如，考虑设计无人机神经符号控制器的挑战：虽然存在针对标准操作的有效确定性控制器，但它们可能难以适应领域外的场景，例如在地面附近、强风中或与其他无人机接近时操作。通过将控制器的某些部分松弛为神经网络 Mθ，系统在处理此类场景时获得了更大的灵活性和响应能力，同时能够快速学习（O’Connell 等，2022；Csomay-Shanklin 等，2024）。

符号蒸馏 符号蒸馏从黑盒神经网络中提取信息并将其转换为符号形式 λ。尽管这一过程涉及生成和优化 λ，类似于神经符号程序合成，但符号蒸馏的重点是将训练有素的神经网络 Mθ 中原本不可解释的权重转换为可解释的形式。

该技术已应用于科学发现领域，例如动物行为分析（Sun 等，2022）。可以从训练有素的神经网络中蒸馏出描述“两只老鼠相互奔跑”等行为的符号程序。另一个应用是用于预测癌症患者死亡率的解释合成（Wu 等，2024）。对于训练用于预测 6 个月死亡率的模型，符号蒸馏可以生成特定预测的解释，为机器学习系统支持的临床决策提供更清晰的见解。

其他组合 除了主要的构建模块外，还有其他值得注意的神经符号组合。例如，AlphaGo（Silver 等，2016）以符号算法——蒙特卡罗树搜索为核心，结合用于策略评估和移动选择的神经网络，创建了一个协同决策过程。另一方面，ChatGPT 插件（OpenAI，2023a）使用大型语言模型作为主要系统，可以调用符号组件（如 Python 解释器、数据库检索或网络搜索）以增强功能。随着神经符号人工智能领域的不断发展，我们预计会出现更多多样化和创新的组合，从而拓宽神经符号方法的范围和应用。

1.4 应用领域

在本节中，我们讨论了 Scallop 最适合的数据模态，并探讨了 Scallop 已展示出有效性的应用领域。同时，我们也指出了 Scallop 的局限性，强调了它可能效果较差的任务。

Scallop 可以广泛应用于需要神经模型和程序化推理模块的应用。当神经模型需要额外训练时，它尤其有用。通过完全可微的端到端神经符号管道，神经模型不需要强监督，而是可以使用算法监督，从而带来数据效率和泛化性等优势。

数据模态 Scallop 基于关系数据模型，因此能够处理多种数据模态。关系范式使其能够与现有的关系数据库和表格数据无缝协作，涵盖知识库、电子健康记录和互联网文档中的信息。此外，自然语言处理（NLP）任务中的自然语言数据可以以多种形式输入：原始句子、嵌入（张量）或结构化表示（如关系数据库或函数式程序）。计算机视觉中的图像数据可以转换为语义表示（如场景图）。视频作为具有时间维度的图像扩展，可以类似地表示为时空场景图以在 Scallop 中进行分析。计算机程序可以转换为关系数据库，捕获抽象语法树和控制流图等详细信息。

应用领域 我们已将 Scallop 应用于多个领域，包括自然语言处理（NLP）、计算机视觉（CV）、规划、程序和安全分析、生物信息学以及医疗保健。在 NLP 领域，我们将其应用于需要推理的任务，例如在数据库中检索文档或分析来自电子健康记录或法律文档的数据。在计算机视觉领域，我们并未专注于对象分割和跟踪等低级感知任务，而是将其应用于混合任务，如视觉问答和支持场景图生成模型的训练。在安全分析中，我们将其应用于污点分析、漏洞检测和故障定位等任务。在生物信息学中，我们将其用于预测 RNA 二级结构和 RNA 剪接等应用。需要注意的是，并非所有 Scallop 解决方案都遵循统一的架构。我们根据每个任务的独特特性调整不同的构建模块（图 1.2）。

Scallop 可能效果较差的应用场景 我们列举了三种 Scallop 可能无法显著提升任务解决效果的场景，这些场景通常由于定义推理组件或合适的中间表示存在挑战。

1. 生成符合主观标准的文本 像 GPT 这样的语言模型的常见用例是生成符合风格或内容上主观标准的文本，例如同理心或政治中立性。虽然语言模型可以生成连贯的段落，但识别特定的逻辑组件以进行整合是具有挑战性的。此类任务的抽象性使得难以确定逻辑推理在哪些方面能够提供超越当前语言模型的实质性价值。

2. 基本数学计算（如 +、−、×、÷） 这类任务本质上是符号化且直接的。现有的工具（如 Python 或 MATLAB）可以直接执行这些操作，因此没有明显的需求引入感知模型。这类任务纯粹是逻辑性的，缺乏能够从 Scallop 的关系或感知能力中受益的组件。

3. 机器人的低级运动控制 Scallop 的语法更适合定义高级离散逻辑规则，而不是处理感官信号的低级数值处理。因此，对于基于原始传感器输入的运动控制任务，命令式语言（如 C 或 Python）可能更适合用于指定数值算法。

1.5 目标读者

Scallop 基于逻辑编程范式，并通过 Python 绑定与 PyTorch 等机器学习框架无缝集成。因此，我们假设读者熟悉逻辑、机器学习、基础微积分（特别是微分）以及 Python 编程语言的基本概念。本教程涵盖的主题包括编程语言的语法和语义、概率理论和近似方法，以及机器学习系统的设计和实现。虽然教程还探讨了自然语言处理和计算机视觉中的应用，但我们为每个任务提供了易于理解的介绍。总体而言，本教程面向希望通过 Scallop 获得神经符号编程实践基础和理论理解的读者，内容涵盖理论概念和实际应用。

1.6 大纲

我们将在第 2 节中从关系编程的基础开始介绍 Scallop 的核心语言。接着，第 3 节深入探讨 Scallop 的内部机制和我们的溯源框架，描述核心推理模块。我们展示了 Scallop 中支持可扩展可微推理的核心编程结构。随后，第 4 节通过几个激励性任务展示了 Scallop 简洁高效地定义神经符号应用的能力。第 5 节将 Scallop 与基础模型联系起来。我们在第 6 节中介绍了一些更高级的神经符号应用。最后，第 7 节总结了 Scallop 的局限性和未来发展方向。

2 Scallop 编程基础

在本章中，我们将Scallop作为一种关系逻辑编程语言进行介绍。它是一种基于Datalog的语言，扩展了诸如否定、聚合、析取头、代数数据类型、外部函数和外部谓词等特性。我们提供了一个全面的核心语言概述，涵盖了所有这些结构。

2.1 关系、数据类型和事实

Scallop中的基本数据类型是关系，它由一组静态类型的原始值元组组成。原始数据类型包括各种大小的有符号和无符号整数（例如i32、usize）、单精度和双精度浮点数（f32、f64）、布尔值（bool）、字符（char）和字符串（String）。表2.1中提供了完整的列表。例如，清单2.1声明了两个二元关系：`mother`和`father`。请注意，我们使用一个`type`关键字声明了多个关系。关系的值可以通过单个元组或一组常量字面量的元组来指定，如清单2.1中的第5行和第8行所示。事实的类型必须符合静态声明的关系类型。`mother`和`father`下的所有元组都是二元组，且两个元素都是字符串。请注意，关键字`rel`被选为`relation`的缩写，用于定义关系。

作为一种简写形式，原始值可以被命名并声明为常量变量，如清单2.2中的第2行所示。类型声明是可选的，因为Scallop支持类型推断。组合关系的类型被推断为`(usize, usize, usize)`，因为常量无符号整数的默认类型是`usize`。类似地，亲属关系的类型将被推断为`(String, usize, String)`。我们注意到，这种新的家族图表示与清单2.1中定义的表示是等价的，尽管只使用了一个关系（`kinship`）而不是两个（`father`和`mother`）。

2.1.1 零元、一元和二元关系

零元或布尔关系 许多事物都可以表示为关系。我们从最基本的编程构造——布尔值开始。虽然Scallop允许值具有布尔类型，但关系本身也可以编码布尔值。清单2.3中展示的示例包含一个名为`is_target`的零元关系。在这种关系中，只有一个可能的元组可以构成事实，即空元组`()`。将`is_target`关系视为一个集合：如果集合中没有元素（即空集），则它编码布尔值“false”；否则，集合最多且恰好包含一个元组，此时关系编码布尔值“true”。

一元关系 一元关系是元数为1的关系。我们可以为“变量”定义一元关系，就像在其他编程语言中看到的那样。清单2.4声明了一个名为`greeting`的关系，其中包含一个字符串“hello world!”。它展示了三种声明关系中单个事实的方式。前两种方式之前已经介绍过，而第三种方式由于关系是一元的，因此省略了括号。

二元关系 顾名思义，二元关系是元数为2的关系。我们通过一个图（图2.1）及其Scallop表示（清单2.5）来演示二元关系。如代码所示，我们定义了一个名为`Node`的枚举类型，包含三个变体`A`、`B`和`C`，分别对应图中的三个节点。一元关系`node`是一个包含这三个节点的集合，而`edge`关系是一个包含图中有向边的二元关系。

2.1.2 类型推断

Scallop支持类型推断，这意味着并非所有类型都需要显式注解。在Scallop中，类型在编译过程中被推断。以清单2.5中的代码为例，Scallop能够推断出`node`关系的类型为`(Node,)`，而`edge`关系的类型为`(Node, Node)`。如果检测到冲突，类型推断将失败。例如，清单2.6展示了一段Scallop代码，在编译期间会导致错误消息。这是因为在`edge`关系的第二个元素中同时观察到了类型为`Node`和`String`的值。

2.2 逻辑规则

由于Scallop的语言基于Datalog，它支持“如果-那么”形式的类Horn子句规则。每条规则由一个头部原子和一个体组成，通过符号`=`连接。如果体“成立”，那么我们可以推导出头部的原子。清单2.7展示了定义`grandmother`关系的三条规则。我们说，如果规则体中的每个变量都可以通过数据库中现有事实的值进行替换，则该规则体可以被“接地”（grounded）。例如，清单2.7中第6行的规则体可以通过两个事实`father("Bob", "Alice")`和`mother("Christine", "Bob")`进行接地。变量`c`可以被接地为“Christine”，`b`可以被接地为“Bob”，而`a`可以被接地为“Alice”。值得注意的是，变量`b`同时出现在`mother(c, b)`原子和`father(b, a)`原子中，这意味着用于接地变量`b`的值必须同时出现在这两个事实中。

在规则中，合取通过规则体中以`and`分隔的原子来指定，而析取则可以通过具有相同头部谓词的多条规则来指定。出现在头部中的每个变量也必须出现在体中的某个正原子中。合取和析取也可以通过逻辑连接符如`and`、`or`和`implies`来表达。例如，清单2.7中的最后一条规则（第9-10行）等价于上述两条规则的组合。

Scallop执行一些编译检查以确保程序是良构的。首先，规则需要进行类型检查。在清单2.7的情况下，所有展示的关系都是二元字符串关系，因此类型推断成功。此外，出现在头部原子中的所有变量必须被体中的原子绑定。以第一条规则（第2行）为例，其中变量`a`被`father`关系绑定，而变量`c`被`mother`关系绑定。因此，该规则的头部原子是绑定且良构的。对于最后一条规则（第9-10行），其体包含析取，头部变量需要在体的所有分支中被绑定。这确实是成立的，因为`a`在析取的两个原子中都被绑定。

Scallop通过外部函数（FFs）支持值的创建。外部函数是多态的，包括算术运算符如`+`和`-`、比较运算符如`!=`和`>=`、类型转换如`[i32] as String`，以及内置函数如`$hash`和`$string_concat`。它们仅操作原始值，而不操作关系元组或原子。清单2.8展示了一些示例。具体来说，第一个示例展示了如何使用浮点数的体重和身高来计算身体质量指数（BMI）。在第二个示例中，字符串通过外部函数连接在一起，生成结果`full_name("John Doe")`。

需要注意的是，外部函数（FFs）可能会由于运行时错误（如除零错误和整数溢出）而失败，在这种情况下，该单个事实的计算会被忽略。在清单2.8的最后一个示例中（第10-12行），当用6除以`denominator`时，对于`denominator`为0的情况不会计算结果，因为这会导致外部函数失败。这种语义的目的是支持概率扩展，而不是静默抑制运行时错误。在处理浮点数时，包含NaN（非数字）的元组也会被丢弃。

2.3 递归、否定和聚合

在本节中，我们将讨论Scallop中逻辑规则的一些稍微高级的特性，即递归、否定和聚合。这些特性是Scallop作为一种表达性语言的关键，使其能够适用于各种应用场景。

2.3.1 递归

Scallop中一个强大的编程构造是声明式地定义递归。在一条规则中，如果出现在头部的谓词也出现在体中，则该规则是递归的。更一般地说，如果关系`s`出现在以`r`为头部原子的规则的体中，则关系`r`依赖于`s`。递归关系是指直接或间接依赖于自身的关系。例如，清单2.9展示了一个包含递归的程序。在该程序中，`path`依赖于`edge`（第5-6行）和`path`自身（第6行）。基于这些信息，我们可以绘制程序的依赖图，如图2.2所示。由于`path`关系上存在自环，我们说该程序是递归的。

递归在递归数学定义中也非常有用。例如，斐波那契数的定义是递归的。回顾斐波那契数的正式定义：

在Scallop中，我们将函数`fib`编码为整数输入和输出之间的二元关系，如清单2.10所示。在第2行，我们定义了`fib(0)`和`fib(1)`的基本情况。对于递归情况，我们通过`y1 = fib(x - 1)`和`y2 = fib(x - 2)`获取结果，并计算`y1 + y2`。这几乎直接转化为第4行的递归规则。我们注意到，必须添加额外的约束`x > 1`以确保计算能够终止。最后，当查询原子`fib(5, y)`时，Scallop将返回事实`fib(5, 8)`，表明8是计算`fib(5)`的结果。

2.3.2 否定

Scallop支持分层否定，通过在规则体中的原子前使用`not`操作符来实现。清单2.11展示了一条定义`has_no_children`关系的规则，该关系表示任何既不是父亲也不是母亲的人`p`（第7-8行）。在规则中，下划线`_`代表通配符，用于匹配任何值。需要注意的是，我们必须通过正原子`person`来绑定`p`，以确保规则是良构的。在无法编译的规则中，变量`p`可以是除"Bob"或"Christine"之外的任何值，这意味着无法枚举这些值。Scallop通过确保所有出现在头部的变量都被体中的正原子绑定来拒绝此类程序。最终，我们得到的关系`has_no_children`包含一个单独的元组`("Alice")`，因为根据上面定义的事实，"Alice"不是任何人的父母。

如果头部原子为`r`的规则体中出现了否定原子`s`，则关系`r`负依赖于`s`。在清单2.11的示例中，`has_no_children`负依赖于`father`。一个关系不能直接或间接地负依赖于自身，因为Scallop仅支持分层否定。以下规则会被编译器拒绝，因为否定不是分层的：

2.3.3聚合

Scallop还支持分层聚合。我们使用赋值符号`:=`来获取从聚合中得出的结果。内置的聚合器包括常见的聚合操作，如`count`、`sum`、`max`以及一阶量词`forall`和`exists`。除了操作符外，聚合构造还指定了绑定变量、用于绑定这些变量的聚合体以及用于分配结果的结果变量。清单2.12中带有聚合的规则可以理解为：“变量`n`被赋值为`p`的计数，其中`p`是一个`person`”。具体来说，`n`是聚合的结果，`count`是聚合器，`p`是用于聚合的限定变量，而`person(p)`是聚合的主体。最终，由于`person`关系中有3个事实，因此推导出`num_people(3)`。在规则中，`p`是绑定变量，`n`是结果变量。根据聚合器的不同，可以有多个绑定变量或多个结果变量。在第7行，我们还展示了一种语法糖，当聚合的结果直接对应于要存储在头部关系中的元组时可以使用。

此外，Scallop还支持SQL风格的分组操作（group-by）。如果某个变量在聚合体中被绑定，并且也在规则的头部中使用，我们称该变量为分组变量。在清单2.13中，我们计算每个人`p`的孩子数量，其中`p`作为分组变量。然而，根据我们是否显式绑定分组变量`p`，会得到不同的结果。在第11行，我们显式使用`where`子句将变量`p`与`person`关系中的每个人绑定。因此，我们也会找到"Alice"的孩子数量，即0。另一方面，在第7行的规则中，我们没有显式绑定分组变量`p`，这意味着除了`parent`关系外，没有其他信息可用。由于"Alice"不是任何人的父母，结果中将不存在`("Alice", 0)`这一条目。

最后，量词聚合器如`forall`和`exists`返回一个布尔变量。例如，对于清单2.14中所示的聚合，变量`sat`被赋值为以下语句的真值（`true`或`false`）：“对于所有的`a`和`b`，如果`b`是`a`的父亲，那么`a`是`b`的儿子或女儿”。最终，我们会得到一个事实`integrity_constraint(true)`，这意味着在给定第1-2行所示的亲属关系事实的情况下，该约束条件得到了满足。

关于聚合，有几点语法检查需要注意。首先，与否定类似，聚合也需要分层——一个关系不能通过聚合依赖于自身。其次，绑定变量必须被聚合体中的至少一个正原子绑定。最后，规则体和聚合体形成嵌套作用域。如果外部作用域中的聚合重新定义了某个变量，则该变量在内部作用域中会被遮蔽。

2.4 概率编程

尽管Scallop主要是为神经符号编程设计的，但其语法也支持概率编程。这在将Scallop代码与神经网络集成之前进行调试时尤其有用。考虑一个机器学习程序员希望从自然语言句子“Bob带他的女儿Alice去海滩”中提取结构化关系。程序员可以模拟神经网络生成Alice（A）和Bob（B）之间亲属关系的概率分布。如清单2.15所示，我们列出了Alice和Bob之间所有可能的亲属关系。对于每一种关系，我们使用语法`[PROB]::[TUPLE]`为亲属关系元组标记概率。分号“;”分隔这些元组，表示它们是互斥的——Bob不能同时是Alice的母亲和父亲。

Scallop还支持从概率分布中采样的操作符。它们与聚合操作共享相同的语法形式，允许在分组（group-by）的情况下进行采样。清单2.16中所示的规则确定性地选择给定一对人`a`和`b`之间最可能的亲属关系，其中`a`和`b`在此聚合中是隐式的分组变量。最终，根据上述概率，只会推导出一个事实`0.95::top_1_kinship(FATHER, A, B)`。还支持其他类型的采样，包括分类采样（`categorical `）和均匀采样（`uniform `），其中静态常量`K`表示试验次数。

最后，规则也可以被标记概率，以反映其置信度。以下规则表明，祖母的女儿是某人的母亲，置信度为90%。概率规则是一种语法糖。它们的实现方式是在规则体中引入一个辅助的零元（即布尔）事实，该事实以标记的概率被视为真。

2.5 按需计算

在普通的Scallop中，事实是以自底向上的方式计算的。也就是说，对于每条规则，我们从用现有事实接地（grounding）规则体开始，然后推导出头部的事实。通常，这会推导出关系的所有可能结果，这可能会很耗费资源。更糟糕的是，由于推导的关系可能是无限的，甚至可能无法完全推导出来。

一个例子是斐波那契数的计算（之前在清单2.10中也展示过）。斐波那契数本身是无限的，因此给定0和1的基本情况，预计所有斐波那契数的计算将永远不会终止。这样的Scallop程序如清单2.18所示。然而，很多时候我们对这些无限关系有特定的查询需求。如清单2.19中第6行所示，我们查询第5个斐波那契数，而不期望其他结果。对于这种情况，我们可以使用按需计算来回答这些查询，而无需计算完整的无限关系。具体来说，数字5是`fib`关系的需求。

我们在Scallop中通过以下方式实现按需计算（清单2.19）。首先，如第2行所示，我们在定义`fib`关系时为变量`x`添加了`bound`关键字。这被称为修饰（adornment），意味着每次计算`fib`关系时，我们将第一个参数`x`视为输入。对于未被`bound`关键字修饰的第二个变量`y`，意味着其值将由规则推导得出。未被`bound`修饰的变量被视为自由变量。我们说`bound-free`（简称`bf`）是`fib`关系的按需模式。在没有明确指定的情况下，普通关系具有全自由（all-free）的按需模式，这意味着它们不是按需关系。

对于以按需关系为头部原子的规则，其良构性与普通规则略有不同。具体来说，不仅正原子体中的变量被视为绑定变量，按需头部原子中绑定的变量也被视为绑定变量。

按需关系可用于优化查询的执行。考虑清单2.20中所示的边-路径示例。假设我们有一个包含数千条边的密集图，为`path`定义的普通传递闭包将枚举图中所有可能的路径。然而，假设我们在第9行有一个查询，希望找到所有可以到达特定汇点`S`的源点，那么就没有必要枚举所有路径。此查询的理想需求模式是`fb`，意味着我们希望将`path`的第二个参数设置为绑定变量（第3行）。通过这种修饰，Scallop将仅计算到达`S`的路径，从而避免对所有可能路径的昂贵探索。

2.6 代数数据类型

代数数据类型（Algebraic Data Types，ADTs）是一种强大的编程构造，允许用户定义自定义数据结构和枚举变体。它们可以用于定义递归数据结构，如列表和树。领域特定语言（DSLs）也可以使用ADTs来表示。例如，图2.3和清单2.21展示了一个简单的整数算术语言，该语言在Scallop中表示为自定义ADT。我们使用`type`关键字开始声明，并使用竖线（`|`）符号分隔每个ADT变体。这里有三个变体，其中`Add`和`Sub`变体被认为是递归的，因为它们的参数包含`Expr`类型本身。另一方面，`Int`变体是一个终端。我们在清单2.21的第6行展示了一个声明为常量的自定义`Expr`类型的实体。

自定义ADT的值可以像Scallop中的其他值一样使用。清单2.21的第9行声明了一个存储此类表达式的一元关系，而第10行展示了该关系的一个事实，其中包含常量`MY_EXPR`。接下来，我们展示了如何在Scallop规则中动态读取和创建实体。

实体可以通过模式匹配表达式进行解构。例如，清单2.22展示了三条规则，每条规则处理`Expr` ADT的某个变体。第一条“规则”表示“对表达式`Int(i)`求值会得到整数`i`”。虽然它看起来像是一个事实，但由于存在未绑定的变量`i`，它将被脱糖并视为一条规则。第二条和第三条规则分别匹配`Add`和`Sub`变体。它们递归地对子表达式`e1`和`e2`求值，然后将结果相加或相减以形成最终结果。

处理ADT实体的关系也可以通过`bound`关键字进行修饰，以指示按需计算模式。例如，在清单2.22的第2行，我们让`eval`接受表达式并生成整数结果。如果未指定模式，Scallop将评估每一个已声明的表达式。然而，现在我们在第10行指定了一个需求（`MY_EXPR`），Scallop将仅评估必要的表达式以计算`MY_EXPR`的结果，从而生成结果事实`eval(MY_EXPR, 2)`。

2.7 外部接口

Scallop支持外部接口，允许外部定义函数、谓词和属性。这些构造使Scallop能够在多种应用中有效发挥作用，包括与基础模型的紧密集成，我们将在第5章中详细描述。在本节中，我们将介绍这些构造以及包含接口项的标准库的一部分。我们注意到，本节中的代码片段可能会展示`extern`关键字的使用，表明外部定义项的声明。然而，在正常使用Scallop时，此类声明并非必需，大多数外部构造会自动导入。

2.7.1 外部函数

在Scallop中，外部函数是纯函数，接受基本值并在成功时返回单个基本值。我们在之前的示例中展示了简单的算术操作和外部函数调用（例如清单2.8），本节将更详细地探讨这些内容。在最简单的形式中，外部函数被定义为`$FUNC(ARG_TYPE, ...) -> RET_TYPE`。函数名称以美元符号`$`开头，可以接受多个带有声明参数类型（`ARG_TYPE`）的参数。函数在成功时必须返回一个返回值类型的值。然而，Scallop的外部函数接口允许一些高级特性，例如：(a) 带有类型参数的泛型函数，(b) 带有可选参数的函数，以及(c) 带有可变参数（vararg）的函数。清单2.23展示了一些使用这些特性的示例。我们现在详细说明这些特性。

泛型函数 在定义函数类型时，我们可以在函数名称后使用额外的尖括号`<...>`来指定泛型类型参数。每个类型参数后面可以跟随一个类型族（type family），以对类型施加额外的约束。例如，清单2.23中展示的`$abs`函数是一个泛型函数，具有一个类型参数`T`，该参数需要属于`Number`类型族。有符号或无符号整数以及浮点数都属于`Number`类型族。绝对值函数可以正确定义在任何此类数据类型上。

Scallop中有一组固定的类型族，包括`Any`、`Number`、`Integer`和`Float`。作为一种语法糖，如果未在类型参数上指定类型族，我们默认其类型族为`Any`，允许传递任何类型的值。

在使用泛型函数时，不需要显式地用具体类型实例化函数，因为Scallop的类型推断模块会自动找到最合适的类型。例如，在没有特殊配置的情况下，Scallop中的表达式`$abs(-3)`将返回类型为`i32`的数字`3`，因为字面量`-3`默认具有`i32`类型。

可选参数 在指定函数的参数类型时，我们可以在类型末尾添加问号（`?`）来表示该参数是可选的。可选参数必须出现在非可选参数之后。例如，清单2.23中展示的`$substring`函数具有一个可选参数`e`。这意味着我们可以以两种不同的方式调用该函数：`$substring("hello", 3)`返回`"lo"`，而`$substring("hello", 3, 4)`返回`"l"`。

可变参数 有些函数可以接受任意数量的参数。我们可以通过在参数类型后添加省略号（`...`）来指定可变参数（vararg）属性。需要注意的是，可变参数与可选参数类似，必须出现在非可变参数之后。一个外部函数最多只能有一个可变参数。清单2.23中展示的`$string_concat`函数是一个示例，它可以接受任意数量的字符串并执行连接操作。例如，`$string_concat("a", "b")`返回`"ab"`，而`$string_concat("a", "b", "c")`返回`"abc"`。

需要注意的是，在指定可变参数时，具有任意数量的参数必须是相同类型或类型族。如果我们希望接受任意类型的参数，可以使用类型族`Any`。例如，`$format`函数接受一个格式字符串和任意数量的任意值。当调用`$format("1 + 1 = {}", 1 + 1)`时，第二个参数是整数（`i32`），返回值将是`"1 + 1 = 2"`。但当调用`$format("{} > 0? {}", 1, 1 > 0)`时，第二个参数是整数，而第三个参数是布尔值，返回值将是`"1 > 0? true"`。

错误处理 外部函数可能会失败。当它们失败时，不会返回值，并且针对该输入的计算将被丢弃。例如，隐式外部函数（如除法）可能会由于除零错误而失败，而显式外部函数（如`$substring`）可能会在给定索引超出字符串范围时失败。默认情况下，不会抛出错误消息，错误会被静默抑制。这是有益的，因为在关系型和声明式语言中，输入可能是概率性的，可能会发生大量冗余计算，并且外部函数可能会在无效输入上调用。尽管如此，Scallop提供了编译器和运行时选项以允许报告错误。

2.7.2 外部谓词

外部谓词是外部函数的广义接口，现在可以生成多个输出并关联附加信息（如概率）。谓词的声明方式与Scallop中的其他关系类似，其中输入应关联`bound`关键字，而输出可以关联`free`关键字。在这里，我们添加`extern`关键字来表示`PREDICATE`应在外部定义。

从概念上讲，外部谓词“关联”输入和输出。这意味着，给定谓词的特定输入，谓词可能会生成涉及输入和输出的多个事实。在清单2.24中，我们展示了一个外部谓词`string_chars`，它可以帮助获取RNA序列字符串中的核苷酸（`{A, C, G, U}`）。以字符串`s`作为输入，`string_chars`生成`(s, i, n)`三元组，其中`i`是字符串中字符的索引，`n`是字符本身。显然，`string_chars`返回多个事实作为输出，而上一节介绍的外部函数只能返回一个输出。

生成概率的外部谓词 外部谓词生成的事实可以与附加标签关联。此特性的最常见用例是概率函数的编码。例如，在标准库中，Scallop提供了一个名为`soft_eq`的外部谓词，用于比较两个数字的相等性。然而，谓词并不返回精确的离散`false`或`true`，而是希望根据两个数字的距离计算它们相等的概率。形式上，其定义如下：

本质上，我们有一个参数`β`，它决定了两个数字可以不同的阈值。当`x = y`时，我们有`Pr(x = y) = 1`。当`x = 0.9`且`y = 1.0`且参数`β = 1.0`时，我们有`Pr(x = y) ≈ 0.998`，这意味着这两个数字非常接近。在Scallop中，此类程序可以写成清单2.25的形式。

生成概率的外部谓词的其他用途包括向量或高维张量之间的相似性。我们将在第5章中展示更多返回带有概率增强事实的外部谓词示例。

2.7.3 外部属性

在Scallop中，属性是一种高阶构造，可用于注释任何Scallop程序项，包括函数、谓词、事实和规则的声明。属性是以`@`符号开头的构造，可以接受任意参数，包括位置参数和关键字参数。从概念上讲，可以将属性视为接受被注释的项并返回另一个项。

清单2.27中的以下示例展示了使用`@file`属性注释名为`edge`的关系。具体来说，它告诉Scallop将外部CSV（逗号分隔值）文件加载到`edge`关系中。从概念上讲，`@file`属性处理原本为空的关系`edge`，并返回一个从文件加载内容填充的`edge`关系。

在Scallop的标准库中，有许多现有的外部属性。例如，`@storage`可用于注释关系，以指定用于该关系的内部存储，这可以帮助程序员优化Scallop程序的性能。此外，`@cmd_arg`将命令行参数（如果可用）检索到被注释的关系中。然而，只有当属性集可以通过外部插件和库扩展时，外部属性的强大功能才能得到充分展示。外部数据库、模型和应用程序都可以成为注释Scallop关系的外部属性。我们将在第5章中进一步讨论这一点。

3 核心推理框架

前一章介绍了Scallop的表面语言，用于表达离散推理。然而，为了支持端到端的训练，该语言还必须支持可微推理。在本章中，我们通过溯源框架（provenance framework）正式定义语言的语义。我们展示了Scallop如何通过定义不同的溯源，统一支持离散、概率和可微推理模式。

我们从溯源框架的基础知识开始（第3.1节），然后介绍一种低级表示SclRam、其操作语义及其与Scallop应用程序其余部分的接口（第3.2-3.3节）。接着，我们展示溯源框架如何支持概率和可微推理（第3.5-3.7节）。最后，我们在第3.8节讨论实际扩展。

3.1 溯源框架

溯源框架在Scallop程序的执行过程中，沿着关系元组传播附加信息（例如概率、证明）。该框架基于溯源半环理论（Green et al., 2007）。图3.1定义了Scallop的溯源代数接口。我们将附加信息称为标签（tag）`t`，它来自标签空间`T`。有两个特殊的标签`0`和`1`，分别表示无条件假和真。标签通过二元析取`⊕`、二元合取`⊗`和一元否定`⊖`操作传播，这些操作分别类似于逻辑或、与和非。最后，饱和检查`⃝=`作为固定点迭代的可定制停止机制。上述所有组件共同构成一个七元组`(T, 0, 1, ⊕, ⊗, ⊖, ⃝=)`，我们称之为溯源`T`。Scallop提供了一个内置的溯源库，用户可以通过实现此接口添加自定义溯源。

来源必须满足一些属性。首先，(T, 0, 1, ⊕, ⊗) 应形成一个交换半环。也就是说，0 是加法单位元且在乘法下消去，1 是乘法单位元，⊕ 和 ⊗ 是结合且交换的，并且 ⊗ 对 ⊕ 分配。为了保证不动点的存在性（在第 3.3 节中讨论），它还必须是吸收的，即 t1 ⊕ (t1 ⊗ t2) = t1（Dannert 等人，2021）。此外，我们需要 ⊖ 0 = 1，⊖ 1 = 0，0⃝̸=1，0⃝=0，以及 1⃝=1。违反个别属性（例如吸收性）的来源对于不使用受影响功能（例如递归）的应用程序或用户希望绕过限制的情况仍然有用。

3.2 SclRam 中间语言

Scallop 程序被编译为一种称为 SclRam 的低级表示形式。图 3.2 展示了 SclRam 核心片段的抽象语法。表达式类似于扩展关系代数中的查询。它们通过对关系谓词（p）进行操作，使用一元操作进行聚合（γg，其中 g 是聚合器）、投影（πα，其中 α 是映射）和选择（σβ，其中 β 是条件），以及二元操作并集（∪）、积（×）、连接（▷◁）、差集（−）和反连接（▷）。我们注意到，还有其他二元操作，例如交集（∩），可以通过组合上述核心操作来编码。

SclRam 中的规则 r 表示为 p ← e，其中谓词 p 是规则头，表达式 e 是规则体。一组无序的规则组合形成一个层（stratum）s，而一系列层 s1; . . . ; sn 构成一个 SclRam 程序。同一层中的规则具有不同的头部谓词。用 Ps 表示层 s 中的头部谓词集合，我们还要求程序中所有 i̸ = j 的 Psi ∩ Psj = ∅。表层语言中的分层否定和聚合在 SclRam 中通过语法限制强制执行：在层 si 的规则中，如果关系谓词 p 在聚合（γ）或差集（−）的右侧使用，则该谓词 p 不能在 Psj 中出现，其中 j ≥ i。

接下来，我们在图 3.3 中定义了语义域，这些域将用于后续定义 SclRam 的语义。一个元组 u 可以是一个常量或一个元组序列。一个事实 p(u) ∈ F 是在关系谓词 p 下命名的元组 u。元组和事实可以被标记，形成标记元组 (t :: u) 和标记事实 (t :: p(u))。给定一组标记元组 UT，当且仅当存在一个 t 使得 t :: u ∈ UT 时，我们说 UT ⊨ u。一组标记事实构成一个数据库 FT。我们使用括号表示法 FT [p] 来表示 FT 中在谓词 p 下的标记事实集合。

3.3 SclRam 的操作语义

我们现在在图 3.4 中为 SclRam 的核心片段提供操作语义。一个 SclRam 程序 s 以扩展数据库（EDB）FT 作为输入，并返回一个意图数据库（IDB）F′T = JsK(FT)。该语义以底层来源 T 为条件。我们称之为带标记的语义，以区别于传统 Datalog 中的无标记语义。

基本关系代数 在 SclRam 中，表达式的评估根据图 3.4 顶部定义的规则生成一组带标记的元组。谓词 p 评估为数据库中该谓词下的所有事实。选择操作过滤满足条件 β 的元组，而投影操作根据映射 α 转换元组。映射函数 α 是部分的：它可能会失败，因为它可以对值应用外部函数。并集 e1 ∪ e2 中的元组可以来自 e1 或 e2。在（笛卡尔）积操作中，每对传入的元组被组合，并使用 ⊗ 计算它们的标记。

差集与否定 为了评估差集表达式 e1 − e2，有两种情况取决于从 e1 评估的元组 u 是否出现在 e2 的结果中。如果没有出现，我们简单地将元组及其标记传播到结果中（Diff-1）；否则，我们从 e1 获取 t1 :: u，从 e2 获取 t2 :: u。与无标记语义中从结果中删除元组 u 不同，我们使用标记 t1 ⊗ (⊖ t2) 传播 u（Diff-2）。通过这种方式，在否定过程中信息不会丢失。图 3.5 比较了不同语义下对示例差集表达式的评估。虽然在无标记语义的结果中元组 (2, 3) 被移除，但在带标记语义中它仍然保留。

聚合 SclRam 中的聚合器是离散函数 g，作用于（无标记的）元组集合 U ∈ U。它们返回一组聚合后的元组，以处理像 argmax 这样可以产生多个结果的聚合器。例如，count(U) = {|U|}。然而，在概率领域中，离散符号并不足够。给定 n 个带标记的元组进行聚合，每个带标记的元组可以被开启或关闭，从而产生 2^n 个不同的世界。每个世界是输入集合 UT（|UT| = n）的一个分区。将正部分记为 XT，负部分记为 XT = UT − XT，与此世界关联的标记是 XT 中标记和 XT 中否定标记的合取。在这个世界上进行聚合涉及将聚合器 g 应用于正部分 XT 中的元组。如果我们枚举所有世界，这本质上是指数级的。然而，我们可以针对每个聚合器和每个来源进行优化，以实现更好的性能。例如，在 max-min-prob 标记元组上进行计数可以通过 O(n log(n)) 的算法实现，比指数级快得多。图 3.6 展示了一个运行示例以及在 max-min-prob 来源下对计数表达式的评估。结果计数可以是 0-9，每个值都可以由多个世界推导得出。

规则与不动点迭代 在数据库 FT 上评估规则 p ← e 涉及评估表达式 e 并将结果与 FT 中谓词 p 下的现有事实合并。由于表达式如并集、投影或聚合，评估 e 的结果可能包含由不同标记标记的重复元组。因此，我们通过对集合进行规范化处理，将对应同一元组的不同标记进行合并（⊕）。接下来，有三种情况需要将新推导的元组（⟨JeK(FT )⟩）与之前推导的元组（JpK(FT )）合并。如果事实仅存在于旧集合或新集合中，我们简单地将该事实传播到输出中。当元组 u 同时出现在旧集合和新集合中时，我们传播旧标记和新标记的析取（told ⊕ tnew）。综合所有情况，我们得到谓词 p 下的一组新标记事实。

SclRam 中的递归执行类似于 Datalog 中的最小不动点迭代（Abiteboul 等，1995）。迭代按层进行，以强制执行分层否定和聚合。评估层 s 的单个步骤意味着评估 s 中的所有规则并返回更新后的数据库。请注意，我们定义了一个专门的最小不动点运算符 lfp◦，一旦整个数据库饱和，迭代就会停止。图 3.7 展示了一个涉及递归和数据库饱和的评估示例。整个数据库在第 7 次迭代时饱和，并找到与迷宫中最优路径关联的标记。由于存在值创建等特性，SclRam 中的终止性并不普遍保证。但其存在性可以在每个来源的基础上证明。例如，可以很容易地证明，如果一个程序在无标记语义下终止，那么它在 max-min-prob 来源的带标记语义下也会终止。

3.4 外部接口与执行流程

到目前为止，我们仅展示了 max-min-prob 来源，其中标记是近似概率。还有其他概率来源具有更复杂的标记，例如证明树或布尔公式。因此，我们为每个来源 T 引入一个输入标记空间 I、一个输出标记空间 O、一个标记函数 τ : I → T 和一个恢复函数 ρ : T → O。例如，所有概率来源共享相同的输入和输出标记空间 I = O = [0, 1]，以实现统一的接口，而内部标记空间 T 可能不同。我们将四元组 (I, O, τ, ρ) 称为来源 T 的外部接口。整个执行流程如下所示：

在 Scallop 应用程序的上下文中，EDB 以 Foption 的形式提供。在标记阶段，τ 被应用于每个输入标记以获得 FT，随后 SclRam 程序在 FT 上运行。为了方便起见，并非所有输入事实都需要被标记——未标记的输入事实在 FT 中被分配标记 1。在恢复阶段，ρ 被应用于获得 FO，即整个流程返回的 IDB。Scallop 允许用户指定一组输出关系，并且 ρ 仅应用于这些关系下的标记，以避免冗余计算。

示例 3.2 来自示例 3.1 的 max-min-prob 来源的外部接口是 ([0, 1], [0, 1], id, id)，其中输入和输出空间是 0 到 1 之间的实数，而标记函数和恢复函数 id 是恒等函数 λx.x。

3.5 基于来源的精确概率推理

如果来源 T 的输入空间 I 和输出空间 O 是 [0, 1] 范围内的实数值，我们称来源 T 是概率性的。因此，示例 3.1 中展示的 max-min-prob 来源是一种概率性来源。然而，尽管 max-min-prob 在实践中很有用，但它仅计算真实概率的近似值。在本节中，我们首先介绍一种能够推导出精确概率的更强大的来源。

我们引入 proofs-prob来源，它跟踪以析取范式（DNF）表示的布尔公式。在高层次上，布尔公式编码了 IDB 中的事实如何从 EDB 中的现有事实推导出的完整谱系。DNF 公式的定义如图 3.8 所示。假设 EDB 中有 n 个独立同分布（i.i.d.）概率的事实；我们创建 n 个布尔变量，分别标记为 v1, . . . , vn。然后，布尔公式中的文字可以是正布尔变量或否定（¬）布尔变量。一组通过逻辑与（∧）连接的不同文字形成一个合取子句，而一组通过逻辑或（∨）连接的子句形成一个析取范式公式 φ。我们注意到有两个特殊的 DNF 公式，即真（⊤）和假（⊥）。⊤ 是一个包含一个空合取子句的单例 DNF 公式，而 ⊥ 是一个空的 DNF 公式。因此，proofs-prob 的正式定义如下：

根据图 3.5，我们在图 3.9 中展示了 proofs-prob 推导过程的一个示例。在这里，除了中间部分展示的标记传播过程外，我们还在顶部包含了标记阶段，在底部包含了恢复阶段。标记函数 τpp 将输入概率转换为内部标记。在布尔公式推导完成后，我们应用恢复函数 ρpp 来计算结果事实的概率。最后，我们注意到通过加权模型计数（WMC）过程计算的结果是对应标记事实的概率。

WMC 过程本质上是根据布尔变量的权重计算布尔公式的权重。在这里，我们直接将每个输入事实关联的概率作为分配的布尔变量的权重。需要注意的是，WMC 是 #P-完全的，这意味着计算精确概率可能是运行时的主要贡献者。与所有操作均为 O(1) 的 max-min-prob 相比，计算精确概率的成本要高得多。在后续章节中，我们将描述在保持不同程度近似的同时，可以促进学习的优化方法。

3.6 基于 Top-K 证明来源的可扩展推理

我们问题设置中的概率性质为近似计算提供了空间。一个关键的观察是，当推理系统用于学习设置时，真实事实的概率应显著高于其他事实，形成一种偏态分布。我们可以通过仅包含“最可能”的证明来利用这一特性。

首先，我们引入一种不同的方式来形式化证明和 top-k 证明。我们将每个 DNF 布尔公式 φ 视为一组证明，其中每个证明是一组文字的集合。因此，⊥ = ∅，而 ⊤ = {∅}，即一个以 ∅ 为唯一元素的单例集合。我们通过图 3.10 中的示例展示了证明构建的过程。形式上，析取（∨）操作被定义为集合的并集（∪），而合取（∧）操作被定义为基于证明的并集的笛卡尔积：

为了执行近似计算，我们定义了修改后的析取和合取操作，即 ⊕(k) 和 ⊗(k)，其中 k 是一个可调参数，用于控制近似的程度。

目标是挑选出结果中的“top-k”证明，其中证明按其各自的概率进行排序。具体来说，每个证明的概率 Pr(η) 按以下方式计算：

直观地说，每当执行 ∨ 或 ∧ 操作时，我们按证明的可能性对其进行排序，并仅保留前 k 个证明。这使得我们能够丢弃绝大多数证明，从而使推理变得可行。在 ∧(k) 操作中合并两个证明时，可能会出现冲突的文字，例如 vi 和 ¬vi，在这种情况下，由于该证明的概率为零，我们会移除整个证明。图 3.11 展示了一个 top-3 合取（⊗(3)）的示例运行过程，其中我们先执行正常的 ⊗ 操作，然后进行 top-3 过滤。

为了对 DNF φ 执行否定 ¬(k)，我们首先否定所有文字以获得与 ¬φ 等价的合取范式（CNF）。然后，我们执行 cnf2dnf 操作（包括冲突检查）将其转换回 DNF。最后执行 top-k 操作，如下所示：

因此，在 top-k 证明来源下，所有标记的证明数量都被限制在 k 以内，这使得 WMC 过程变得可行。假设 n 是事实的数量且 k ≪ n，我们仍然需要每次合取操作花费 O(n²) 的时间，而否定操作花费 O(2ⁿ) 的时间。这使得 top-k 证明来源比 prob-proofs 来源更具可扩展性。

我们还注意到，我们的 top-k 推理算法与束搜索（beam search）有相似之处。两种方法都是迭代的，并且在每一步仅探索前 k 个元素。然而，有两个主要区别将我们与束搜索区分开来。首先，虽然束搜索是启发式的，但我们的算法基于 Datalog 语义和来源半环框架，确保了其正确性。我们还提供了关于其近似误差界限的形式化保证。其次，我们的算法在每个推导事实的证明集 ϕ 上操作，而束搜索通常用于搜索输出。

3.7 可微分推理

我们现在阐述来源如何支持可微分推理。假设我们有 n 个与概率相关联的输入事实。让 EDB 中的所有概率形成一个向量 ⃗r ∈ Rⁿ，而结果 IDB 中的概率形成一个向量 ⃗y ∈ Rᵐ。微分涉及推导输出概率 ⃗y 以及导数 ∇⃗y = ∂⃗y/∂⃗r ∈ Rᵐ×ⁿ。从学习的角度来看，输出概率 ⃗y 可用于计算后续步骤中的损失，而导数 ∇⃗y 可用于反向传播梯度以进行优化。

在 Scallop 中，可以使用可微分来源来获取这些值。可微分来源共享相同的外部接口——让输入标记空间 I = [0, 1]，输出标记空间 O 为对偶数空间 D（图 3.12）。现在，每个输入标记 ri ∈ [0, 1] 是一个概率，而每个输出标记封装了输出概率 yj 及其对输入的导数 ∇yj。从这里，我们可以通过分别堆叠 yj 和 ∇yj 来获得预期的输出 ⃗y 和 ∇⃗y。

Scallop 提供了 8 种可配置的内置可微分来源，这些来源在运行时效率、推理粒度和性能方面具有不同的经验优势。在本节中，我们将详细阐述 3 种简单但多功能的可微分来源，其定义如图 3.13 所示。在接下来的讨论中，我们使用 ri 表示向量 ⃗r 的第 i 个元素，其中 i 称为变量（ID）。向量 ⃗ei ∈ Rⁿ 是标准基向量，其中除第 i 个条目外，所有条目均为 0。

3.7.1 diff-max-min-prob (dmmp)

该来源是 mmp 的可微分版本。当从输入标记中获取 ri 时，我们通过附加 ⃗ei 作为其导数将其转换为对偶数。请注意，在整个执行过程中，导数始终最多只有一个非零条目，具体为 1 或 -1。饱和检查仅基于概率部分的相等性，因此导数不会影响终止性。其所有操作都可以通过时间复杂度为 O(1) 的算法实现，使其在运行时极为高效。

3.7.2 diff-add-mult-prob (damp)

该来源具有与 dmmp 相同的内部标记空间、标记函数和恢复函数。如其名称所示，其析取和合取操作分别是对偶数的加法和乘法。在执行析取时，我们对通过加法获得的对偶数的实部进行截断，同时保持导数不变。damp 的饱和函数设计为始终返回 true，以避免非终止性。但这一决定使其不太适合复杂的递归程序。damp 中操作的时间复杂度为 O(n)，虽然比 dmmp 慢，但在实践中仍然非常高效。

3.7.3 diff-top-k-proofs (dtkp)

该来源扩展了最初由 Huang 等人于 2021 年提出的 top-k 证明半环，以额外支持否定和聚合。如第 3.6 节所介绍并在图 3.13 中所示，dtkp 的标记是析取范式（DNF）中的布尔公式 φ ∈ Φ。dtkp 与普通 top-k 证明来源的区别仅在于外部接口：可微分来源将对偶数作为输入标记，并需要输出对偶数作为输出标记。具体来说，dtkp 的标记函数和恢复函数定义如下：

其中，WMC 是一种可微分的加权模型计数过程，借鉴自 Manhaeve 等人于 2021 年的工作。除了布尔公式 φ 外，WMC 还接受每个概率变量 i 的权重。与 top-k 证明中使用的简单概率不同，权重现在是对偶数，例如 (Pr(vi), ⃗ei)。在可微分 WMC 过程中，将应用对偶数的加法和乘法规则（图 3.12）。在实现方面，Scallop 采用 Sentential Decision Diagram (SDD)（Darwiche, 2011）来执行 WMC 过程。

3.8 实际扩展

在本节中，我们讨论了使 Scallop 的计算具有可扩展性、易处理性和广泛适用性的实际扩展。

3.8.1 事实的早期移除

在计算过程中，标记为 0 的事实通常是无用的，因此保留这些被标记为 0 的事实是没有意义的。在 Scallop 的来源框架中，我们允许每个来源指定是否要提前移除这些事实。我们在来源接口中引入了一个新函数 discard : T → Bool。当对某个事实的标记调用该函数并返回 true（⊤）时，该事实将从进一步的计算中移除。此函数的默认实现是discard(t) = t ⃝= 0。

3.8.2 事实的互斥性

回顾一下，Scallop 允许用户指定互斥的概率事实集合（见清单 2.15）。事实的互斥性由每个来源选择性地处理。这是因为完全处理互斥性需要额外的计算，而这可能并不总是可取的。具体来说，它需要显式编码逻辑推导过程，以确保可满足性不仅仅依赖于两个互斥的事实。虽然这可以通过多种方式实现，但在像 prob-proofs 和 top-k-proofs 这样的来源中使用的证明数据结构可以自然地扩展以处理互斥性。相反，像 max-min-prob 和 add-mult-prob 这样更简单的来源由于其标记过于简单而无法处理互斥性。

我们以 prob-proofs 为例，展示如何扩展它以处理互斥性。在 Scallop 中，prob-proofs（以及其他如 top-k-proofs）已经扩展了此功能。但为了演示目的，我们考虑一个新的来源，命名为 prob-proofs-me，其中 me 代表互斥性。在 prob-proofs-me 中，它不再接受简单的概率作为输入标记，而是接受一个包含概率和可选互斥集合 ID（N）的元组。即，Iprob-proofs-me = [0, 1] × option 。

考虑清单 3.1 中所示的示例。两组互斥事实被转换为两个不同的互斥 ID，我们分别标记为 0 和 1。事实 color(OBJ_A, "red") 在技术上被标记为 (0.9, 0)。第一个元素 0.9 被视为正常的概率，而从此事实 ID 到互斥 ID 的映射被存储以供将来参考。当执行规则（第 4 行）时，会推导出一个临时证明，其中包含事实 color(OBJ_A, "red") 和 color(OBJ_A, "green")。然而，在查找互斥信息时，我们发现这两个事实不能在同一证明中共存。prob-proofs 来源将拒绝这样的证明，使结果标记为 0。因此，结合早期移除功能，should_not_exist 关系被计算为空，符合预期。

3.8.3 针对来源的专门化

Scallop 来源框架的设计允许推理算法针对每个来源进行专门化。例如，如图 3.4 所示，聚合操作原则上需要枚举子集，这本质上是一个 O(2ⁿ) 的操作，假设 n 是用于聚合的事实数量。然而，并非所有聚合都需要这种复杂的推理。例如，当对一组 max-min-prob 标记的元组执行计数聚合器时，可以优化为 O(n log(n)) 的操作。我们在算法 1 中展示了优化后的计数算法。请注意，为了简单起见，我们仅展示了针对 mmp 的算法，但它可以轻松扩展到 dmmp。可以很容易地证明其运行时复杂度为 O(n log(n))，因为运行时的上限是第 1 行的排序操作。Scallop 还实现了许多其他优化，具有不同程度的近似性，使得在应用于实际场景时，原则上昂贵的操作变得可行。

3.8.4 采样操作

Scallop 支持诸如 top、categorical 和 uniform 等采样操作。为了实现这些操作，必须有一个信号来对标记事实进行排序。因此，我们在来源中引入了一个新函数：weight : T → R。顾名思义，weight 函数接受一个标记并返回其权重。对于概率来源，默认实现就是恢复函数，因为返回值是一个概率 p ∈ [0, 1]，非常适合作为权重。返回的权重将用于对事实进行排序或加权采样。

3.8.5 来源选择

一个自然的问题是，如何为给定的 Scallop 应用程序选择可微分来源。根据我们的经验评估，dtkp 通常是性能最佳的选择，而设置 k = 3 通常在运行时效率和学习性能方面都是一个不错的选择。这表明用户可以从 dtkp 作为默认选择开始。一般来说，来源选择过程类似于机器学习中常见的超参数调优过程。

4 实践中的 Scallop：端到端示例

在本章中，我们展示了端到端的示例，展示如何使用 Scallop 在相对简单的任务上进行神经符号学习。对于每个案例研究，我们提供了全面的问题设置、Scallop 代码以及最终结果。

4.1 两个 MNIST 数字的求和

来自 Manhaeve 等人（2021）的 MNIST-Sum2 任务涉及对手写数字对的求和进行分类，例如 + = 10。模型仅接收两个 MNIST 数字作为输入，并且需要在仅有的求和监督下学习识别这两个数字。

如图 4.1 所示，我们按照 DeepProbLog（Manhaeve 等人，2021）的风格，使用神经组件和符号组件来指定此任务。神经组件是一个感知模型，它接收手写数字图像（Lecun 等人，1998）并将其分类为离散值 {0, . . . , 9}。另一方面，符号组件是一个用于计算结果的 Datalog 逻辑程序。神经组件和符号组件之间的接口是一个概率数据库，它将感知模型的每个候选输出与一个概率关联起来。例如，事实 0.85 :: d 表示图像被识别为数字 3 的概率为 0.85。因此，数据库由 20 个事实组成——每个图像对应的 10 个可能数字各有一个事实。

在概率数据库上评估逻辑程序会为两个数字之和的每个可能结果（即范围 {0, . . . , 18} 中的值）生成一个加权布尔公式。每个公式的子句代表相应结果的不同证明。例如，图 4.1 的左下角显示了代表真实结果 10 的所有 9 个证明的公式。每个这样的公式都被输入到一个现成的加权模型计数（WMC）求解器中，以生成相应结果的概率，例如 0.7261 :: sum(10)。

在实践中，精确可微分概率推理的可扩展性受到 WMC 求解的限制，其复杂度至少为 #P-难。正如 top-k 证明来源的讨论所建议的那样，仅计算前 k 个最可能的证明可以将每个公式的大小限制为 k 个子句，从而允许以少量的准确性损失换取可扩展性的大幅提升。此外，深度感知模型的随机训练本身可以容忍数据中的噪声。在这种情况下，仅使用 k = 1 即可实现 97.46% 的性能，这在实际中被证明是 k ∈ {1, 3, 5, 10} 中的最佳表现。

实际实现如清单 4.1 所示。mnist_net（第 4 行）是将单个 MNIST 图像分类为 10 个类别分布的神经网络，而 sum_2（第 5-13 行）是用于对两个数字求和进行概率推理的 Scallop 推理模块。我们没有编写包含推理程序的单独 Scallop 文件，而是将程序作为字符串传递给 scallopy.Module 进行构造。我们注意到，为了更清晰的展示，此处展示的程序与图 4.1 中的程序略有不同。第 10-12 行说明了如何将输入分布转换为关系符号（反之亦然用于输出）。第 13 行配置了用于推理的来源，即使用 k = 1 的 dtkp来源。

在推理过程中，如 **forward** 函数（第 15-21 行）所示，我们将两批图像分别传递给 **mnist_net**，以生成两批图像的分布。最后，我们将这两批分布传递给 **sum_2** 推理模块，以获得形状为 19 的批处理输出张量，其中每个元素对应 19 种可能结果（[0, 18]）之一。至此，我们的训练管道完成。Scallop 的所有算法和微分细节都对用户隐藏，提供了一个简洁的编程接口。

4.2 手写公式的评估

在这个案例研究中，我们将 MNIST-Sum2 任务进一步扩展，允许包含多个符号，包括手写数字以及简单的算术运算符（如 +、−、× 和 ÷）。这就是手写公式评估（HWF）任务（Li 等人，2020）。任务的输入是一系列手写符号的图像，形成一个手写公式。输出是评估公式后得到的有理数结果。为此任务提供的数据集包含 1 到 7 个符号的可变长度公式，其中操作数均为个位数。为了简洁起见，我们假设输入公式始终可以解析且没有除以零错误。

解决此任务的一个自然方法是将问题分解为独立的感知和推理组件。感知组件是一个标准的卷积神经网络（CNN），它将每个符号分类为离散类别（数字 0-9 以及 +、−、×、÷）。推理组件随后接收分类后的概率符号，解析并评估公式，并返回结果的概率分布。值得注意的是，神经模型不会收到公式中每个单独符号标签的监督。相反，我们只有对最终评估结果的监督。Scallop 的可微分推理引擎使得可以以端到端的方式训练生成的程序，即仅使用可观察的输入-输出数据的监督来学习神经模型的参数——这被称为算法监督（Petersen，2022）。

推理组件用 Scallop 编写，如清单 4.2 所示。该程序使用类似 Datalog 的语法。它指定了两个输入关系：symbol和 length（第 2-3 行）。前者将每个符号图像的索引与其识别的符号（数字和运算符表示为字符串）关联起来，后者编码了公式的长度。

程序的其余部分定义了关系 factor（第 9-10 行）、term（第 12-15 行）和 expr（第 17-20 行），遵循简单算术表达式的标准上下文无关文法。这些关系的第一个参数是一个浮点数（类型为 f32），表示相应表达式的评估结果。最后，我们获取覆盖整个公式的表达式（第 23 行），并将评估结果存储在 result 一元关系中。

接下来，我们可以将此程序集成到端到端的学习管道中。清单 4.3 展示了用于 HWF 任务的 PyTorch 模块。在初始化期间，我们设置 CNN 来处理每个符号图像（第 6 行）。然后，我们创建一个 Scallop 模块以从文件 hwf.scl加载程序（第 8-13 行）。我们还将来源半环配置为使用 diff-top-k-proofs，并将 k 设置为 3。在训练或推理阶段，我们只需将符号图像传递给 CNN（第 17 行），并将结果分布传递给我们的 Scallop 模块（第 19 行）。由于 CNN 和 Scallop 模块都是可微分的，因此我们获得了一个端到端的学习管道。虽然在概念上相似，但与 MNIST-Sum2 相比，HWF 存在一些核心复杂性。我们现在解释这些复杂性以及 Python 接口如何帮助简化这些复杂性的处理。

输入数量的变化 首先，与接受固定数量的 2 个数字不同，HWF 推理模块需要接受长度可变的公式。在 PyTorch 中，此类信息编码在二维张量中，其中第一维编码每个符号的索引，第二维编码字母表上的分布。对于未达到最大长度的公式，张量包含填充的 0。为了处理此张量，我们为 symbol关系设置了二维的 input_mapping（第 10-12 行）。第一维（dim 0）映射到 range(MAX_LEN)，即 0, . . . , 6，因为数据集中公式的最大长度为 7。第二维将每个元素映射到 ALPHABET 中的一个符号。对于 length，我们指定它是非概率的（第 13 行）。

符号采样的需求 HWF 输入的输入空间非常大，因为可能有 7 个符号，每个符号属于 14 个类别之一，这为我们提供了大约个可能的推导树。如果不采取任何措施，Scallop 将探索所有推导树，这将非常缓慢。因此，我们不是将每个事实传递给 Scallop，而是基于预测概率进行采样。在配置 symbol的输入映射时，参数 retain_k=3和 sample_dim=1 指定在符号张量上，我们仅为每个符号（在维度 1 上）选择前 3 个类别。通过这些参数，我们能够使推理过程更具可扩展性。我们注意到，对于 HWF，仅采样 3 个类别在训练时间和学习准确性之间达到了良好的平衡。但一般来说，采样率越低，端到端训练模型所需的时间就越长。

无界的输出集合 与 MNIST-Sum2 中固定的可能输出集合（{0, . . . , 18}）不同，HWF 的潜在输出集合要大得多，因为公式包含除法运算符（÷）。枚举所有这些输出是不现实的，这就是为什么我们没有显式指定输出映射。结果是，eval_formula不能返回一个直接的向量化张量作为输出。如第 19 行所示，我们获得两个结果：out_symbols 和 out_distr。具体来说，out_symbols 将是一个分数列表，这些分数是通过采样的输入实际推导出来的。同时，out_distr 将包含对 out_symbols 中结果的分布计算。我们在清单 4.4 中展示了用于处理此类输出的损失函数。

4.3 玩 PacMan-Maze 游戏

我们进一步使用基于强化学习（RL）的规划应用程序来说明 Scallop，我们称之为 PacMan-Maze。该应用程序如图 4.3a 所示，涉及一个智能代理在简化版的 PacMan 迷宫游戏中实现一系列动作。迷宫是一个隐式的 5×5 单元格网格。每个单元格要么是空的，要么有一个实体，可以是演员（PacMan）、目标（旗帜）或敌人（幽灵）。在每一步，代理将演员移动到四个方向之一：上、下、左或右。当演员到达目标或碰到敌人时，游戏结束。迷宫以原始图像的形式提供给代理，并在每一步更新，要求代理处理感官输入，提取相关特征，并逻辑规划要采取的路径。此外，每局游戏的演员、目标和敌人的初始位置都是随机的。

具体来说，游戏被建模为代理与环境之间的一系列交互，如图 4.3b 所示。第 i 步的游戏状态 si ∈ S 是一个 200×200 的彩色图像（S = R^{200×200×3}）。代理向环境提出一个动作 ai ∈ A = {上、下、左、右}，环境生成一个新图像 si+1 作为下一个状态。环境还向代理返回一个奖励 ri：达到目标时为 1，否则为 0。此过程重复进行，直到游戏结束或达到预定义的步数限制。

实现我们应用程序的一种流行的 RL 方法是 Q-Learning（Watkins，1989）。其目标是学习一个函数 Q : S × A → R，该函数返回在状态 si 下采取动作 ai 的预期奖励。由于游戏状态是图像，我们采用深度 Q-Learning（Mnih 等，2015），它使用具有学习参数 θ 的卷积神经网络（CNN）模型来近似 Q 函数。我们应用程序的端到端深度学习方法涉及训练模型以预测给定游戏状态下每个动作的 Q 值。这...