Transformers are Inherently Succinct

⚠️ 本期方法论声明（坦诚性前置）

本追踪标准要求「五基准 × 六方法的性能矩阵、消融研究、超参敏感性曲线」。本期核心论文是一篇纯理论论文，不含任何实验、基准或超参数。强行套用实验模板只会产出虚假数据，因此本期做了如下等价替换，并在各章节明确标注：

核心论文

版本：v1 = 2025-10-22，v2 = 2025-10-23，v3 = 2026-05-15（本报告基于 v2）。学科分类中 cs.FL 为主分类——这是一篇真正的理论计算机科学论文。

相关工作

2.1 一句话定位

这句话的关键不在「Transformer 很强」，而在连接词：正因为它把同一个概念压缩得如此之小，任何试图把它展开来检查的工具（自动机、逻辑公式）都会爆炸，于是验证它必然是 EXPSPACE-完全的。简洁性与可验证性是同一枚硬币的两面——这是全文最深的一层论证。

2.2 Motivation 与问题论证

2.2.1 领域的「坏消息」叙事

过去六年，Transformer 形式化表达力研究基本是一条负面结论累积的路径：

这条链读下来的自然结论是：Transformer（在这个理想化模型下）表达力弱于 RNN——因为有限精度 RNN 可识别全部正则语言，而 star-free 是正则语言的真子集（经典反例：(aa)*，即「a 的个数为偶数」，正则但非 star-free）。

2.2.2 论文指出的具体错位

作者指出该叙事与经验事实存在明显张力：实践中没有人认为 Transformer 比同规模 RNN 弱。他们诊断出问题根源不在结论错，而在度量维度选错了：

一个具体类比：假设某概念在 Transformer 里需要 O(n) 个参数描述，在 DFA 里需要 2^(2^n) 个状态。表达力度量会说「两者都能识别，无差别」；任何工程直觉都会说「这是天壤之别」。

这就是新颖之处：问题不是「能不能」，而是在等表达力的前提下，规模差距有多大。这个问题此前从未被提出过——即使 Yang et al. (2024) 给出了精确的三方等价，也完全没有分析等价转换的规模代价。我在阅读 NeurIPS 2024 正文时确认：该论文唯一涉及规模的陈述出现在 Appendix B.2——「每个 attention operation 至多翻译成 2^(T_A+T_B) 个操作」——且没有给出跨多步翻译的总体规模关系。一个指数爆炸在等价性证明的脚注里躺了两年，无人追问。

2.2.3 为什么这个问题值得解决

1. 理论层：简洁性（succinctness）在逻辑学中是成熟工具（Stockmeyer 1974；Grohe & Schweikardt 2004），但从未被引入神经网络表达力研究。这是一次方法论移植。
2. 可验证性层：若想形式化验证 Transformer（AI safety 的圣杯之一），规模差距直接决定验证算法的复杂度下界。简洁性是坏消息的来源。
3. 架构选择层：为「为什么 Transformer 好用」提供了一个与优化 / 并行性无关的纯表示论解释：同样的知识，它需要的参数更少。

2.3 论文的故事线（论证结构）

全文逻辑是一个「正—反」结构，同一个技术构造被两次使用：

关键转折点

转折点 A（正面结论的引擎）：作者观察到 UHAT 的严格掩码 + 最右 tie-breaking 组合恰好提供了「找到最近的、满足某谓词的前驱位置」这一原语，用它同时完成计数器的递增与约束校验。由此推断：Transformer 可以用多项式大小编码双指数大的计数器——而任何有限自动机要显式表示这个计数器，就必须有双指数多个状态。

转折点 B（同一构造的反面用法）：这个计数器构造同时是 EXPSPACE-hardness 归约的载体。2^n-tiling 问题（在 2^n × 2^n 网格上铺砖）是 EXPSPACE-完全的；能编码双指数计数器就意味着能编码该网格，于是 B-RASP 的非空性至少是 EXPSPACE-hard（Prop. 6）。

转折点 C（上界的技术核心）：要把 hardness 补成 completeness 需要 EXPSPACE 上界。朴素想法「翻译成 LTL 再用已知算法」会因 Yang et al. 的双指数翻译而只得到 2-EXPSPACE。作者靠 Prop. 11（UHAT 计算中出现的所有数值只需多项式位数表示）把翻译降到单指数（Prop. 12），从而闭合上下界。

隐含的设计权衡

论文选择 UHAT + 固定精度，作者自述这是「表达力上最弱的一类 Transformer」。这是故意的自我设限：牺牲了对 softmax / average-hard attention 的直接覆盖，换取了 (a) 结论的下界性质——最弱的模型都这么简洁，更强的只会更简洁；(b) 固定精度「忠实于真实实现」；(c) 可以嫁接 Yang et al. 已有的精确刻画。

2.4 方法论与机制解剖

2.4.1 形式化定义

UHAT（掩码唯一硬注意力 Transformer）。一个 masked unique hard-attention 层由五元组构成：

固定精度（fixed precision）的精确含义：论文定义为「计算始终在可用常数 k 位表示的实数上进行」。这是与 log-precision / 无限精度路线的关键分野。

B-RASP 在输入词上定义一族布尔向量，通过两类操作：位置级操作（对已有向量在同一位置取布尔组合）与注意力操作（由掩码谓词 + 得分谓词选出位置，输出值谓词或默认值）。当指定输出向量在指定位置取 1 时接受该词。它在本文中扮演 Transformer 与 LTL 之间的中间语言（角色继承自 Yang et al. 2024）。

简洁性差距（succinctness gap）—— 本文的核心定义：

两个易被忽略的技术细节：

• 量词顺序：「对每个 f，存在 R₁」而非反之。差距是渐近族意义上的，不是单个反例。
• 规模度量的公平性：规模用标准二进制编码；但对 RNN，精度 k 以一进制（unary）计入规模。这是防止对手用「精度 = 2ⁿ，但写作 n 位二进制」偷藏一个指数。这一处细节决定了 Cor. 17 是否成立（见 §2.7 批判 4）。

2.4.2 关键机制表格

2.4.3 核心构造：双指数计数器（Example 4 的机制还原）

这是全文的技术心脏。目标：让一个多项式规模的 UHAT 判定「这个串编码了一个合法的 2ⁿ × 2ⁿ 铺砖」。

3.1 主结果矩阵：简洁性差距

行 = 源系统（Transformer 侧），列 = 被比较的目标系统。

3.2 复杂度矩阵：验证问题

这个相变点值得单独强调，因为它把两条独立研究线接上了：Jerad et al. (2025, ACL) 已证明 tie-breaking 方向影响表达力（最左 UHAT 对应 LTL 的严格更弱片段）；本文证明它同时影响验证复杂度。同一个开关，同时控制表达力和可验证性。

3.3 「消融」：假设松弛格

理论论文的消融 = 逐条拿掉前提，看哪条定理垮掉。下表根据证明依赖关系整理（论文本身未以此形式呈现，这是我的重构，可能有误）：

3.4 与前驱工作的定量改进对照

这是全文最有说服力的定量证据表：本文在同一个问题上同时抬高下界、压低上界，直到两者相遇。理论工作中「上下界闭合」是最高等级的结果形态，而本文对非空性、等价性、普遍性三个问题都做到了。

4.1 真正的贡献是什么

不是「证明了 Transformer 更简洁」，而是：把一个在逻辑学里成熟了 50 年的度量（succinctness, Stockmeyer 1974）引入神经网络表达力研究，并证明这个度量在此处不是学术趣味，而是解释力的关键来源。

1. 重新定义了问题：expressivity（能否）→ succinctness（多大）。这个转向使「Transformer 弱于 RNN」这个此前令人困惑的结论不再矛盾——它在集合包含意义上确实弱，在规模意义上确实强。
2. 建立了简洁性与可验证性的联系：不是两个独立结论并列，而是同一个构造（双指数计数器）的正反两面。
3. 闭合了一批开放的复杂度边界：把 NEXPTIME-hard 与无上界之间的缺口收紧为 EXPSPACE-完全。

可脱离本文单独复用的设计

4.2 局限性 · 第一类：论文自述

1. 固定（有限）精度假设。作者辩护称这「忠实于真实实现」，但排除了 log-precision 路线——而后者恰是 Merrill & Sabharwal 等一系列工作的标准设定。两条路线的结论因此不可直接比较。
2. 仅覆盖 unique hard attention。作者自述 UHAT 是「表达力上最弱的一类 Transformer」，并明确承认 softmax / average-hard attention 超出 AC⁰，「更广的 Transformer 类可能表达更多语言」。
3. 结论仅适用于 star-free 语言。这是 UHAT 刻画的直接后果。
4. 未来工作的自我定位：作者希望「开发一个自动分析、验证、解释 Transformer 的工具」，尽管有 EXPSPACE-完全性，并提议借助「符号技术、仿真等」手段。这实际上是承认本文主结论之一是一个需要绕过的负面结果。

4.3 局限性 · 第二类：补充批判（独立观察）

批判 1｜简洁性结论与可验证性结论建立在不同的模型上，论文未标注这一断裂。（论证缺口）

Thm 14 / Thm 16 的计数器构造依赖最右 tie-breaking；而 Cor. 13 的 NEXP 好消息依赖最左 tie-breaking + 严格未来掩码。因此论文实际给出的是：模型 A（最右）极其简洁、EXPSPACE-完全；模型 B（最左+严格未来）NEXP、简洁性未知。论文的叙事（「简洁性带来不可验证性」）暗示这是同一模型内的权衡，但证据并不支持这个因果读法。要坐实因果，需要证明「模型 B 的简洁性差距严格小于模型 A」，论文没有做。

批判 2｜双指数简洁性的证据是单点存在性，而非分布性质。（实验设计问题的理论对应物）

简洁性定义是存在量词形式。因此 Thm 16 只保证存在一族语言（本质上就是 tiling 编码）在 DFA 下双指数爆炸，完全没有说这类语言在自然语言 / 实际任务中的占比。类比实验论文：这相当于在一个精心构造的对抗基准上报告 +∞ 的提升，而不报告标准基准表现。论文缺少任何形式的「典型情形（average-case）简洁性」讨论。

批判 3｜与 Sälzer et al. 的比较不是 head-to-head。（缺乏关键竞品对比）

本文声称把非空性下界从 NEXPTIME-hard 提升到 EXPSPACE-hard。但 Sälzer et al. 研究的是量化 Transformer Encoder 的可满足性（trSAT），其结论是「一般情形不可判定，量化情形 NEXPTIME-hard 且在 NEXPTIME 内」。两个设定的模型类与问题定义并不相同：Sälzer 的量化 TE 在 NEXPTIME 内（上界更低），而本文的 UHAT 是 EXPSPACE-完全（更高）。「提升了下界」这个读法需要两个模型类可比才成立，而据我读到的 v2 内容，论文没有给出严格的模型翻译来支撑这个比较。§3.4 表中的该行应视为待核实项，而非既成事实。

批判 4｜RNN 比较的公平性依赖一个未被充分辩护的约定。（指标有效性问题）

Cor. 17（比 RNN 指数级简洁）是经由 Prop. 3（RNN ≡ 有限自动机）+ Thm 16 得到的推论，而非独立证明。它的成立高度依赖「RNN 精度 k 以一进制计入规模」这一约定，而论文对此的辩护只有一句「防止用任意精度做不公平比较」。这是一个实质性的建模选择：真实 RNN 精度是 fp16/fp32 即常数，此时一进制与二进制无差别；但若考虑精度随 n 增长的理论 RNN，一进制计入会人为地给 RNN 规模加上一个指数惩罚。Cor. 17 的指数差距中，有多少来自注意力的真实优势、多少来自这个计数约定，论文没有拆解。这是全文我认为最脆弱的结论。

批判 5｜「简洁 ⇒ 难验证」的因果箭头可能是反的，或两者都由第三个因素导致。（论证缺口）

更保守的解释是：EXPSPACE-hardness 和双指数简洁性都源自「UHAT 能编码 2ⁿ-tiling」这一单一事实——它们不是因果关系，而是共同原因（common cause）。这个区别对后续工作很重要：如果是共同原因，那么可能存在既简洁又易验证的模型（只要它简洁的方式不经由 tiling 编码）；如果是真因果，则不可能。论文选择了更有传播力的表述，而非更严谨的表述。

批判 6｜EXPSPACE-完全的实践意义被高估。（指标有效性问题）

论文（及获奖宣传）把 EXPSPACE-完全描述为「provably intractable」。但这是最坏情形复杂度，且是关于 UHAT 描述规模而非输入长度的复杂度。对形式验证社区常用的小规模抽象模型，实际可行性完全取决于常数与结构，而非渐近类——SAT/SMT 求解器日常处理 NP-完全和 PSPACE-完全问题。论文提出「用符号技术绕过」作为未来工作，恰恰说明作者自己也认为渐近类不是终局；但正文表述没有这份克制。

批判 7｜没有任何经验性的印证（sanity check）。（可复现性风险）

纯理论论文无代码（Poster 页确认），这在 cs.FL 完全正常。但本文的核心构造（双指数计数器）是可实现的——完全可以构造一个几十参数的玩具 UHAT，实际跑出它对 2ⁿ-tiling 的判定。这类「理论构造的可执行验证」在 mechanistic interpretability 社区已成惯例（如 Tracr）。不做这件事使 Example 4 的构造细节无法被独立复核，而这个构造承载了 Thm 14 / Thm 16 / Prop. 6 三个主结果。

批判 8｜v2 → v3 的变更不透明。（我的分析不完备之处）

arXiv 显示存在 v3（2026-05-15），即 ICLR camera-ready 之后的更新，我未能获取其 HTML 渲染。本报告全部定理编号与陈述以 v2 为准；若 v3 有改动，本报告的引用可能失准。此为已知不完备之处，在此明确标注。

5.1 Hahn (2020) — Theoretical Limitations of Self-Attention in Neural Sequence Models

TACL 2020 · ACL Anthology · arXiv:1906.06755

① 解决了什么问题。在 Transformer 席卷 NLP 的第三年，第一次给出硬性的不可能性结果：硬注意力 Transformer 无法识别 PARITY 与 DYCK-1。核心技术是 Lipschitz 型敏感度论证：单个 token 的改变对硬注意力输出的影响被有界地限制住，而 PARITY 要求任一位翻转都改变结果。一句话贡献：把「Transformer 表达力」从直觉话题变成可证明的数学对象。

② 遗留了什么缺口。它给的是否定结果的集合，不是刻画。更关键的是引发了持续多年的误读：既然连 PARITY 都不行，Transformer 就是「弱」的。Hahn 的度量是纯粹的集合包含关系，对代价完全不敏感——这个盲点在此埋下，直到本期核心论文才被点破。

③ 核心论文如何回应。没有推翻 Hahn，而是换了坐标轴。它接受「UHAT 表达力受限于 star-free」，然后指出：在受限的表达力范围内，Transformer 的编码效率远超所有等表达力的经典系统。Hahn 说的「弱」和本文说的「强」在数学上同时为真，因为它们度量的是不同的东西。

④ 关键设计的传递。Hahn 确立的「用形式语言类刻画神经架构」这一研究范式被完整继承；本文只是把范式中的比较关系从 ⊆ 换成了 |·|。

5.2 Barceló, Kozachinskiy, Lin, Podolskii (2024) — Logical Languages Accepted by Transformer Encoders with Hard Attention

ICLR 2024 · proceedings · arXiv:2310.03817

① 解决了什么问题。把 Hahn 的零散否定结果升级为电路复杂度层面的定位：UHAT 只能识别 AC⁰ 内的语言，且不能识别全部 AC⁰ 语言；UHAT 可识别所有由「带任意一元数值谓词的一阶逻辑」定义的语言。同时给出 AHAT 的对照：可以走出 AC⁰、进入 TC⁰，并能识别全部 FO(All) 语言（甚至加上计数项）。

② 遗留了什么缺口。「⊊ AC⁰」是上界而非精确刻画——UHAT 到底恰好等于什么仍悬空。而且 UHAT / AHAT 的对照反而使问题更复杂：如果 AHAT 更强，为什么实践中用 softmax 的模型没有表现出对应的能力跃迁？规模维度的缺失在这里第二次显形。

③ 核心论文如何回应。继承了它的模型定义与 UHAT/AHAT 分层，并明确把自己限制在 UHAT 这个「最弱的类」上——正因 Barceló et al. 已确立 UHAT 是分层底部，在 UHAT 上证明的简洁性下界自动传递到更强的类。没有这个分层，「最弱的类都这么简洁」这一论证力度就不存在。

④ 关键设计的传递。「逻辑刻画作为分析工具」这条路线被完整继承。Barceló et al. 用 FO(All)，核心论文用 LTL——而 LTL = FO 在字上的等价（Kamp 定理）正是两者的接口。

5.3 ★ Yang, Chiang, Angluin (2024) — Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages

NeurIPS 2024 · proceedings PDF · arXiv:2310.13897

① 解决了什么问题。把 Barceló et al. 的上界收紧为精确刻画：满足「硬注意力 + 注意力掩码 + 严格掩码 + 无位置编码」的 Transformer 恰好等价于 LTL，即恰好定义 star-free 语言。技术上引入 B-RASP 作为中间语言，并分别刻画了位置编码、严格掩码、深度对表达力的增益。

② 遗留了什么缺口。它给了等价，但没有给代价。我在阅读该论文 NeurIPS 正文时确认：全文唯一涉及规模的陈述在 Appendix B.2——「每个 attention operation 至多翻译成 2^(T_A+T_B) 个操作」（在把依赖 query 与 key 双方的得分谓词化归为只依赖 key 的范式时产生的指数爆炸）。该论文没有给出跨多步翻译的总体规模关系，也没有讨论三者之间是否可高效编译。这个缺口的代价是双重的：概念上，读者会把「expressively equivalent」误读为「等价」，从而认为 Transformer 相对 LTL 没有优势；技术上，任何想借道 LTL 分析 UHAT 的算法都会白白付出一个指数。

③ 核心论文如何回应——直接、正面、双向地填这个洞：

• 上界方向：Prop. 11 + Prop. 12 把 UHAT → LTL 从双指数压到单指数。正是这一步让 Thm 5 得以给出 EXPSPACE（而非 2-EXPSPACE）上界。
• 下界方向：Thm 14 证明这个指数不可消除；配合 Prop. 15（LTL → UHAT 只需多项式），得到一个方向不对称的精确刻画。

④ 关键设计的传递。B-RASP 被原样继承为中间语言——核心论文的 Thm 5 和 Prop. 6 都是先在 B-RASP 上做，再传回 UHAT。技术迁移形式：从「用 B-RASP 证明表达力等价」→「用 B-RASP 证明规模下界与复杂度 hardness」。同一个脚手架，两种用途。

5.4 Sälzer et al. (2024/2025) — Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning

arXiv:2405.18548

① 解决了什么问题。第一次系统地问「验证 Transformer 有多难」。定义 trSAT，并证明：在表达力社区常用的 TE 模型下 trSAT 不可判定；限制到固定位宽算术（量化）后变为可判定，但 NEXPTIME-hard，同时给出量化 TE 的 NEXPTIME 上界。一句话贡献：把「形式验证 Transformer」从愿景变成一个有复杂度标价的问题，并指出量化是可判定性的关键开关。

② 遗留了什么缺口。它的可判定性开关是量化 / 精度，没有触及注意力结构（掩码、tie-breaking）——后者恰是核心论文发现的第二个开关。而对 UHAT 这个已被精确刻画的子类，其复杂度没有被单独定位。

③ 核心论文如何回应。Thm 5 / Thm 18 给出 UHAT 上非空性、等价性、普遍性的完全性结果——上下界闭合。更重要的是，Cor. 13 提供了一个 Sälzer 路线之外的新的复杂度调节旋钮：不是调精度，而是调注意力的掩码方向与 tie-breaking。

④ 关键设计的传递。「把神经网络验证问题归约到经典判定问题」的方法论被继承；核心论文换了归约源（2ⁿ-tiling 而非 SAT 变体），从而抬高到 EXPSPACE。

5.5 Jerad, Svete, Li, Cotterell (2025) — Unique Hard Attention: A Tale of Two Sides

ACL 2025 Short, pp. 977–996 · ACL Anthology · arXiv:2503.14615 · DOI 10.18653/v1/2025.acl-short.76

注：Ryan Cotterell 同时是本篇与核心论文的作者，这是一条同一课题组内部的问题传递。

① 解决了什么问题。指出 Yang et al. 的等价性依赖一个未被注意的实现细节：tie-breaking 同时允许最左与最右。该文证明：只有最左 tie-breaking 的 UHAT 对应 LTL 的一个严格更弱的片段；更有意思的是，最左硬注意力与 soft attention 等价，因此它「可能比最右模型更好地近似真实 Transformer」。一句话贡献：tie-breaking 的方向——一个通常被视为实现噪声的选择——是表达力的分水岭，而且更贴近真实实现的那一侧反而更弱。

② 遗留了什么缺口。它证明了 tie-breaking 影响表达力，但完全没有触及：它是否也影响规模 / 简洁性？是否影响验证复杂度？该文的分析路径仍经由 Yang et al. 的双指数翻译，因此无法给出好的算法上界。

③ 核心论文如何回应。Cor. 13 是对第二个问题的直接回答：限制到「严格未来掩码 + 最左 tie-breaking」的 UHAT，非空性在 NEXP 内——而且论文明确说明，这是通过改进 Jerad et al. 的双指数翻译得到的。也就是说，核心论文的 Prop. 11/12 技术在这里被第二次复用。

④ 关键设计的传递。从「区分 tie-breaking 方向」这一细粒度模型区分 → 核心论文把它升级为一个复杂度分类的维度。迁移形式：从「哪个更有表达力」→「哪个更可判定」。

6.1 演进树

6.2 演进的内在逻辑

推动力：度量的精细化

每一步都是在前一步「看起来已经回答完了」的地方，发现了一个被前一个度量平均掉的维度。特别地，第 3 步（精确等价）产生了一个假性完结感——「等价」这个词太强，让社区默认问题已经关闭了两年。

其中 Yang → Sälzer 的转折最关键：研究从「刻画 Transformer」变成「用 Transformer 的刻画去做算法」。一旦进入算法视角，规模就不再能被忽略，因为它直接进入复杂度界。核心论文可以看作这个转折的必然产物——只是花了两年才有人正式提出。

社区关注点的转移

早期（2020–2023）关注能力边界，动机是理解「Transformer 为什么强」；近期（2024–2026）关注可验证性与实现细节，动机转向 AI safety / 形式保证。核心论文的获奖本身就是这个转移的标志——ICLR 把 Outstanding Paper 给了一篇主分类为 cs.FL 的纯理论论文，且其最被强调的结论是一个负面结果。

演进阶梯读法：「✗PARITY」（单点反例）→「⊊ AC⁰」（类包含）→「≡ star-free」（精确等价）→「NEXPTIME-hard」（算法代价）→「tie-breaking 分岔」（模型细化）→「2-exp 规模差 + EXPSPACE-完全」（规模与复杂度同时闭合）。每一级的「指标」都比上一级更定量。

8.1 理论层面

T1｜最左片段的简洁性是否保持？（本文最直接的空白）

具体问题：Thm 14/16 的构造用了最右 tie-breaking；Cor. 13 的 NEXP 结果用了最左。限制到最左 + 严格未来掩码后，UHAT 相对 LTL / DFA 的简洁性差距是否仍为指数 / 双指数？

为什么高价值低门槛：若答案是「是」，我们得到一个帕累托改进的架构约束——同样简洁，但验证便宜一个指数层级，对形式验证工具设计有直接指导；若答案是「否」，则本文的因果叙事被坐实。无论哪个答案都重要，而所需技术全部已在两篇论文中就位。

T2｜平均情形简洁性（average-case succinctness）

具体问题：现有定义是存在量词形式，只保证存在一族坏语言。能否定义并证明一个分布敏感的简洁性度量，例如「在某个自然语言族上的期望规模比」？可操作切入点：先在 star-free 的自然子类（如 piecewise testable languages）上算出精确规模比，看是否仍是指数。

T3｜CoT 的简洁性增益

具体问题：Merrill & Sabharwal 证明了 CoT 提升表达力。在同一形式框架下，允许 k 步 CoT 的 UHAT 相对无 CoT 的 UHAT，简洁性差距是多少？

T4｜跨架构简洁性对标

具体问题：SSM / Mamba / 线性注意力与 Transformer 的表达力比较已有多篇工作，但简洁性维度完全空白。建议的设计：在相同的形式语言类（例如都限制到 star-free）上，对 Mamba 与 UHAT 做 head-to-head 的规模比较。这正是判决「线性注意力是否真正等价」的关键 head-to-head 空白——现有争论全部停留在表达力层面，而实践中的差距很可能是规模层面的。

8.2 工程与应用层

E1｜Tracr 式的构造可执行化

具体问题：把 Example 4 / Prop. 6 的双指数计数器构造实际编译成权重，验证其在小 n（如 n = 3, 4）时确实判定 2ⁿ-tiling。价值：(a) 独立复核三个主定理所依赖的构造；(b) 给 mechanistic interpretability 社区一个已知 ground-truth 的电路作为探针基准。门槛评估：低——Tracr 类工具已成熟，构造本身是显式的。

E2｜EXPSPACE 的实践绕行

具体问题：作者自己提出用「符号技术、仿真」绕过。更具体地：能否给出一个参数化复杂度结果，例如「以注意力层数 d 为参数时，非空性是 FPT 的」？真实小模型的层数是个位数。如果复杂度的指数塔只由层数驱动，而其他维度是多项式的，那么 EXPSPACE 在实践中就是可控的。论文的渐近分析没有做这个拆解，这是一个明确的空白。

E3｜简洁性作为架构搜索的目标函数

具体问题：如果简洁性是 Transformer 优势的来源，能否把「编码同一任务所需的最小模型规模」变成可测量的经验指标？具体形式：固定一族合成形式语言，测量各架构达到 100% 准确率所需的最小参数量，画出规模—架构曲线。这是把本文理论结论转成经验协议的最直接路径，且完全可做。

8.3 新兴与跨界方向

N1｜简洁性与可解释性的张力

本文暗示了一个不安的推论——模型越简洁，其行为越难被展开检查。可解释性研究默认「找到电路 = 理解模型」，但若电路本身是一个双指数压缩，那么「理解」它可能在计算上不可行。可操作化：定义「解释的规模」（explanation size）——把一个 UHAT 翻译成人类可读形式（如 LTL 公式或决策树）所需的规模。Thm 14 实际上已经给出了这个量的下界：指数级。这是对可解释性研究的一个形式化的负面结果，尚未有人明确提出。

N2｜简洁性与记忆 / 泛化的联系

本期候选池中另一篇 ICML 2026 荣誉提名 How much can language models memorize? 测量了「每参数约 3.6 bits」的容量。简洁性给出的是同一枚硬币的另一面：同样的信息，Transformer 需要的参数更少。能否把两条线定量地接起来——「每参数比特数」与「相对 DFA 的规模比」是否可互相推导？门槛：中。

N3｜可验证架构的设计规范

Cor. 13 表明结构约束能降低验证复杂度一个指数层级。能否系统地枚举「复杂度友好」的注意力结构约束，形成一份设计规范？若未来监管要求「关键系统的模型必须可形式验证」，这份规范就是从理论到合规的接口。

How much can language models memorize? (ICML 2026 Oral / Honorable Mention)

Morris, Sitawarin, Kokhlikyan, Guo, Suh, Rush, Chaudhuri, Mahloujifar. 提出把「记忆」与「泛化」在信息论上分离的容量度量，给出「每参数约 3.6 bits」的经验估计。与本期核心论文构成同一问题的信息论对偶（见 N2），是本期最推荐的配套阅读。
arXiv:2505.24832 🔎 · ICML Oral 🔎 · OpenReview 🔎

To Grok Grokking: Provable Grokking in Ridge Regression (ICML 2026 HM)

Mingyue Xu, Gal Vardi, Itay Safran. 在岭回归这一可解析模型上给出 grokking 的可证明刻画。价值在于把长期靠经验观察的现象降到了有闭式解的设定——理论工作处理神秘现象的标准且有效的路数。
ICML 2026 获奖公告 ✅

The Obfuscation Atlas: Mapping Where Honesty Emerges in RLVR with Deception Probes (ICML 2026 HM)

Taufeeque, Heimersheim, Gleave, Cundy. 用探针方法定位 RLVR 训练中诚实性出现（与消失）的位置。对齐研究中少见的机制层面而非行为层面的工作。
ICML 2026 获奖公告 ✅

Position: The Alignment Community is Unintentionally Building a Censor's Toolkit (ICML 2026 Outstanding Position Paper)

Sarah Ball, Phil Hackemann. ICML 2026 唯一的杰出立场论文。论点：对齐社区开发的控制技术与审查工具在技术上难以区分。无论是否同意，这是本年度对齐领域最值得读的反方论证。
ICML 2026 获奖公告 ✅

The Polar Express: Optimal Matrix Sign Methods and their Application to the Muon Algorithm (ICLR 2026 HM)

Amsel, Persson, Musco, Gower. 用逼近论为 Muon 优化器中的极分解设计最优多项式逼近，专门针对 GPU 与低精度场景。理论直接落到工程的罕见范例。
OpenReview 🔎 · ICLR 公告 ✅

LLMs Get Lost In Multi-Turn Conversation (ICLR 2026 Outstanding Paper)

Laban, Hayashi, Zhou, Neville. 可扩展的多轮评测方法，显示指令不明确时 LLM 可靠性显著下降。与本期核心论文同批获奖，但走纯经验路线——两者并列获奖本身说明 ICLR 对「理论」与「评测」的同等重视。
OpenReview 🔎

Model Capacity Determines Grokking through Competing Memorisation and Generalisation Speeds (arXiv 2026.05)

把 grokking 归因于记忆与泛化两条学习速度的竞争，且由模型容量调节。与上面两篇构成一个自洽的三角，适合合起来读。
arXiv:2605.09724 🔎

Unique Hard Attention: A Tale of Two Sides (ACL 2025 Short)

已在 §5.5 详述。若只读一篇本文的前置文献，读这篇：它最短，且直接解释了核心论文 Cor. 13 的来龙去脉。
ACL Anthology ✅ · arXiv:2503.14615 ✅