发表机构
Ashoka University（阿育王大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本工作建立了Transformer与加权自动机之间的形式化桥梁，并提出恒等性测试算法，为严格验证大语言模型行为提供了首个理论框架。
AI 中文摘要
大语言模型（LLMs）越来越多地被部署在安全关键环境中，然而其黑箱特性使得对其行为提供形式化保证变得困难。现有的验证方法主要依赖于经验性的探测和测试，这留下了如何对通用Transformer架构进行严格推理的问题。在本工作中，我们建立了Transformer与加权自动机（形式语言理论中的经典模型）之间的原则性桥梁。这一联系使我们能够将自动机理论中的验证工具迁移到LLMs的分析中。我们的贡献有两方面：首先，我们发展了Transformer架构与实数域上加权自动机之间的形式对应关系，展示了LLMs的分布特性如何在此框架内被捕获。其次，我们提出了一种用于加权自动机的恒等性测试算法，该算法提供了一种统计方法，用于区分两个随机模型是否在容差阈值内定义了相同的分布。本工作为现代神经序列模型与经典自动机理论之间提供了首个形式化桥梁，阐明了严格LLM验证的潜力与计算挑战。
英文摘要
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.
Journal refDATAMOD 2025
DOI：10.1007/978-3-032-25552-5_10
