一个图灵完备神经网络的 PyTorch 库

arXiv cs.LG 工具

摘要

一个 PyTorch 库,可根据图灵机描述编译神经网络,从而实现无需训练的精确模拟。

arXiv:2605.08150v1 公告类型:新文章 摘要:我们提出了一个 PyTorch 包,它可以根据图灵机描述编译神经网络及其权重,生成无需任何训练即可精确模拟指定机器的模型。给定一个转移函数和一组终止状态,该包构建的模型其前向传播对应于图灵机的一步执行。实现两种架构,每种架构分别实现不同的理论结果:(1) 基于 Wei、Chen 和 Ma (2021) 的研究,采用自注意力、交叉注意力和前馈层的 Transformer;(2) 基于 Siegelmann 和 Sontag (1995) 的研究,将堆栈编码为康托尔集的循环神经网络。我们从基本原理出发开发这些构造,展示 ReLU 网络如何实现布尔电路(与、或、非、异或门及其组合成析取范式公式和二进制加法器),以及硬注意力如何实现磁带上的位置查找。该包作为符号与神经桥梁的具体可运行参考,并为未来研究梯度优化下构造解的稳定性奠定了基础。代码可在 https://github.com/jonrbates/turing 获取。
查看原文
查看缓存全文

缓存时间: 2026/05/12 06:56

# 一个包含图灵完备神经网络的 PyTorch 库
来源: https://arxiv.org/html/2605.08150
###### 摘要

我们提供了一个 PyTorch 包,该包可以从图灵机的描述中编译神经网络及其权重,生成能够精确模拟指定机器而无需任何训练的模型。给定一个转移函数和一组终止状态,该包构建的模型的前向传播对应于图灵机的一步操作。实现了两种架构,每种架构都实现了不同的理论结果:(1)基于 Wei, Chen 和 Ma (2021) 的具有自注意力、交叉注意力和前馈层的 Transformer;(2)基于 Siegelmann 和 Sontag (1995) 的循环网络,该网络使用康托尔集编码栈。我们从基本原理出发开发了这些构造,展示了 ReLU 网络如何实现布尔电路(AND、OR、NOT、XOR 门以及它们组合成的析取范式公式和二进制加法器),以及硬注意力如何实现对磁带上的位置查找。该包作为符号-神经网络桥梁的具体、可运行的参考,并为未来研究梯度优化下构建解的稳定性的工作奠定了基础。代码可在 https://github.com/jonrbates/turing 获取。

## 1 引言

神经网络能够模拟图灵机吗?理论文献中已经多次对此给出了肯定的回答:Siegelmann 和 Sontag\[8 (https://arxiv.org/html/2605.08150#bib.bib8),9 (https://arxiv.org/html/2605.08150#bib.bib9)\]使用循环网络,Pérez 等人\[7 (https://arxiv.org/html/2605.08150#bib.bib7)\]使用具有硬注意力的 Transformer,以及 Wei, Chen 和 Ma\[11 (https://arxiv.org/html/2605.08150#bib.bib11)\]使用具有二进制位置编码的有限精度 Transformer 实现了这一点。最近,Li 和 Wang\[4 (https://arxiv.org/html/2605.08150#bib.bib4)\]表明,即使恒定比特大小的 Transformer,在拥有足够长的上下文窗口和思维链步骤的情况下,也是图灵完备的。这些结果提供了显式的构造,但它们停留在纸面上:指定权重矩阵的证明与可运行实现之间的差距依然存在。

在本文中,我们描述了一个 PyTorch 包,它填补了这一差距。给定由其转移函数和终止状态指定的图灵机,该包构建一个神经网络并*指定*所有权重和偏置,使得网络的前向传播精确实现机器的一个步骤。不需要训练:网络通过构造本身就是正确的。(对于 WCM21 Transformer,权重通过从转移表直接构造来设定;对于 SS95 循环网络,最小二乘解从配置空间中确定权重。)

从机器描述到神经网络的编译过程通过一系列组件层次进行:

1. 逻辑门。ReLU 网络在状态向量的二值子集上计算 AND、OR、NOT 和 XOR。
2. 转移函数。有限查找表 $\delta$ 被实现为一个两层析取范式(DNF)电路:每个状态-符号对对应一个隐藏神经元。
3. 二进制算术。由上述门组成的半加器和全加器形成进位加法器,用于更新头部位置。
4. 位置查找。具有二进制键-查询匹配的硬注意力层从磁带历史和原始输入中检索符号。
5. 符号组装。前馈层通过优先级选择新头部位置处的正确符号:最后写入、原始磁带或空。

结果网络中的每个权重都有已知且可解释的用途。这种可解释性是*构造过程*的一个属性,而不是事后分析的属性,这一点我们在讨论部分会再次提到。

提供了两种模拟架构:

- WCM21(Wei, Chen & Ma, 2021):一个编码器-解码器 Transformer,其中编码器存储初始磁带,解码器自回归地跟踪计算历史。自注意力检索过去的写入;交叉注意力读取原始磁带;前馈层实现转移函数和二进制算术。
- SS95(Siegelmann & Sontag, 1992; 1995):一个循环网络,将图灵机重构为栈机,并使用康托尔集编码将每个栈编码为单个有理数。实现了两个版本:一个具有显式流水线阶段的 4 层网络,和一个 1 层“实时”变体。

#### 贡献。

1. 关于 ReLU 网络如何实现布尔电路的自包含阐述,从单个门构建到 DNF,再到二进制加法器。
2. 作为 PyTorch 包的两个图灵机模拟结果的构造实现,权重由机器描述指定。
3. 一个开源代码库,适合研究在扰动和基于梯度的微调下构造解的稳定性。

#### 相关工作。

Pérez 等人\[7 (https://arxiv.org/html/2605.08150#bib.bib7)\]给出了一个具有硬注意力的 Transformer 的显式构造,该 Transformer 可以模拟任何图灵机,使用单层编码器和三层解码器。他们的构造在任意精度的有理数上运行;当多个位置在最大注意力得分上平局时,hardmax 会产生像 $1/t$ 这样的分数,需要精度随序列长度增长。

Wei, Chen 和 Ma\[11 (https://arxiv.org/html/2605.08150#bib.bib11)\]通过使用*二进制位置编码*避免了这个问题。头部位置和步骤号表示为固定宽度的二进制向量,并且通过永远不会产生分数平局的注意力得分来匹配二进制位以执行位置查找。这是使构造在有限精度下可实施的关键修改。参数数量是字母表大小 $\|\Gamma\|$、状态空间大小 $\|Q\|$ 和 $\log T$ 的多项式,而不是随输入长度增长。WCM21 实现直接遵循 Wei-Chen-Ma 的构造,将 Claim C.4–C.6 和 Lemma C.1, C.2, C.7, C.8 翻译为 PyTorch 模块;二进制编码通过进位加法器和二进制搜索层实现。

下一系列工作引入了*思维链(CoT)*作为 Transformer 的计算资源。Li 等人\[3 (https://arxiv.org/html/2605.08150#bib.bib3)\]证明,增强有 $O(\log t)$ 思维链步骤的恒定深度、恒定精度 Transformer 可以解决需要串行计算的问题,Merrill 和 Sabharwal\[5 (https://arxiv.org/html/2605.08150#bib.bib5)\]刻画了这种 CoT 增强 Transformer 的表达力,表明多项式 CoT 步骤产生了多项式时间图灵机的能力。这些结果形式化了中间生成步骤可以用作工作磁带的直觉。

Li 和 Wang\[4 (https://arxiv.org/html/2605.08150#bib.bib4)\]更进一步,证明即使恒定比特大小的 Transformer(固定精度和固定参数计数)在给定足够的上下文窗口长度时也是图灵完备的,方法是使用带有思维链步骤的 Post 机模拟。

表 1:神经网络图灵完备性构造的资源需求。$t$ 和 $s$ 分别表示模拟机器在长度为 $n$ 的输入上的最坏情况运行时间和空间。Transformer 行改编自 Li 和 Wang\[4 (https://arxiv.org/html/2605.08150#bib.bib4)\],表 1。Smolensky 等人\[10 (https://arxiv.org/html/2605.08150#bib.bib10)\]开发了 PSL(产生式系统语言),这是一种用于符号程序的高级语言,编译成使用张量积表示的 Transformer 权重。PSL 在结构化工作记忆上的产生式规则级别运行;这里的构造揭示了实现计算的底层电路原语(门、加法器、硬注意力)。

神经图灵机\[2 (https://arxiv.org/html/2605.08150#bib.bib2)\]和相关的可微内存架构受到启发并带有归纳偏差以模仿计算机架构。这里的方法则是将任何给定的程序编译为固定权重。

## 2 预备知识

### 2.1 图灵机

###### 定义 1(图灵机)。

图灵机是一个元组 $M=(Q, \Gamma, \delta, q_0, F)$,其中 $Q$ 是状态的有限集合,$\Gamma$ 是磁带字母表的有限集合,$\delta: Q \times \Gamma \to Q \times \Gamma \times \{-1, +1\}$ 是(偏)转移函数,$q_0 \in Q$ 是初始状态,$F \subseteq Q$ 是终止(停机)状态集合。给定状态 $q$ 和头部下的符号 $a$,$\delta(q, a) = (q', a', d)$ 指定下一个状态 $q'$,要写入的符号 $a'$,以及移动头部的方向 $d$。

时间 $t$ 时的*配置*是三元组 $(q_t, h_t, \tau_t)$:当前状态 $q_t \in Q$,头部位置 $h_t \in \{0, \dots, n-1\}$,以及磁带内容 $\tau_t \in \Gamma^n$。当 $q_t \in F$ 时机器停机。

###### 示例 1(平衡括号)。

考虑平衡括号字符串的语言。我们定义一个具有状态 $Q=\{I, R, M, V, T, F\}$、字母表 $\Gamma=\{B, E, (, ), *\}$、初始状态 $q_0=I$ 和终止状态 $\{T, F\}$(“真”和“假”)的图灵机。磁带初始化为带有哨兵 $B$ 和 $E$ 框住输入,例如,$B()(())()E$。转移函数如表 2 (https://arxiv.org/html/2605.08150#S2.T2) 所示。

机器在状态 $R$ 中向右扫描,直到找到一个右括号;切换到状态 $M$ 并向左扫描以找到匹配的左括号(将两者替换为 $*$);然后恢复向右扫描。状态 $V$ 验证没有剩余的不匹配符号。

表 2:平衡括号机器的转移函数 $\delta$。
| 状态 | 读取 | 下一状态 | 写入 | 移动 |
| :--- | :--- | :--- | :--- | :--- |
| I | B | R | B | +1 |
| R | ( | R | ( | +1 |
| R | ) | M | * | -1 |
| R | * | R | * | +1 |
| R | E | V | E | -1 |
| M | B | F | * | -1 |
| M | ( | R | * | +1 |
| M | * | M | * | -1 |
| V | ( | F | * | -1 |
| V | * | V | * | -1 |
| V | B | T | B | +1 |

图 1:在输入 $B()E$ 上的执行跟踪。头部在状态 $R$ 中向右扫描,在状态 $M$ 中匹配括号,并在状态 $V$ 中验证。匹配的对被替换为 $*$。头部符号高亮显示。

### 2.2 符号和激活

我们将修正线性单元写为 $\mathrm{ReLU}(x) = \max(x, 0)$。当输入限制为 $\{0, 1\}$ 时,本文中的构造设计使得所有中间值在 $\mathrm{ReLU}$ 下保持为 $\{0, 1\}$。*饱和线性*激活 $\sigma(x) = \operatorname{clamp}(x, 0, 1)$,它明确地将输出限制在 $[0, 1]$,用于 SS95 构造(§6 (https://arxiv.org/html/2605.08150#S6)),其中康托尔集编码值需要有界激活。

## 3 ReLU 网络中的布尔电路

构成这些构造基础的一个基本观察是,具有分段线性激活的网络可以精确实现布尔逻辑。我们将系统地展开这一点。

### 3.1 基本门

###### 命题 2(NOT)。

对于 $x \in \{0, 1\}$:$\neg x = \mathrm{ReLU}(1 - x)$。

###### 命题 3(AND)。

对于 $x_1, x_2 \in \{0, 1\}$:$x_1 \land x_2 = \mathrm{ReLU}(x_1 + x_2 - 1)$。这可以推广:$\bigwedge_{i=1}^k x_i = \mathrm{ReLU}(\sum_{i=1}^k x_i - (k - 1))$。

###### 命题 4(NOR 和 OR)。

$\mathrm{NOR}(x_1, x_2) = \mathrm{ReLU}(1 - x_1 - x_2)$ 且

$\mathrm{OR}(x_1, x_2) = \mathrm{NOT}(\mathrm{NOR}(x_1, x_2)) = \mathrm{ReLU}(1 - \mathrm{ReLU}(1 - x_1 - x_2))$。

###### 命题 5(XOR)。

$x_1 \oplus x_2$ 不是线性可分的,不能由单个神经元计算。实现使用:

$x_1 \oplus x_2 = \mathrm{AND}(\mathrm{NAND}(x_1, x_2), \mathrm{OR}(x_1, x_2))$。 (1)

### 3.2 在权重矩阵中嵌入门

一个关键的实现技术是,操作在维度*子集*上的门可以嵌入到一个大的权重矩阵中,该矩阵在所有其他维度上充当恒等映射。从 $W=I$ 开始,我们修改对应于门输入和输出的行和列。这允许多个门并行应用,并通过序列矩阵-ReLU $\mathrm{ReLU}$ 层组合电路。

例如,为了计算 $\mathrm{AND}(x_i, x_j)$ 并将结果存储在位置 $i$,同时保持所有其他维度不变地传递:

$W=I, \quad W_{ij}=1, \quad b_i=-1$, (2)

使得

$[\mathrm{ReLU}(Wx + b)]_i = \mathrm{ReLU}(x_i + x_j - 1)$

且

$[\mathrm{ReLU}(Wx + b)]_k = x_k$

对于 $k \neq i$。

### 3.3 DNF 实现和转移函数

任何布尔函数 $f: \{0, 1\}^n \to \{0, 1\}$ 都可以写成析取范式(DNF):$f(x) = \bigvee_j C_j(x)$,其中每个子句 $C_j$ 是文字的合取。

###### 定理 6(DNF 实现)。

任何具有 $m$ 个子句的 $n$ 个变量的 DNF 可以通过三层 ReLU 网络计算:第 1 层通过 AND 计算每个子句($m$ 个隐藏神经元),第 2 层计算子句输出的 NOR,第 3 层取反以产生 OR。当子句互斥(最多只有一个激活)时,第 2 层可以通过求和直接计算 OR,将网络减少到两层。

图灵机转移函数 $\delta$ 是一个有限查找表,将 $(q, a)$ 对映射到 $(q', a', d)$ 三元组。使用 one-hot 编码,每个表条目是一个子句:“状态是 $q$” AND “符号是 $a$”。第一层附加 $|Q| \cdot |\Gamma|$ 个检测维度(每个状态-符号对一个),每个是一个偏置为 $-1$ 的 2 输入 AND。在 $\mathrm{ReLU}$ 之后,恰好有一个检测器触发。第二层路由输出:对于每个条目 $\delta(q, a) = (q', a', d)$,它在下一状态 $q'$、写入符号 $a'$ 和方向 $d$ 的输出列中设置 1。位置编码位(pos1, pos2)通过恒等块不变地传递。

在包中,这是 Transition 模块:$W_1 \in \mathbb{R}^{(w+sg) \times w}$ 和 $W_2 \in \mathbb{R}^{w \times (w+sg)}$。

## 4 二进制算术

为了更新头部位置,我们必须向二进制编码的整数加 1 或减 1。这需要由 §3 (https://arxiv.org/html/2605.08150#S3) 中的门构建的二进制加法电路。

### 4.1 半加器

半加器接收两个位 $a, b \in \{0, 1\}$ 并产生和 $s = a \oplus b$ 和进位 $c = a \land b$。实现使用三层,每层嵌入在加法维度的恒等矩阵中,在位置 $i$(被和覆盖)和 $j$(被进位覆盖)上操作:

1. 在位置 $i$ 计算 $\mathrm{AND}(x_i, x_j)$ 同时在位置 $j$ 计算 $\mathrm{NOR}(x_i, x_j)$。
2. 对两者取反:在位置 $i$ $\mathrm{NAND} = \mathrm{NOT}(\mathrm{AND}(x_i, x_j))$,在位置 $j$ $\mathrm{OR} = \mathrm{NOT}(\mathrm{NOR}(x_i, x_j))$。
3. 组合:$s = x_i \oplus x_j = \mathrm{AND}(\mathrm{NAND}, \mathrm

相似文章

迷你可修改的CUDA语言模型实现

Hacker News Top

一个最小化的、可修改的CUDA实现,类似于GPT的变压器语言模型,处理字节序列,附带示例输出和构建说明。

@NFTCPS: 天天喊着搞AI,结果你连Transformer是个啥都说不清? 有个仓库够狠,从零手搓一个GPT,不调任何高级库。Attention、多头、前馈、Embedding、残差、Layer Norm,怎么拼起来的全摊给你看。而且不止模型,整条链…

X AI KOLs Timeline

一个GitHub开源项目,从零实现完整的GPT训练流程,包含数据预处理、预训练、SFT和RLHF后训练,全部基于原生PyTorch,适合想深入理解Transformer原理的开发者。

@AnimaAnandkumar: TorchLean 代码库现已开放!TorchLean 是一个用于可验证神经网络软件的 Lean 4 框架。它支持……

X AI KOLs Following

TorchLean 是一款全新发布的 Lean 4 框架,可实现神经网络软件的形式化验证,具备类型化张量、可验证自动微分、PyTorch 互操作性及 GPU 执行等特性。此次发布进一步扩展了对扩散模型、GPT 风格 Transformer 和状态空间模型等现代架构的支持,将实际的机器学习工作流与数学证明检查紧密连接。