The Underlying Logic of Language Models: The Underlying Logic of Language Models: Transformers and Formal Logics

The Underlying Logic of Language Models: Transformers and Formal Logics

Speakers: Jiaoda Li, Ryan Cotterell, Franz Nowak, Anej Svete

Conference: ICML 2025

YouTube: https://slideslive.com/39043866

Overview

This talk, presented at ICML 2025 by Jiaoda Li and collaborators, delves into the fundamental expressive power of Transformer architectures by establishing formal equivalences with fragments of mathematical logic. The presenters aim to bridge the gap between classical theoretical computer science concepts—such as formal languages and logic—and modern neural network architectures, specifically focusing on how Transformers process and represent information. This tutorial is particularly geared towards making complex theoretical results more accessible to the wider ML community, hoping to foster further growth in this interdisciplinary area.

The core of the presentation demonstrates that specific configurations of Transformers, particularly decoder-only models with future masking and constant precision, possess expressive power precisely equivalent to Past First-Order Logic with two variables (PFO2) and Linear Temporal Logic (LTL) with only Past operators (LTL Past). This theoretical equivalence not only provides a rigorous understanding of what Transformers can and cannot reliably learn but also offers a novel method for interpreting the internal workings of trained models by extracting their equivalent logical formulas. The implications are profound, offering insights into the inherent limitations of current large language models (LLMs) and suggesting pathways for augmenting their capabilities.

The research presented is significant because it moves beyond empirical observations of Transformer performance to a formal characterization of their computational limits. By comparing different attention mechanisms and the impact of practical considerations like numerical precision and positional encodings, the talk provides a foundational framework for analyzing Transformer expressivity. This understanding is crucial for practitioners designing robust ML systems, as it helps identify tasks where Transformers can be fully trusted versus those where they might exhibit high but ultimately unreliable performance, failing on edge cases not covered by training data.

Background

▶ Watch: Introduction to formal languages and regular expressions (0:00)

The field of Natural Language Processing (NLP) has a rich history rooted in formal language theory, automata theory, and mathematical logic. An alphabet ($\Sigma$) is a finite set of symbols, and its Kleene closure ($\Sigma^$) represents all possible strings formed from these symbols, including the empty string. A formal language is any subset of $\Sigma^$. A regular language is a specific type of formal language describable by regular expressions or recognizable by a finite state automaton (FSA). More complex languages require more powerful automata, such as pushdown automata (PDA) for context-free languages or Turing machines for recursively enumerable languages. Historically, these mathematical tools have been instrumental in defining the capabilities of computational systems.

In recent years, a burgeoning community within NLP has sought to connect these classical mathematical frameworks with modern neural network architectures, particularly Transformers. This tutorial aims to facilitate this connection by focusing on several logical fragments that are especially useful for characterizing Transformer behavior and capacity.

The first fragment introduced is First-Order Logic (FO) defined over strings. In this context, variables (e.g., X, Y) are interpreted as positions within a string of length N, ranging from 1 to N. Atomic formulas like $\pi_A X$ assert that the symbol at position X is A. Standard logical connectives (AND, OR, NOT) are available, along with quantifiers (EXISTS, FOR ALL) that bind variables, allowing for statements about the existence or universality of properties across string positions. A binary predicate, typically 'less than' ($<$), enables reasoning about the sequential order of positions. A formula with no free variables is called a sentence and can define formal languages. For example, $\exists X (\pi_A X)$ defines the language $\Sigma^ A \Sigma^$ (strings containing A). A well-established result shows that FO with the 'less than' predicate defines exactly the class of star-free regular languages—languages describable by regular expressions without the Kleene star operator. While (AB) is star-free, (AA) (strings of even length containing only A's) is a famous example of a regular language that is not star-free and thus not definable in FO.

The discussion then refines FO into more restrictive fragments. FO2 is First-Order Logic restricted to using at most two variables (free or bound) at any given point in a formula. This restriction significantly limits expressivity; for instance, the language $\Sigma^ A B \Sigma^$ (strings containing AB as a contiguous substring) is not definable in FO2 because expressing "A at X, B at Y, and nothing between X and Y" typically requires three variables. In contrast, piecewise testable languages, which require subsequences (not necessarily contiguous) rather than substrings, are definable in FO2 (e.g., $\Sigma^ A \Sigma^ B \Sigma^ C \Sigma^$ for the subsequence ABC). PFO2 (Past First-Order Logic with two variables) further restricts FO2 by only allowing quantifiers to bind variables to positions earlier than any free variable in their scope. This mirrors the "past-only" attention mechanism common in decoder-only Transformers. Consequently, languages requiring future information, such as $\Sigma^* A$ (strings ending with A), are not definable in PFO2.

Another crucial logical framework is Linear Temporal Logic (LTL), introduced in the 1970s and widely used for formal verification. Unlike FO, LTL has no explicit variables; formulas are evaluated relative to a single, implicit position in the string. LTL includes atomic formulas ($\pi_A$) and standard connectives, but replaces quantifiers with four temporal operators: Past (P), Future (F), Since (S), and Until (U). For example, P psi means psi holds at some point in the past relative to the current position, and psi1 S psi2 means psi2 held at some past position M, and psi1 held at all positions between M and the current position. A string satisfies an LTL formula if it holds at a specific position (e.g., N+1 or 0, depending on the direction). P pi A defines $\Sigma^ A \Sigma^$. Similar to FO fragments, LTOPF (LTL with only unary operators P and F) is equivalent in expressivity to FO2, and LTL Past (LTL with only the P operator) is equivalent to PFO2. These equivalences lay the groundwork for understanding the logical underpinnings of Transformer capabilities.

Key Findings

▶ Watch: Defining First-Order Logic (FO) over strings (3:00)

The central and most significant finding of this research is the establishment of a formal equivalence between a specific class of Transformer models and fragments of formal logic. Specifically, the talk demonstrates that decoder-only Transformers operating with future masking, constant precision, and initially without positional encodings, have the exact same expressive power as Past First-Order Logic with two variables (PFO2) and Linear Temporal Logic with only Past operators (LTL Past). This means any language definable in PFO2/LTL Past can be recognized by such a Transformer, and conversely, any computation performed by such a Transformer can be translated into a PFO2/LTL Past formula.

A crucial discovery relates to the expressivity of different attention mechanisms:

• Soft attention, average hard attention, and leftmost unique hard attention are all shown to be equally expressive, aligning with the PFO2/LTL Past fragment. This implies that for these common attention types, the theoretical expressivity ceiling is the same.
• In contrast, rightmost unique hard attention is found to be significantly more expressive, requiring the full power of First-Order Logic (FO) to simulate, thus surpassing the PFO2/LTL Past boundary. The technical reason for this difference lies in the need to quantify over positions between two other variables, which pushes it beyond the two-variable restriction of PFO2.

The research also provides a concrete method for interpreting Transformers by extracting their equivalent logical formulas. This allows researchers to:

• Understand precisely what a trained Transformer is doing, even in intermediate layers.
• Identify "shortcuts" or unintended heuristics learned by the model during training.
• Diagnose where a model fails or succeeds by inspecting the logic implemented by individual components (e.g., attention versus feed-forward layers). An example showed a Transformer initially learning a simpler, incorrect logic (pi A X at the last position) before converging to the correct exists y <= x such that pi A y for $\Sigma^ A \Sigma^$.

Experimental validation strongly supports these theoretical predictions. Using a standard length generalization setup (training on lengths 1-40, testing on 41-500), the authors observed:

• Transformers achieved 100% generalization accuracy on all languages definable in PFO2 (e.g., $\Sigma^ A \Sigma^$, $A \Sigma^*$).
• For languages not definable in PFO2 (e.g., $\Sigma^ A$ (Last), Dyck languages with depth 1, $(AA)^$), Transformers consistently failed to achieve 100% accuracy, regardless of hyperparameter tuning, supporting the theoretical lower bound.

Finally, the talk explores factors that can augment Transformer expressivity:

• Positional encodings can increase expressive power by introducing "numerical predicates" that depend only on position. However, practically implemented positional encodings are not well understood theoretically and often do not yield the expected boost for specific tasks.
• Relaxing the constant precision assumption (e.g., to logarithmic precision with respect to input length) significantly increases expressivity, allowing Transformers to simulate counting quantifiers and even rightmost unique hard attention with soft attention. Arbitrary precision further expands these capabilities. This highlights the practical interplay between theoretical computational power and hardware/numerical constraints.

Technical Deep Dive

▶ Watch: Using FO sentences to define formal languages (6:00)

The technical core of the talk revolves around formally defining Transformers and then demonstrating the two-way simulation between these models and the logical fragments PFO2/LTL Past.

A Transformer is formally defined as a function mapping an input string $w \in \Sigma^N$ (where $N$ is the length) to a matrix in the space $F^{D \times N}$, where $F$ is a finite set of values (representing constant precision, e.g., float32) and $D$ is the dimension. For language recognition, $D=1$ and the output at the last position is typically observed. For language modeling, the output is a distribution over $\Sigma$ plus an EOS token. The analysis primarily focuses on decoder-only models with future masking, meaning each token can only attend to past tokens and itself. A stricter variant, strict future masking, where a token cannot attend to itself, is also considered, mirroring the strictness of the past operator in logic.

The talk meticulously details how logical formulas can be extracted from a trained Transformer, layer by layer, for the direction Transformer $\rightarrow$ PFO2. This is illustrated with a simple one-layer, one-dimension, one-attention-head Transformer trained on the language $\Sigma^ A \Sigma^$ (strings containing 'A').

1. Embedding Layer: This layer assigns a fixed numerical value (from $F$) to each symbol. Logically, this is straightforward: $E_f(X)$ is true if the embedding at position $X$ is $f$. For example, if symbol 'A' is assigned -1.15, then $E_{-1.15}(X) \iff \pi_A X$.
2. Query, Key, Value Projections: These linear transformations also map embedding values to new values. If an embedding value $f$ maps to $f'$ for query, then $Q_{f'}(X) \iff E_f(X)$. If multiple input values map to the same output value, a logical disjunction is used (e.g., $Q_{-1.11}(X) \iff E_{0.07}(X) \lor E_0(X)$).
3. Scaled Dot Product: This computes attention scores between positions $X$ and $Y$. Since the precision is constant, there's a finite set of possible score outcomes (e.g., 0.1, 0.2, 0.3, 0.5). For each outcome $s$, a two-variable formula $S_s(X, Y)$ can be written that is true if the dot product of query at $X$ and key at $Y$ equals $s$. This combines the logical statements for $Q_f(X)$ and $K_f(Y)$.
4. Argmax Operation: For hard attention, this selects positions with the maximum score. $M_s(X, Y)$ is true if $S_s(X, Y)$ is true AND there is no other position $Z$ such that $S_{s'}(X, Z)$ is true for $s' > s$. This involves a universally quantified subformula for negation.
5. Tie-Breaking (Leftmost Unique Hard Attention): If multiple positions share the maximum score, this mechanism selects the leftmost one. The logic for this, $L_s(X, Y)$, combines $M_s(X, Y)$ with a condition that there is no $Z < Y$ such that $M_s(X, Z)$ is true. Crucially, the talk demonstrates a simplification of this formula:

• $\exists Y \le X (M_s(X, Y) \land \neg \exists Z < Y (M_s(X, Z)))$
• Through variable substitution and elimination of redundant terms (given $Z < Y \le X$), this formula simplifies to one that always involves at most two free variables (X and Y or X and Z at different scopes), thus remaining within PFO2.

1. Tie-Breaking (Rightmost Unique Hard Attention): In contrast, if the rightmost tie-breaking is used, the logical formula requires quantifying over a variable $Z$ such that $Y < Z < X$. This structure inherently requires three variables, making it not definable in PFO2, thus demonstrating its higher expressivity.
2. Weighted Sum (for Unique Hard Attention): For unique hard attention, this step is simplified: the output value at position $X$ is simply the value $V_f(Y)$ from the unique position $Y$ selected by the hard attention.
3. Residual Connections and Feed-Forward Layers: Residual connections involve summing values, which, under constant precision, can be enumerated as a disjunction of possible outcomes. Feed-forward layers operate position-wise, meaning their logic only depends on the symbol at $X$ itself, and thus do not introduce quantifiers or complex variable dependencies.
4. Final Output Layer: For a binary classification task, positive output values are typically mapped to 'true'. The final logic is a disjunction of the formulas corresponding to these positive values. For the $\Sigma^ A \Sigma^$ example, the extracted logic is $\exists Y \le X (\pi_A Y)$, perfectly matching the target language. The ability to extract this logic from intermediate checkpoints also allows for diagnosis of learning, showing how a model might initially learn shortcuts (e.g., pi A X for $\Sigma^ A \Sigma^` with 66% accuracy) before converging.

For the reverse direction, LTL Past $\rightarrow$ Transformer, the talk outlines how to construct a Transformer that simulates a given LTL Past formula, using Past pi A as an example.

1. One-Hot Embedding: Each distinct symbol is assigned a unique dimension in the embedding space.
2. Attention Layer: To simulate Past pi A, the attention mechanism is designed to attend specifically to the dimension corresponding to symbol 'A'.
3. Fixed Precision Challenge: A key challenge arises with fixed precision. If multiple 'A's appear in the past, the attention weights might be equally distributed (e.g., 0.5 for two 'A's). However, under fixed precision, if the maximum number of positions that can be attended to is limited (e.g., one), these weights can vanish (e.g., 0.5 becomes 0), leading to incorrect simulation.
4. Circumventing Vanishing Weights: This issue can be addressed by adding a second attention layer that checks for patterns like Past pi A and Past pi A (i.e., whether there are at least two 'A's in the past). The final feed-forward layer then takes the disjunction of the potentially incorrect single-A simulation and this two-A simulation. This clever technique shows that multi-layer Transformers can overcome some limitations imposed by fixed precision, effectively counting up to a certain bound.

The takeaway from this deep dive is that softmax attention, average hard attention, and leftmost unique hard attention are all equally expressive, falling into the PFO2/LTL Past class. Only rightmost unique hard attention extends beyond this due to its inherent need for more complex variable dependencies. The analysis of iterative addition in average hard attention and softmax (exponentials are non-negative) also shows how these, under fixed precision, can be expressed in PFO2, provided the number of summed terms is bounded.

Experimental Setup & Results

▶ Watch: Example of non-star-free language (A A star) (7:30)

To validate their theoretical predictions, the researchers conducted experiments using a standard length generalization setup. This involves training Transformer models on input strings of relatively short lengths (1 to 40 tokens) and then evaluating their performance on significantly longer, unseen strings (41 to 500 tokens). This setup is critical for testing whether models learn robust, generalizable patterns or merely memorize training examples.

The experiments focused on two categories of formal languages:

1. Languages definable in PFO2: These are tasks that, according to the theory, Transformers with the specified architectural constraints (decoder-only, future masking, constant precision, no positional encodings) should be able to solve perfectly. Examples include:

• Sigma* A Sigma*: strings containing the symbol 'A'.
• A Sigma*: strings starting with 'A'.
• Past pi A: a logical representation equivalent to Sigma* A Sigma* when evaluated at the string's end.

1. Languages not definable in PFO2: These are tasks that, theoretically, fall outside the expressive power of such Transformers. Examples include:

• Sigma* A (Last): strings ending with 'A'. This requires looking at the "future" (ensuring no symbols follow 'A'), which PFO2 cannot express.
• Dyck languages (bounded): specifically, Dyck languages with only one pair of parentheses and a maximum depth of one (e.g., (AB)*). These are simple hierarchical languages related to context-free grammars.
• (AA)*: strings consisting of an even number of 'A's, which is a non-star-free regular language.

The experimental results perfectly aligned with the theoretical predictions:

• For all languages definable in PFO2, the trained Transformers achieved 100% generalization accuracy on the longer, unseen test strings. This demonstrates that for tasks within this expressive class, Transformers can reliably learn the underlying logic and generalize perfectly.
• Conversely, for all languages not definable in PFO2, the Transformers consistently failed to achieve 100% accuracy on the generalization tasks. This failure persisted despite extensive hyperparameter tuning, including variations in learning rates, initialization strategies, and random seeds. While models might achieve high accuracy (e.g., 80-90%) on these harder tasks, they invariably made mistakes on specific edge cases or longer sequences, indicating a fundamental limitation rather than just a training challenge.

These findings are particularly striking because some of the "simple" tasks that Transformers failed to generalize perfectly on (like Sigma* A or bounded Dyck languages) are often intuitively expected to be within their grasp. The results underscore that PFO2 represents a verifiable "lower bound" for tasks that Transformers can reliably execute with absolute certainty. For any language outside this class, practitioners must exercise caution, as models, even if appearing to perform well, may exhibit unpredictable failures in certain scenarios.

Practical Implications

▶ Watch: Introduction to FO2: First-Order Logic with two variables (8:00)

The findings presented in this talk carry significant practical implications for anyone involved in designing, training, or deploying AI/ML models, especially those based on Transformer architectures.

First, the identification of PFO2/LTL Past as the inherent expressive limit for a common class of Transformers (decoder-only, future masking, constant precision, no positional encodings) provides a crucial theoretical lower bound for reliable performance. This means that for tasks whose underlying logic can be expressed within PFO2, practitioners can have high confidence that a properly trained Transformer will achieve 100% accuracy and generalize perfectly, without unexpected failures on edge cases. These are the "safe" tasks where Transformers can be fully trusted.

Conversely, for tasks that fall outside the PFO2 class, practitioners must proceed with extreme caution. This includes seemingly simple tasks like recognizing strings ending with a specific symbol ($\Sigma^* A$), or more complex ones like basic Dyck languages (well-balanced parentheses) or multiplication. While Transformers might achieve high empirical accuracy (e.g., 80-90%) on these tasks, the experiments demonstrate that they will not reach 100% generalization. This implies that such models are likely learning statistical correlations or heuristics rather than the true underlying formal logic, making them susceptible to failure on unseen or adversarial examples, or simply longer sequences. This insight is vital for critical applications where even minor errors are unacceptable.

The ability to extract logical formulas from trained Transformers offers a powerful new tool for model interpretation and debugging. Instead of relying on opaque black-box metrics, researchers and engineers can now precisely understand what a model has learned. This can reveal if a model has taken a "shortcut" during training (e.g., classifying based on the last token instead of a more complex past pattern) or if a specific layer (e.g., attention vs. feed-forward) is failing to implement its intended logic. This level of transparency is invaluable for diagnosing performance issues, improving model robustness, and building trust in AI systems.

The discussion on augmenting Transformer expressivity also has practical consequences:

• Positional Encodings: While theoretically capable of adding "numerical predicates" and boosting expressivity, the talk highlights that many bespoke positional encodings proposed in theory do not work well in practice, and commonly used ones (learned, relative) are not yet well-understood from a formal perspective. This suggests that simply adding positional encodings isn't a silver bullet for overcoming fundamental limitations.
• Numerical Precision: Relaxing the constant precision assumption (e.g., to logarithmic precision with respect to input length) significantly enhances Transformer capabilities, enabling them to simulate counting quantifiers and even the more expressive rightmost unique hard attention. This suggests that the numerical precision of hardware and software implementations plays a direct role in the actual computational power of Transformers. For tasks requiring more complex counting or precise numerical operations, higher effective precision (or architectural changes that simulate it) might be necessary. Arbitrary precision further expands these capabilities, though it comes with computational costs.

Finally, the talk implicitly touches upon the tradeoffs between theoretical expressivity and practical utility. While Transformers, under these constraints, are theoretically less expressive than, for example, vanilla Recurrent Neural Networks (RNNs) (which are equivalent to second-order logic with monadic predicates, corresponding to regular languages), they dominate the modern AI landscape. This suggests that their efficiency in leveraging modern parallel computing hardware (GPUs/TPUs) and their ability to achieve high, if not perfect, accuracy on complex tasks often outweigh their theoretical limitations in practice. The challenge lies in understanding when this "good enough" performance is truly sufficient and when the PFO2 limitations become critical.

Key Takeaways

• Formal Equivalence: Decoder-only Transformers with future masking and constant precision are precisely as expressive as Past First-Order Logic with two variables (PFO2) and LTL Past.
• Attention Mechanism Differences: Soft, average hard, and leftmost unique hard attention share this PFO2/LTL Past expressivity, while rightmost unique hard attention is significantly more expressive, requiring full First-Order Logic.
• Reliable Performance Lower Bound: PFO2 defines the class of tasks that Transformers can reliably solve with 100% generalization accuracy; tasks outside this class may achieve high but not perfect accuracy, indicating potential unreliability.
• Model Interpretation Tool: The ability to extract logical formulas from Transformers provides a powerful method for understanding learned behaviors, diagnosing failures, and identifying shortcuts.
• Impact of Precision and Positional Encodings: Increasing numerical precision (e.g., logarithmically with input length) can significantly boost Transformer expressivity beyond PFO2, enabling tasks like counting; practical positional encodings are less understood and often don't reliably overcome these limitations.
• Theoretical vs. Practical Success: Despite theoretical expressivity limitations compared to models like RNNs, Transformers' ability to efficiently leverage modern compute resources allows them to perform exceptionally well on many real-world tasks, albeit sometimes with inherent limitations on absolute accuracy for certain logical operations.

About the Speaker(s)

The talk was delivered by Jiaoda Li, with contributions from Ryan Cotterell, Franz Nowak, and Anej Svete. Jiaoda Li presented the initial sections, focusing on the logical fragments and the first direction of the equivalence (Transformer to PFO2), and later addressed audience questions regarding the implications and future work. The collaborative nature of the research, involving multiple authors, underscores a shared interest in rigorously understanding the theoretical underpinnings and limitations of modern neural network architectures, particularly Transformers, by drawing connections to established fields of formal logic and automata theory. Their collective work aims to make these complex theoretical insights more accessible to the broader machine learning community.