Formally Verified Autoresearch for Analyzing the Expressivity of Multi-Head Attention
Organizations: Verified Mechanisms · MATS Research · University of California, Berkeley
Abstract
Multi-head attention is a central component of the transformer architecture, yet how its expressivity depends on the number of heads remains poorly understood. We study a one-layer, attention-only transformer with additive positional embeddings and define the head complexity of a Boolean function as the minimum number of attention heads required to represent it. We derive an exact linear-fractional normal form for head complexity, prove a general threshold-degree lower bound, and give an explicit ten-bit function for which this bound is strict. For symmetric Boolean functions, we independently show that head complexity equals the number of times the function changes value between consecutive Hamming-weight levels, even when positional embeddings are allowed. This agrees with the concurrent characterization of Hsu and Xu (arXiv:2608.04243) in a model without positional embeddings. The symmetric lower bound combines our general threshold-degree bound with the classical result of Aspnes et al. (1994). These results were discovered and formalized by a frontier model through conjecture generation, theorem proving, and machine verification, while human researchers asked the high-level questions and reviewed the generated theorems. We make the Lean formalization and research traces publicly available to support agent-assisted theorem proving and formal verification in mechanistic interpretability. This work provides a proof of concept for using the capabilities of frontier models, grounded by formal verification, to develop an understanding of transformer architectures.
Figures & tables
| Command category | Calls |
|---|---|
| Python invocations | 153 |
| sed inspections | 70 |
| rg searches | 40 |
| Runs of empirical checks | 24 |
| Numbered file inspections | 17 |
| Git queries | 14 |
| Measure | Summary |
|---|---|
| Messages | intermediate assistant messages and one final answer. The context was compacted four times. |
| Tool use | The log records 949 tool calls and 960 operations within those calls. The latter comprise 387 shell commands, 307 file edits, 205 continuations of shell sessions, 55 goal checks, and six goal or plan updates. |
| Token use | The platform reported about 142.4 million cumulative input tokens, of which 140.2 million were cached, and 0.64 million output tokens, including 0.32 million reasoning tokens. |
| Research process | The agent registered thirteen approach families and used no public web search, external connector, or delegated model call. |
| Goal | Approach | Outcome |
|---|---|---|
| Reformulate head complexity | Replace the full matrix parameterization with a scalar description of each head’s contribution. | Derived Theorem 1 . |
| Prove upper bounds | Construct representations for functions determined by weighted sums and for symmetric functions. | Derived Theorems 4 and 5 , plus bounds not included in the paper. |
| Prove lower bounds | Compare head complexity with threshold degree and study functions that require more heads. | Derived Theorem 2 and additional lower-bound arguments. |
| Evaluate candidate approaches | Check proposed identities and constructions on finite instances. | Rejected approaches that failed finite checks and set aside those that still required an unproved lemma. |
Transformer Expressivity
Transformer expressivity studies which functions and computations attention-based models can represent, and how depth, precision, and context shape those limits.
See all 53 papers