Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models

• URL: http://arxiv.org/abs/2311.09793v2
• Date: Tue, 16 Apr 2024 12:51:47 GMT
• Title: Fossil 2.0: Formal Certificate Synthesis for the Verification and Control of Dynamical Models
• Authors: Alec Edwards, Andrea Peruffo, Alessandro Abate,
• Abstract summary: This paper presents Fossil 2.0, a new major release of a software tool for the synthesis of certificates. Fossil 2.0 is much improved from its original release, including new interfaces and a significantly expanded certificate portfolio.
• Score: 54.959571890098786
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper presents Fossil 2.0, a new major release of a software tool for the synthesis of certificates (e.g., Lyapunov and barrier functions) for dynamical systems modelled as ordinary differential and difference equations. Fossil 2.0 is much improved from its original release, including new interfaces, a significantly expanded certificate portfolio, controller synthesis and enhanced extensibility. We present these new features as part of this tool paper. Fossil implements a counterexample-guided inductive synthesis (CEGIS) loop ensuring the soundness of the method. Our tool uses neural networks as templates to generate candidate functions, which are then formally proven by an SMT solver acting as an assertion verifier. Improvements with respect to the first release include a wider range of certificates, synthesis of control laws, and support for discrete-time models.

Related papers

• CAR: Controllable Autoregressive Modeling for Visual Generation [100.33455832783416]
  Controllable AutoRegressive Modeling (CAR) is a novel, plug-and-play framework that integrates conditional control into multi-scale latent variable modeling. CAR progressively refines and captures control representations, which are injected into each autoregressive step of the pre-trained model to guide the generation process. Our approach demonstrates excellent controllability across various types of conditions and delivers higher image quality compared to previous methods.
  arXiv  Detail & Related papers  (2024-10-07T00:55:42Z)
• Random Features Approximation for Control-Affine Systems [6.067043299145924]
  We propose two novel classes of nonlinear feature representations which capture control affine structure. Our methods make use of random features (RF) approximations, inheriting the expressiveness of kernel methods at a lower computational cost.
  arXiv  Detail & Related papers  (2024-06-10T17:54:57Z)
• FAENet: Frame Averaging Equivariant GNN for Materials Modeling [123.19473575281357]
  We introduce a flexible framework relying on frameaveraging (SFA) to make any model E(3)-equivariant or invariant through data transformations. We prove the validity of our method theoretically and empirically demonstrate its superior accuracy and computational scalability in materials modeling.
  arXiv  Detail & Related papers  (2023-04-28T21:48:31Z)
• Controllable Text Generation with Neurally-Decomposed Oracle [91.18959622763055]
  We propose a framework to control auto-regressive generation models with NeurAlly-Decomposed Oracle (NADO) We present a closed-form optimal solution to incorporate the token-level guidance into the base model for controllable generation.
  arXiv  Detail & Related papers  (2022-05-27T20:17:53Z)
• Better Feature Integration for Named Entity Recognition [30.676768644145]
  We propose a simple and robust solution to incorporate both types of features with our Synergized-LSTM (Syn-LSTM) The results demonstrate that the proposed model achieves better performance than previous approaches while requiring fewer parameters.
  arXiv  Detail & Related papers  (2021-04-12T09:55:06Z)
• AILearn: An Adaptive Incremental Learning Model for Spoof Fingerprint Detection [12.676356746752893]
  Incremental learning enables the learner to accommodate new knowledge without retraining the existing model. We propose AILearn, a generic model for incremental learning which overcomes the stability-plasticity dilemma. We demonstrate the efficacy of the proposed AILearn model on spoof fingerprint detection application.
  arXiv  Detail & Related papers  (2020-12-29T07:26:37Z)
• Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models [70.70479436076238]
  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.
  arXiv  Detail & Related papers  (2020-07-07T07:39:42Z)
• Formal Synthesis of Lyapunov Neural Networks [61.79595926825511]
  We propose an automatic and formally sound method for synthesising Lyapunov functions. We employ a counterexample-guided approach where a numerical learner and a symbolic verifier interact to construct provably correct Lyapunov neural networks. Our method synthesises Lyapunov functions faster and over wider spatial domains than the alternatives, yet providing stronger or equal guarantees.
  arXiv  Detail & Related papers  (2020-03-19T17:21:02Z)

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.