Bounded PCTL Model Checking of Large Language Model Outputs

2025/09/23 by Dennis Gross, Gross, Dennis, Helge Spieker +3
Computer Science · #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Natural Language Processing Techniques

paper · pdf · doi:10.48550/arxiv.2509.18836

openalex publication_date 2025/09/23 · openalex created_date 2025/10/16 · openalex updated_date 2026/07/28

Abstract

In this paper, we introduce LLMCHECKER, a model-checking-based verification method to verify the probabilistic computation tree logic (PCTL) properties of an LLM text generation process. We empirically show that only a limited number of tokens are typically chosen during text generation, which are not always the same. This insight drives the creation of α-k-bounded text generation, narrowing the focus to the α maximal cumulative probability on the top-k tokens at every step of the text generation process. Our verification method considers an initial string and the subsequent top-k tokens while accommodating diverse text quantification methods, such as evaluating text quality and biases. The threshold α further reduces the selected tokens, only choosing those that exceed or meet it in cumulative probability. LLMCHECKER then allows us to formally verify the PCTL properties of α-k-bounded LLMs. We demonstrate the applicability of our method in several LLMs, including Llama, Gemma, Mistral, Genstruct, and BERT. To our knowledge, this is the first time PCTL-based model checking has been used to check the consistency of the LLM text generation process.

Citations

• Prompting for Performance: Exploring LLMs for Configuring Software
• Exploring the Roles of Large Language Models in Reshaping Transportation Systems: A Survey, Framework, and Roadmap
• The Role of Language Models in Modern Healthcare: A Comprehensive Review
• Leave No Context Behind: Efficient Infinite Context Transformers with Infini-attention
• Gemma: Open Models Based on Gemini Research and Technology
• Sora: A Review on Background, Technology, Limitations, and Opportunities of Large Vision Models
• MeTMaP: Metamorphic Testing for Detecting False Vector Matching Problems in LLM Augmented Generation
• RITFIS: Robust input testing framework for LLMs-based intelligent software
• Generating Valid and Natural Adversarial Examples with Large Language Models
• Hallucination Detection: Robustly Discerning Reliable Answers in Large Language Models
• Copyright Violations and Large Language Models
• Mistral 7B
• Provably safe systems: the only path to controllable AGI
• LEAP: Efficient and Automated Test Method for NLP Software
• Llama 2: Open Foundation and Fine-Tuned Chat Models
• A Survey on Evaluation of Large Language Models
• A Survey on Evaluation of Large Language Models
• A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation
• Generative Agents: Interactive Simulacra of Human Behavior
• Exploring the Use of Large Language Models for Reference-Free Text Quality Evaluation: An Empirical Study
• nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
• The King is Naked: on the Notion of Robustness for Natural Language Processing
• Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning
• The Probabilistic Model Checker Storm
• Robustness Verification for Transformers
• Natural Language Adversarial Defense through Synonym Encoding
• Attention Is All You Need
• Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks
• ImageNet classification with deep convolutional neural networks
• BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding

Related

• BEAVER: An Efficient Deterministic LLM Verifier
• Exploring the Hidden Capacity of LLMs for One-Step Text Generation
• Generation Meets Verification: Accelerating Large Language Model Inference with Smart Parallel Auto-Correct Decoding
• ProPD: Dynamic Token Tree Pruning and Generation for LLM Parallel Decoding
• Adaptable Logical Control for Large Language Models