Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers
Andy Yang, David Chiang
TL;DR
The paper develops a formal framework to bound and understand the expressivity of future-masked soft attention transformers by introducing the temporal counting logic $K_{\text{t}}[\#]$ and a RASP variant $\textsf{C-RASP}$, proving their equivalence. It demonstrates that any $K_{\text{t}}[\#]$ formula can be compiled into a standard, future-masked SMAT encoder, establishing a tight lower bound on SMAT expressivity for unbounded input length. It also shows that $K_{\text{t}}[\#]$ subsumes prior lower bounds like $FOC[+;\textsf{MOD}]$ and that fixed-precision transformers can be simulated within this logic, bridging theory with practical transformer implementations. The work provides constructive methods for counting and arithmetic through masked uniform attention and FFNs, enabling interpretable compilation of known algorithms into SMATs and offering a foundation for comparing the expressive power of hard vs soft attention models. Overall, it paves the way for deeper theoretical analysis and practical exploration of transformer capabilities through a precise logical lens.
Abstract
Deriving formal bounds on the expressivity of transformers, as well as studying transformers that are constructed to implement known algorithms, are both effective methods for better understanding the computational power of transformers. Towards both ends, we introduce the temporal counting logic $\textsf{K}_\text{t}$[#] alongside the RASP variant $\textsf{C-RASP}$. We show they are equivalent to each other, and that together they are the best-known lower bound on the formal expressivity of future-masked soft attention transformers with unbounded input size. We prove this by showing all $\textsf{K}_\text{t}$[#] formulas can be compiled into these transformers.