What Are the Odds? Improving the foundations of Statistical Model Checking

• URL: http://arxiv.org/abs/2404.05424v1
• Date: Mon, 8 Apr 2024 11:47:46 GMT
• Title: What Are the Odds? Improving the foundations of Statistical Model Checking
• Authors: Tobias Meggendorfer, Maximilian Weininger, Patrick Wienhöft,
• Abstract summary: Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. Traditionally verification algorithms assume exact knowledge of the probabilities that govern the behaviour of an MDP. We propose specialised approaches that exploit our knowledge of the MDP.
• Score: 3.789219860006095
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Markov decision processes (MDPs) are a fundamental model for decision making under uncertainty. They exhibit non-deterministic choice as well as probabilistic uncertainty. Traditionally, verification algorithms assume exact knowledge of the probabilities that govern the behaviour of an MDP. As this assumption is often unrealistic in practice, statistical model checking (SMC) was developed in the past two decades. It allows to analyse MDPs with unknown transition probabilities and provide probably approximately correct (PAC) guarantees on the result. Model-based SMC algorithms sample the MDP and build a model of it by estimating all transition probabilities, essentially for every transition answering the question: ``What are the odds?'' However, so far the statistical methods employed by the state of the art SMC algorithms are quite naive. Our contribution are several fundamental improvements to those methods: On the one hand, we survey statistics literature for better concentration inequalities; on the other hand, we propose specialised approaches that exploit our knowledge of the MDP. Our improvements are generally applicable to many kinds of problem statements because they are largely independent of the setting. Moreover, our experimental evaluation shows that they lead to significant gains, reducing the number of samples that the SMC algorithm has to collect by up to two orders of magnitude.

Related papers

• Robust Counterfactual Inference in Markov Decision Processes [1.5197843979051473]
  Current approaches assume a specific causal model to make counterfactuals identifiable. We propose a novel non-parametric approach that computes tight bounds on counterfactual transition probabilities.
  arXiv  Detail & Related papers  (2025-02-19T13:56:20Z)
• A Probabilistic Perspective on Unlearning and Alignment for Large Language Models [48.96686419141881]
  We introduce the first formal probabilistic evaluation framework for Large Language Models (LLMs) Namely, we propose novel metrics with high probability guarantees concerning the output distribution of a model. Our metrics are application-independent and allow practitioners to make more reliable estimates about model capabilities before deployment.
  arXiv  Detail & Related papers  (2024-10-04T15:44:23Z)
• Learning Algorithms for Verification of Markov Decision Processes [20.5951492453299]
  We present a general framework for applying learning algorithms to the verification of Markov decision processes (MDPs) The presented framework focuses on probabilistic reachability, which is a core problem in verification.
  arXiv  Detail & Related papers  (2024-03-14T08:54:19Z)
• 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)
• Meta-Uncertainty in Bayesian Model Comparison [0.0]
  We propose a fully probabilistic framework for quantifying meta-uncertainty. We demonstrate the utility of the proposed method in the context of conjugate Bayesian regression, likelihood-based inference with Markov chain Monte Carlo, and simulation-based inference with neural networks.
  arXiv  Detail & Related papers  (2022-10-13T18:10:29Z)
• PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP [0.34410212782758043]
  We provide the first algorithm to compute mean payoff probably approximately correctly in unknown MDP. We do not require any knowledge of the state space, only a lower bound on the minimum transition probability. In addition to providing probably approximately correct (PAC) bounds for our algorithm, we also demonstrate its practical nature by running experiments on standard benchmarks.
  arXiv  Detail & Related papers  (2022-06-03T09:13:27Z)
• Robust Anytime Learning of Markov Decision Processes [8.799182983019557]
  In data-driven applications, deriving precise probabilities from limited data introduces statistical errors. Uncertain MDPs (uMDPs) do not require precise probabilities but instead use so-called uncertainty sets in the transitions. We propose a robust anytime-learning approach that combines a dedicated Bayesian inference scheme with the computation of robust policies.
  arXiv  Detail & Related papers  (2022-05-31T14:29:55Z)
• Sampling-Based Robust Control of Autonomous Systems with Non-Gaussian Noise [59.47042225257565]
  We present a novel planning method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP)
  arXiv  Detail & Related papers  (2021-10-25T06:18:55Z)
• Probabilistic Gradient Boosting Machines for Large-Scale Probabilistic Regression [51.770998056563094]
  Probabilistic Gradient Boosting Machines (PGBM) is a method to create probabilistic predictions with a single ensemble of decision trees. We empirically demonstrate the advantages of PGBM compared to existing state-of-the-art methods.
  arXiv  Detail & Related papers  (2021-06-03T08:32:13Z)
• 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)
• Density of States Estimation for Out-of-Distribution Detection [69.90130863160384]
  DoSE is the density of states estimator. We demonstrate DoSE's state-of-the-art performance against other unsupervised OOD detectors.
  arXiv  Detail & Related papers  (2020-06-16T16:06:25Z)

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.