Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification

• URL: http://arxiv.org/abs/2407.21029v1
• Date: Mon, 15 Jul 2024 11:49:44 GMT
• Title: Data-Driven Abstractions via Binary-Tree Gaussian Processes for Formal Verification
• Authors: Oliver Schön, Shammakh Naseer, Ben Wooding, Sadegh Soudjani,
• Abstract summary: abstraction-based solutions based on Gaussian process (GP) regression have become popular for their ability to learn a representation of the latent system from data with a quantified error. We show that the binary-tree Gaussian process (BTGP) allows us to construct an interval Markov chain model of the unknown system. We provide a delocalized error quantification via a unified formula even when the true dynamics do not live in the function space of the BTGP.
• Score: 0.22499166814992438
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: To advance formal verification of stochastic systems against temporal logic requirements for handling unknown dynamics, researchers have been designing data-driven approaches inspired by breakthroughs in the underlying machine learning techniques. As one promising research direction, abstraction-based solutions based on Gaussian process (GP) regression have become popular for their ability to learn a representation of the latent system from data with a quantified error. Results obtained based on this model are then translated to the true system via various methods. In a recent publication, GPs using a so-called binary-tree kernel have demonstrated a polynomial speedup w.r.t. the size of the data compared to their vanilla version, outcompeting all existing sparse GP approximations. Incidentally, the resulting binary-tree Gaussian process (BTGP) is characteristic for its piecewise-constant posterior mean and covariance functions, naturally abstracting the input space into discrete partitions. In this paper, we leverage this natural abstraction of the BTGP for formal verification, eliminating the need for cumbersome abstraction and error quantification procedures. We show that the BTGP allows us to construct an interval Markov chain model of the unknown system with a speedup that is polynomial w.r.t. the size of the abstraction compared to alternative approaches. We provide a delocalized error quantification via a unified formula even when the true dynamics do not live in the function space of the BTGP. This allows us to compute upper and lower bounds on the probability of satisfying reachability specifications that are robust to both aleatoric and epistemic uncertainties.

Related papers

• Conditionally-Conjugate Gaussian Process Factor Analysis for Spike Count Data via Data Augmentation [8.114880112033644]
  Recently, GPFA has been extended to model spike count data. We propose a conditionally-conjugate Gaussian process factor analysis (ccGPFA) resulting in both analytically and computationally tractable inference.
  arXiv  Detail & Related papers  (2024-05-19T21:53:36Z)
• Data-driven Modeling and Inference for Bayesian Gaussian Process ODEs via Double Normalizing Flows [28.62579476863723]
  We introduce normalizing flows to re parameterize the ODE vector field, resulting in a data-driven prior distribution. We also apply normalizing flows to the posterior inference of GP ODEs to resolve the issue of strong mean-field assumptions. We validate the effectiveness of our approach on simulated dynamical systems and real-world human motion data.
  arXiv  Detail & Related papers  (2023-09-17T09:28:47Z)
• Score-based Diffusion Models in Function Space [140.792362459734]
  Diffusion models have recently emerged as a powerful framework for generative modeling. We introduce a mathematically rigorous framework called Denoising Diffusion Operators (DDOs) for training diffusion models in function space. We show that the corresponding discretized algorithm generates accurate samples at a fixed cost independent of the data resolution.
  arXiv  Detail & Related papers  (2023-02-14T23:50:53Z)
• FaDIn: Fast Discretized Inference for Hawkes Processes with General Parametric Kernels [82.53569355337586]
  This work offers an efficient solution to temporal point processes inference using general parametric kernels with finite support. The method's effectiveness is evaluated by modeling the occurrence of stimuli-induced patterns from brain signals recorded with magnetoencephalography (MEG) Results show that the proposed approach leads to an improved estimation of pattern latency than the state-of-the-art.
  arXiv  Detail & Related papers  (2022-10-10T12:35:02Z)
• Formal Verification of Unknown Dynamical Systems via Gaussian Process Regression [11.729744197698718]
  Leveraging autonomous systems in safety-critical scenarios requires verifying their behaviors in the presence of uncertainties. We develop a framework for verifying discrete-time dynamical systems with unmodelled dynamics and noisy measurements.
  arXiv  Detail & Related papers  (2021-12-31T05:10:05Z)
• Inverting brain grey matter models with likelihood-free inference: a tool for trustable cytoarchitecture measurements [62.997667081978825]
  characterisation of the brain grey matter cytoarchitecture with quantitative sensitivity to soma density and volume remains an unsolved challenge in dMRI. We propose a new forward model, specifically a new system of equations, requiring a few relatively sparse b-shells. We then apply modern tools from Bayesian analysis known as likelihood-free inference (LFI) to invert our proposed model.
  arXiv  Detail & Related papers  (2021-11-15T09:08:27Z)
• Non-Gaussian Gaussian Processes for Few-Shot Regression [71.33730039795921]
  We propose an invertible ODE-based mapping that operates on each component of the random variable vectors and shares the parameters across all of them. NGGPs outperform the competing state-of-the-art approaches on a diversified set of benchmarks and applications.
  arXiv  Detail & Related papers  (2021-10-26T10:45:25Z)
• Bayesian inference of ODEs with Gaussian processes [17.138448665454373]
  We propose a novel Bayesian nonparametric model that uses Gaussian processes to infer posteriors of unknown ODE systems directly from data. We derive sparse variational inference with decoupled functional sampling to represent vector field posteriors. The method demonstrates the benefit of computing vector field posteriors, with predictive uncertainty scores outperforming alternative methods on multiple ODE learning tasks.
  arXiv  Detail & Related papers  (2021-06-21T08:09:17Z)
• Probabilistic Numeric Convolutional Neural Networks [80.42120128330411]
  Continuous input signals like images and time series that are irregularly sampled or have missing values are challenging for existing deep learning methods. We propose Probabilistic Convolutional Neural Networks which represent features as Gaussian processes (GPs) We then define a convolutional layer as the evolution of a PDE defined on this GP, followed by a nonlinearity. In experiments we show that our approach yields a $3times$ reduction of error from the previous state of the art on the SuperPixel-MNIST dataset and competitive performance on the medical time2012 dataset PhysioNet.
  arXiv  Detail & Related papers  (2020-10-21T10:08:21Z)
• Weak SINDy For Partial Differential Equations [0.0]
  We extend our Weak SINDy (WSINDy) framework to the setting of partial differential equations (PDEs) The elimination of pointwise derivative approximations via the weak form enables effective machine-precision recovery of model coefficients from noise-free data. We demonstrate WSINDy's robustness, speed and accuracy on several challenging PDEs.
  arXiv  Detail & Related papers  (2020-07-06T16:03:51Z)
• The data-driven physical-based equations discovery using evolutionary approach [77.34726150561087]
  We describe the algorithm for the mathematical equations discovery from the given observations data. The algorithm combines genetic programming with the sparse regression. It could be used for governing analytical equation discovery as well as for partial differential equations (PDE) discovery.
  arXiv  Detail & Related papers  (2020-04-03T17:21:57Z)

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.