💬 NLP

Modeling Next-Token Prediction as Left-Nested Intuitionistic Implication

本文介绍了 Arrow 语言模型，这是一种将下一标记预测重新诠释为通过左嵌套直觉主义蕴含进行构造性证明延展的神经架构，从而推导出一种乘法循环神经网络（RNN）结构，其中序列处理对应于肯定前件推理（modus ponens），且顺序通过非交换组合得以保持。

原作者： Paul Tarau

发布于 2026-01-29

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Paul Tarau

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

核心思想：从“猜测”到“构建”

大多数现代 AI 模型（比如你正在聊天的那些）的工作方式有点像一个超级聪明的“猜谜者”。它们观察你输入的词，计算这些词与它们以前见过的词之间的相似度，并基于统计模式来预测下一个词。它们把词看作是汤里的食材，将它们混合在一起以获得某种味道。

作者 Paul Tarau 提出了另一种思考方式。他建议我们不要再把词看作是待混合的食材，而是要把它们看作是改变机器状态的工具或算子。

与其问：“通常哪个词会跟在这个词后面？”模型实际上是在问：“如果我将这个词作为一个规则应用到当前情况中，我会创造出什么样的全新情况？”

核心类比：多米诺骨牌链 vs. 搅拌碗

旧方式（Transformer）： 想象一个搅拌碗。你扔进“The”（定冠词）、“cat”（猫）和“sat”（坐）。AI 将它们全部搅拌在一起，同时观察“cat”如何与“sat”关联，以及“The”如何与“cat”关联。它使用一种特殊的“位置编码”（就像在每个词上贴一个小标签，写着“我是第1个”、“我是第2个”）来记住顺序。

新方式（Arrow 模型）： 想象一排多米诺骨牌，但这些骨牌不仅仅是在倒下，它们还在相互转化。

你从一个空白状态开始（初始状态）。
你放置单词“The”。它充当了一台机器，将空白状态转变为特定的“The-状态”。
你放置“cat”。这不仅仅是把它加入堆中；它是一台机器，它接收“The-状态”并将之转化为“The-cat-状态”。
你放置“sits”。这台机器接收“The-cat-状态”，并将其转化为“The-cat-sits-状态”。

在这种视角下，顺序至关重要，因为你不能把“sits”机器放在“The”机器之前。这些机器是“左嵌套”的，这意味着每个新词都会包裹住之前的链条。如果你交换顺序，机器就无法契合，链条就会断裂。这自然地保留了句子的顺序，而无需任何特殊的“标签”。

逻辑学：一场“如果……那么……”的游戏

论文使用了数学的一个分支——直觉主义逻辑（Intuitionistic Logic）。你可以把它看作是一种逻辑演绎的游戏。

设定： 你有一系列假设（你目前看到的词）。
目标： 你想要证明下一个词是成立的。
机制： 模型使用了一个叫做“肯定前件”（Modus Ponens）的规则。用通俗的话说，这个规则是：“如果你有一个规则说‘如果 A，那么 B’，并且你也拥有 ‘A’，那么你可以得出结论 ‘B’。”

在 Arrow 模型中：

AI 当前的状态就是“A”（假设）。
下一个词就是“B”（结论）。
单词本身充当了桥梁（蕴含关系），将当前状态转化为下一个状态。

因此，预测下一个词本质上等同于完成一个证明。AI 正在一步步构建一个逻辑论证。

“Arrow”架构

作者构建了一个名为 Arrow 语言模型 的神经网络来测试这个想法。

工作原理： 这个模型不是通过相加数字（像标准 AI 那样）来工作的，而是通过乘法和变换数字。每一个词都是一个独特的“算子”，扭转并改变当前的数据。
为什么很酷： 因为乘法不具备交换律（即 $A \times B$ 不等于 $B \times A$ ），所以词的顺序被内置到了数学运算之中。你不需要告诉计算机“这个词先出现”；数学本身就强制要求它必须知道。
结果： 该模型通过扮演“证明引擎”的角色，成功学会了预测下一个词。它证明了你可以构建一个以“证明”而非仅仅是“模式”进行思考的语言模型。

实验：记忆 vs. 理解

为了测试这是否真的有效，作者做了以下几件事：

“过拟合”测试： 他们给模型极少量的文本，并要求它完美地记住它。标准的 AI 模型如果过于复杂，有时会在这种情况下遇到困难，但 Arrow 模型轻松完成了。这证明了该架构具备学习模式的能力。
“检索”测试： 他们创建了一个句子数据库。当他们给出一个部分句子（例如“The cat...”）时，模型可以查看其内部的“证明状态”，并找到它所记忆的以这些词开头的确切句子。
对比测试： 他们将此与标准的 Prolog（一种逻辑编程语言）系统进行了比较。该 AI 神经网络的行为与逻辑系统非常相似，这表明其数学运算确实如逻辑所言在起作用。

这意味着什么（根据论文观点）

论文声称：

我们可以将语言生成视为构建一个证明，而不仅仅是猜测下一个词。
我们可以通过数学运算（非交换组合）而非人工的位置标签，来自然地处理语言中的词序。
这种方法为模型为何有效提供了一个清晰的逻辑解释，架起了符号逻辑（如数学证明）与神经网络（如深度学习）之间的桥梁。

作者提供了开源代码，以便他人可以尝试构建这些“基于证明”的语言模型。论文并未止步于声称这会立即取代所有 AI 或解决复杂的现实问题，但它成功证明了：基于逻辑的语言建模方法不仅可行，而且行之有效。

技术摘要：将下文预测建模为左嵌套直觉主义蕴涵

问题陈述

基础生成式人工智能模型（尤其是 Transformer）依赖于在海量数据集上进行的无监督下文标记（next-token）预测。尽管这种方法非常有效，但标准的 Transformer 架构掩盖了序列预测的逻辑结构。它将标记视为通过注意力机制进行混合的加性嵌入，这需要显式的相对位置编码来捕捉顺序。这种方法在解释符号推理或构造性证明推导方面提供的联系有限。本文提出了一个基本问题：能否将下文标记预测理解为直觉主义命题逻辑中证明的扩展？这种解释是否能产生一种无需依赖加性嵌入或显式位置编码的可行的、具有顺序敏感性的神经架构？

方法论

作者提出了 Arrow 语言模型，这是一种源自直觉主义逻辑解释下文标记预测的神经架构。该方法论通过符号逻辑推导、定理证明和神经实现展开。

1. 逻辑形式化：左嵌套蕴涵

核心洞察在于，不将序列 $w_1, \dots, w_n$ 表示为一个集合或右嵌套链（在合取运算下具有置换不变性），而是表示为一个左嵌套蕴含链：
$L_n = ((((w_1 \to w_2) \to w_3) \to \dots) \to w_n)$
在直觉主义逻辑中，这种结构是顺序敏感的；置换标记会改变前件的函数类型。

下文标记预测即肯定前件（Modus Ponens）： 给定前缀 $P$ 预测下一个标记 $w$ ，对应于逻辑推理 $P \to w$ 。如果前缀被表示为蕴含链 $I_p$ ，而完整序列为 $I_f = (I_p \to w)$ ，那么推导 $w$ 就是一个肯定前件的实例。
Curry–Howard 同构： 在此同构下，命题即类型，证明即 $\lambda$ -项。前缀是一个部分应用的 $\lambda$ -项，而预测下一个标记则是提供一个参数以实现进一步的函数应用（蕴含消去）。

2. 定理证明与符号检索

作者利用专门的基于 Prolog 的定理证明器（实现了 Roy Dyckhoff 的 LJT 演算）来验证这些蕴含链的属性。

定理： 他们证明了左嵌套链支持单步和多步预测。例如，定理展示了如何将前缀“编译”为可重用的延续算子（例如，将 $((E \to a) \to b) \to c$ 转换为生成 $b$ 然后生成 $c$ 的规则）。
信息检索： 实现了一种符号检索机制，将句子存储为蕴含链。查询（子序列）作为子公式用于从数据库中检索精确的补全。

3. 神经实现：Arrow 模型

论文推导了一种镜像逻辑结构的循环神经网络架构：

隐藏状态作为证明上下文： 隐藏状态 $h_t \in \mathbb{R}^d$ 代表消耗前缀后的累积证明上下文。
标记作为算子： 标记不再是加性嵌入，而是作为变换当前状态的线性算子 $M_t$ 。
低秩参数化： 为了处理大规模词表，算子被定义为低秩更新：
$M_t = I + U \text{diag}(s_t) V^\top$
其中 $U, V$ 是共享矩阵， $s_t$ 是从嵌入查找中导出的标记特定门控向量。
状态更新（肯定前件）： 循环实现了蕴含消去：
$h_{t+1} = \text{LayerNorm}(h_t + U((V^\top h_t) \odot s_t))$
这种更新本质上是非交换的（ $M_a M_b \neq M_b M_a$ ），从而在无需位置编码的情况下内在地编码了顺序。
训练： 模型使用标准的下文标记交叉熵配合教师强制（teacher forcing）进行训练。损失以流式方式计算，以在普通 GPU 上管理内存。

核心贡献

基于逻辑的推导： 论文建立了左嵌套直觉主义蕴含的深度与循环计算步骤之间的正式对应关系，为序列建模提供了证明论基础。
Arrow 架构： 它引入了一种特定的神经架构，其中标记是状态变换算子而非加性向量，将归纳偏置从“通过注意力进行检索”转向“通过组合进行变换”。
符号-神经桥梁： 该工作展示了符号定理证明（通过合一实现精确检索）与神经预测（通过学习到的延续分数实现近似检索）之间的紧密联系。
顺序的理论分析： 论文证明了左嵌套蕴含自然地保留了顺序，而右嵌套蕴含（在没有位置编码的标准注意力公式中常见）则不然。

实验结果

实验侧重于验证该架构学习顺序敏感模式的能力以及模仿符号检索的能力，而非在通用基准测试上与最先进的语言模型竞争。

过拟合/健全性检查： 模型在小型数据集（Project Gutenberg 文本）上进行了测试，并采用了刻意的过拟合机制。训练集通过包含所有连续的句子片段进行了增强，以模拟子公式的逻辑级检索。
性能： 模型成功过拟合了训练数据，在小型文档（如《绿野仙踪》、《白鲸》）上仅需几分钟即可在单块 RTX 3090 GPU 上达到接近零的训练损失。
检索 vs. 生成：
- 符号基准： 基于 Prolog 的检索通过查询对存储的蕴含链进行精确匹配。
- 神经模仿： 当使用前缀查询时，Arrow 模型可以根据学习到的延续分数对候选后缀补全（源自训练语料库）进行排序，有效地模仿了逻辑检索过程。
- 自由生成： 模型能够生成超出精确记忆匹配的流畅延续，这表明学习到的算子组合具有可泛化的序列结构。
可扩展性： 模型的训练吞吐量与序列长度呈线性关系，由于使用了流式损失计算，该模型可以以可控的内存占用扩展到书本长度的语料库（如《战争与和平》）。

意义与主张

论文声称提供了一种用于下文标记预测的逻辑优先基础，这与基于相似度的注意力机制或卷积/状态空间替代方案截然不同。

内在顺序： 通过将顺序编码在非交换算子组合中，Arrow 模型消除了对显式位置编码的需求，使架构更贴近证明扩展的构造性质。
可解释性： 该架构提供了到直觉主义逻辑的直接映射，其中状态更新对应于证明步骤（肯定前件），而隐藏状态对应于证明上下文。这为更具可解释性的神经模型提供了一条潜在路径。
替代范式： 这项工作将自己定位为 Transformer 类基础模型的可行替代方案，暗示乘法 RNN（Arrow 模型所呈现的形式）是从序列预测的证明论解释中自然产生的。

作者对处理噪声、真实世界提示词的泛化能力保持谦逊，指出目前的实验依赖于精确的连续子结构。他们将这项工作视为迈向“Transformer 的证明论解释”的一步，并提出了未来方向，即注意力机制可以被解释为近似的蕴含消去和软假设选择。