Bounded PCTL Model Checking of Large Language Model Outputs
This addresses the need for formal verification of LLM outputs to ensure consistency and reliability, though it is incremental as it adapts existing model-checking techniques to a new domain.
The paper tackles the problem of verifying probabilistic properties in large language model (LLM) text generation by introducing LLMCHECKER, a model-checking method based on probabilistic computation tree logic (PCTL), and demonstrates its applicability across models like Llama and BERT, showing it can handle diverse text quantification such as quality and bias evaluation.
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.