Transformers are Inherently Succinct——Transformer 天生简洁

论文《Transformers Are Inherently Succinct》（Transformer 天生简洁）的核心贡献是从“简洁性”这一全新视角，重新审视并量化了 Transformer 的表达能力。它通过严格的数学证明，揭示了 Transformer 在描述某些语言时异常紧凑，并因此带来了验证上的高复杂性。

以下是该研究的全面总结：

1. 核心研究问题

论文不再仅仅关注 Transformer“能识别哪些语言”（表达能力），而是问一个更精细的问题：Transformer 能用多紧凑的规模（参数数量）来描述这些语言？这种“紧凑程度”即简洁性。

2. 核心发现（主要结论）

论文通过构造性证明，得出三个层级的简洁性结论：

• 比 LTL 和 RNN 指数级更简洁：存在一系列语言，可以用多项式规模的 UHAT（一种 Transformer 抽象）描述，但任何等价的线性时序逻辑（LTL）公式或循环神经网络（RNN）的规模都必须是指数级的。

• 比有限自动机双指数级更简洁：对于同样的语言族，任何等价的有限自动机的规模必须是双指数级的。

• 匹配的上界：任何 UHAT 都可以转换为规模至多指数级膨胀的 LTL 公式（改进了前人双指数级的结果），以及规模至多双指数级膨胀的有限自动机。

3. 关键技术机制

• 用注意力机制实现双指数级计数：作者展示了 UHAT 可以通过巧妙的注意力得分编码，实现从 0 到 22N22N 的计数，即拥有双指数级大小的计数器。

• 基于平铺问题的归约：通过将图灵机运行编码为平铺问题，再构造出识别这些平铺的 UHAT，从而保证其最短接受词的长度是双指数级的。这是证明下界（即其他模型必须更大）的关键。

4. 理论后果（验证的复杂性）

由于 Transformer 极其简洁（能用小模型描述极长、极复杂的语言），导致对其行为的形式化验证在计算上极为困难：

• 主要结果：UHAT 的非空性问题（判断其是否识别任何语言）和等价性问题（判断两个 Transformer 是否行为相同）都是EXPSPACE-完全的。

• 意义：这意味着在最坏情况下，不存在能在低于双指数时间内解决这些验证问题的算法，为 Transformer 的可靠性验证（如安全、公平性检查）设定了极高的理论障碍。

5. 研究的创新点与对比

• 新视角：将逻辑学和自动机理论中的“简洁性”概念首次系统性地引入 Transformer 分析。

• 优于前人工作：显著改进了 Salzer 等人 (2025) 的结果。后者只证明 Transformer 比自动机单指数级更简洁，而本工作将其推进到双指数级，且模型假设更简单（仅用硬注意力，而非软硬混合）。

• 固定精度设置：所有结论均在固定精度（最符合实际硬件）下成立，增强了现实意义。

6. 研究局限与未来方向

• 模型简化：研究基于 UHAT（唯一硬注意力 Transformer），这是对实际 Softmax 注意力的一种近似。如何推广到真实 Softmax Transformer 是未来工作。

• 实践与理论的鸿沟：虽然最坏情况是 EXPSPACE-完全的，但论文提出未来可研究无法编码大计数器的子类，这些子类可能允许更高效的验证。

• 可学习性问题：虽然 Transformer 可以简洁地表示这些语言，但模型是否能通过梯度下降学习到这种表示，仍是开放的。

该论文证明，固定精度的 Transformer 能用极小的模型“压缩”极其复杂的语言（其最短描述长度远超 LTL、RNN 和有限自动机），但这种“简洁”是一把双刃剑，它直接导致了 Transformer 的验证问题在理论上是极高的复杂度（EXPSPACE-完全）。这里是自己的论文阅读记录，感兴趣的话可以参考一下，如果需要阅读原文的话可以看这里，如下所示：

摘要

我们研究简洁性（succinctness）作为衡量 Transformer 表达能力的指标。简洁性——即一种形式体系相对于其他形式体系描述语言时的紧凑程度——是逻辑学和自动机理论中的一个经典概念。我们证明，固定精度（fixed-precision）的 Transformer 具有显著的简洁性：它们可以比线性时序逻辑（LTL）和循环神经网络（RNN）指数级地更简洁，并且比有限自动机双指数级地更简洁。换句话说，存在一系列语言族，它们可以用多项式大小的 Transformer 描述，但与之等价的 LTL 公式或 RNN 的最小规模是指数级的，而与之等价的有限自动机的最小规模则是双指数级的。我们还建立了匹配的上界，证明了任何固定精度的 Transformer 都可以转换为规模最多为指数级爆炸的 LTL 公式——这改进了先前的一个双指数级翻译。作为这种简洁性的一个结果，我们证明了 Transformer 的基本验证问题，如空性（emptiness）和等价性（equivalence），在理论上是难解的：具体而言，它们是 EXPSPACE-完全的。

1 引言

Transformer (Vaswani et al., 2017) 是支撑大多数现代大型语言模型的主导架构。大量近期的理论工作研究了它们的表达能力 (Strobl et al., 2024; Barcelo et al., 2024; Yang et al., 2024; Hahn, 2020; Pérez et al., 2021; Chiang and Cholak, 2022; Jerad et al., 2025)、其可训练性和泛化到未见过的更长字符串的能力 (Zhou et al., 2024; Huang et al., 2025; Chiang and Cholak, 2022)，以及其行为可被形式验证的程度 (Salzer et al., 2025)。这一系列工作的一个关键发现是，具有有限精度——最符合现实世界硬件的设置——的 Transformer 能够识别各种亚正则（subregular）语言类别，具体取决于所采用的确切假设 (Yang et al., 2024; Barcelo et al., 2024; Jerad et al., 2025; Li and Cotterell, 2025)。

在本文中，我们提出将简洁性作为理解 Transformer 表达能力的另一种视角。一个语言 LL 相对于一个语言识别器类别 C（例如，Transformer、有限自动机和 FO[<] 公式）的简洁性衡量了识别 L 的最小 C 识别器的大小。换句话说，简洁性告诉我们，相对于类别 C，描述 L 需要多少符号。简洁性是逻辑学和计算机科学中的一个经典概念 (Stockmeyer, 1974; Grohe and Schweikardt, 2004)，它将表达能力细化为一个复杂度理论的细化：它不是仅仅询问一种形式体系能识别哪些语言，而是询问每种这样的语言在其中能被描述得有多紧凑。更高的简洁性是有代价的——更简洁的形式体系通常伴随着相应更难的决策问题，因为它们的紧凑描述迫使任何决策过程展开更大数量的底层结构。一个众所周知的例子涉及线性时序逻辑（LTL; Pnueli, 1977），它在表达能力上等价于星自由语言 (Libkin, 2004)，因此也等价于 McNaughton 和 Papert (1971) 的无计数器自动机。尽管在表达能力上等价，LTL 可以比有限自动机指数级地更简洁 (Sistla and Clarke, 1985)，即某些语言允许多项式大小的 LTL 公式，但需要指数级更大的自动机。一个直接的后果是，LTL 的决策问题，例如检查一个公式是否识别平凡语言，被证明比自动机的相应问题更难 (Sistla and Clarke, 1985)。

本文提供了一个正式结果，可以总结如下：Transformer 能够极其简洁地描述某些语言。具体来说，我们证明 Transformer 可以比 LTL 和 RNN，以及状态空间模型（SSM; Gu and Dao, 2023; Merrill et al., 2024）指数级地更简洁。此外，它们比有限自动机双指数级地更简洁。具体而言，存在一系列语言族，它们可以用多项式大小的 Transformer 描述，但需要指数级更大的 LTL 公式或 RNN，以及双指数级更大的自动机。我们还建立了匹配的上界：我们给出了一个从有限精度 Transformer 到规模为指数级的 LTL 公式的翻译，显著改进了 Yang 等人 (2024) 的双指数级翻译。由此可知，对于任何固定精度的 Transformer，都存在一个规模为指数级的等价 LTL 公式和一个规模为双指数级的等价有限自动机。这些结果背后的关键技术成分是证明 Transformer 可以通过一种使用注意力的巧妙编码从 0 计数到——即实现双指数级大的计数器。然后我们证明，由此产生的语言需要指数级更大的 LTL 公式或 RNN 描述，以及双指数级更大的有限自动机描述。这种简洁性的一个自然结果是，分析 Transformer 在计算上应该具有挑战性。确实，我们证明了检查给定的 Transformer 是否识别平凡语言是 EXPSPACE-完全的。在标准的复杂性理论假设下，这意味着没有算法能在低于双指数时间的时间内解决这个问题。

我们研究的具体 Transformer 模型是唯一硬注意力 Transformer（UHAT），这是自注意力机制的一种简单且广泛使用的抽象 (Yang et al., 2024; Jerad et al., 2025; Strobl et al., 2024; Hao et al., 2022; Li and Cotterell, 2025; Hahn, 2020; Barcelo et al., 2024; Bergstrasser et al., 2024)。特别地，Jerad 等人 (2025) 表明，对 UHAT 的表达性界限意味着对具有固定精度的 softmax Transformer 也有相应的界限。本文的不同结果在不同的精度假设下成立：UHAT 的上界是针对任意有理数权重陈述的，而相应的 RNN 结果则假设了固定（有限）精度。重要的是，这意味着我们的结论在最忠实反映现实世界实现的设置——固定精度算术——中是有效的。

2 预备知识

2.1 线性时序逻辑

2.2 唯一硬注意力 Transformer

2.3 布尔 RASP

2.4 循环神经网络

2.5 规模度量与简洁性

3 通过非空性问题得到的最短见证规模

命题 10.UHAT 的非空性问题是 EXPSPACE-难的。

证明.结合命题 7、引理 8 和引理 9 蕴含了 UHAT 的 EXPSPACE 下界。

推论 11.在每一层都使用严格未来掩码和最右平局打破（或对偶地，严格过去掩码和最左平局打破）的 UHAT 的非空性问题是 EXPSPACE-难的。

证明.引理 8 中构造的 B-RASP 程序仅使用严格未来掩码和最右平局打破，并且可以改编为仅使用严格过去掩码和最左平局打破。引理 9 中的 UHAT 翻译保留了掩码谓词和平局打破。因此，由命题 7、引理 8 和引理 9 建立的 EXPSPACE 下界可以转移到这两种受限类别中的任何一种 UHAT。

我们现在证明定理 4 中的上界。为此，我们首先注意到任何 B-RASP 程序都可以在指数时间内使用 Yang 等人 (2024) 给出的构造转换为 LTL 公式。在命题 13 中，我们证明同样的结论对 UHAT 也成立，这改进了 Yang 等人 (2024) 给出的先将 UHAT 转换为 B-RASP 程序的双指数级构造。这些构造足以证明定理 4 中的指数空间上界，因为由 LTL 公式给出的语言的非空性在多项式空间内可判定 (Sistla and Clarke, 1985)。

为了执行从 UHAT 到 LTL 的翻译，我们首先必须做出一个关键观察：在 UHAT 计算过程中出现的值不会太大。下一个命题的证明见附录 A.4。

4 不同表示之间的简洁性

我们现在研究 Transformer 与形式语言理论中的标准模型相比，能多简洁地表示语言。我们首先将 Transformer 与 LTL 进行比较。一种建议是 Transformer 比 LTL 指数级地更简洁。

定理 15.UHAT 比 LTL 指数级地更简洁。

证明.证明分为两部分：构造一个多项式大小的 UHAT 见证族，然后证明任何等价的 LTL 公式必须是指数级大的。

存在一个多项式大小的 UHAT。这个方向分 3 步进行。

5 应用

作为我们结果的一个推论，我们可以证明关于 UHAT 所接受语言的推理，例如检查等价性和空性，是难解的。将此与确定性有限自动机（这些问题可以在多项式时间内完成 (Kozen, 1997)）进行对比。作为一个例子，我们给出关于等价性问题（即检查两个 UHAT 是否识别相同语言的问题）复杂性的精确陈述。证明见附录 A.7。

定理 19.判定两个 UHAT 之间的等价性是 EXPSPACE-完全的。

6 结论与展望

相关工作。我们的工作直接借鉴了许多近期成果 (Yang et al., 2024; Barcelo et al., 2024; Jerad et al., 2025; Li and Cotterell, 2025)，这些成果展示了唯一硬注意力 Transformer 与 LTL 之间的紧密联系，因此也与星自由正则语言紧密相关。然而，这些结果都没有涉及简洁性和验证的计算复杂性。更接近我们的复杂性理论视角，Salzer 等人 (2025) 研究了不同精度下 Transformer 的验证问题，并表明固定精度 Transformer 至少是 NEXP-Hard（即对于由运行在指数时间内的非确定性算法解决的问题类是难的）。他们的技术意味着 Transformer 可以比有限自动机（单）指数级地更简洁，但无法得出它们相对于 LTL 或 RNN 等表示的简洁性结论。我们的结果通过证明 Transformer 可以比自动机双指数级地更简洁，并且比 LTL 和 RNN 指数级地更简洁，显著改进了这一点。我们的模型也更简单：我们使用唯一硬注意力，而 Salzer 等人 (2025) 结合了软注意力和硬注意力。我们的设置还将位置信息限制为位置掩码——这是 Yang 等人 (2024)、Jerad 等人 (2025) 和 Li 与 Cotterell (2025) 也考虑过的一类简单位置嵌入——与 Salzer 等人 (2025) 允许的任意固定精度位置编码形成对比。在没有位置编码的情况下，Salzer 等人 (2026) 最近表明，对于具有有限但无界精度的平均硬注意力和 softmax 注意力 Transformer，验证是不可判定的。

Transformer 的形式验证。最后，我们将我们的发现置于更广泛的形式验证计划中——即 Transformer 的自动化分析、验证和解释——这是可解释 AI 的核心关注点 (Huang et al., 2020)。在过去十年中，验证前馈神经网络取得了实质性的实践进展，开发了多种工具，并在年度 VNN 竞赛中进行基准测试 (Brix et al., 2024)；相比之下，Transformer 在很大程度上仍然遥不可及。尽管最坏情况下的复杂度很高（EXPSPACE-完全），我们提出一个挑战，即将自动验证 (Clarke et al., 2018) 的技术——符号方法、模拟等——应用于实践中的 Transformer 验证。因为我们的 EXPSPACE-硬度证明需要编码大型计数器的 Transformer，一个互补的方向是识别无法编码此类计数器从而允许较低复杂度验证的子类。一个相关的开放问题是简洁 Transformer 的可学习性，对此实证证据仍然褒贬不一 (Garg et al., 2022; Naim et al., 2025; Huang et al., 2025)。最后，我们的结果是理解 Transformer 相对于其他语言接受器模型（例如，固定精度 softmax Transformer (Li and Cotterell, 2025)，UHAT 对其进行了过近似）能有多简洁的第一步。我们将固定精度 softmax 和平均硬注意力 Transformer 的简洁性留作未来的工作；参见 Yang 等人 (2026) 的初步尝试。