A Logic for Expressing Log-Precision Transformers

One way to interpret the reasoning power of transformer-based language models is to describe the types of logical rules they can resolve over some input text. Recently, Chiang et al. (2023) showed that finite-precision transformer classifiers can be equivalently expressed in a generalization of first-order logic. However, finite-precision transformers are a weak transformer variant because, as we show, a single head can only attend to a constant number of tokens and, in particular, cannot represent uniform attention. Since attending broadly is a core capability for transformers, we ask whether a minimally more expressive model that can attend universally can also be characterized in logic. To this end, we analyze transformers whose forward pass is computed in log n precision on contexts of length n. We prove any log-precision transformer classifier can be equivalently expressed as a first-order logic sentence that, in addition to standard universal and existential quantifiers, may also contain majority-vote quantifiers. This is the tightest known upper bound and first logical characterization of log-precision transformers. Any log-precision transformer can be re-expressed as a sentence in FO(M) logic, e.g.: Mi. a(i) ∧ Mj. b(j) ∧ ¬∃k, ℓ. (a(k) ∧ b(ℓ) ∧ ℓ < k) (m a's followed by m b's, i.e., a m b m ) aaaabbbb ✓ aaabbbbb ✗ baaaabbb ✗ Figure 1: A first-order logic with majority (FO(M)) sentence for a m b m . In addition to standard ∀ and ∃ quantifiers over string indices, FO(M) allows majority quantifiers (M) that take a majority-vote across indices. a(i) indicates whether token i is a (and analogously for b). We prove FO(M) can express any function computed by a log-precision transformer.