# Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 9 of its 43 references that are in the map.
- First posted on arXiv 14 May 2026.

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

- [DESPOT: Online POMDP Planning with Regularization](https://mlsanity.com/paper/1609.03250/) (2016)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Enforcing Almost-Sure Reachability in POMDPs](https://mlsanity.com/paper/2007.00085/) (2020)
- [Verification of indefinite-horizon POMDPs](https://mlsanity.com/paper/2007.00102/) (2020)
- [Under-Approximating Expected Total Rewards in POMDPs](https://mlsanity.com/paper/2201.08772/) (2022)
- [Search and Explore: Symbiotic Policy Synthesis in POMDPs](https://mlsanity.com/paper/2305.14149/) (2023)
- [The Value Problem for Multiple-Environment MDPs with Parity Objective](https://mlsanity.com/paper/2504.15960/) (2025)
- [Learning Explainable and Better Performing Representations of POMDP Strategies](https://mlsanity.com/paper/2401.07656/) (2024)
- [Efficient Black-Box Checking via Model Checking with Strengthened Specifications](https://mlsanity.com/paper/2109.04656/) (2021)

## Abstract (arXiv)

Partially Observable Markov Decision Processes (POMDPs) are the standard framework for decision-making under uncertainty. While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications. Conversely, formal synthesis techniques provide correctness-by-construction but often struggle with scalability, as general POMDP synthesis is undecidable. To bridge this gap, we propose a synthesis framework that integrates sampling, automata learning, and model-checking. Inspired by Angluin's L^* algorithm, our approach utilizes sampling as a membership oracle and model-checking as an equivalence oracle. This enables the synthesis of finite-state controllers with formal guarantees, provided the sampling-induced policy is regular. We establish a relative completeness result for this framework. Experimental results from our prototypical implementation demonstrate that this method successfully solves threshold-safety problems that remain challenging for existing formal synthesis tools. We believe our algorithm serves as a valuable component in a portfolio approach to tackling the inherent difficulty of POMDP synthesis problems.