Research map / Architectures and efficiency / Attention and transformers
Logical Languages Accepted by Transformer Encoders with Hard Attention
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Shows that unique hard attention transformer encoders (UHAT) recognize all FO(Mon) languages (hence regular AC0 languages) but not all AC0 languages, and that average hard attention transformers (AHAT) recognize LTL(C,+) languages including majority and parity.
Problem
Which formal languages can transformer encoders with hard attention recognize, relative to circuit complexity classes AC0 and TC0 and logical characterizations?
Approach
Proves UHAT encoders accept all languages definable in FO with arbitrary unary numerical predicates by routing through Kamp's theorem and LTL(Mon) with position-wise induction; extends AHAT to LTL with counting terms and linear inequalities, which captures majority, parity, and permutation closures.
Key results
- There is an AC0 language (approximate majority) that no UHAT can accept, and a polynomial-time computable such language.
- Every FO(Mon) sentence, hence every regular language in AC0, is accepted by a UHAT.
- Every LTL(C,+) formula, including majority and parity, is accepted by an AHAT; permutation closures of regular languages and all permutation-closed binary languages are AHAT-recognizable.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use UHAT to recognize languages definable in FO(Mon) | UHAT · FO(Mon)-definable languages | language recognition | Helped |
| Use UHAT to recognize approximate majority | UHAT · Approximate majority | language recognition | Hurt |
| Replace unique hard attention with average hard attention | Transformer encoder · LTL(C,+)-definable languages | recognition capability | Helped |
| Use UHAT to recognize regular languages in AC^0 | UHAT · Regular languages in AC^0 | language recognition | Helped |
| Use AHAT to recognize permutation closures of regular languages | AHAT · Permutation closure of regular languages | language recognition | Helped |
| Use AHAT to recognize permutation-closed languages over a binary alphabet | AHAT · Permutation-closed languages over a binary alphabet | language recognition | Helped |
| Use AHAT to recognize parity | AHAT · Parity | language recognition | Helped |
Surprising findings
- Parity is accepted by an AHAT, a result the paper states is new.
Limitations
- Open whether UHATs accept languages not definable in FO(Mon).
- Open whether some TC0 language is not recognizable by AHATs.
- Open whether AHAT languages are exactly those definable in LTL(C,+).
Experimental setup
Builds on: Kamp's theorem Parikh's theorem average hard attention transformers
Closest papers by meaning
- Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages (NeurIPS 2024 · similarity 0.91)
- The Power of Hard Attention Transformers on Data Sequences: A formal language theoretic perspective (NeurIPS 2024 · similarity 0.90)
- Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning (ICLR 2025 · similarity 0.87)
- Chain of Thought Empowers Transformers to Solve Inherently Serial Problems (ICLR 2024 · similarity 0.87)
- Characterizing the Expressivity of Fixed-Precision Transformer Language Models (NeurIPS 2025 · similarity 0.87)
- Rethinking Circuit Completeness in Language Models: AND, OR, and ADDER Gates (NeurIPS 2025 · similarity 0.87)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.