One-sentence Summary

Researchers at RPTU Kaiserslautern-Landau, ETH Zurich, and MPI-SWS prove that fixed-precision transformers are exponentially more succinct than linear temporal logic and recurrent neural networks, doubly exponentially more succinct than finite automata, and with matching upper bounds that improve prior doubly exponential translations, they further show that verification problems such as emptiness and equivalence are $$\text{EXPSPACE}$-complete$−complete.

Key Contributions

• 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.

Introduction

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.

Method

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

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

The authors then define the argmax set

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

The UHA layer then outputs the sequence

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

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

Thus the acceptance decision depends only on the final encoded vector, making the recognition procedure a sequence of attention-based transformations followed by a single linear threshold test.

The authors also use a programmatic abstraction closely related to the UHAT stack. This abstraction expresses attention-like Boolean predicates, where each operation selects positions through a mask and tie-breaker, filters them by Boolean conditions, and evaluates a value predicate involving the selected position and the current position. This program layer acts as a bridge between logical predicates and transformer components. It allows the authors to describe succinct computational gadgets, such as counter increment checks and adjacency-constraint checks, before translating them into UHA and ReLU layers.

One central gadget checks that a binary counter encoded in the input increments correctly. Words are constructed as blocks separated by a special symbol, each block containing a binary counter followed by a symbol. The program uses an attention operation that, for a separator position, selects the rightmost earlier separator and then verifies that the binary word between the two separators represents an increment of the previous binary word. The mask and rightmost tie-breaking rule are essential here: they allow the model to look backward to the immediately preceding counter block without needing recurrence or an explicit memory state.

Another gadget verifies local symbol constraints between neighboring non-counter symbols. For a given symbol position, attention selects the rightmost earlier symbol from the relevant set and checks whether the pair belongs to a permitted adjacency set. The authors extend this idea by stacking many counter-encoded words to form a grid-like structure. Horizontal constraints check consistency between adjacent symbols in the same row, while vertical constraints check consistency between a position and the most recent earlier position carrying the same counter value. In the intended interpretation, that earlier position represents the same column in the previous row. Strict future masking with rightmost tie-breaking, or the dual strict past masking with leftmost tie-breaking, lets the attention mechanism perform these column-to-column consistency checks across rows.

This construction is used to reduce a succinctly encoded tiling problem to non-emptiness of the corresponding program or transformer. The tiling instance is represented by words that encode rows and columns of tiles. The constructed program accepts an input if and only if the input describes a valid tiling configuration. Because the counter can grow exponentially with its bit length, the shortest accepted word can be exponentially large. By adding additional encoded rows and columns, the authors obtain succinct recognizers for instances whose shortest witnesses can grow doubly exponentially. This explains why reasoning problems such as non-emptiness become computationally expensive despite the compact transformer-like representation.

The translation from the programmatic layer to a UHAT is handled component by component. Boolean combinations of position-wise predicates are simulated by sequences of affine and ReLU layers, where an attention layer may compute its affine map $C$C while effectively ignoring the selected attention vector. Each programmatic attention operation is translated into a single UHA layer whose mask matches the programmatic mask and whose tie-breaker matches the programmatic selection rule. The affine maps $A$A and $B$B construct a score that encodes the relevant comparison among candidate positions. The affine map $C$C copies or combines the vector chosen by the hard attention operation. A small ReLU subnetwork then evaluates the value predicate on the copied components. If the predicate depends only on the selected position, a preliminary layer can compute that value at every position before the attention selection. If the predicate requires equality between two binary numbers, the score function is designed so that attention selects exactly those positions where the encoded binary values agree. This preserves the mask predicate and tie-breaking behavior, allowing the UHAT to emulate the programmatic construction.

For the upper-bound side of the complexity analysis, the authors rely on a precision argument. They show that all rational values that arise during evaluation of a UHAT require only polynomially many bits relative to the model description. Consequently, the set of possible intermediate vectors is finite and has size exponential in the model size, although each individual vector has polynomial bit length. This makes it possible to enumerate the relevant value space and build a temporal-logic representation of the transformer computation layer by layer. The translation needs to encode the position-wise behavior of attention layers, including which positions are masked and which position is selected, rather than simulating arbitrary real-valued arithmetic. Since non-emptiness for the resulting temporal formulas can be checked using polynomial space, this yields the desired exponential-space upper bound.

In restricted variants where each attention layer uses one fixed directional mask and the compatible tie-breaking rule, the translation uses only one temporal direction. These restricted models correspond to smaller fragments of the temporal logic, which improves the decision complexity for those restricted cases. The authors also use the same expressive and decision-theoretic framework to analyze equivalence, showing that checking whether two unique hard-attention transformers recognize the same language remains computationally intractable.

Experiment

A formal succinctness comparison evaluates UHATs as a transformer based representation against LTL, finite automata, and RNNs by constructing witness languages and analyzing representation size and translation bounds. UHATs are shown to be exponentially more succinct than LTL on certain language families, while every LTL formula can be represented by a polynomially larger UHAT, indicating a polynomial universal relationship with an exponential gap on witnesses. The same construction yields doubly exponential succinctness over finite automata and exponential succinctness over RNNs, supporting the conclusion that transformer style representations can capture some languages far more compactly than these classical formalisms.