The Power of Hard Attention Transformers on Data Sequences: A Formal Language Theoretic Perspective

Summary

This paper focuses on analyzing the expressive power of transformers through the lens of formal languages, inspired by Angluin's approach. Specifically, while traditional unique hard attention transformers (UHAT) on strings are associated with $AC^0$ and regular languages definable in first-order logic, the authors here explore the implications of using data sequences instead of words as input. The main findings are: - UHATs over data sequences with positional encodings fall within $TC^0$, not $AC^0$. - Non-regular languages can be recognized even by masked UHATs without positional encodings. - UHATs can recognize all languages definable in $(LT^2)L$, an extension of LTL with unary predicates and local arithmetic tests over finite windows over the data.

Strengths

**S1: Important Contribution** Understanding the expressive power of significant classes of transformers is crucial, given their widespread popularity. Moreover, considering data sequences is a natural and worthwhile extension. The results obtained are both elegant and insightful. **S2: Clarity** For readers familiar with the topic, this is a well-written paper. The authors effectively set the stage and explain most concepts and proof ideas in sufficient detail within the main text. **S3: Elegant Proofs** The results linking UHAT with $TC^0$ involve a well-crafted stepwise reduction using polynomial equations and polyhedral analysis.

Weaknesses

**W1: Coverage of $TC^0$** While the characterization of UHAT on data sequences in $TC^0$ is commendable, it does not fully encompass $TC^0$. A precise characterization of the power of UHATs would strengthen the paper. This observation also applies to the other main results: Which logic precisely captures UHAT? **W2: Accessibility** The authors make little effort to make the paper accessible to the broader ML community. As it stands, the paper could have been submitted to any computer science theory conference. Consequently, the results may not be surprising to those communities. **W3: Practical Implications** The paper lacks discussion on the practical implications of the theoretical analysis for transformer design. Coupling the theory with practical insights would enhance the paper's value. In summary, the paper provides significant insights into the expressive power of transformers over data sequences, presenting elegant and theoretically sound results. However, a broader characterization of UHATs' power, increased accessibility for a wider audience, and practical implications would strengthen the paper further.

Questions

Please comment on **W1** and **W3**.

Rating

6

Confidence

4

Soundness

3

Presentation

3

Contribution

2

Limitations

This has been addressed in a satisfactory way by the authors.

Summary

The paper studies the computational expressiveness of unique hard attention transformers (UHAT) on formal languages formed over an infinite alphabet. The work is motivated by the application of transformers to time series forecasting where input values can be unbounded. Specifically, the authors assume the language to be formed over tuples of rational numbers. To this end, the paper contributes three novel results: (1) The languages recognized by UHAT belong to the circuit complexity class $\mathsf{TC}^0$ and there exists a language recognized by UHAT which is $\mathsf{TC}^0$-hard. (2) There exists a non-regular language over the alphabet $\mathbb{Q}^d$ that is recognized by a UHAT with past masking and no positional encoding. (3) UHAT with positional encoding recognize all languages expressible in an extension linear-time temporal logic with unary numerical predicates and linear rational arithmetic.

Strengths

- To the best of my knowledge, the paper is the first to connect the formal language theory over infinite alphabets with the computation expressiveness of transformers. For unique hard attention transformers, a comprehensive set of results is established. - The paper's results are particularly interesting in the light of existing results for finite alphabets. For finite alphabets, the languages accepted by UHAT are contained in $\mathsf{AC}^0$ and are exactly the star-free regular languages when masking is applied. Therefore the results provide insights into the increase in computational expressiveness due to an infinite alphabet. - The paper’s technical claims are well presented. For each claim, either a full proof or a proof sketch with references to a full proof in the appendix is provided. - Although the paper is densely written the contributions are clear and the paper is easy to navigate.

Weaknesses

- There seems to be an important restriction to the first result: because real precision is assumed for UHAT, language inclusion can only be shown for words up to a particular length n. I assume that without this restriction the two classes are actually incomparable. At the same time, the authors seem to suggest in the concluding remarks that some results still hold when assuming rational precision for UHAT. The importance and implications of this choice should be discussed more clearly in the paper. - The paper does not clearly convey the practical implications of the results. The infinite precision of rational numbers can not be represented in real-world systems. Instead, they would be approximated by floating point numbers such that the result of previous work applies. - Minor: It would be helpful if the abstract already states that arbitrary input refers to the rational numbers, to avoid confusion with a real-valued input.

Questions

Do the same results hold for formal languages over the alphabet $\mathbb{Q}$? If yes, why are the results derived in terms of tuples?

Rating

6

Confidence

3

Soundness

4

Presentation

3

Contribution

3

Limitations

The authors have addressed limitations adequately, except for the real precision of UHAT. As detailed in the review it seems that some results only hold for inputs up to a particular length n. The theorems themselves do not state this.

Summary

This paper studies the expressive power of transformer encoders with leftmost-hard attention and strict past-masking, where the input is not a sequence of symbols from a finite alphabet, but a sequence of rational vectors. The three main results are: 1. Transformers (under the assumptions above, with or without position encodings) are in TC0 but not in AC0. 2. There is a UHAT that recognizes a non-regular language (that is, cannot be accepted by a finite automaton whose transitions are labeled with arithmetic constraints instead of symbols). 3. Every language definable in locally testable linear temporal logic (that is, linear temporal logic where an atomic formula can check a linear constraint on the current “symbol” and k lookahead “symbols”) is recognizable by a UHAT with position encoding.

Strengths

Theorem 1: This proof (because the transformer weights are real) looks ambitious and interesting, although I was not able to check the details. Theorem 2: This proof looks correct. Theorem 3: Although I didn’t check every line of this proof, I definitely agree that the result is correct.

Weaknesses

Theorem 1: I didn’t exactly understand why the inputs are rational vectors but the parameters are allowed to be real. Appendix A shows why allowing reals makes a difference, but: (a) It doesn’t explain why the difference is important. (b) It doesn’t show that language (2) requires real parameters, only that a particular UHAT requires real parameters to recognize language (2). (c) One could make exactly the same argument about UHATs for strings over a finite alphabet. With rational weights, I take it Proposition 9 would be fairly easy. How do you define Boolean circuits that take sequences of rational vectors as input? This is hinted at in line 273 but should be spelled out more explicitly for Proposition 10 and its proof to be clear. Theorem 2: I think it would be helpful not to reuse variable names. Theorem 3: Just a minor comment on the phrase “logical language” in the title of Section 5. I understand a “logical language” to be the syntax of a logic, not the set of strings models of a logical sentence, so I find this phrase confusing.

Questions

Could you explain why it's important for the parameters to be real, not just rational? How do you define Boolean circuits that take sequences of rational vectors as input? Could you expand on the significance, in this setting, of the classes AC0, regular, and TC0? Perhaps it would be helpful to give some examples of languages that do/don’t belong to these classes and expand on the practical implications. You allude to the language at lines 321-324 being important, but don’t explain why.

Rating

6

Confidence

4

Soundness

4

Presentation

3

Contribution

3

Limitations

Yes

Rebuttal Read

I have read the rebuttal. Thank you for your responses. There are indeed interesting open questions here related to the logic. The "application" related comment serves as a good additional motivation and should preferably be added to the paper.