Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning

• URL: http://arxiv.org/abs/2605.14440v1
• Date: Thu, 14 May 2026 06:37:31 GMT
• Title: Synthesizing POMDP Policies: Sampling Meets Model-checking via Learning
• Abstract summary: POMDPs are the standard framework for decision-making under uncertainty.<n>While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications.<n>We propose a synthesis framework that integrates sampling, automata learning, and model-checking.
• Score: 2.375990942704781
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Too Correct to Learn: Reinforcement Learning on Saturated Reasoning Data [55.84428098924793]
  We propose Constrained Uniform Top-K Sampling (CUTS), a parameter-free decoding strategy enforcing structure-preserving exploration.<n>We integrate this into Mixed-CUTS, a training framework synergizing exploitative and exploratory rollouts to amplify intra-group advantage variance.<n> Notably, Mixed-CUTS improves Pass@1 accuracy on the challenging AIME25 benchmark by up to 15.1% over standard GRPO.
  arXiv  Detail & Related papers  (2026-04-20T16:43:28Z)
• Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking [4.064849471241967]
  This paper contributes the first approach to effectively compute robust policies subject to arbitrary structural constraints.<n> Experiments on a few hundred benchmarks demonstrate the feasibility for constrained and robust policy synthesis.
  arXiv  Detail & Related papers  (2025-11-11T10:28:42Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  We propose an end-to-end deep learning (DL) framework with low inference complexity for symbol-level precoding.<n>We show that the proposed framework captures substantial performance gains of optimal SLP, while achieving an approximately 80-times speedup over conventional methods.
  arXiv  Detail & Related papers  (2025-10-02T15:15:50Z)
• Step-Aware Policy Optimization for Reasoning in Diffusion Large Language Models [57.42778606399764]
  Diffusion language models (dLLMs) offer a promising, non-autoregressive paradigm for text generation.<n>Current reinforcement learning approaches often rely on sparse, outcome-based rewards.<n>We argue that this stems from a fundamental mismatch with the natural structure of reasoning.
  arXiv  Detail & Related papers  (2025-10-02T00:34:15Z)
• Efficient Solution and Learning of Robust Factored MDPs [57.2416302384766]
  Learning r-MDPs from interactions with an unknown environment enables the synthesis of robust policies with provable guarantees on performance.<n>We propose novel methods for solving and learning r-MDPs based on factored state representations.
  arXiv  Detail & Related papers  (2025-08-01T15:23:15Z)
• Control Synthesis in Partially Observable Environments for Complex Perception-Related Objectives [2.7038841665524846]
  This work studies the problem of synthesizing optimal policies for perception-related objectives in environments modeled by partially observable Markov decision processes.<n>Our solution is to transform the mboxsc-iLTL objectives into reachability objectives by constructing the product of the belief MDP and a deterministic finite automaton built from the sc-iLTL objective.<n>To overcome the scalability challenge due to the product, we introduce a Monte Carlo Tree Search (MCTS) method that converges in probability to the optimal policy.
  arXiv  Detail & Related papers  (2025-06-27T22:02:07Z)
• Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions [44.99833362998488]
  We develop an abstraction framework that can be used to solve this problem under various modeling assumptions. We use state-of-the-art verification techniques to compute an optimal policy on the iMDP with guarantees for satisfying the given specification. We then show that, by construction, we can refine this policy into a feedback controller for which these guarantees carry over to the dynamical model.
  arXiv  Detail & Related papers  (2023-11-16T11:03:54Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  We propose a method for synthesising controllers for Markov jump linear systems. Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
  arXiv  Detail & Related papers  (2022-12-01T17:36:30Z)
• Sample Complexity of Robust Reinforcement Learning with a Generative Model [0.0]
  We propose a model-based reinforcement learning (RL) algorithm for learning an $epsilon$-optimal robust policy. We consider three different forms of uncertainty sets, characterized by the total variation distance, chi-square divergence, and KL divergence. In addition to the sample complexity results, we also present a formal analytical argument on the benefit of using robust policies.
  arXiv  Detail & Related papers  (2021-12-02T18:55:51Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)
• Learning with Safety Constraints: Sample Complexity of Reinforcement Learning for Constrained MDPs [13.922754427601491]
  We characterize the relationship between safety constraints and the number of samples needed to ensure a desired level of accuracy. Our main finding is that compared to the best known bounds of the unconstrained regime, the sample of constrained RL algorithms are increased by a factor that is logarithmic in the number of constraints.
  arXiv  Detail & Related papers  (2020-08-01T18:17:08Z)
• Control as Hybrid Inference [62.997667081978825]
  We present an implementation of CHI which naturally mediates the balance between iterative and amortised inference. We verify the scalability of our algorithm on a continuous control benchmark, demonstrating that it outperforms strong model-free and model-based baselines.
  arXiv  Detail & Related papers  (2020-07-11T19:44:09Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.