One-sentence Summary

Researchers at ETH Zürich prove that local attention in transformers introduces a second temporal operator beyond the single past operator characterizing global attention, strictly enlarging the class of recognizable regular languages, and show that hybrid global-local architectures are expressively complementary and empirically outperform global-only transformers on formal language recognition and natural language modeling.

Key Contributions

• The paper links fixed-precision transformers to fragments of linear temporal logic, showing that global attention corresponds to LTL[P] and that local attention adds a bounded past operator, strictly enlarging the class of recognizable regular languages.
• The analysis establishes precise expressivity relationships, including that k-local attention is maximally expressive at k=1, that k-local and global attention are incomparable, and that hybrid global and local attention corresponds to a strictly richer fragment, while modular predicates can close the expressive gap for larger k.
• Experiments on formal language recognition and WikiText-2 language modeling support the theory, showing that hybrid global and local transformers outperform global-only models and that the 1-local hybrid achieves the strongest language-modeling performance.

Introduction

Transformers rely on attention, and local attention restricts aggregation to a fixed window, making sequence modeling more efficient while unexpectedly improving language modeling and translation even under matched compute. Prior work characterized global attention as a limited fragment of linear temporal logic, but did not explain why local attention can increase expressivity. The authors connect attention patterns to logic fragments, showing that local attention adds a new past operator and that hybrid global local attention recognizes strictly more formal languages than global or local attention alone. They also show that purely local attention collapses expressivity to dependence on a fixed length suffix, while one token local windows give the strongest practical gains.

Dataset

• The dataset is a curated collection of formal languages used to evaluate temporal logic fragments. The authors select two representative languages from each definability class, using regular language definitions as the source. The excerpt does not report dataset size, string length, sampling distribution, or train and evaluation split.

• LTL[Y] subset: contains languages definable with future temporal operators. The authors include Σa, strings ending with a, and Σab, strings ending with ab. These capture suffix-based properties.

• LTL[P] subset: contains languages definable with past temporal operators. The authors include aΣ*, strings starting with a, and ΣaΣbΣ*, strings containing ab as a non-contiguous subsequence. These capture prefix and subsequence properties.

• LTL[P, Y] exclusive subset: contains languages definable with both past and future operators but not by LTL[P] or LTL[Y] alone. The authors include (ab), strings formed by repeated ab, and ΣabΣ*, strings containing ab as a contiguous substring. The filtering rule removes languages already expressible in either past-only or future-only fragments.

• LTL[S] exclusive subset: contains languages definable with the separation operator but not by LTL[P, Y]. The authors include {a,b,d}a{c,d}, a right-deterministic polynomial over a restricted alphabet, and (a(ab)b), a bounded Dyck language with maximum nesting depth 2. The filtering rule removes languages expressible in the past and future fragment.

• The paper uses the data as an evaluation suite for language membership and temporal logic definability. The models are evaluated on generated or selected strings from these languages. The provided text does not describe cropping, metadata construction, mixture ratios, or detailed preprocessing steps.

Method

The authors leverage a logical and automata-theoretic characterization to analyze transformer expressivity. The overall pipeline first restricts linear temporal logic to fragments generated by past operators, then formalizes a transformer as a fixed-precision language recognizer, and finally maps attention masks to those fragments. The analysis treats the transformer as a classifier over padded sequences. An input $\mathbf{w}=w_1\cdots w_N$w=w1​⋯wN​ is processed as $\overline{\mathbf{w}}=w_1\cdots w_N\mathrm{EOS}$w=w1​⋯wN​EOS, and the decision is read from the EOS position. This convention aligns transformer evaluation with temporal-logic evaluation just after the last token.

The logical side focuses on linear temporal logic fragments generated by the past operator $\mathbf{P}$P and the one-step past operator $\mathbf{Y}$Y. The operator $\mathbf{P}\psi$Pψ asks whether $\psi$ψ held at some earlier position, while $\mathbf{Y}\psi$Yψ asks whether $\psi$ψ held at the immediately preceding position. The combined fragment $\mathrm{LTL}[\mathbf{P},\mathbf{Y}]$LTL[P,Y] strictly contains both $\mathrm{LTL}[\mathbf{P}]$LTL[P] and $\mathrm{LTL}[\mathbf{Y}]$LTL[Y], because the two fragments are incomparable. To study bounded past access, the authors introduce $\mathbf{Y}^{\le k}$Y≤k and $\mathbf{Y}^{\ast}$Y∗:

The operator $\mathbf{Y}$Y is the special case $\mathbf{Y}^{\le 1}$Y≤1, and $\mathbf{Y}^{\ast}$Y∗ coincides with $\mathbf{P}$P. Thus, adding $\mathbf{Y}^{\ast}$Y∗ to $\mathrm{LTL}[\mathbf{P}]$LTL[P] does not increase expressive power, while adding the full one-step operator $\mathbf{Y}$Y does.

The characterization of $\mathrm{LTL}[\mathbf{P},\mathbf{Y}]$LTL[P,Y] also uses standard automata-theoretic objects. For a regular language $L\subseteq \Sigma^{\ast}$L⊆Σ∗, let $S$S be its syntactic semigroup and let $\mathcal{A}$A be its minimal DFA. The language $L$L is definable in $\mathrm{LTL}[\mathbf{P},\mathbf{Y}]$LTL[P,Y] exactly when $S$S satisfies a local triviality condition and $\mathcal{A}$A avoids a specific forbidden two-state pattern. This pattern contains two states $q$q and $q'$q′ that are connected by opposite transitions under symbols $u$u and $v$v, while each state also admits a self-loop under a symbol $x$x. Refer to the automata configuration below:

The transformer module is defined directly as a language recognizer. A $(D,L)$(D,L) transformer contains a token encoder $\mathbf{e}:\overline{\Sigma}\to \mathbb{F}^{D}$e:Σ→FD, a family of attention mechanisms $\{\mathbf{A}^{\ell}\}_{\ell=1}^{L}${Aℓ}ℓ=1L​, a family of column-wise nonlinear functions $\{\mathbf{F}^{\ell}\}_{\ell=1}^{L}${Fℓ}ℓ=1L​, and a classification function $c:\mathbb{F}^{D}\to \{0,1\}$c:FD→{0,1}. Given $\overline{\mathbf{w}}=w_1\cdots w_N\mathrm{EOS}$w=w1​⋯wN​EOS, the initial hidden matrix is initialized as

For each layer $\ell=1,\ldots,L$ℓ=1,…,L, the model computes

where $\mathrm{LN}$LN denotes layer normalization. The final decision is read from the EOS column:

The attention mechanism is where the relevant structural constraints enter. For a hidden matrix $\mathbf{H}\in \mathbb{F}^{D\times (N+1)}$H∈FD×(N+1), query, key, and value matrices are produced by learned linear maps

The raw score for position pair $(n,m)$(n,m) is

and the masked softmax weights are

The attention output is then

The binary mask $\mathbf{M}$M determines which past positions are visible. A global mask allows access to all earlier tokens:

A $k$k-local mask allows access only to the previous $k$k positions:

Multi-head attention combines several such masked heads by learned linear projections:

Different heads may use different masks, so an architecture can mix global and local access in the same block.

A crucial assumption is fixed precision. All parameters, activations, and primitive operations such as multiplication, exponentiation, and softmax normalization are assumed to lie in a finite representable set $\mathbb{F}$F. Results are rounded back into $\mathbb{F}$F, which makes addition and softmax-sensitive summation order technically relevant. This assumption is central because it keeps the transformer’s arithmetic behavior finite-state in character and makes the connection to automata and temporal logic possible.

The mask-to-logic correspondence is the core architectural result of the analysis. If every attention head uses the global mask $\mathbf{M}^{\ast}$M∗, the transformer EOS-recognizes exactly the languages definable in $\mathrm{LTL}[\mathbf{P}]$LTL[P]. If every head uses the $k$k-local mask $\mathbf{M}^{\le k}$M≤k, the recognizable languages are exactly those definable in $\mathrm{LTL}[\mathbf{Y}^{\le k}]$LTL[Y≤k]. If some heads use $\mathbf{M}^{\ast}$M∗ and others use $\mathbf{M}^{\le k}$M≤k, the hybrid architecture EOS-recognizes exactly the languages definable in $\mathrm{LTL}[\mathbf{P},\mathbf{Y}^{\le k}]$LTL[P,Y≤k]. Thus, mixing global and local attention yields a strict expressive gain over either pure global attention or pure $k$k-local attention.

The analysis also distinguishes the logical role of different window sizes. The one-step local mask directly mirrors $\mathbf{Y}$Y, while larger bounded windows are analyzed through $\mathbf{Y}^{\le k}$Y≤k. Expressing a bounded $k$k-window lookback using repeated one-step access can preserve expressive power only by increasing depth, since a bounded disjunction over positions $1,\ldots,k$1,…,k may require several stacked single-step operations. Positional information can change this picture. Modular predicates such as

allow the logic to refer to position modulo $m$m. If transformer positional encodings provide comparable position-dependent information, a $k$k-local head can identify the immediate predecessor inside a $k$k-window, which affects the expressive separation between different local masking schemes.

Experiment

The experiments evaluate transformer variants with local-only, hybrid, and global-only attention on formal languages selected from temporal-logic definability classes and on next-token modeling over WikiText-2. Without positional encodings, the results closely validate the theory: local attention recognizes the corresponding future-oriented languages, global attention recognizes the corresponding past-oriented languages, and hybrid attention recognizes their union, with very small local windows performing strongest. Positional encodings produce mixed effects and do not remove the advantage of hybrid attention, while the natural-language experiment similarly shows that hybrid attention, especially with minimal local windows, provides the best overall performance. Overall, local and global attention are complementary, and hybrid designs combine their strengths.