# From Transformers to Weighted Automata: Towards the Verification of Large Language Models

arXiv: https://arxiv.org/abs/2610.04569 · HTML: https://mlsanity.com/paper/2610.04569/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 20 of its 30 references that are in the map.
- First posted on arXiv 3 Oct 2026.

## Builds on (most cited first, 20 of 20)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [The Illusion of Thinking: Understanding the Strengths and Limitations of Reasoning Models via the Lens of Problem Complexity](https://mlsanity.com/paper/2506.06941/) (2025)
- [Benchmark Data Contamination of Large Language Models: A Survey](https://mlsanity.com/paper/2406.04244/) (2024)
- [Investigating Data Contamination in Modern Benchmarks for Large Language Models](https://mlsanity.com/paper/2311.09783/) (2023)
- [What Formal Languages Can Transformers Express? A Survey](https://mlsanity.com/paper/2311.00208/) (2023)
- [Formal Language Recognition by Hard Attention Transformers: Perspectives from Circuit Complexity](https://mlsanity.com/paper/2204.06618/) (2022)
- [A Formal Hierarchy of RNN Architectures](https://mlsanity.com/paper/2004.08500/) (2020)
- [Rethinking Lipschitz Neural Networks and Certified Robustness: A Boolean Function Perspective](https://mlsanity.com/paper/2210.01787/) (2022)
- [Limitations of the Lipschitz constant as a defense against adversarial examples](https://mlsanity.com/paper/1807.09705/) (2018)
- [LipsFormer: Introducing Lipschitz Continuity to Vision Transformers](https://mlsanity.com/paper/2304.09856/) (2023)
- [Some Fundamental Aspects about Lipschitz Continuity of Neural Networks](https://mlsanity.com/paper/2302.10886/) (2023)
- [Improving Lipschitz-Constrained Neural Networks by Learning Activation Functions](https://mlsanity.com/paper/2210.16222/) (2022)
- [Weighted Automata Extraction from Recurrent Neural Networks via Regression on State Spaces](https://mlsanity.com/paper/1904.02931/) (2019)
- [Training Transformers with Enforced Lipschitz Constants](https://mlsanity.com/paper/2507.13338/) (2025)
- [On the expressivity of bi-Lipschitz normalizing flows](https://mlsanity.com/paper/2107.07232/) (2021)
- [The Price of Tolerance in Distribution Testing](https://mlsanity.com/paper/2106.13414/) (2021)
- [Forget What You Know about LLMs Evaluations -- LLMs are Like a Chameleon](https://mlsanity.com/paper/2502.07445/) (2025)
- [InductionBench: LLMs Fail in the Simplest Complexity Class](https://mlsanity.com/paper/2502.15823/) (2025)
- [The Lipschitz-Variance-Margin Tradeoff for Enhanced Randomized Smoothing](https://mlsanity.com/paper/2309.16883/) (2023)
- [A One-Layer Decoder-Only Transformer is a Two-Layer RNN: With an Application to Certified Robustness](https://mlsanity.com/paper/2405.17361/) (2024)

## Abstract (arXiv)

Large language models (LLMs) are increasingly deployed in safety-critical settings, yet their black-box nature makes it difficult to provide formal guaranties about their behavior. Existing verification approaches rely primarily on empirical probing and testing, leaving open the question of how to reason rigorously about general-purpose trans- former architectures. In this work, we establish a principled bridge between transformers and weighted automata, a classical model from formal language theory. This connection enables us to transfer verification tools from automata the- ory to the analysis of LLMs. Our contributions are twofold: First, we develop a formal correspondence between transformer architectures and weighted automata over reals, showing how distributional properties of LLMs can be captured within this framework. Second, we introduce an identity testing algorithm for weighted automata that provides a statis- tical method for distinguishing whether two stochastic models define the same distribution up to a tolerance threshold. This work provides the first formal bridge between modern neural se- quence models and classical automata theory, clarifying both the poten- tial and the computational challenges for rigorous LLM verification.