A single attention head can linearly realize
We make that precise, prove what we can, and measure the rest empirically.
Fix a single-layer, attention-only transformer:
The central problem: understand
The precise model (embeddings, softmax head, residual readout, masking convention) is in
model.md; the formal problem statement and the list of core questions is in
problem_statement.md.
The results below are written up in full under theorems/ and indexed, with the
dependency order between them, in theorems.md.
Lower bounds (a function needs many heads).
-
Checkerboard obstruction. If
$f$ has a 2-bit "checkerboard" restriction (one diagonal of some 2-cube slice disagrees with the other, the way$\mathrm{XOR}$ does), then$H^{\ast}(f) \geq 2$ . One head can never separate the two diagonals. -
Threshold-degree bound. Head complexity dominates threshold degree:
$\deg_{\pm}(f) \leq H^{\ast}(f)$ .
Upper bounds (a function needs few heads).
-
Symmetric thresholds need one head. Every
$T_{n,t}(x) = \mathbf{1}[|x| \geq t]$ is computable with a single head, so$H^{\ast}(\mathrm{AND}_n) = H^{\ast}(\mathrm{OR}_n) = H^{\ast}(\mathrm{MAJORITY}_n) = 1$ . -
Weighted-sum interpolation. If
$f(x) = F\left(\sum_i \lambda_i x_i\right)$ for positive weights$\lambda_i$ and the weighted sum takes$M$ distinct values, then$H^{\ast}(f) \leq M - 1$ . Consequently every symmetric function needs at most$n$ heads and every Boolean function at most$2^n - 1$ .
Exact answers.
-
Parity is the extremal case.
$H^{\ast}(\mathrm{XOR}_n) = n$ : in this model, parity needs exactly one head per input bit. The lower bound comes from$\deg _{\pm}(\mathrm{PARITY}_n) = n$ , the upper bound from an explicit$n$ -head construction. - A first split inside the symmetric functions: monotone thresholds have complexity
$1$ , while parity and the internal exact-count predicates$\mathrm{EXACT}_{n,k}$ need at least$2$ .
Strict separation.
-
Theorem 13
gives an explicit ten-bit function
$f_{10}$ with$\deg_{\pm}(f_{10})=2 \lt 3\leq H^{\ast}(f_{10})$ . Thus threshold degree is a genuine lower bound, not an exact characterization of head complexity.
Taken together this is a partial characterization, not yet a single invariant
- Determine the exact value of
$H^{\ast}(f_{10})$ , and find scalable families with a growing gap between threshold degree and head complexity. - Tighten the gap between the threshold-degree lower bound and the weighted-sum upper bound.
- Push the formalization in
formalization/to cover more of the theorem stack. - Extend the empirical search to larger
$n$ and reconcile it with the proofs.
| Path | What it is |
|---|---|
problem_statement.md |
The question and the core open problems. |
model.md |
The precise attention model and the definition of |
theorems.md |
Ledger of the main theorems, their status, and how they fit together. |
theorems/ |
Full writeups: initial results, normal forms, and explicit separations. |
artifacts/intro-materials/writeup.md |
Original blog-post writeup of the two-bit XOR result. |
literature_survey.md |
Related work across transformers and Boolean complexity. |
formalization/ |
Lean 4 formalization of the results (depends on mathlib). |
system-design/ |
Independent from-scratch autonomous re-derivation of the head-complexity answer (answer.md, approach registry, self-tests, and its own Lean check), the evidence base for the system-design part of the paper. |
experiments/hstar/ |
Python package that empirically estimates |
artifacts/intro-materials/proposal.pdf / proposal.tex
|
Project proposal (build with ./artifacts/scripts/compile_pdf.sh). |
AGENTS.md |
Markdown conventions used across the writeups. |
New here? Read problem_statement.md, then skim
theorems.md. The individual files under theorems/ are self-contained.
Lean proofs. Needs Lean 4 / elan.
bash artifacts/scripts/validate.sh --fetch-cachePython search. Needs Python with PyTorch. The package
enumerates symmetry-class representatives of
# Estimate H*(f) over all 3-bit representatives, trying up to 3 heads.
PYTHONPATH=experiments python -m hstar.cli --n 3 --max-heads 3Useful flags: --limit / --start-index / --end-index to slice the representative
list, --robust for a stronger second-pass search, --device {cpu,cuda,mps}, and
--output result.json to save the payload. Run with --help for the full list.
Proposal PDF.
./artifacts/scripts/compile_pdf.sh # runs pdflatex on proposal.tex and cleans up aux files