Summary
The paper presents results about several forms of masked unique hard-attention transformers by classifying the class of languages recognized by these models using formal languages. Roughly put, a masked unique hard-attention transformer is an encoder that uses unique hardmax as its attention mechanism. In cases of ambiguity, either the leftmost or the rightmost position is attended to. Additionally, the attention heads are masked, meaning that a position only attends to (strictly) preceding ones (future masking) or (strictly) succeeding ones (past masking).
In summary, the presented results are:
- Future-masked rightmost-hard attention transformers without positional embedding recognize exactly the star-free languages (Theorem 5).
- Non-strict masked hard-attention transformers without positional embedding recognize exactly the stutter-invariant star-free languages (Theorem 6).
To establish these results, the paper introduces an auxiliary language called B-RASP to analyze masked hard-attention architectures. The paper shows that B-RASP exactly captures the considered transformer models (Theorems 3 and 4) and that it is as expressive as strict or non-strict Linear Temporal Logic (LTL) (Theorems 1 and 2). Then, the general proof idea of Theorems 5 and 6 is to translate results from strict or non-strict LTL via B-RASP to the respective transformer model. Additionally, the authors also establish that masked-hard attention transformer recognize the same languages as LTL with monadic predicates.
Strengths
The results, mainly Theorem 5 and 6, in this paper follow an intriguing line of research trying to understand the expressive capabilities of transformer models from a formal languages perspective and, therefore, this research is well placed.
In general, the technical proofs of the appendix are convincing and sufficiently argued and, thus, allow to verify them.
Weaknesses
The contribution of this work is intriguing, though its significance may not be immediately apparent. The primary contributions are Theorems 5 and 6, and the transformer architectures considered are quite specific, possibly tailored for these particular results. There is some uncertainty about their broader interest. As the authors note, masked attention is almost exclusively used in the decoder parts of transformers. However, in this work, it is extensively used in encoder-only transformers.
The presentation of the paper is mixed. The first 5 pages are primarily devoted to preliminaries and the introduction of B-RASP, which, while interesting, serves mainly as a tool. This allocation of space would be justified if B-RASP were particularly complex, but it is relatively straightforward. Consequently, almost all theorems in the main paper lack proof sketches or intuitive explanations. Although the appendix adequately supports the theorems’ statements, the main paper itself does not. Additionally, the paper features a very brief introduction and lacks sections like ‘outlook’, ‘open questions’, ‘limitations’, or an equivalent closing and summarizing section. This omission makes it challenging for readers to place the results in the broader context of research.
The clarity of the paper is also mixed. First, the paper uses a form of LTL with a strict until operator and no next operator. Most readers are likely more familiar with non-strict until and the inclusion of the next operator. While this is a minor issue, a single sentence clarifying this would assist non-expert readers. There are more significant issues, which I address in my questions below. For example, in the brief sketch of Theorem 4, it is stated that the transformer “… can be represented using $\mathcal{O}(1)$ bits.” It is unclear why this result focuses on representation sizes. Another example is Theorem 5, which states that future-only masking transformers recognize exactly the star-free languages. The proof relies on a translation from B-RASP to the transformer, and in this translation, it appears they use a self-attention mechanism requiring mixed masking. This may be a case of unclear explanation, but the current version of the paper makes it difficult to understand. If not clarified, this result could be incorrect.
Edit: My concern about the correctness were cleared in the rebuttal. I changed my rating accordingly.
Questions
- Can you explain in more detail why masked attention is of interest in the encoder parts of transformers?
- In the proof of Theorem 3, Lemma 20 establishes a translation from B-RASP to masked hard-attention transformers. It appears that you use non-strict masking in the first layer to achieve self-attention. Am I correct? If so, how can you prove Theorem 5 based on this, since it concerns future-only masked hard-attention transformers?
- In the proof sketch of Theorem 4, can you elaborate on why you focus on precision?
- Can you explain in more detail the idea presented in line 264 regarding how a specific symbol BOS helps?
- 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?
Limitations
The authors clearly describe their considered transformer model and specify where it differs from those commonly used in practice. However, these statements are somewhat scattered throughout the paper. A dedicated subsection summarizing all relevant limitations would be very helpful.