Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models

• URL: http://arxiv.org/abs/2007.03251v2
• Date: Mon, 19 Oct 2020 13:27:10 GMT
• Title: Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models
• Authors: Andrea Peruffo, Daniele Ahmed, Alessandro Abate
• Abstract summary: We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) The approach is underpinned by an inductive framework, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate's validity or generates counter-examples. The outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine.
• Score: 70.70479436076238
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce an automated, formal, counterexample-based approach to synthesise Barrier Certificates (BC) for the safety verification of continuous and hybrid dynamical models. The approach is underpinned by an inductive framework: this is structured as a sequential loop between a learner, which manipulates a candidate BC structured as a neural network, and a sound verifier, which either certifies the candidate's validity or generates counter-examples to further guide the learner. We compare the approach against state-of-the-art techniques, over polynomial and non-polynomial dynamical models: the outcomes show that we can synthesise sound BCs up to two orders of magnitude faster, with in particular a stark speedup on the verification engine (up to five orders less), whilst needing a far smaller data set (up to three orders less) for the learning part. Beyond improvements over the state of the art, we further challenge the new approach on a hybrid dynamical model and on larger-dimensional models, and showcase the numerical robustness of our algorithms and codebase.

Related papers

• On the Trade-off Between Efficiency and Precision of Neural Abstraction [62.046646433536104]
  Neural abstractions have been recently introduced as formal approximations of complex, nonlinear dynamical models. We employ formal inductive synthesis procedures to generate neural abstractions that result in dynamical models with these semantics.
  arXiv  Detail & Related papers  (2023-07-28T13:22:32Z)
• Dynamic Mixed Membership Stochastic Block Model for Weighted Labeled Networks [3.5450828190071655]
  A new family of Mixed Membership Block Models (MMSBM) allows to model static labeled networks under the assumption of mixed-membership clustering. We show that our method significantly differs from existing approaches, and allows to model more complex systems --dynamic labeled networks.
  arXiv  Detail & Related papers  (2023-04-12T15:01:03Z)
• ConCerNet: A Contrastive Learning Based Framework for Automated Conservation Law Discovery and Trustworthy Dynamical System Prediction [82.81767856234956]
  This paper proposes a new learning framework named ConCerNet to improve the trustworthiness of the DNN based dynamics modeling. We show that our method consistently outperforms the baseline neural networks in both coordinate error and conservation metrics.
  arXiv  Detail & Related papers  (2023-02-11T21:07:30Z)
• Neural Abstractions [72.42530499990028]
  We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. We demonstrate that our approach performs comparably to the mature tool Flow* on existing benchmark nonlinear models.
  arXiv  Detail & Related papers  (2023-01-27T12:38:09Z)
• Evolve Smoothly, Fit Consistently: Learning Smooth Latent Dynamics For Advection-Dominated Systems [14.553972457854517]
  We present a data-driven, space-time continuous framework to learn surrogatemodels for complex physical systems. We leverage the expressive power of the network and aspecially designed consistency-inducing regularization to obtain latent trajectories that are both low-dimensional and smooth.
  arXiv  Detail & Related papers  (2023-01-25T03:06:03Z)
• Dynamically-Scaled Deep Canonical Correlation Analysis [77.34726150561087]
  Canonical Correlation Analysis (CCA) is a method for feature extraction of two views by finding maximally correlated linear projections of them. We introduce a novel dynamic scaling method for training an input-dependent canonical correlation model.
  arXiv  Detail & Related papers  (2022-03-23T12:52:49Z)
• Contrastively Disentangled Sequential Variational Autoencoder [20.75922928324671]
  We propose a novel sequence representation learning method, named Contrastively Disentangled Sequential Variational Autoencoder (C-DSVAE) We use a novel evidence lower bound which maximizes the mutual information between the input and the latent factors, while penalizes the mutual information between the static and dynamic factors. Our experiments show that C-DSVAE significantly outperforms the previous state-of-the-art methods on multiple metrics.
  arXiv  Detail & Related papers  (2021-10-22T23:00:32Z)
• The Role of Isomorphism Classes in Multi-Relational Datasets [6.419762264544509]
  We show that isomorphism leakage overestimates performance in multi-relational inference. We propose isomorphism-aware synthetic benchmarks for model evaluation. We also demonstrate that isomorphism classes can be utilised through a simple prioritisation scheme.
  arXiv  Detail & Related papers  (2020-09-30T12:15:24Z)
• Forecasting Sequential Data using Consistent Koopman Autoencoders [52.209416711500005]
  A new class of physics-based methods related to Koopman theory has been introduced, offering an alternative for processing nonlinear dynamical systems. We propose a novel Consistent Koopman Autoencoder model which, unlike the majority of existing work, leverages the forward and backward dynamics. Key to our approach is a new analysis which explores the interplay between consistent dynamics and their associated Koopman operators.
  arXiv  Detail & Related papers  (2020-03-04T18:24:30Z)

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.