Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes

• URL: http://arxiv.org/abs/2206.02169v1
• Date: Sun, 5 Jun 2022 13:03:34 GMT
• Title: Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes
• Authors: Maximilian Sch\"afeller and Mohammad Abdulaziz
• Abstract summary: We build on existing formalizations of probability theory to analyze the expected total reward criterion on infinite-horizon problems. Our developments formalize the Bellman equation and give conditions under which optimal policies exist. We show that our system can compete with and even outperform state-of-the-art systems.
• Score: 7.538482310185133
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We formally verify executable algorithms for solving Markov decision processes (MDPs) in the interactive theorem prover Isabelle/HOL. We build on existing formalizations of probability theory to analyze the expected total reward criterion on infinite-horizon problems. Our developments formalize the Bellman equation and give conditions under which optimal policies exist. Based on this analysis, we verify dynamic programming algorithms to solve tabular MDPs. We evaluate the formally verified implementations experimentally on standard problems and show they are practical. Furthermore, we show that, combined with efficient unverified implementations, our system can compete with and even outperform state-of-the-art systems.

Related papers

• On Policy Evaluation Algorithms in Distributional Reinforcement Learning [0.0]
  We introduce a novel class of algorithms to efficiently approximate the unknown return distributions in policy evaluation problems from distributional reinforcement learning (DRL) For a plain instance of our proposed class of algorithms we prove error bounds, both within Wasserstein and Kolmogorov--Smirnov distances. For return distributions having probability density functions the algorithms yield approximations for these densities; error bounds are given within supremum norm.
  arXiv  Detail & Related papers  (2024-07-19T10:06:01Z)
• Formally Verified Approximate Policy Iteration [11.602089225841633]
  We show how the formalized algorithm can be refined to an executable, verified implementation. The implementation is evaluated on benchmark problems to show its practicability. As part of the refinement, we develop verified software to certify Linear Programming solutions.
  arXiv  Detail & Related papers  (2024-06-11T15:07:08Z)
• Online POMDP Planning with Anytime Deterministic Guarantees [11.157761902108692]
  Planning under uncertainty can be mathematically formalized using partially observable Markov decision processes (POMDPs) Finding an optimal plan for POMDPs can be computationally expensive and is feasible only for small tasks. We derive a deterministic relationship between a simplified solution that is easier to obtain and the theoretically optimal one.
  arXiv  Detail & Related papers  (2023-10-03T04:40:38Z)
• Provably Efficient UCB-type Algorithms For Learning Predictive State Representations [55.00359893021461]
  The sequential decision-making problem is statistically learnable if it admits a low-rank structure modeled by predictive state representations (PSRs) This paper proposes the first known UCB-type approach for PSRs, featuring a novel bonus term that upper bounds the total variation distance between the estimated and true models. In contrast to existing approaches for PSRs, our UCB-type algorithms enjoy computational tractability, last-iterate guaranteed near-optimal policy, and guaranteed model accuracy.
  arXiv  Detail & Related papers  (2023-07-01T18:35:21Z)
• Making Linear MDPs Practical via Contrastive Representation Learning [101.75885788118131]
  It is common to address the curse of dimensionality in Markov decision processes (MDPs) by exploiting low-rank representations. We consider an alternative definition of linear MDPs that automatically ensures normalization while allowing efficient representation learning. We demonstrate superior performance over existing state-of-the-art model-based and model-free algorithms on several benchmarks.
  arXiv  Detail & Related papers  (2022-07-14T18:18:02Z)
• Identification of Unexpected Decisions in Partially Observable Monte-Carlo Planning: a Rule-Based Approach [78.05638156687343]
  We propose a methodology for analyzing POMCP policies by inspecting their traces. The proposed method explores local properties of policy behavior to identify unexpected decisions. We evaluate our approach on Tiger, a standard benchmark for POMDPs, and a real-world problem related to mobile robot navigation.
  arXiv  Detail & Related papers  (2020-12-23T15:09:28Z)
• Stein Variational Model Predictive Control [130.60527864489168]
  Decision making under uncertainty is critical to real-world, autonomous systems. Model Predictive Control (MPC) methods have demonstrated favorable performance in practice, but remain limited when dealing with complex distributions. We show that this framework leads to successful planning in challenging, non optimal control problems.
  arXiv  Detail & Related papers  (2020-11-15T22:36:59Z)
• Logistic Q-Learning [87.00813469969167]
  We propose a new reinforcement learning algorithm derived from a regularized linear-programming formulation of optimal control in MDPs. The main feature of our algorithm is a convex loss function for policy evaluation that serves as a theoretically sound alternative to the widely used squared Bellman error.
  arXiv  Detail & Related papers  (2020-10-21T17:14:31Z)
• Partial Policy Iteration for L1-Robust Markov Decision Processes [13.555107578858307]
  This paper describes new efficient algorithms for solving the common class of robust MDPs. We propose partial policy iteration, a new, efficient, flexible, and general policy iteration scheme for robust MDPs. Our experimental results indicate that the proposed methods are many orders of magnitude faster than the state-of-the-art approach.
  arXiv  Detail & Related papers  (2020-06-16T19:50:14Z)
• Planning in Markov Decision Processes with Gap-Dependent Sample Complexity [48.98199700043158]
  We propose MDP-GapE, a new trajectory-based Monte-Carlo Tree Search algorithm for planning in a Markov Decision Process. We prove an upper bound on the number of calls to the generative models needed for MDP-GapE to identify a near-optimal action with high probability.
  arXiv  Detail & Related papers  (2020-06-10T15:05:51Z)

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.