# Bounded PCTL Model Checking of Large Language Model Outputs

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 30 of its 53 references that are in the map.
- First posted on arXiv 23 Sep 2025.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Llama 2: Open Foundation and Fine-Tuned Chat Models](https://mlsanity.com/paper/2307.09288/) (2023)
- [Generative Agents: Interactive Simulacra of Human Behavior](https://mlsanity.com/paper/2304.03442/) (2023)
- [Mistral 7B](https://mlsanity.com/paper/2310.06825/) (2023)
- [A Survey on Evaluation of Large Language Models](https://mlsanity.com/paper/2307.03109/) (2023)
- [Gemma: Open Models Based on Gemini Research and Technology](https://mlsanity.com/paper/2403.08295/) (2024)
- [Sora: A Review on Background, Technology, Limitations, and Opportunities of Large Vision Models](https://mlsanity.com/paper/2402.17177/) (2024)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Leave No Context Behind: Efficient Infinite Context Transformers with Infini-attention](https://mlsanity.com/paper/2404.07143/) (2024)
- [Copyright Violations and Large Language Models](https://mlsanity.com/paper/2310.13771/) (2023)
- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [Exploring the Use of Large Language Models for Reference-Free Text Quality Evaluation: An Empirical Study](https://mlsanity.com/paper/2304.00723/) (2023)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Large Language Models to Identify Social Determinants of Health in Electronic Health Records](https://mlsanity.com/paper/2308.06354/) (2023)
- [Hallucination Detection: Robustly Discerning Reliable Answers in Large Language Models](https://mlsanity.com/paper/2407.04121/) (2024)
- [Natural Language Adversarial Defense through Synonym Encoding](https://mlsanity.com/paper/1909.06723/) (2019)
- [Provably safe systems: the only path to controllable AGI](https://mlsanity.com/paper/2309.01933/) (2023)
- [Exploring the Roles of Large Language Models in Reshaping Transportation Systems: A Survey, Framework, and Roadmap](https://mlsanity.com/paper/2503.21411/) (2025)
- [The King is Naked: on the Notion of Robustness for Natural Language Processing](https://mlsanity.com/paper/2112.07605/) (2021)
- [Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning](https://mlsanity.com/paper/2004.00273/) (2020)
- [Generating Valid and Natural Adversarial Examples with Large Language Models](https://mlsanity.com/paper/2311.11861/) (2023)
- [LEAP: Efficient and Automated Test Method for NLP Software](https://mlsanity.com/paper/2308.11284/) (2023)
- [Are Transformers More Robust? Towards Exact Robustness Verification for Transformers](https://mlsanity.com/paper/2202.03932/) (2022)
- [MeTMaP: Metamorphic Testing for Detecting False Vector Matching Problems in LLM Augmented Generation](https://mlsanity.com/paper/2402.14480/) (2024)
- [RITFIS: Robust input testing framework for LLMs-based intelligent software](https://mlsanity.com/paper/2402.13518/) (2024)
- [The Role of Language Models in Modern Healthcare: A Comprehensive Review](https://mlsanity.com/paper/2409.16860/) (2024)
- [Prompting for Performance: Exploring LLMs for Configuring Software](https://mlsanity.com/paper/2507.09790/) (2025)

## Built on by (most cited first, 1 of 1)

- [Probabilistic Model Checking of Autoregressive Neural Sequence Models](https://mlsanity.com/paper/2609.00838/) (2026)

## Abstract (arXiv)

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.