Counting Like Transformers: Compiling Temporal Counting Logic Into Softmax Transformers

Summary

This paper extends the original RASP language to a variant called C-RASP to express temporal counting logic $\textbf{K}_t$[#] and compile them to future-masked soft attention transformers with unbounded input sizes. They show that any constant precision softmax decoder Transformer can be expressed via the C-RASP language. Further, they show how to use $\textbf{C-RASP}$ to construct language models that via greedy decoding generate sentences that have properties specified in $\textbf{K}_t$[#].

Rating

8

Confidence

4

Ethics flag

1

Reasons to accept

1. The paper makes a solid contribution to the softmax decoder Transformer's lower bound of expressivity. In particular, counting logic is required for a variety of tasks. RASP is known for its inability for seemingly simple addition, and the problem is addressed in this paper. 2. The paper is clear, with abundant examples. The proof in the appendix is also well organized.

Reasons to reject

1. The paper may require some rewriting to be understood by a broader audience. Currently, the reader may need a familiarity with representation theory and RASP language.

Questions to authors

1. The paper mentions that any constant precision softmax decoder Transformer can be expressed via the C-RASP language. In the proof that compiles the C-RASP language, the transformer constructed has uniform attention. Does this mean it is possible to compile a general Transformer to a larger uniform attention Transformer with more precision? If such is the case, how large would the larger Transformer be if one would translate a 4-bit GPT-2 Transformer with 124M parameters as an example?

Summary

This paper proposes to use Kt[#], a temporal counting logic, as a formalism for characterizing soft attention transformers. The paper also introduces C-RASP, a variant of RASP corresponding to Kt[#]. The paper proves that Kt[#] formulas can be compiled into transformers, fixed-precision transformers can be compiled into Kt[#], and it offers a tighter lower bound on expressiveness compared to the best prior result (that used a counting logic).

Rating

7

Confidence

3

Ethics flag

1

Reasons to accept

- This paper is written very clearly for the most part, and I enjoyed reading it. - I think Kt[#] could be a useful logic for thinking about softmax transformers. Kt[#] brings together several ideas from prior work: counting logics (used by Chiang et al., 2023; Merrill and Sabharwal, 2023) and temporal logics (used by Angluin et al., 2023; Barcelo ́ et al., 2024), and authors also connect it to RASP (Weiss et al., 2021). I find this to be a nice and intuitive formalism for thinking about transformers: temporal logics are a natural way of thinking about operations on strings, and incorporating counting makes them more expressive and better aligned with soft attention/hard averaging attention transformers. - I also appreciate that the paper provides explicit feed-forward constructions for the unary predicates in the logic. Compared to RASP/Tracr, this means all expressions can be compiled into a standard transformer, and it also makes it possible to give upper bounds on the number of layers. - The paper gives a tighter lower bound for soft attention transformers. Overall, despite some reservations (see below), I think the paper is clearly written and introduces an interesting and potentially useful set of tools, and I would recommend accepting it.

Reasons to reject

- It's not entirely clear to me how much these results reveal about soft attention transformers in particular, as apposed to averaging hard attention transformers (AHATs). It seems that the translation from Kt[#] to transformers (section 5.3/appendix B.2) exclusively uses uniform attention. (So Kt[#] is not necessarily so useful as a language for thinking about soft attention transformers---for example, constructing transformers with soft but non-uniform attention patterns.) It does seem notable that that softmax transformers can be decompiled into Kt[#] expressions (but this is also true of FO[+]). I think it would be helpful to include some discussion about why Kt[#] is specifically useful for softmax transformers and not just AHATs. - The paper states that it derives a "much better lower-bound result," but I find it a little difficult to understand how much better it is. From what I understand, the main lower-bound result is that Kt[#] can define Dyck-1, but FO[+;MOD] cannot. It would be nice if there was a more general characterization of the lower-bound, or at least a more detailed discussion of how exactly this compares to expressivity results from prior work. - The paper might benefit from some more discussion of other formalisms in section 6, like first-order logic with majority quantifiers (Merrill and Sabharwal, 2023). In particular, Angluin et al. (2023) also introduce a RASP variant (Boolean RASP) for unique hard attention transformers, and prove that it recognizes exactly the star-free languages. I think it would be worthwhile to discuss the relationship between these results at greater length. To summarize, my main concerns are related to how the contributions are framed relative to prior work. While I still think the paper is worth accepting, it would be stronger if it could offer a clearer discussion of how exactly these results differ from prior work.

Questions to authors

- The introduction states that AHATs and UHATs "are not known to be either a subset or superset of standard, soft-attention transformers." What exactly does this mean? It seems to me that AHATs and UHATs clearly aren't supersets of soft-attention transformers. Is the point that some AHATs/UHATs might not be expressible using a standard transformer? Is there a reference for this point? - Could you elaborate on why exactly FOC[+;MOD] is underpowered (section 2.2)? Is this saying that every sentence in FOC[+;MOD] can be expressed as a two layer transformer? I think it would be helpful to make this more clear. - Regarding the translation from a transformer to a Kt[#] expression: Would it be possible to give any characterization of the size of the Kt[#] expression?

Summary

This paper introduces two equivalent formalisms (a temporal logic Kt[#] and a RASP fragment called C-RASP) which aim to describe counting capabilities in transformers. The authors show that they are the tightest known lower bound on the expressive power of transformers with causal masking (no positional embeddings). Simultaneously, they show that such transformers, when using fixed-precision, can be compiled back into these formalisms. Given the topic, I found the dimensions listed on https://colmweb.org/ReviewGuide.html very hard to apply. Nonetheless, I believe the paper to be a good fit to the "Science of LMs" Research Area of COLM. I'm evaluating the paper according to the four categories given in the review form: CLARITY: I found the paper to be generally clearly written and presented. The paper nicely fits with a recent line of research on investigating the expressive power of transformers. QUALITY: I followed the constructions and believe the formal results to be correct. ORIGINALITY: My main concern here is the comparison to the recent result about LTL(C, +) proven by [1], as described under “Questions”. Clarification from the authors could help here. SIGNIFICANCE: Providing stronger formal lower bounds on the expressive capacity of transformers addresses foundational questions about modern LMs.

Rating

7

Confidence

4

Ethics flag

1

Reasons to accept

* Provides simple and intuitive formalisms lower-bounding the capacity of realistic transformers, addressing foundational questions about transformers and LMs * Unlike a good deal of the literature on transformer expressiveness, this work applies to realistic soft-attention transformers * Provides a construction applying at arbitrary input lengths * Provides some idea of how the result could lead to understanding of expressiveness, through example languages and a construction of piecewise testable languages

Reasons to reject

Weaknesses: * Except for the finite precision setting (with sinusoidal embeddings), the results do not apply to transformers with positional embeddings. * As described in the Summary and under Questions, I believe the paper does not currently do a sufficiently good job of explaining how the result substantially adds over the LTL(C, +) result by [1]: this appears to be a similar recent result, in that it also shows that a temporal logic lower-bounds the power of a certain formalization of transformers. The paper under review could do a much stronger job making clear how the new results are substantially novel compared to the LTL(C, +) result beyond replacing positional encodings with positional masking and AHAT by soft attention, or why these changes require substantial innovations. UPDATE: The authors have provided useful clarification, which I encourage them to include in the paper.

Questions to authors

* I would like to know more about the link to LTL(C, +), proven by [1] to lower-bound AHAT. An obvious difference is that LTL(C, +) includes general unary predicates, establishing that it is strictly more powerful than Kt[#], but this difference just concerns whether or not positional encodings are used. The authors point out that the result from the paper under review applies to soft-attention transformers, different from and more realistic than AHAT. Nonetheless, I’m curious about what’s so different: can’t the construction from [1] be just adapted to softmax transformers? * How is a finite-precision transformer defined? While the proof of Lemma C.7 asks the reader to recall the definition, I couldn’t find it anywhere. Naively: For any given head, its attention weights will be 1/N on average where N is the input length. When N is large and precision is finite, many of these will – if one naively applies finite precision – be rounded to 0. If one claims finite precision as a realistic theoretical assumption for transformers, then this seems like an undesirable result, as it effectively prevents finite-precision transformers from performing averaging. Lemma C.7 apparently gets around this by applying rounding after division. Is that the *definition* of finite-precision transformers? * Page 7: “integer values get overwritten” – I didn’t follow this, the statement might be made clearer. * first paragraph of Section 5.1 has LaTeX "??" [1] Pablo Barcel ´o, Alexander Kozachinskiy, Anthony Widjaja Lin, and Vladimir Podolskii. Logical languages accepted by transformer encoders with hard attention. In Proc. ICLR, 2024.

Summary

The paper studies the representation power of Transformer and proves that constant layer Transformer could recognize all the formal languages defined by formulas of Kt[#]. This is proved by showing Transformer could recognize C-RASP, a variant of RASP (Restricted Access Sequence Processing Language), and then prove the equivalence of Kt[#] and C-RASP.

Rating

5

Confidence

3

Ethics flag

1

Reasons to accept

The paper shows Transformer could recognize language in Kt[#], this gives some improvement on the previous expressiveness result.

Reasons to reject

While the construction of Transformer to recognize language in Kt[#] gives some improvement on the previous expressiveness result, the improvement is not so clear since there is no good characterization of Kt[#], and this result is very hard to parse for people outside of programming language area. Moreover, the expressive result is restricting as it does not count the decoding step performed by Transformer (e.g. CoT) and this gap might be very large. ----------------- Post rebuttal: I slightly raise my score.

Questions to authors

.

Thank you for your reply

> First, the paper gives the particular example of Dyck-1, which is definable in Kₜ[#] but not FOC[+;MOD]. Many other separating languages exist, due to the inability of FOC[+;MOD] to model ordering, but this is an especially important one. It has clear practical relevance to modeling natural languages and programming languages, and we also know empirically (Ebrahimi, 2020) that transformers can learn Dyck-1. The inclusion of Dyck1 is nice. Do you have other examples that are not in FOC[+; MOD] but in $K_t[#]$? I ask this because [1] already shows Dyck can be represented by two-layer Transformer. (actually not only dyck1 but also general deck language, but of course it only shows dyck so it has no confliction with this work) [1] Self-attention networks can process bounded hierarchical languages, ACL 2021, Yao S, Peng B, Papadimitriou C, et al. > Second, whereas the translation from FOC[+;MOD] outputs a transformer of bounded depth, our translation from Kₜ[#] outputs deeper transformers for deeper formulas. While we don't know whether deeper transformers are in fact more expressive, we suspect that they are, and practical applications certainly suggest that they are. So the fact that Kₜ[#] translates to deeper transformers suggests Kₜ[#] is much stronger and closer to actual transformers than FOC[+;MOD]. What do you mean by deeper? Does the number of layer you constructed depends on $t$?

Thank you for your response

We thank the reviewer for the comments. As the discussion period is close to its end, we believe that we have addressed all of your questions, but please let us know if there are any remaining concerns.