Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking

• URL: http://arxiv.org/abs/2205.05398v3
• Date: Thu, 6 Apr 2023 10:53:49 GMT
• Title: Scalable Stochastic Parametric Verification with Stochastic Variational Smoothed Model Checking
• Authors: Luca Bortolussi, Francesca Cairoli, Ginevra Carbone, Paolo Pulcini
• Abstract summary: Smoothed model checking (smMC) aims at inferring the satisfaction function over the entire parameter space from a limited set of observations. In this paper, we exploit recent advances in probabilistic machine learning to push this limitation forward. We compare the performances of smMC against those of SV-smMC by looking at the scalability, the computational efficiency and the accuracy of the reconstructed satisfaction function.
• Score: 1.5293427903448025
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Parametric verification of linear temporal properties for stochastic models can be expressed as computing the satisfaction probability of a certain property as a function of the parameters of the model. Smoothed model checking (smMC) aims at inferring the satisfaction function over the entire parameter space from a limited set of observations obtained via simulation. As observations are costly and noisy, smMC is framed as a Bayesian inference problem so that the estimates have an additional quantification of the uncertainty. In smMC the authors use Gaussian Processes (GP), inferred by means of the Expectation Propagation algorithm. This approach provides accurate reconstructions with statistically sound quantification of the uncertainty. However, it inherits the well-known scalability issues of GP. In this paper, we exploit recent advances in probabilistic machine learning to push this limitation forward, making Bayesian inference of smMC scalable to larger datasets and enabling its application to models with high dimensional parameter spaces. We propose Stochastic Variational Smoothed Model Checking (SV-smMC), a solution that exploits stochastic variational inference (SVI) to approximate the posterior distribution of the smMC problem. The strength and flexibility of SVI make SV-smMC applicable to two alternative probabilistic models: Gaussian Processes (GP) and Bayesian Neural Networks (BNN). The core ingredient of SVI is a stochastic gradient-based optimization that makes inference easily parallelizable and that enables GPU acceleration. In this paper, we compare the performances of smMC against those of SV-smMC by looking at the scalability, the computational efficiency and the accuracy of the reconstructed satisfaction function.

Related papers

• Accelerated zero-order SGD under high-order smoothness and overparameterized regime [79.85163929026146]
  We present a novel gradient-free algorithm to solve convex optimization problems. Such problems are encountered in medicine, physics, and machine learning. We provide convergence guarantees for the proposed algorithm under both types of noise.
  arXiv  Detail & Related papers  (2024-11-21T10:26:17Z)
• Variational Bayesian surrogate modelling with application to robust design optimisation [0.9626666671366836]
  Surrogate models provide a quick-to-evaluate approximation to complex computational models. We consider Bayesian inference for constructing statistical surrogates with input uncertainties and dimensionality reduction. We demonstrate intrinsic and robust structural optimisation problems where cost functions depend on a weighted sum of the mean and standard deviation of model outputs.
  arXiv  Detail & Related papers  (2024-04-23T09:22:35Z)
• Online Variational Sequential Monte Carlo [49.97673761305336]
  We build upon the variational sequential Monte Carlo (VSMC) method, which provides computationally efficient and accurate model parameter estimation and Bayesian latent-state inference. Online VSMC is capable of performing efficiently, entirely on-the-fly, both parameter estimation and particle proposal adaptation.
  arXiv  Detail & Related papers  (2023-12-19T21:45:38Z)
• Monte Carlo Neural PDE Solver for Learning PDEs via Probabilistic Representation [59.45669299295436]
  We propose a Monte Carlo PDE solver for training unsupervised neural solvers. We use the PDEs' probabilistic representation, which regards macroscopic phenomena as ensembles of random particles. Our experiments on convection-diffusion, Allen-Cahn, and Navier-Stokes equations demonstrate significant improvements in accuracy and efficiency.
  arXiv  Detail & Related papers  (2023-02-10T08:05:19Z)
• Numerically Stable Sparse Gaussian Processes via Minimum Separation using Cover Trees [57.67528738886731]
  We study the numerical stability of scalable sparse approximations based on inducing points. For low-dimensional tasks such as geospatial modeling, we propose an automated method for computing inducing points satisfying these conditions.
  arXiv  Detail & Related papers  (2022-10-14T15:20:17Z)
• Information Theoretic Structured Generative Modeling [13.117829542251188]
  A novel generative model framework called the structured generative model (SGM) is proposed that makes straightforward optimization possible. The implementation employs a single neural network driven by an orthonormal input to a single white noise source adapted to learn an infinite Gaussian mixture model. Preliminary results show that SGM significantly improves MINE estimation in terms of data efficiency and variance, conventional and variational Gaussian mixture models, as well as for training adversarial networks.
  arXiv  Detail & Related papers  (2021-10-12T07:44:18Z)
• Structured Stochastic Gradient MCMC [20.68905354115655]
  We propose a new non-parametric variational approximation that makes no assumptions about the approximate posterior's functional form. We obtain better predictive likelihoods and larger effective sample sizes than full SGMCMC.
  arXiv  Detail & Related papers  (2021-07-19T17:18:10Z)
• Sinkhorn Natural Gradient for Generative Models [125.89871274202439]
  We propose a novel Sinkhorn Natural Gradient (SiNG) algorithm which acts as a steepest descent method on the probability space endowed with the Sinkhorn divergence. We show that the Sinkhorn information matrix (SIM), a key component of SiNG, has an explicit expression and can be evaluated accurately in complexity that scales logarithmically. In our experiments, we quantitatively compare SiNG with state-of-the-art SGD-type solvers on generative tasks to demonstrate its efficiency and efficacy of our method.
  arXiv  Detail & Related papers  (2020-11-09T02:51:17Z)
• An adaptive Hessian approximated stochastic gradient MCMC method [12.93317525451798]
  We present an adaptive Hessian approximated gradient MCMC method to incorporate local geometric information while sampling from the posterior. We adopt a magnitude-based weight pruning method to enforce the sparsity of the network.
  arXiv  Detail & Related papers  (2020-10-03T16:22:15Z)
• Improving Sampling Accuracy of Stochastic Gradient MCMC Methods via Non-uniform Subsampling of Gradients [54.90670513852325]
  We propose a non-uniform subsampling scheme to improve the sampling accuracy. EWSG is designed so that a non-uniform gradient-MCMC method mimics the statistical behavior of a batch-gradient-MCMC method. In our practical implementation of EWSG, the non-uniform subsampling is performed efficiently via a Metropolis-Hastings chain on the data index.
  arXiv  Detail & Related papers  (2020-02-20T18:56:18Z)

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.