NeSyCat Torch：神经符号学习范畴语义的可微张量实现

背景

神经符号学习（Neurosymbolic Learning, NeSy）旨在结合神经网络的感知能力与符号逻辑的推理能力。然而，当前的神经符号语义体系呈现出碎片化的状态：经典逻辑、模糊逻辑、概率系统以及纯神经网络系统各自依据其归纳规则来定义“真值”。这种分裂导致不同系统之间缺乏统一的理论基础，难以在一个框架内无缝切换或融合。

为了解决这一问题，研究人员提出了 NeSyCat 框架。该框架是对 ULLER（Universal Logic for Learning and Reasoning）的扩展，旨在通过一个基于强单子（strong monad）和真值聚合结构的单一归纳定义，统摄上述所有逻辑系统。尽管 NeSyCat 在理论层面实现了统一，但其早期版本存在一个关键缺失：缺乏对由神经网络学习的谓词（predicates）和函数（functions）的明确描述。这使得该理论框架难以直接应用于实际的可微训练场景。

核心内容

本文介绍了 NeSyCat Torch，作为填补上述理论空白的关键链接。该工作将计算符号通过神经网络进行解释，并在概率编程和基于张量（tensor）的后端中实现了这一框架。

1. 统一语义与张量实现

NeSyCat Torch 的核心贡献在于将范畴语义转化为可微的张量操作。它不再局限于单一的逻辑范式，而是通过参数化的单子结构来适应不同的语义需求：

• 参考语义与度量评估：使用分布单子（distribution monad）来处理参考语义，并支持基于分布的度量评估。
• 数值稳定与可微训练：为了支持高效的反向传播和训练，框架引入了一个基于对数半环（log-semiring）上的惰性对数张单子（lazy log-tensor monad）。这个单子确保了数值稳定性，并允许梯度通过逻辑运算流动。
• 批量处理优化：为了支持高效的批量训练，框架进一步采用了批量单子（batch monad）。

2. “公即代码”的设计理念

该框架遵循“公理即源代码”（The axioms are the source code）的设计哲学。逻辑公理以基于单子的 do 表示法（do-notation）编写。在这种范式下，单子绑定（monadic bind）操作自动执行边缘化（marginalization）过程，并通过惰性求值机制剪枝不需要的计算分支，从而在保持理论严谨性的同时提升计算效率。

3. 实验验证与性能对比

作者在 MNIST 加法任务上进行了实证研究，对比了 HaskTorch、JAX 和 PyTorch 三种实现版本。结果显示：

• 速度与精度：NeSyCat Torch 的实现版本在速度和准确性上均优于 LTN（Logical Tensor Networks）和 DeepProbLog。
• 接近 SOTA：其精度几乎达到了 DeepStochLog 的水平。
• 框架优势：与 DeepStochLog 不同，NeSyCat Torch 保持在一个统一的框架内，该框架适用于多种一阶神经符号方法。

4. 可扩展性与未来方向

由于构造是参数化于单子的，该框架具有极高的扩展性。例如，若实例化为 Giry 单子，该方法可轻松扩展至连续概率领域（尽管神经网络在此类连续概率中的具体表示留待未来工作研究）。这种参数化设计使得 NeSyCat Torch 能够作为一个通用的底层引擎，支撑多种不同的神经符号推理策略。

关键要点

• 解决碎片化问题：NeSyCat Torch 通过引入强单子和真值聚合结构，统一了经典、模糊、概率和神经系统的真值定义，解决了神经符号语义碎片化的问题。
• 填补理论空白：作为 NeSyCat 框架的缺失环节，NeSyCat Torch 首次提供了对由神经网络学习的谓词和函数的完整描述，实现了从理论到可微实现的闭环。
• 双重单子机制：
  • 使用分布单子处理参考语义和评估。
  • 使用惰性对数张单子（基于对数半环）确保数值稳定性并支持可微训练。
  • 引入批量单子以优化批量训练效率。
• 代码即公理：逻辑规则通过基于单子的 do 表示法编写，单子绑定自动处理边缘化和剪枝，实现了理论公理与执行代码的高度统一。
• 性能优越且通用：在 MNIST 加法任务中，其速度和精度优于 LTN 和 DeepProbLog，精度接近 DeepStochLog，且保持了适用于多种一阶神经符号方法的统一框架特性。
• 高度可扩展：框架的单子参数化设计允许轻松切换至连续概率领域（如使用 Giry 单子），展示了其在更广泛概率推理场景中的潜力。

意义与影响

NeSyCat Torch 的提出标志着神经符号学习从“拼凑式”方法向“统一理论驱动”方法的重要转变。

首先，它证明了范畴论中的单子理论可以作为一种强大的工程工具，用于构建统一、可微且高效的神经符号推理引擎。通过将复杂的逻辑推理转化为张量操作，它消除了不同逻辑范式之间的壁垒，使得研究人员可以在同一个框架内灵活组合不同的推理策略。

其次，该工作强调了数值稳定性与理论严谨性在深度学习中的重要性。通过引入惰性对数张单子，它不仅解决了概率计算中的下溢问题，还保留了逻辑剪枝的效率，为构建大规模、复杂的神经符号系统提供了可行的技术路径。

最后，其参数化设计为未来的扩展奠定了坚实基础。随着连续概率推理、高阶逻辑等更复杂场景的需求增长，NeSyCat Torch 提供的统一接口使得新方法的集成变得简单而自然。这不仅加速了神经符号 AI 的落地应用，也为探索更通用的智能系统架构提供了新的理论视角和技术范式。