验证大规模语言模型的无记忆序贯决策
Verifying Memoryless Sequential Decision-making of Large Language Models
AI总结：
本文提出一种自动化验证工具，通过增量构建MDP可达状态并利用Storm检查PCTL安全属性，验证LLM策略在无记忆序贯决策中的安全性，实验表明开源LLM可验证但逊于强化学习基线。
摘要：
我们引入了一种工具，用于对基于大规模语言模型（LLM）的策略在无记忆序贯决策任务中进行严格且自动化的验证。给定一个表示序贯决策任务的马尔可夫决策过程（MDP）、一个LLM策略以及一个以PCTL公式表达的安全要求，我们的方法在LLM所选动作的引导下，仅增量地构建MDP的可达部分。每个状态被编码为自然语言提示，LLM的响应被解析为一个动作，策略的可达后继状态被展开。所得的形式化模型使用Storm进行检查，以确定该策略是否满足指定的安全属性。在标准网格世界基准的实验表明，通过Ollama访问的开源LLM在确定性种子设置下可以被验证，但总体上表现不如深度强化学习基线。我们的工具原生集成Ollama，并支持PRISM指定的任务，从而能够在用户指定的序贯决策任务中进行持续基准测试，为正式验证日益强大的LLM奠定实践基础。
英文摘要：
We introduce a tool for rigorous and automated verification of large language model (LLM)- based policies in memoryless sequential decision-making tasks. Given a Markov decision process (MDP) representing the sequential decision-making task, an LLM policy, and a safety requirement expressed as a PCTL formula, our approach incrementally constructs only the reachable portion of the MDP guided by the LLM's chosen actions. Each state is encoded as a natural language prompt, the LLM's response is parsed into an action, and reachable successor states by the policy are expanded. The resulting formal model is checked with Storm to determine whether the policy satisfies the specified safety property. In experiments on standard grid world benchmarks, we show that open source LLMs accessed via Ollama can be verified when deterministically seeded, but generally underperform deep reinforcement learning baselines. Our tool natively integrates with Ollama and supports PRISM-specified tasks, enabling continuous benchmarking in user-specified sequential decision-making tasks and laying a practical foundation for formally verifying increasingly capable LLMs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
