用形式化方法验证大模型在无记忆决策任务中的安全行为
Verifying Memoryless Sequential Decision-making of Large Language Models
- 基于强化学习框架构建可验证的决策模型，仅扩展大模型实际可达状态
- 在网格世界任务中，确定性种子下开源大模型可被验证，但性能低于深度强化学习
- 支持Ollama和PRISM，适合关注大模型安全性的研究人员和开发者
我们提出一种工具，用于在无记忆的序列决策任务中对基于大语言模型（LLM）的策略进行严格且自动化的验证。给定表示决策任务的马尔可夫决策过程（MDP）、LLM策略以及以PCTL公式表达的安全需求，该方法在LLM所选动作引导下，增量式构建仅可达的MDP部分。每个状态以自然语言提示编码，LLM响应解析为动作，并拓展其可达后继状态。生成的形式化模型通过Storm验证是否满足指定安全属性。在标准网格世界基准测试中，我们发现通过Ollama调用的开源大模型在确定性种子下可被验证，但整体表现普遍弱于深度强化学习基线。该工具原生集成Ollama并支持PRISM定义的任务，可在用户自定义的序列决策任务中实现持续评测，为日益强大的大模型提供形式化验证的实用基础。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。