Bounded PCTL Model Checking of Large Language Model Outputs

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.