Transformers are Inherently Succinct

Paper: arXiv:2510.19315v3；OpenReview Code: 代码搜索未找到开源实现（Web + GitHub repo/code search，2026-05-18） Code reference: N/A — no public repository, no github_ref

1. Motivation (研究动机)

1.1 这篇论文要修正什么直觉？

经典表达能力讨论通常问的是「一个模型能识别哪类形式语言」。 在这个视角下，有限精度 Transformer 的理论结果并不显得强： 固定精度 Transformer 常落在某些 subregular language class 中。 一个重要例子是 star-free languages。 Star-free regular languages 可由不使用 Kleene star、但允许交与补的正则表达式刻画。 论文给出的例子是 $a^{\text{*}}{b}^{\text{*}}$ 是 star-free，而 $(aa{)}^{\text{*}}$ 不是 star-free。 相比之下，固定精度 RNN 在形式语言视角下可识别所有 regular languages。 如果只看「语言类包含关系」，会得到一个反直觉印象： Transformer 似乎比 RNN 更弱。 这个结论与现代 LLM 的经验性能不匹配。 论文认为问题不在于现有表达能力结果错误，而在于它们只看了「能不能表示」，没有看「表示得多短」。

1.2 本文使用的替代指标：succinctness

Succinctness 衡量的是：给定同一个语言 $L$，某个形式系统 $C$ 中最小描述需要多大。 形式化地，若 $R$ 是语言 $L$ 的一种有限表示，则论文用 $|R|$ 表示最小 binary encoding 的长度。 对一类表示 $C$，succinctness 关注： 是否存在一族语言 $\{L_n\}$，使得 $C^{(1)}$ 只需小表示，而 $C^{(2)}$ 必须用大很多的表示。 这不是「能不能识别」的问题，而是「识别同一语言要付出多少描述长度」的问题。 该视角在逻辑和自动机理论中很经典。 例如 LTL 与 star-free languages 表达能力等价。 但 LTL 可以比有限自动机指数级更 succinct。 这种 succinctness 差异会直接反映在 decision problem 的复杂度上。 直觉是：更短的描述压缩了更大的展开结构，决策算法必须在某种意义上把这些结构展开。

1.3 本文主问题

本文问：有限精度 Transformer 是否虽然语言类不更大，却能以远短于 LTL、RNN、有限自动机的描述表示某些语言？ 这把 Transformer 理论从「expressivity class」推进到「descriptional complexity」。 论文的主要对象不是完整工程 Transformer，而是 unique-hard attention transformer（UHAT）。 UHAT 是硬注意力抽象。 论文引用 Jerad et al. (2025) 的结果说明： UHAT 上的表达能力界限可转移到固定精度 softmax Transformer 的相应界限。 论文的 lower bounds 甚至在 fixed-precision integers 下成立。 论文的 upper bounds 对 arbitrary rational weights 陈述，因此强于只在固定精度下陈述。 但作者强调其结论仍覆盖最贴近硬件实现的 fixed-precision arithmetic 场景。

1.4 为什么这个问题值得研究？

第一，它解释了一个表面矛盾： 有限精度 Transformer 的语言类可能不大，但它可以用极短描述编码极复杂的 regular/star-free 结构。 第二，它给「Transformer 为什么实践上有强表示效率」提供了一个可证明的描述复杂度解释。 第三，它揭示了验证 Transformer 语言性质的内在困难。 论文证明 non-emptiness 和 equivalence 等基本问题达到 EXPSPACE-complete。 这意味着即使模型形式化得非常简单，推理其接受语言仍可能需要双指数时间量级的展开。 第四，它把 LTL、finite automata、RNN、SSM 与 Transformer 放在同一个 succinctness 坐标系里比较。 这种比较比单纯「哪类语言可识别」更细。

1.5 论文版本与代码核验

本笔记基于 arXiv:2510.19315v3。arXiv 页面显示：2025-10-22 提交 v1，2026-05-15 最后修订 v3。OpenReview 页面显示：Published 2026-01-26，Last Modified 2026-05-13，ICLR 2026 Oral。旧笔记中写作 ICLR 2026 (poster); arXiv 2510.19315v2，此处已按当前页面修正为 Oral / v3。

代码搜索使用了： "Transformers are Inherently Succinct" github "Transformers are Inherently Succinct" code "Pascal Bergsträßer" "Transformers are Inherently Succinct" GitHub "Yxz92UuPLQ" GitHub gh search repos '"Transformers are Inherently Succinct"' gh search code '"Transformers are Inherently Succinct"' gh search repos 'Bergsträßer Cotterell Lin succinct transformer' gh search code '"UHAT" "B-RASP" "succinct" "Berg"' GitHub 命中主要是 daily digest、survey、metadata、paper summary 类仓库。

未找到官方或第三方可运行实现。因此本笔记不设置 github_ref frontmatter。因此也不写 source-code mapping table。论文自身是理论证明工作，不包含训练脚本、实验代码或可复现实验配置。

2. Idea (核心思想)

2.1 一句话核心 insight

本文的核心 insight 是： Transformer 的强处不必表现为「可识别语言类更大」。 即使在与 LTL / star-free languages 相关的有限精度设置中，UHAT 仍可用多项式大小表示某些语言。 这些语言若由 LTL 或 RNN 表示需要指数大小，若由有限自动机表示需要双指数大小。 也就是说，Transformer 把巨大的自动机状态空间压缩进了短的 attention-based description。

2.2 与既有方法的根本差异

以往工作常证明 UHAT、B-RASP、LTL、star-free languages 之间的表达能力关系。 这些结果回答「同一语言类是否可表达」。 本文则问「同一语言最短表示有多大」。 因此它不是又给出一个语言类包含定理。 它给出的是 descriptional complexity separation。 对比 LTL： LTL 与 star-free languages 表达能力相关，但对某些 witness languages，LTL 最小公式仍至少指数大。 对比有限自动机： 有限自动机必须显式或半显式展开双指数多的状态/前缀结构。 对比 RNN： 固定精度 RNN 可被映射到有限自动机，状态数为 $2^{kD}$。 因而若有限自动机需要双指数状态，固定精度 RNN 的描述也至少指数级增长。

2.3 技术路线的最短概括

先证明 UHAT / B-RASP 的 non-emptiness 是 EXPSPACE-complete。 关键 lower bound 来自 $2^N$-tiling。 该问题要求在宽度 $2^N$ 的网格上放置 tiles，满足边界、水平兼容、垂直兼容、终止 tile 等约束。 论文构造一个多项式大小 B-RASP 程序。 该程序接受一个编码后的 tiling configuration，当且仅当原 tiling 实例有解。 关键操作是 strict future masking + rightmost tie-breaking。 它让程序能在压缩表示上定位后继列/后继行，并检查相邻约束。 再把特殊形式的 B-RASP 多项式时间翻译成 UHAT。 由此得到 UHAT non-emptiness 的 EXPSPACE-hardness。 接着证明 upper bound： UHAT 运行中出现的中间向量只需要 polynomial bit-length。 因此可在指数时间枚举这些向量。 然后逐层把 UHAT 翻译成指数大小 LTL 公式。 用 LTL satisfiability 的 PSPACE 决策过程得到 EXPSPACE membership。

2.4 从 non-emptiness 到 succinctness

论文构造 witness family $\{L_n\}$。 每个 $L_n$ 都可由大小 $\mathrm{poly}(n)$ 的 UHAT $T_n$ 识别。 但 $L_n$ 的最短 accepted word 至少有双指数长度。 若一个 LTL 公式 ${\phi }_n$ 识别同一 $L_n$，则由于 LTL 最短模型长度至多对公式大小指数增长，${\phi }_n$ 必须至少指数大。 若一个有限自动机识别同一 $L_n$，则有限自动机的最短 accepted word 长度至多线性受状态数约束，故自动机必须至少双指数大。 固定精度 RNN 又可被有限自动机模拟，因此得到 UHAT 相对 RNN 的指数 succinctness gap。

2.5 自制路线图

Figure 1 解读：该自制图把论文的证明压缩成五步：从 EXPSPACE-hard 的 $2^N$-tiling 出发，构造 B-RASP 程序，再用 Lemma 9 翻译到 UHAT；反方向通过 polynomial-bit intermediate vectors 枚举，把 UHAT 翻译成指数大小 LTL，从而同时得到复杂度 upper bound 和 succinctness upper/lower matching picture。

3. Method (方法)

3.1 形式对象：UHAT as language recognizer

论文采用 unique-hard attention transformer（UHAT）。输入是非空字符串 $a=a_1\dots a_N\in {\Sigma }^{+}$。Symbol embedding 是一个函数： $\mathrm{emb}:\Sigma \to {\mathbb{Q}}^D$。它逐 token 应用于字符串，得到向量序列。UHA layer 的核心组成包括： 三个 affine transformations：$A,B:{\mathbb{Q}}^R\to {\mathbb{Q}}^R$，以及 $C:({\mathbb{Q}}^R\times {\mathbb{Q}}^R)\to {\mathbb{Q}}^S$。

一个 mask predicate $M:\mathbb{N}\times \mathbb{N}\to \{0,1\}$。一个 tie-breaking function $\tau$，用于在 hard attention 的 argmax 集合中选唯一位置。ReLU layer 对指定坐标逐位置应用 $\max (0,\cdot )$。UHAT 是 embedding、UHA layers、ReLU layers 的复合： $T:{\Sigma }^{+}\to ({\mathbb{Q}}^S{)}^{+}$。作为语言识别器时，给定 acceptance vector $t\in {\mathbb{Q}}^S$。

若 $T(a)=v_1,\dots ,v_N$ 且 $⟨t,v_N⟩>0$，则 $a\in L(T)$。对只允许 strict past masking 的片段，论文也讨论用第一位置读取接受值的对应变体。

3.2 固定精度假设的边界

作者在定义 UHAT 时允许 arbitrary rational numbers。 这是为了 upper bounds 更一般。 但下界可在 fixed-precision integers 下成立。 论文脚注强调固定精度算术需要固定 deterministic evaluation order。 原因是标准 floating-point arithmetic 不满足结合律。 例如 attention head 中 dot product 的求和顺序会影响结果。 因此形式定理应理解为在固定求值顺序下讨论。 这点很重要： 论文并没有假设无限精度实数计算来制造不现实的下界。 它把描述复杂度 gap 放在与现实硬件更接近的有限精度语境中。

3.3 B-RASP：证明 lower bound 的中间语言

B-RASP 是 Boolean RASP。论文使用它作为中间步骤，因为已有工作表明 B-RASP 与 UHAT 表达能力紧密相关。一个 B-RASP 程序是谓词序列： $P_1,\dots ,P_{\Pi }\in \{0,1{\}}^{[N]}$。对输入词 $a=a_1\dots a_N$，前 $|\Sigma |$ 个谓词是 token lookup： 对每个 $a\in \Sigma$，$Q_a(n)=1$ 当且仅当 $a_n=a$。后续谓词由两类操作构成。第一类是 position-wise operation： $P_{t+1}(i):=R(i)$。其中 $R(i)$ 是当前已知谓词在同一位置 $i$ 上的 Boolean combination。

第二类是 attention operation： $P_{t+1}(i):=◃{▹}_j[M(i,j),S(i,j)]V(i,j):D(i)$。$◃$ 与 $▹$ 分别表示 leftmost 与 rightmost tie-breaking。$M(i,j)$ 是 mask predicate。$S(i,j)$ 是 score predicate。$V(i,j)$ 是 value predicate。$D(i)$ 是没有可选位置时使用的 default predicate。

若存在满足 mask 与 score 的 $j$，attention 选 leftmost 或 rightmost 的一个 $o(i)$。然后输出 $V(i,o(i))$。若不存在这样的 $j$，输出 $D(i)$。语言接受条件是最后一个谓词在末位置为 1： $P_{\Pi }(N)=1$。

3.4 Succinctness 的两个定义

论文定义 $f$-more succinct。 对两类语言表示 $C^{(1)}$、$C^{(2)}$，若存在语言族 $\{L_n\}$ 与 $C^{(1)}$ 表示 $R_n^{(1)}$，使得每个等价的 $C^{(2)}$ 表示 $R_n^{(2)}$ 都满足： $|R_n^{(2)}|\ge f(|R_n^{(1)}|)$， 则 $C^{(1)}$ 对 $C^{(2)}$ 是 $f$-more succinct。 指数更 succinct 指 $f(n)\in \Omega (2^{c{n}^d})$。 双指数更 succinct 指 $f(n)\in \Omega (2^{2^{c{n}^d}})$。 论文还定义 $g$-bounded expansion。 若对每个语言 $L$ 和每个 $C^{(2)}$ 表示 $R^{(2)}$，都存在等价的 $C^{(1)}$ 表示 $R^{(1)}$，且： $|R^{(1)}|\le g(|R^{(2)}|)$， 则 $C^{(1)}$ 对 $C^{(2)}$ 有 $g$-bounded expansion。 前者是 witness-family lower bound。 后者是 universal translation upper bound。 两者配合才能说明 gap 既存在又不会更大到无法界定。

3.5 Lower bound：从 $2^N$-tiling 到 B-RASP non-emptiness

Theorem 4：UHAT 与 B-RASP 的 non-emptiness problem 是 EXPSPACE-complete。Lower bound 的第一步是 Proposition 5： B-RASP non-emptiness 是 EXPSPACE-hard。证明从 $2^N$-tiling problem 归约。$2^N$-tiling 的一个 tile 是四元组： $t=⟨a,b,c,d⟩\in {\mathbb{N}}_{40}^4$。论文写作 $left(t)=a$，$up(t)=b$，$right(t)=c$，$down(t)=d$。输入包括有限 tile set $T$、初始/终止相关条件、以及宽度参数 $N$。

目标是判断是否存在 $M\in \mathbb{N}$ 与函数： $\tau :[2^N]\times [M]\to T$， 使得网格满足边界、水平兼容、垂直兼容、终止 tile 等条件。论文引用 Schwarzentruber (2019) 得到 Proposition 7： $2^N$-tiling 是 EXPSPACE-complete。Lemma 8： 给定一个 $2^N$-tiling 实例，可以在关于 $N$ 的多项式时间内构造 B-RASP 程序。该程序语言非空当且仅当 tiling 实例有解。构造思想是把候选 configuration 编码成带分隔符的多行/多列字符串。每一行用二进制计数器标识列。# 等分隔符把行/列结构显式放进字符串。

B-RASP 谓词检查每个位置是否具有合法 tile、合法坐标、合法分隔。水平约束检查同一行相邻列的 right/left 是否匹配。垂直约束检查相邻行同一列的 up/down 是否匹配。关键观察是 strict future masking + rightmost tie-breaking 可以定位「后面最近的相关位置」。这让程序用固定数量的 attention-like 操作跨过长编码，比较 successive configurations。因为 width 是 $2^N$，而 B-RASP 程序大小仍是 $\mathrm{poly}(N)$，这里已经产生指数压缩。

3.6 B-RASP 到 UHAT：Lemma 9

Lemma 9 处理一种特殊形式的 B-RASP attention operation。若每个 attention operation 的 score predicate 可拆成： 一部分只依赖 $j$；一部分比较 $i$ 与 $j$ 上若干已有谓词是否相等；则可在多项式时间构造等价 UHAT。构造使用 one-hot symbol embedding。初始 token lookup 谓词直接成为输入向量坐标。UHAT 在每层保留已有坐标，并逐步追加新坐标存储 $P_t(i)$。

对 position-wise Boolean combination： affine + ReLU 层逐位置计算 negation、conjunction、disjunction 等 Boolean 子式。对 B-RASP attention： 使用一个 UHA layer。该层的 mask predicate 与 B-RASP 的 $M$ 一致。tie-breaker 与 B-RASP 的 leftmost/rightmost 一致。affine maps $A,B$ 计算 score 所需的坐标。affine map $C$ 把当前位置向量与被 attention 选中的向量组合。

value predicate $V(i,j)$ 通过复制被选中位置的相关分量，再由小型 ReLU 子网计算。score 中只依赖 $j$ 的部分可通过 preliminary layer 预先在每个位置算好。score 中比较二进制数相等的部分，通过设计 attention score，让相等时取得最大值。因此 Lemma 8 的 B-RASP lower-bound construction 可以转移到 UHAT。Proposition 10 随即得到： UHAT non-emptiness 是 EXPSPACE-hard。

3.7 Upper bound：UHAT 到 LTL 的指数翻译

Hardness 只说明问题至少难。为了得到 EXPSPACE-complete，还要证明 membership。论文的上界核心是 Proposition 12 与 Proposition 13。Proposition 12： 对每个 UHAT $T$，在任意输入上评估 $T$ 所需 precision 关于 $|T|$ 是多项式。这意味着每层可能出现的向量集合虽然很大，但每个向量只需 polynomial bit-length。因此可在指数时间内枚举该有限集合。Proposition 13： 给定识别语言 $L\subseteq {\Sigma }^{+}$ 的 UHAT $T$，可在指数时间内构造等价 LTL 公式 $\phi$。构造是逐层模拟。

对每一层、每个可能向量值，构造 LTL 子公式表示「当前位置在该层的向量等于这个值」。对 attention 层，LTL 公式表达 mask、score、tie-breaking 选择与 value transfer。对 ReLU 层，LTL 公式表达坐标上的 piecewise-linear update。因为可枚举向量数至多指数级，所以 LTL 公式大小至多指数级。这比 Yang et al. (2024) 的 doubly exponential translation 更紧。对 B-RASP，Yang et al. (2024) 已给出到 LTL 的指数构造。LTL satisfiability 在公式大小上可用 polynomial space 决定。

若公式本身是原 UHAT/B-RASP 的指数大小，则总空间是指数级。所以 non-emptiness 属于 EXPSPACE。与 lower bound 合并即 Theorem 4。

3.8 Restricted mask/tie-breaking 的细节

Corollary 11： 若 UHAT 每层只使用 strict future masking + rightmost tie-breaking，non-emptiness 仍 EXPSPACE-hard。 对偶地，strict past masking + leftmost tie-breaking 也保持 EXPSPACE-hard。 这是因为 Lemma 8 的 B-RASP 构造本身使用 strict future/rightmost。 Lemma 9 的 UHAT 翻译保留 mask predicate 与 tie-breaking。 Corollary 14 给另一个 restricted upper-bound： 若每层使用 strict future masking + leftmost tie-breaking，或 strict past masking + rightmost tie-breaking，则 non-emptiness 在 NEXP 中。 作者指出 Jerad et al. (2025) 曾把这些 restricted UHAT 与只含 $P$ 或只含 $F$ 的 LTL fragment 联系起来。 但此前 UHAT 到这些 fragment 的构造有双指数 blow-up。 本文的指数翻译使该 restricted case 的上界更紧。

3.9 Succinctness 定理：Theorem 15 / 17 / Corollary 18

Figure 2 解读：该自制图展示本文最终 separation：同一 witness language family 可由 $\mathrm{poly}(n)$ 大小 UHAT 表示；任何等价 LTL 或固定精度 RNN 至少指数大；任何等价有限自动机至少双指数大。图中的大小关系来自 Theorem 15、Theorem 17 与 Corollary 18。

Theorem 15： UHATs are exponentially more succinct than LTL。 证明复用 non-emptiness lower bound 的 witness。 构造语言族 $L_n$ 与大小 $\mathrm{poly}(n)$ 的 UHAT $T_n$。 $T_n$ 识别 $L_n$，且 $L_n$ 的最短 accepted word 至少双指数长。 若 LTL 公式 ${\phi }_n$ 识别 $L_n$，则 ${\phi }_n$ 的最短模型长度至多指数依赖于 $|{\phi }_n|$。 因为实际最短 accepted word 是双指数，所以 $|{\phi }_n|$ 必须至少指数大。 Proposition 16： UHATs have polynomially bounded expansion over LTL。 给定 LTL 公式 $\phi$，可多项式时间构造等价 UHAT $T$。 证明按 LTL 子公式归纳。 对原子 $Q_a$，token embedding 已经给出 $1[a_n=a]$。 对 Boolean combinations，用 affine + ReLU point-wise 计算。 对 since / until 等 temporal operators，用 strict future/rightmost 或 strict past/leftmost attention 定位 witness。 因此 LTL 到 UHAT 不需要指数 blow-up。 Theorem 17： UHATs are doubly exponentially more succinct than finite automata。 仍复用 Theorem 15 的 witness family。 对有限自动机，最短 accepted word 长度至多与状态数线性相关。 若 $L_n$ 的最短 accepted word 已达双指数，则等价自动机状态数也至少双指数。 Corollary 18： UHATs are exponentially more succinct than RNNs。 这是 Theorem 17 与 Proposition 1 的组合。 Proposition 1 说明固定精度 RNN 可由 $2^{kD}$ 状态的有限自动机表示。 若自动机至少双指数大，则固定精度 RNN 描述至少指数大。

3.10 Verification hardness：Theorem 19

Section 5 把 succinctness 后果落实到 reasoning / verification。 Theorem 19： Deciding equivalence between two UHATs is EXPSPACE-complete。 Lower bound： 从 UHAT non-emptiness 归约。 给定 UHAT $T$，固定一个识别空语言的 UHAT $T_0$。 $T$ 与 $T_0$ 等价当且仅当 $T$ 识别空语言。 因此 equivalence 至少与 non-emptiness 一样难。 Upper bound： 对两个 UHAT $T_1,T_2$，用 Proposition 13 分别翻译成 LTL 公式 ${\phi }_1,{\phi }_2$。 $T_1,T_2$ 等价当且仅当 ${\phi }_1,{\phi }_2$ 等价。 LTL equivalence 可在 polynomial space 中决定。 因为公式大小相对原 UHAT 指数大，所以整体为 EXPSPACE。

3.11 证明结构伪代码（非 released code）

def prove_nonemptiness_expspace_complete(tiling_instance):
    """
    这是论文证明流程的伪代码，不是 released implementation。
    输入是 2^N-tiling instance；输出是复杂度归约链条。
    """
    b_rasp_program = construct_b_rasp_for_tiling(tiling_instance)
    assert size(b_rasp_program) <= poly(tiling_instance.N)
 
    # Lemma 8:
    # L(b_rasp_program) is non-empty iff the tiling instance has a solution.
    lower_bound_for_b_rasp = reduce_from_2N_tiling(b_rasp_program)
 
    uhat = translate_special_b_rasp_to_uhat(b_rasp_program)
    assert size(uhat) <= poly(size(b_rasp_program))
 
    # Lemma 9 + Proposition 10:
    # The same lower bound transfers to UHAT.
    lower_bound_for_uhat = transfer_nonemptiness_hardness(lower_bound_for_b_rasp, uhat)
 
    # Proposition 13:
    # Enumerate polynomial-bit intermediate vectors and build an exponential-size LTL formula.
    ltl_formula = translate_uhat_to_ltl(uhat)
    assert size(ltl_formula) <= exp(poly(size(uhat)))
 
    # LTL satisfiability is PSPACE in formula size.
    upper_bound = decide_ltl_satisfiability_in_pspace(ltl_formula)
    return lower_bound_for_uhat, upper_bound

def witness_family_succinctness(n):
    """
    这是 Theorem 15/17 的证明骨架。
    它抽象 witness family，而非计算论文中的完整构造。
    """
    T_n = construct_polynomial_size_uhat(n)
    L_n = language_recognized_by(T_n)
 
    shortest_word = shortest_accepted_word_length(L_n)
    assert shortest_word >= double_exponential(n)
 
    min_ltl_size = lower_bound_ltl_size_from_shortest_model(shortest_word)
    assert min_ltl_size >= exponential(n)
 
    min_dfa_size = lower_bound_dfa_size_from_shortest_word(shortest_word)
    assert min_dfa_size >= double_exponential(n)
 
    min_rnn_size = lower_bound_rnn_via_finite_precision_dfa(min_dfa_size)
    assert min_rnn_size >= exponential(n)
 
    return {
        "UHAT": "poly(n)",
        "LTL": ">= exp(n)",
        "finite_automata": ">= double_exp(n)",
        "fixed_precision_RNN": ">= exp(n)",
    }

3.12 论文公式与 released code 实现差异

代码搜索未找到开源实现。 因此不存在可核对的 released code 与 paper formula 差异。 本文所有伪代码均为证明结构复述，不是从仓库源码抽取。 若未来出现官方实现，应补充： github_ref: <branch>@<short_sha>。 source-code mapping table。 released code 与论文公式差异段落。

4. Experimental Setup (实验设置)

4.1 这不是经验实验论文

本文没有数据集训练实验。 没有模型训练配置。 没有 GPU / batch size / learning rate / optimizer。 没有 benchmark accuracy、loss、F1 等经验指标。 其「实验设置」应理解为理论比较设置： representation classes； language recognizer semantics； size measure； witness problem； decision problems。

4.2 比较对象

UHAT： unique-hard attention transformer。 作为语言识别器读取最后位置的 acceptance score。 B-RASP： Boolean RASP 程序。 用作证明 EXPSPACE-hardness 的中间形式。 LTL： linear temporal logic。 与 star-free languages / counter-free automata 有经典联系。 Finite automata： 用于自动机大小下界与 RNN 模拟。 Fixed-precision RNN： 按论文定义为 $(\Sigma ,g,h_0,f)$。 在固定 $k$ bit precision 下，$D$ 维 hidden state 空间可映射到 $2^{kD}$ 个有限自动机状态。 SSM： 论文在 introduction 中把 RNN gap 延伸到 state-space models 的相关讨论。

4.3 评价指标

Primary metric 1：succinctness gap。 衡量同一语言族在不同表示类中的最小表示大小差异。 Primary metric 2：bounded expansion。 衡量任意一个表示能否被另一表示在 polynomial / exponential size blow-up 内模拟。 Primary metric 3：decision complexity。 包括 non-emptiness 与 equivalence。 Primary metric 4：translation size。 例如 UHAT 到 LTL 的翻译是 singly exponential，而不是 prior work 的 doubly exponential。 Primary metric 5：shortest accepted word length。 Witness family 的核心性质是最短 accepted word 至少双指数长。

4.4 理论 benchmark：$2^N$-tiling

$2^N$-tiling 是 reduction source problem。 输入是 tile set 与约束。 宽度固定为 $2^N$。 高度 $M$ 是待存在量。 要求存在 $\tau :[2^N]\times [M]\to T$。 约束包括： final tile condition：$\tau (2^N,M)=t_{\mathrm{fin}}$。 vertical boundary：每列顶部/底部满足指定 boundary color 0。 horizontal boundary：最左/最右满足指定 boundary color 0。 horizontal compatibility：相邻列的 right/left 匹配。 vertical compatibility：相邻行的 up/down 匹配。 Proposition 7 给出该问题 EXPSPACE-complete。 论文利用该问题把双指数结构压进多项式大小 B-RASP / UHAT 表示。

4.5 证明设置中的大小记账

表示大小 $|R|$ 是最小 binary encoding 长度。 RNN 的 precision $k$ 以 unary 计入大小。 这是为了避免不公平比较： 不能让 RNN 通过把 precision 暗中增大到 $2^k$ 来免费获得更大状态空间。 UHAT lower bound 在 fixed-precision integers 下成立。 UHAT upper bound 在 arbitrary rationals 下成立。 LTL 公式大小按公式符号/编码长度计。 Finite automata 大小按自动机描述/状态规模计。 对 witness family，论文关注的是 asymptotic gap： UHAT $\mathrm{poly}(n)$。 LTL / RNN $\ge 2^{\Omega (n^c)}$。 finite automata $\ge 2^{2^{\Omega (n^c)}}$。

4.6 图像/资产处理

对 arXiv:2510.19315 运行 extract_figures.py --arxiv。 arXiv source 提取到的唯一图像文件是 eu-erc_cropped.svg。 该文件是资助/机构相关图标，不是论文技术图。 PDF 正文没有架构图、结果图或表格图。 因此本笔记没有嵌入原论文 figure。 为帮助阅读，本笔记在 vault mirror asset path 下创建了两个自制 SVG： proof_pipeline.svg。 succinctness_ladder.svg。 二者均明确标注为自制图，不冒充论文原图。

5. Experimental Results (实验结果)

5.1 主结果总览

Result	Statement	Meaning
Theorem 4	UHAT / B-RASP non-emptiness is EXPSPACE-complete	检查语言非空已双指数空间级难
Theorem 15	UHATs are exponentially more succinct than LTL	有些语言 UHAT 多项式表示，LTL 至少指数表示
Proposition 16	UHATs have polynomially bounded expansion over LTL	LTL 可多项式翻译到 UHAT
Theorem 17	UHATs are doubly exponentially more succinct than finite automata	有些语言 UHAT 多项式表示，自动机至少双指数表示
Corollary 18	UHATs are exponentially more succinct than RNNs	固定精度 RNN 因可被自动机模拟而至少指数变大
Theorem 19	UHAT equivalence is EXPSPACE-complete	判断两个 UHAT 是否识别同一语言也极难

5.2 对 LTL 的结果

Theorem 15 给出 lower bound： 存在语言族 $\{L_n\}$。 每个 $L_n$ 有大小 $\mathrm{poly}(n)$ 的 UHAT 表示。 每个等价 LTL 公式大小至少指数级。 证明核心不是直接数 LTL operators。 它通过最短 accepted word 的长度来反推 LTL 公式大小。 若 LTL 公式较小，则其最短模型不会太长。 但 witness language 的最短 accepted word 已经双指数长。 因此 LTL 公式必须指数大。 Proposition 16 则给出上界： 任意 LTL 公式可多项式翻译成 UHAT。 这说明 UHAT 至少不会比 LTL 在描述上差。 两者合起来说明： UHAT 对 LTL 的 gap 是真实的、方向明确的 succinctness 优势。

5.3 对有限自动机的结果

Theorem 17 更强。 UHAT 比 finite automata 双指数更 succinct。 它复用 Theorem 15 的 witness family。 对 DFA/NFA 类自动机，若接受某个非空语言，则存在长度受状态数线性控制的 accepted word。 如果语言的最短 accepted word 本身是双指数长，则自动机状态数必须双指数大。 这个结果比「LTL 比 automata 指数 succinct」更强一层。 因为 UHAT 先比 LTL 指数 succinct，而 LTL 又与 counter-free automata 有指数翻译关系。 最终体现为 UHAT 对有限自动机的双指数压缩。

5.4 对 RNN / SSM 的结果

Corollary 18 给出 UHAT 相对固定精度 RNN 的指数 succinctness。 关键是 Proposition 1： 一个固定精度 RNN，若 hidden dimension 是 $D$、precision 是 $k$，可被 $2^{kD}$ 状态有限自动机表示。 因此固定精度 RNN 的可区分 hidden states 是有限的。 对需要双指数自动机状态的 witness languages，RNN 若要等价识别，就必须把 $kD$ 推到指数级。 由于 precision $k$ 计入表示大小，不能通过提高精度免费绕过。 因此 RNN 表示大小至少指数大。 论文 introduction 也把该结论关联到 state-space models。 读法是： 若某类模型在固定精度下可被类似有限状态机制刻画，那么 UHAT 的 succinctness advantage 会转化为该类模型的描述长度劣势。

5.5 对 verification 的结果

Non-emptiness： 给定一个 UHAT，问 $L(T)$ 是否非空。 Theorem 4 证明该问题 EXPSPACE-complete。 Equivalence： 给定两个 UHAT，问它们是否识别相同语言。 Theorem 19 证明该问题 EXPSPACE-complete。 Lower bound 的 equivalence 归约很直接： 令 $T_0$ 识别空语言。 判断 $T$ 是否与 $T_0$ 等价，等价于判断 $L(T)$ 是否为空。 Upper bound 依赖 UHAT 到 LTL 的指数翻译。 LTL equivalence 本身可在 polynomial space 中决定。 总体上，短 UHAT 描述可能隐藏巨大语言结构。 因此验证它的语言性质不可避免地很难。

5.6 与 prior work 的差异

Yang et al. (2024)、Barceló et al. (2024)、Jerad et al. (2025)、Li and Cotterell (2025) 等工作建立 UHAT、B-RASP、LTL、star-free languages 的紧密关系。 本文的新增点不是再证明一个等价表达能力结论。 新增点是 succinctness 与 verification complexity。 Sälzer et al. (2025) 研究不同精度 Transformer verification，并给出 fixed-precision Transformer 的 NEXP-hardness。 该技术可推出 Transformer 比有限自动机 singly exponentially more succinct。 但不能给出本文的 double-exponential automata gap。 本文通过 $2^N$-tiling 与 B-RASP/UHAT 构造获得更强的 EXPSPACE 级结果。 另一个重要改进是 UHAT 到 LTL 的 translation。 论文把之前双指数 blow-up 改进到单指数 blow-up。

5.7 限制与适用边界

该论文是理论工作。 它不直接解释某个具体大模型 checkpoint 的 empirical performance。 它使用 UHAT 作为 Transformer 抽象。 虽然该抽象有文献支持，但仍不是完整 softmax multi-head Transformer 工程实现。 Lower bound 与 upper bound 在 precision assumptions 上表述不同： lower bounds 在 fixed-precision integers 下成立。 upper bounds 对 arbitrary rational weights 成立。 读者需要注意二者不是同一个最小假设集合。 结论是 worst-case / existence-style。 它证明存在某些语言族能被 UHAT 极其 succinctly 表示。 它不声称所有自然语言任务都自动具有同样的 separation。 论文没有 released code。 因此没有可直接运行的 construction generator 或 verifier。 本笔记中的伪代码只服务于理解证明路线。

5.8 我的读后结论

这篇论文最重要的贡献是把 Transformer 理论讨论从 expressivity class 推向 succinctness。 它解释了为什么「有限精度 Transformer 只识别 subregular languages」并不意味着它在表示上弱。 如果一个模型可以用短 attention construction 编码双指数长的 witness structure，那么语言类相同也可能掩盖巨大效率差异。 这也解释了 verification 难度为何会暴涨。 简短模型描述并不等于简单语言。 对形式验证和 mechanistic interpretability 来说，这是一条负面但重要的信息： 即使模型架构被抽象得很干净，判断其全局语言性质仍可达到 EXPSPACE-complete。 对 LLM/VLM theory taxonomy 来说，它应归入 LLM & VLM/Theory。 标签应突出 transformer-succinctness、UHAT、Boolean-RASP、LTL、EXPSPACE-completeness，而不是泛泛写成 Transformer paper。