Cross-Attention and Encoder-Decoder Transformers: A Logical Characterization
This work offers a theoretical understanding of encoder-decoder transformers for researchers in formal methods and machine learning, but it is primarily a logical analysis without empirical results.
The paper provides a novel logical characterization of encoder-decoder transformers, the foundational architecture for LLMs, using a new temporal logic that extends propositional logic with a counting global modality and a past modality. It also characterizes these transformers via distributed automata and discusses the autoregressive setting.
We give a novel logical characterization of encoder-decoder transformers, the foundational architecture for LLMs that also sees use in various settings that benefit from cross-attention. We study such transformers over text in the practical setting of floating-point numbers and soft-attention, characterizing them with a new temporal logic. This logic extends propositional logic with a counting global modality over the encoder input and a past modality over the decoder input. We also give an additional characterization of such transformers via a type of distributed automata, and show that our results are not limited to the specific choices in the architecture and can account for changes in, e.g., masking. Finally, we discuss encoder-decoder transformers in the autoregressive setting.