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

arXiv:2610.04569v1 Announce Type: cross Abstract: 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.

Abstract: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.

Formal Languages and Automata Theory (cs.FL); Machine Learning (cs.LG)

arXiv:2610.04569 [cs.FL]

(or arXiv:2610.04569v1 [cs.FL] for this version)

https://doi.org/10.48550/arXiv.2610.04569 Focus to learn more arXiv-issued DOI via DataCite (pending registration)

https://doi.org/10.1007/978-3-032-25552-5_10 Focus to learn more DOI(s) linking to related resources

arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.

Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.

Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.

aiqbench analysis

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

Related coverage