Cross-Attention and Encoder-Decoder Transformers: A Logical Characterization

TL;DR

This paper provides a logical and automata-based characterization of encoder-decoder transformers, fundamental for LLMs, in practical floating-point and soft-attention settings, extending their theoretical understanding.

Contribution

It introduces a new temporal logic and automata framework to characterize encoder-decoder transformers, accounting for architectural variations and masking.

Findings

Logical characterization using a new temporal logic with counting and past modalities.

Automata-based characterization that is robust to architectural changes.

Discussion of autoregressive encoder-decoder transformers.

Abstract

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.