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

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

来源：https://arxiv.org/html/2606.19279
\\clearauthor\\Name

Daniel Romero Schellhorn\\Emaildaniel\.schellhorn@uni\-osnabrueck\.de \\NameTill Mossakowski\\Emailtill\.mossakowski@uni\-osnabrueck\.de \\NameBjörn Gehrke\\Emailbjoern\.gehrke@uni\-osnabrueck\.de \\addrUniversity of Osnabrück, Osnabrück, Germany

###### 摘要

神经符号语义是碎片化的：经典、模糊、概率和神经系统各自通过其归纳规则定义真值。NeSyCat 扩展了 ULLER，将它们统一在一个单一的归纳真值定义下，该定义以强单子和真值上的聚合结构为参数。此前，NeSyCat 缺乏对由神经网络学习的谓词和函数的描述。我们提供了 NeSyCat Torch\xspace 作为缺失的环节，通过神经网络解释计算符号，并在概率编程和张量后端上实现该框架。我们使用分布单子进行参考语义和度量评估，并补充了一个用于数值稳定、可微训练的单子：对数半环上的惰性对数张量单子。为了实现高效的批量训练，我们还采用了批量单子。*公理即源代码*：在基于单子的 do 记号\xspace 中编写一次，单子绑定执行边际化，惰性地修剪不需要的分支。在 MNIST 加法任务上，我们的 HaskTorch、JAX 和 PyTorch 实现在速度和准确率上均优于 LTN 和 DeepProbLog，同时达到了与 DeepStochLog 几乎相同的准确率。然而，与 DeepStochLog 不同，我们保持在一个统一的框架内，适用于许多一阶神经符号方法。也就是说，该构造以单子为参数；例如，用 Giry 单子实例化它，可将方法扩展到连续概率（此处神经表示的构建留作未来工作）。

## 1 引言

神经符号 AI 结合了神经网络的感知能力与符号逻辑的结构化、可验证推理能力。一个反复出现的障碍是碎片化：经典、模糊和概率神经符号系统各自拥有自己的逻辑语言和语义，因此知识库和学习目标很少能在它们之间迁移。ULLER —— 统一学习与推理语言（vankriekenULLER2024）—— 为一阶逻辑语法赋予了三种两两独立的语义——经典、模糊、概率——每种语义都带有自己的归纳真值定义。

最近的工作（schellhornNeSyCatCategorical2026）将所有三种语义重新表述为基于*单子*的单一*范畴*框架的实例，Moggi 在函数式编程中引入的用于计算效应的构造（moggiNotionsComputation1991）。关键观察是，ULLER 计算公式 `x := m (T1, ..., Tn) (F)`，解释为“运行模型 m，将其结果绑定到 x，然后评估 F”，正是单子 do 记号。固定一个强单子 M（效应）和一个带有连接词和量词的聚合真值空间 Ω，便产生一个*神经符号框架*；经典、模糊、概率、LTN 和可能性语义都作为 M 和 Ω 的选择重新出现，并由*一个*归纳真值定义进行评估。

出于效率原因，我们使用*惰性*单子。分布单子中的提升操作通过边际化计算概率；惰性单子确保仅在确实需要时才执行边际化。

除了通常的一阶逻辑函数和谓词符号，我们还考虑计算函数符号 `X → M Y` 和计算谓词符号 `X → M Ω`。在深度学习层面，我们还需要考虑双侧计算函数符号 `M X → M Y` 和双侧计算谓词符号 `M X → M Ω`。

现在我们回顾单子，并在表 LABEL:tab:monads-nesycat 中给出本文使用的单子：

## 2 用于计算效应的单子

###### 定义 2.1（单子（kohlSchwaigerMonads2021, §3.1））。

一个单子由三元组 `m` 给出，其中 `m` 是一个类型构造器，将类型 `a` 映射为带有来自 `return` 的值的计算效应类型 `m a`，将值嵌入到计算中，并且 `(>>=)` :: `m a -> (a -> m b) -> m b`。此处，`c :: m a` 是一个计算，`(>>=)` 将其值传递给函数 `f :: a -> m b`，该函数返回类型 `b` 上的计算。定义：

```haskell
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
```

Haskell 提供了 `do x <- y; f` 作为 `y >>= \x -> f` 的语法糖。

## 附录 A 范畴背景

### 单子。

范畴论中，范畴 C 上的一个单子是一个函子 `T: C -> C`，并带有自然变换 `η: id_C ⇒ T`（*单位*）和 `μ: TT ⇒ T`（*乘法*），满足 `μ ∘ ηT = id = μ ∘ Tη` 和 `μ ∘ Tμ = μ ∘ μT`。上述编程定义与作为 *Kleisli 三元组*（T, η, (·)^M）的等价表示一一对应，其中对于 `f: A -> T B`，`f^M: TA -> T B` 满足 `η_A^M = id_TA`，`f^M ∘ η_A = f`，以及 `g^M ∘ f^M = (g^M ∘ f)^M`：`(>>=)` 是 Kleisli 提升 (·)^M（翻转应用），而第 2 节的 do 记号是其语法糖。

### 状态。

我们在一个*具体*的笛卡尔范畴 C 上工作：对象是带结构的集合（例如可测空间、张量空间或普通集合），态射是保持结构的映射，有限积存在，终对象 1 是单元素集合。效应性映射始终显式写成所选强单子 M 的映射 `f: S -> M T`。由于 C 是具体的且笛卡尔的，S 上的一个*状态*（形式上是 Kleisli 点 `1 -> M S`）等同于 `M S` 的一个*元素*；我们一直使用此同一性，并记 `D ∈ M S`。

###### 命题 A.1（逐点评估）。

对于每一个 `i ∈ B̄`，评估 `ev_i: B M X -> M X`，`m ↦ m(i)`，是一个单子态射，因此与 do 记号程序的解释可交换：对于批量 `s: B̄ → S`，

```
⟦φ⟧^{B M}(s)(i) = ⟦φ⟧^{M}(s_i)  (i ∈ B̄).
```

一次批量运行便得到所有每个样本的真值；在整个样本上这些是 `N` 个数字 `L̂` 的平均值，一个小批量则给出 `L̂` 的无偏估计。