Masked Hard-Attention Transformers Recognize Exactly the Star-Free Languages

Thank you very much for your review. We are glad that you find our work convincing, intriguing, and well-placed.

On B-RASP, please see our global response.

[T]he paper...makes it challenging for readers to place the results in the broader context of research.

This point is well-taken, and we'll be sure to expand on this given extra space in the final version. Although there are some interesting remaining open questions about unique hard attention transformers, we primarily see these results as showcasing what kinds of results we can hope to obtain in the future: in particular, how do attention masking, position embeddings, and network depth affect expressivity? We've given rigorous answers for unique-hard attention transformers, and hope to obtain answers for more realistic (i.e., soft attention) transformers.

Regarding LTL with strict "since" versus non-strict "since" and "previous": We'll be happy to include a brief remark about this.

[T]he transformer architectures considered are quite specific, possibly tailored for these particular results.

Our results, which consider strict and non-strict masking (Thm 6), masking direction (Thm 5), and position embeddings ranging from nothing to sinusoidal to Mon (Thm 7, Cor 8-9), run the gamut of masked hard-attention architectures, both common and uncommon. It's true that our main result concerns an unusual combination of strict masking and position embeddings, but this is because it corresponds to the most well-known language class (star-free regular languages). (It may be worth noting that transformers with masking but no position embedding have been tried in practice and perform rather well (e.g., Haviv et al 2022, Kazemnejad et al 2023.))

Can you explain in more detail why masked attention is of interest in the encoder parts of transformers?

It's true that masking is more commonly associated with decoders than encoders. We call the transformers studied here "encoders" because the string is the input rather than the output. But if one wishes, one could view them as decoders, with the string as the prompt and the accept/reject decision as the single-symbol output. On this view, perhaps, the use of future masking seems more natural.

In the proof of Theorem 3, Lemma 20...It appears that you use non-strict masking in the first layer to achieve self-attention. Am I correct?

We think you are referring line 629, which says: "The first self-attention simply computes the identity function". This means that the self-attention uses zero vectors for the values, letting the residual connection compute the identity function. The masking in this self-attention does not matter. We'll be sure to clarify this in the final version.

On the other hand, if you're referring to the fact that whatever masking is used in the B-RASP program is preserved in the transformer (line 631), then it's true that the transformer uses a mix of masks. But it's explained under Theorem 5 (line 233) that in LTL, any star-free language can be defined using only strict "since," which translates to only strict future-masking in B-RASP, which translates to only strict future-masking in the transformer.

In the proof sketch of Theorem 4, can you elaborate on why you focus on precision?

Yes, we can elaborate on this in the final version. As explained in the full proof (line 663 and below), this makes it possible to represent any number computed by the transformer using a finite-sized logical formula. We do agree that line 676 is too terse and will expand it in the final version.

Can you explain in more detail the idea presented in line 264 regarding how a specific symbol BOS helps?

This idea is tangential to our paper, as it concerns soft-attention transformers, but if a string has a prefix $\ell^k$, then at position $k$, a transformer (without position embeddings) cannot count how many $\ell$'s there are; it can only measure what fraction of symbols are $\ell$, which is 100%. But if we add a BOS symbol, then the fraction of symbols becomes $k/(k+1)$, so the transformer can discern different numbers of $\ell$'s.

Can you explain in more detail how attention masking helps in recognizing all LTL[Mon] languages, as discussed in the paragraph starting on line 308?

It's possible that this paragraph is misplaced and is really more about LTL rather than LTL[Mon].

With neither position embedding nor attention masking, transformers are "permutation equivariant" (Yun et al 2020) (insensitive to reordering of the vectors in its input sequence). Position embeddings are one way to break the symmetry, and attention masking is another.

This paragraph makes the further point that even a transformer with a finite-image position embedding and no attention masking would not recognize all languages in LTL. For the final version, we'll reevaluate where the best place to make this point is.

A dedicated subsection summarizing all relevant limitations would be very helpful.

We'll definitely give this some thought for the final version.

Thank you very much for your review and your positive assessment of our paper!

In my eyes, the main contribution of this paper is therefore the result that this characterisation is exact and the results on strict vs. non-strict masking.

Yes, but we would also remind the reviewer of the other results in Section 5, which consider not only strict and non-strict masking (Thm 6) but also masking direction (Thm 5), position embeddings (Thm 7, Cor 8-9), and network depth (Thm 10). Put together, these results run the gamut of masked hard-attention architectures, and form a fuller picture with the two results you highlighted.

I was missing a discussion about implications of the results and possible future work.

This point is well-taken, and we'll be sure to expand on this given extra space in the final version. Although there are some interesting remaining open questions about unique hard attention transformers, we primarily see these results as showcasing what kinds of results we can hope to obtain in the future: in particular, how do attention masking, position embeddings, and network depth affect expressivity? We've given rigorous answers for unique-hard attention transformers, and hope to obtain answers for more realistic (i.e., soft attention) transformers.

Thank you very much for your review! We're glad you found the paper interesting and see its potential to inspire future work.

The main results [focus] on architectures with strict future masking and without positional encodings. Both choices are a very uncommon configuration for Transformers.

Our results, which consider strict and non-strict masking (Thm 6), masking direction (Thm 5), and position embeddings ranging from nothing to sinusoidal to Mon (Thm 7, Cor 8-9), run the gamut of masked hard-attention architectures, both common and uncommon. It's true that our main result concerns an unusual combination of strict masking and position embeddings, but this is because it corresponds to the most well-known language class (star-free regular languages). (It may be worth noting that transformers with masking but no position embedding have been tried in practice and perform rather well (e.g., Haviv et al 2022, Kazemnejad et al 2023).)

Is there an example of a commonly used positional encoding scheme with "infinite image"? (section 4.3)

It depends what you mean by "commonly used". In theoretical papers, yes, it's common to use quantities like 1/(i+1), i, or i² in position embeddings (e.g., Perez et al 2019). In practice, many commonly-used embeddings only go up to a fixed maximum position and therefore trivially have finite image, while many (e.g., RoPE, ALiBi) are architectural modifications and not just embeddings from positions to vectors.

It seems commonly used schemes for relative position encodings (e.g. Shaw et al 2018, Raffel et al 2020) could presumably enable expressing attention operations with strict future masking, without requiring this to be an implicit part of the architecture. Is this true? (section 4.3)

Relative position encodings would be interesting objects of further study. In principle, it seems that they could be used to simulate attention masking, but the encodings of Shaw et al 2018 and Raffel et al 2020 only go up to a fixed maximum distance, so they would not be suitable for this purpose.

[P]erhaps briefly defining terms such as complexity classes AC0 and P on their first mention could help make paper more accessible.

Thanks for the suggestion; we'll do that in the final version.

[I]t might be helpful to have an explicit limitations section.

We'll definitely give this some thought for the final version.

Thank you for your response. I confirm my original recommendation to accept.

Relative position encodings would be interesting objects of further study. In principle, it seems that they could be used to simulate attention masking, but the encodings of Shaw et al 2018 and Raffel et al 2020 only go up to a fixed maximum distance, so they would not be suitable for this purpose.

nit: I believe both approaches use clipping of relative distances to handle, in theory, inputs of unbounded length. It seems a casual attention mask could be implemented with relative distance buckets [\leq-1, 0, \geq1\], and a bias of $-\inf$ for the appropriate buckets, which would be supported by either parameterization.

Thank you very much for your review, and for your assessment of our results as "beautiful" (!).

It's true that the equivalence of LTL and masked hard-attention transformers could be proven directly, without going through B-RASP. We have worked out the LTL to transformer direction outside of this paper. However, we forsee that the proof from transformers to LTL would have the same challenges as the proof of transformers to B-RASP, and would be harder to follow.

We would need a version of Lemma 12 for transformers: every unique hard attention transformer is equivalent to one in which the attention queries do not depend on the position. We think the matrix manipulations needed to prove this would be far more difficult than the present Lemma 12.

This is because LTL does not have a syntax for binary predicates, so we must eliminate relations that depend on two positions before doing the translation into LTL. While this works for masked-hard attention transformers due to Lemma 21, the same technique will not apply to other transformer variants. Thus we foresee the proof of transformers into B-RASP, with its binary score predicates S(i,j), as more relevant to future work than the version directly to LTL. By publishing this version of the proof, we hope to provide a template for extensions towards more realistic transformers.

For the general conceptual benefits of B-RASP, please see our global response.