用形式化方法验证大模型生成文本的逻辑一致性。
Bounded PCTL Model Checking of Large Language Model Outputs
- 限定每步生成的前k个高概率词，再按累积概率阈值筛选。
- 首次实现对大模型文本生成过程的PCTL性质形式化验证。
- 适用于Llama、Gemma等主流模型，可检测质量与偏见问题。
本文提出LLMCHECKER，一种基于模型检查的验证方法，用于检验大语言模型（LLM）文本生成过程的随机计算树逻辑（PCTL）性质。我们实证发现，文本生成过程中通常仅选择有限数量的词，且这些词并非固定不变。这一洞察催生了α-k有界生成机制：在每一步生成中，仅关注前k个词的累积概率最大值α，进一步筛选出累积概率不低于α的词。该方法支持初始字符串与后续前k个候选词的分析，并兼容多种文本量化方式，如质量评估和偏见检测。最终，通过α-k有界设定，实现对大模型生成过程的正式PCTL验证。我们在Llama、Gemma、Mistral、Genstruct及BERT等多个模型上验证了该方法的有效性。据我们所知，这是首次将基于PCTL的模型检查应用于大模型生成过程的一致性验证。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。