一句话总结

RPTU Kaiserslautern-Landau、ETH Zurich 和 MPI-SWS 的研究人员证明，固定精度 Transformer 比线性时序逻辑和循环神经网络指数级更简洁，比有限自动机双指数级更简洁，并给出匹配的上界，改进了先前的双指数级翻译，他们进一步证明，空性和等价性等验证问题属于 $$\text{EXPSPACE}$-complete$−complete.

核心贡献

• For certain language families, fixed-precision transformers of polynomial size describe languages whose smallest equivalent linear temporal logic formula or recurrent neural network is exponentially large, and whose smallest equivalent finite automaton is doubly exponentially large.
• Matching upper bounds are established by translating any fixed-precision transformer into an equivalent linear temporal logic formula with at most exponential size growth, improving a prior doubly exponential translation bound.
• This succinctness implies that basic verification problems for transformers, including emptiness and equivalence, are EXPSPACE-complete, establishing provable intractability for fixed-precision transformers.

引言

Transformers are the dominant architecture behind modern large language models, so understanding their formal capabilities is important for reasoning about generalization, expressivity, and automated verification. Prior theoretical work mostly asks which languages finite precision transformers can recognize, a setting related to subregular languages. However, under fixed precision, this perspective can make transformers appear less expressive than recurrent networks, leaving open the question of whether raw expressive power is the best way to compare architectures.

The authors instead study succinctness, which measures how compactly a model can describe a language. They show that transformers, especially the unique hard attention transformer used as their main abstraction, can encode very large counters through attention. This lets them describe some languages with polynomial size transformers, while equivalent linear temporal logic formulas or recurrent networks require exponentially larger representations, and finite automata require doubly exponentially larger ones.

Their main contribution is a set of tight succinctness and verification results. They prove that transformers can be exponentially more succinct than LTL and RNNs, and doubly exponentially more succinct than finite automata, while also giving matching upper bounds by translating transformers into exponential size LTL formulas and doubly exponential size automata. They further show that checking whether a transformer recognizes a trivial language is EXPSPACE complete, which means transformer analysis is computationally hard in the worst case.

方法

The authors leverage a unique hard-attention transformer, or UHAT, as the central computational object. Rather than relying on the usual soft weighted-average attention, this model uses a hard, deterministic selection rule: every attention position chooses exactly one vector from a set of allowed earlier or later positions. The authors build the full system by composing token embeddings, hard attention modules, pointwise nonlinearities, and a final linear acceptance test, yielding a length-preserving sequence model that maps words to vectors.

The first module is the symbol embedding. Let $\Sigma$Σ denote an input alphabet. A symbol embedding is a function $\operatorname{emb}:\Sigma\to\mathbb{Q}^{D}$emb:Σ→QD for some dimension $D>0$D>0. This mapping extends naturally to words by embedding each symbol independently, so that a word $\mathbf{a}_1\cdots \mathbf{a}_N$a1​⋯aN​ becomes the sequence $\operatorname{emb}(\mathbf{a}_1),\ldots,\operatorname{emb}(\mathbf{a}_N)$emb(a1​),…,emb(aN​). This stage converts discrete sequences into rational vector representations that can be processed by the attention stack.

The core module is the unique hard-attention layer. A UHA layer of width $R>0$R>0 is specified by three affine transformations $A:\mathbb{Q}^{R}\to\mathbb{Q}^{R}$A:QR→QR, $B:\mathbb{Q}^{R}\to\mathbb{Q}^{R}$B:QR→QR, and $C:\mathbb{Q}^{R}\times\mathbb{Q}^{R}\to\mathbb{Q}^{S}$C:QR×QR→QS, together with a masking predicate $M:\mathbb{N}\times\mathbb{N}\to\{0,1\}$M:N×N→{0,1} and a tie-breaking function $\tau$τ. The mask is chosen from one of three forms: no masking, strict future masking, or strict past masking. The tie-breaking function is either leftmost, $\tau=\min$τ=min, or rightmost, $\tau=\max$τ=max. These components make the attention selection deterministic and positionally controlled.

Given a sequence of input vectors $\mathbf{v}_1,\ldots,\mathbf{v}_N\in\mathbb{Q}^{R}$v1​,…,vN​∈QR, the layer first computes a pairwise score

$$\mathrm{S}(\mathbf{v}_n,\mathbf{v}_m)=\langle A(\mathbf{v}_n),B(\mathbf{v}_m)\rangle.$$S(vn​,vm​)=⟨A(vn​),B(vm​)⟩.

For each query position $n$n, the allowed positions are the unmasked set

$$U_n=\{m\in[N]\mid M(n,m)=1\}.$$Un​={m∈[N]∣M(n,m)=1}.

The authors then define the argmax set

$$B_n=\{m\in U_n\mid \forall m'\in U_n:\mathrm{S}(\mathbf{v}_n,\mathbf{v}_m)\ge \mathrm{S}(\mathbf{v}_n,\mathbf{v}_{m'})\}.$$Bn​={m∈Un​∣∀m′∈Un​:S(vn​,vm​)≥S(vn​,vm′​)}.

Because the layer requires unique attention, the tie-breaking function resolves $B_n$Bn​ into a single position $\tau(B_n)$τ(Bn​). The attention vector at position $n$n is therefore

$$\mathbf{a}_n= \begin{cases} \mathbf{v}_{\tau(B_n)}, & \text{if } U_n\neq\emptyset,\\ \mathbf{0}, & \text{otherwise}. \end{cases}.$$an​={vτ(Bn​)​,0,​if Un​=∅,otherwise.​.

The UHA layer then outputs the sequence

$$C(\mathbf{v}_1,\mathbf{a}_1),\ldots,C(\mathbf{v}_N,\mathbf{a}_N).$$C(v1​,a1​),…,C(vN​,aN​).

This design differs from standard transformers by combining hard argmax attention, deterministic tie-breaking, and an explicit affine mixing of the current position with the selected attention vector. The mask controls which positions may participate, while the tie-breaker controls which winning position is chosen when several positions attain the maximum score.

The second lightweight module is a ReLU layer. The authors use a coordinate-specific rectified linear unit. For a designated coordinate $r\in[R]$r∈[R], the map $\rho_r:\mathbb{Q}^{R}\to\mathbb{Q}^{R}$ρr​:QR→QR is defined by

$$\rho_r(\mathbf{v})=(v_1,\ldots,v_{r-1},\max(0,v_r),v_{r+1},\ldots,v_R).$$ρr​(v)=(v1​,…,vr−1​,max(0,vr​),vr+1​,…,vR​).

Given a sequence $\mathbf{v}_1,\ldots,\mathbf{v}_N$v1​,…,vN​, the ReLU layer outputs $\rho_r(\mathbf{v}_1),\ldots,\rho_r(\mathbf{v}_N)$ρr​(v1​),…,ρr​(vN​) by applying this operation position-wise. This component supplies the nonlinearity needed for more complex Boolean and threshold-like behavior while keeping the architecture structurally simple. The authors note that one could equivalently place a small feedforward network at the end of each encoder layer.

The full UHAT is formed by composing the symbol embedding with a finite sequence of UHA and ReLU layers whose widths are compatible. The resulting model is a length-preserving function $\mathcal{T}:\Sigma^{+}\to(\mathbb{Q}^{S})^{+}$T:Σ+→(QS)+. To use it as a language recognizer, the authors equip the transformer with an acceptance vector $\mathbf{t}\in\mathbb{Q}^{S}$t∈QS. If $\mathcal{T}(\mathbf{a})=\mathbf{v}_1,\ldots,\mathbf{v}_N$T(a)=v1​,…,vN​, then the language recognized by $\mathcal{T}$T consists of all words satisfying

$$\langle \mathbf{t},\mathbf{v}_N\rangle>0.$$⟨t,vN​⟩>0.

因此，接受判定仅依赖于最终编码向量，使得识别过程成为一连串基于注意力的变换，随后仅进行一次线性阈值测试。

作者还使用了一种与 UHAT 堆栈密切相关的程序化抽象。该抽象表达类注意力的布尔谓词，其中每个操作通过掩码和打破平局规则选择位置，根据布尔条件筛选这些位置，并计算一个涉及被选中位置和当前位置的值谓词。这一程序层充当逻辑谓词与 Transformer 组件之间的桥梁。它使作者能够在把这些组件翻译成 UHA 和 ReLU 层之前，描述简洁的计算部件，例如计数器递增检查和邻接约束检查。

一个核心部件检查输入中编码的二进制计数器是否正确递增。词被构造为由特殊符号分隔的块，每个块包含一个二进制计数器和一个符号。程序使用一个注意力操作：对于一个分隔符位置，它选择最右侧的较早分隔符，然后验证两个分隔符之间的二进制词是否表示前一个二进制词的递增。这里的掩码和最右侧打破平局规则至关重要：它们使模型无需递归或显式记忆状态，就能回看紧邻的前一个计数器块。

另一个部件验证相邻非计数器符号之间的局部符号约束。对于给定符号位置，注意力从相关集合中选择最右侧的较早符号，并检查该符号对是否属于允许邻接集合。作者通过堆叠许多用计数器编码的词来扩展这一思想，从而形成网格状结构。水平约束检查同一行中相邻符号之间的一致性，垂直约束检查一个位置与携带相同计数器值的最近较早位置之间的一致性。在预期解释下，那个较早位置表示上一行中的同一列。使用严格未来掩码并配合最右侧打破平局，或使用其对偶形式严格过去掩码并配合最左侧打破平局，注意力机制能够在行间执行这些列间一致性检查。

该构造用于将简洁编码的铺砖问题归约到相应程序或 Transformer 的非空性。铺砖实例由编码瓦片行和列的词表示。所构造的程序接受输入当且仅当输入描述有效铺砖配置。由于计数器可以随其二进制长度呈指数增长，最短可接受词可以指数级庞大。通过添加更多编码行和列，作者得到了简洁识别器，其对应实例的最短见证可以呈双指数增长。这解释了为何尽管具有紧凑的类 Transformer 表示，诸如非空性之类的推理问题仍会在计算上变得昂贵。

从程序层到 UHAT 的翻译逐部件完成。逐位置谓词的布尔组合通过仿射层和 ReLU 层的序列进行模拟，其中注意力层可以计算其仿射映射 $C$C，同时实际上忽略所选注意力向量。每个程序化注意力操作被翻译为一个单独的 UHA 层，其掩码与程序化掩码匹配，其打破平局规则与程序化选择规则匹配。仿射映射 $A$A 和 $B$B 构造一个分数，该分数编码候选位置之间的相关比较。仿射映射 $C$C 复制或组合硬注意力操作选择的向量。随后，一个小型 ReLU 子网络在被复制的组件上计算值谓词。如果谓词仅依赖被选中位置，则一个预备层可以在注意力选择之前计算每个位置上的该值。如果谓词要求两个二进制数相等，则分数函数被设计为让注意力恰好选择那些编码二进制值一致的位置。这样便保留了掩码谓词和打破平局行为，使 UHAT 能够模拟该程序化构造。

在复杂度分析的上界部分，作者依赖一个精度论证。他们证明，UHAT 求值过程中出现的所有有理数值，相对于模型描述只需多项式数量的比特。因此，可能的中间向量集合是有限的，并且其大小相对于模型规模呈指数级，尽管每个单独向量的比特长度都是多项式的。这使得枚举相关值空间并逐层构建 Transformer 计算的时序逻辑表示成为可能。翻译需要编码注意力层的逐位置行为，包括哪些位置被掩码以及哪个位置被选择，而不是模拟任意实值算术。由于所得时序公式的非空性可用多项式空间检查，因此得到所需的指数空间上界。

在受限变体中，每个注意力层使用一个固定方向掩码和兼容的打破平局规则，此时翻译只使用一个时序方向。这些受限模型对应时序逻辑的更小片段，从而改善了那些受限情况的决策复杂度。作者还使用同样的表达能力和决策论框架来分析等价性，表明检查两个唯一硬注意力 Transformer 是否识别同一语言仍然在计算上难以处理。

实验

一种形式化简洁性比较通过构造见证语言并分析表示大小与翻译界限，将 UHAT 作为一种基于 Transformer 的表示，与 LTL、有限自动机和 RNN 进行比较。结果显示，在某些语言族上，UHAT 比 LTL 指数级更简洁；同时每个 LTL 公式都可以由多项式更大的 UHAT 表示，这表明存在多项式级别的普遍关系，而在见证上存在指数级差距。同一构造在有限自动机之上得到双指数级简洁性，在 RNN 之上得到指数级简洁性，从而支持如下结论：Transformer 风格表示能够比这些经典形式系统更紧凑地刻画某些语言。