# Verifying Memoryless Sequential Decision-making of Large Language Models

arXiv: https://arxiv.org/abs/2510.06756 · HTML: https://mlsanity.com/paper/2510.06756/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 26 of its 42 references that are in the map.
- First posted on arXiv 8 Oct 2025.

## Builds on (most cited first, 26 of 26)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [Mistral 7B](https://mlsanity.com/paper/2310.06825/) (2023)
- [Avalon's Game of Thoughts: Battle Against Deception through Recursive Contemplation](https://mlsanity.com/paper/2310.01320/) (2023)
- [A Survey of Safety and Trustworthiness of Large Language Models through the Lens of Verification and Validation](https://mlsanity.com/paper/2305.11391/) (2023)
- [MindAgent: Emergent Gaming Interaction](https://mlsanity.com/paper/2309.09971/) (2023)
- [Robustness Verification for Transformers](https://mlsanity.com/paper/2002.06622/) (2020)
- [A Review of Prominent Paradigms for LLM-Based Agents: Tool Use (Including RAG), Planning, and Feedback Learning](https://mlsanity.com/paper/2406.05804/) (2024)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [An Inductive Synthesis Framework for Verifiable Reinforcement Learning](https://mlsanity.com/paper/1907.07273/) (2019)
- [Provably safe systems: the only path to controllable AGI](https://mlsanity.com/paper/2309.01933/) (2023)
- [Playing Atari Games with Deep Reinforcement Learning and Human Checkpoint Replay](https://mlsanity.com/paper/1607.05077/) (2016)
- [VeriPlan: Integrating Formal Verification and LLMs into End-User Planning](https://mlsanity.com/paper/2502.17898/) (2025)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [Self-Generated In-Context Examples Improve LLM Agents for Sequential Decision-Making Tasks](https://mlsanity.com/paper/2505.00234/) (2025)
- [The King is Naked: on the Notion of Robustness for Natural Language Processing](https://mlsanity.com/paper/2112.07605/) (2021)
- [Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning](https://mlsanity.com/paper/2004.00273/) (2020)
- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Meta-Prompt Optimization for LLM-Based Sequential Decision Making](https://mlsanity.com/paper/2502.00728/) (2025)
- [UNO Arena for Evaluating Sequential Decision-Making Capability of Large Language Models](https://mlsanity.com/paper/2406.16382/) (2024)
- [Communication and Control Co-Design in 6G: Sequential Decision-Making with LLMs](https://mlsanity.com/paper/2407.06227/) (2024)
- [Enhancing RL Safety with Counterfactual LLM Reasoning](https://mlsanity.com/paper/2409.10188/) (2024)
- [Are Transformers More Robust? Towards Exact Robustness Verification for Transformers](https://mlsanity.com/paper/2202.03932/) (2022)
- [Probabilistic Model Checking of Stochastic Reinforcement Learning Policies](https://mlsanity.com/paper/2403.18725/) (2024)
- [Co-Activation Graph Analysis of Safety-Verified and Explainable Deep Reinforcement Learning Policies](https://mlsanity.com/paper/2501.03142/) (2025)

## Built on by (most cited first, 1 of 1)

- [Automated Testing of LLM-Based Post Hoc Explainers Using Model Checking as an Oracle](https://mlsanity.com/paper/2608.30581/) (2026)

## Abstract (arXiv)

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.