Extracting Linear Temporal Logic Formulas from Hard Attention Transformers

There has been an increased interest into finding exact encodings of hard attention transformers (HAT) for binary classification into Linear Temporal Logic (LTL), so that the mature ecosystem of LTL tools can be applied to verify and reason about such models. Although several theoretical encoding approaches have been proposed, to the best of our knowledge, none of them have been implemented. In this work, we propose an exact encoding of a HAT into LTL with past operators amenable to practical implementation. We also propose an encoding of the notion of a sufficient reason w.r.t. an input w, that is, a formula extracted from a HAT with the property that any other input w′ that satisfies it has the same classification as w. We implement both the encoding of a HAT and of a sufficient reason for an input and perform experiments using synthetic data. We also include experiments for the balanced parenthesis problem.