Local Attention as a Temporal Logic Operator: Why Windowed Transformers See More

Paper: 2605.00768 Authors: Jiaoda Li, Ryan Cotterell Categories: cs.CL

The Gap

Transformers with global attention can look at all previous tokens, yet adding local attention (restricting to a fixed window) empirically improves performance. This contradicts intuition: why does seeing less help you see better? Prior work showed global attention corresponds to a fragment of linear temporal logic (LTL) with one past operator, but couldn’t explain local attention’s advantage. The gap: no formal account of what expressive power local attention adds.

Empirical observation:
  Global attention (see everything) < Hybrid (global + local windows)
                                        ^
                                        |
                                   Why does restriction
                                   increase capability?
                                        |
                                        v
Prior theory:                    This paper:
  Global attention                 Local attention
       |                                |
       v                                v
  One LTL operator              Second LTL operator
  (unbounded past)               (bounded past)
       |                                |
       +---------> Combined = Richer fragment
                   (neither subsumes other)

The Increment

One sentence: Before, we knew transformers could express some temporal logic; now we know local attention adds a complementary temporal operator that strictly enlarges the recognizable language class.

Core Mechanism

The paper maps attention mechanisms to temporal logic operators. Global attention implements an “eventually in the past” operator (◇⁻) that checks if some property held anywhere before. Local attention implements a “within-k-steps-past” operator (◇⁻ₖ) that checks bounded history. These operators are expressively incomparable: neither can simulate the other.

A fixed-precision transformer processes sequences by maintaining a finite state and using attention to query history. Global attention can detect “did X ever happen?” but cannot distinguish “X happened 2 steps ago” from “X happened 100 steps ago” without consuming exponential states. Local attention can count within windows but cannot check arbitrarily distant history.

Token sequence:  t1 -> t2 -> t3 -> t4 -> t5 -> t6
                                          ^
                                       current
Global attention:
  [t1  t2  t3  t4  t5] <--- unbounded backward scan
   |   |   |   |   |
   +---+---+---+---+-----> "Did property P ever hold?"
                           (LTL operator: <>- P)

Local attention (window=3):
  [        t4  t5] <--- bounded window
           |   |
           +---+---------> "Did P hold in last 3 steps?"
                           (LTL operator: <>-_k P)

Hybrid:
  Global: "Was there ever an 'a'?"
  Local:  "Was the last token 'b'?"
  Combined: Recognize \{a^n b | n >= 1\} 
            (neither alone can do this efficiently)

Think of it like two types of memory access. Global attention is like having a search function over your entire email history—you can find if something ever happened, but you can’t efficiently answer “what were the last 3 emails?” without reading everything. Local attention is like a cache of recent items—you know exactly what just happened, but you’ve forgotten older events. The search function can’t replace the cache (too slow for recency queries), and the cache can’t replace search (limited horizon). You need both.

Key Concepts

• Linear Temporal Logic (LTL) fragment: A formal language for expressing properties about sequences over time. Instead of saying “the sequence contains an ‘a’,” you say “eventually in the past, property ‘a’ held.” The “fragment” means we’re using only a subset of LTL operators. This matters because it lets us prove what patterns a model can and cannot recognize—it’s the difference between “seems to work” and “provably can/cannot express X.”

• Recognizer expressivity: The set of formal languages (patterns) a model can distinguish with finite precision. A model “recognizes” a language if it can correctly classify any sequence as in or out of that language. For example, recognizing {aⁿbⁿ | n ≥ 1} (equal a’s and b’s) requires counting, which needs unbounded memory. Recognizing {aⁿb | n ≥ 1} (any a’s followed by one b) only needs to remember “saw a” and “saw b after a.” Expressivity hierarchies tell us which architectures can handle which patterns.

• Complementary operators: Two operators are complementary if neither can simulate the other, but combining them increases power. Here, global attention’s ◇⁻ (unbounded past) cannot efficiently implement local attention’s ◇⁻ₖ (bounded past) without exponential state blowup, and vice versa. It’s like addition and multiplication: you can’t build multiplication from just addition (without exponential repetition), and you can’t build addition from just multiplication. You need both primitives.

Framework Shift

Before (global-only):                After (hybrid global+local):

Attention = one backward scan        Attention = two query types
                                     
    [====================]               [=======] [===]
     unbounded history                    global   local
           |                                  |      |
           v                                  v      v
    One temporal operator                Two complementary
    (eventually-past)                    operators
           |                                  |
           v                                  +------+
    Language class L1                               |
                                                     v
                                            Strictly larger
                                            language class L2
                                            (L1 is proper subset)

One sentence: From a single unbounded query mechanism to dual complementary mechanisms—one for distant search, one for recent context—that together recognize a provably richer class of patterns.

Expert Assessment

Problem choice: Real gap. The empirical observation (local attention helps) has been known for years but lacked theoretical grounding. Connecting it to formal language theory is the right move—it transforms a mysterious trick into a principled design choice. This sits at the intersection of practical architecture design and theoretical foundations, which is where the field needs more work.

Method maturity: Elegant. The proof technique (mapping attention to LTL operators) is not brute force—it’s a conceptual bridge that makes the result almost obvious in hindsight. The complementarity proof is tight: they show explicit languages that each mechanism can recognize but the other cannot. No simpler approach is being overlooked; this is the natural formalism for the question.

Experimental integrity: Baselines are fair. They test on both formal languages (where theory predicts outcomes) and natural language (where theory should correlate with practice). The formal language experiments directly validate the theory. The natural language results are more modest (small but consistent gains), which is honest—they don’t oversell. One weakness: experiments are on relatively small models. Scaling behavior is unknown.

Writing quality: Section 3 (the formal proof) is dense and could use more intuition-building before diving into notation. The paper front-loads formalism, which will lose practitioners. Rewriting Section 2 to lead with the “two types of memory” intuition before introducing LTL would make the paper accessible to a wider audience. The experimental section is clear.

Verdict: strong accept — Provides the first formal explanation for a widely observed phenomenon, with clean theory and supporting experiments.

Takeaways

For architecture designers: Don’t treat local attention as just an efficiency hack. It’s a complementary operator. If your task requires both long-range dependencies (global) and precise recent context (local), hybrid attention isn’t a compromise—it’s strictly more expressive. Design your window sizes based on the temporal scales your task needs.

For theorists: The LTL-to-attention mapping is a transferable technique. You can use this framework to analyze other architectural variants (sparse attention, sliding windows, hierarchical attention) by asking what temporal operators they implement.

For practitioners debugging models: If your global-attention model fails on tasks requiring precise recency (e.g., “repeat the last 3 tokens”), adding local attention isn’t just faster—it’s giving the model a capability it didn’t have. Conversely, if local-only models fail on long-range tasks, it’s not a tuning problem; it’s a fundamental expressivity limit.

Concrete steal: When designing attention patterns, ask “what temporal queries does my task need?” Map them to operators (unbounded past, bounded past, future, counting). Then pick attention mechanisms that provide those operators. This paper gives you the mapping for global and local; extend it to your custom patterns.