论文《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 模型是唯一硬注意力 TransformerUHAT这是自注意力机制的一种简单且广泛使用的抽象 (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 唯一硬注意力 Transformer2.3 布尔 RASP2.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) 的初步尝试。