Transformer Encoder Satisfiability: Complexity and Impact on Formal Reasoning

TL;DR

This paper investigates the computational complexity of the satisfiability problem for transformer encoders in formal reasoning, revealing undecidability in general and decidability under certain quantized conditions, with implications for verification.

Contribution

It provides the first complexity analysis of trSAT for transformer encoders, identifying decidable cases with complexity bounds and discussing their significance in formal reasoning.

Findings

trSAT is undecidable for general transformer encoders

Quantized TE makes trSAT decidable due to limited attention

Decidable cases of trSAT are NEXPTIME-complete or NEXPTIME-hard

Abstract

We analyse the complexity of the satisfiability problem, or similarly feasibility problem, (trSAT) for transformer encoders (TE), which naturally occurs in formal verification or interpretation, collectively referred to as formal reasoning. We find that trSAT is undecidable when considering TE as they are commonly studied in the expressiveness community. Furthermore, we identify practical scenarios where trSAT is decidable and establish corresponding complexity bounds. Beyond trivial cases, we find that quantized TE, those restricted by fixed-width arithmetic, lead to the decidability of trSAT due to their limited attention capabilities. However, the problem remains difficult, as we establish scenarios where trSAT is NEXPTIME-hard and others where it is solvable in NEXPTIME for quantized TE. To complement our complexity results, we place our findings and their implications in the broader context of formal reasoning.