Logical Distillation of Transformer Encoders

We present an algorithm that distills transformer encoders into logical formulas. Interpretable surrogates for transformers are important for safety and scientific knowledge discovery. Recent work extracts sparse latent features from transformer activations, but these features alone do not express how information is composed across a sequence. Building on theoretical connections between transformer expressivity and linear temporal logic (LTL), we introduce iterated temporal decision trees (ITDTs), a model that can express any LTL formula as a sequence of decision trees. Each decision tree builds on the previous ones, producing LTL formulas of increasing temporal depth. Our algorithm distills a transformer encoder into an ITDT. Empirically, our algorithm recovers succinct and accurate formulas on established LTL learning benchmarks and distills interpretable rules for multiple protein sequence datasets from ESM-2-T6, an established protein language model.