Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Neural Proofs for Sound Verification and Control of Complex Systems

Alessandro Abate

TL;DR

The paper outlines a neural-proof framework for sound verification and control of complex CPS, integrating proof rules with certificates learned through inductive synthesis in a CEGIS loop. By leveraging neural networks to craft certificates and SMT checks to validate them, the approach aims to efficiently handle uncountable, stochastic, and partially observable dynamics, including black-box components. It positions neural proofs as an alternative to formal abstractions to mitigate state-space explosion, while connecting to established concepts like Lyapunov functions, barrier certificates, and invariants. The authors highlight current methods, potential benefits for CPS applications, and a roadmap of future work, including scalability, probabilistic guarantees, and expanded tooling.

Abstract

This informal contribution presents an ongoing line of research that is pursuing a new approach to the construction of sound proofs for the formal verification and control of complex stochastic models of dynamical systems, of reactive programs and, more generally, of models of Cyber-Physical Systems. Neural proofs are made up of two key components: 1) proof rules encode requirements entailing the verification of general temporal specifications over the models of interest; and 2) certificates that discharge such rules, namely they are constructed from said proof rules with an inductive (that is, cyclic, repetitive) approach; this inductive approach involves: 2a) accessing samples from the model's dynamics and accordingly training neural networks, whilst 2b) generalising such networks via SAT-modulo-theory (SMT) queries that leverage the full knowledge of the models. In the context of sequential decision making problems over complex stochastic models, it is possible to additionally generate provably-correct policies/strategies/controllers, namely state-feedback functions that, in conjunction with neural certificates, formally attain the given specifications for the models of interest.

Neural Proofs for Sound Verification and Control of Complex Systems

TL;DR

The paper outlines a neural-proof framework for sound verification and control of complex CPS, integrating proof rules with certificates learned through inductive synthesis in a CEGIS loop. By leveraging neural networks to craft certificates and SMT checks to validate them, the approach aims to efficiently handle uncountable, stochastic, and partially observable dynamics, including black-box components. It positions neural proofs as an alternative to formal abstractions to mitigate state-space explosion, while connecting to established concepts like Lyapunov functions, barrier certificates, and invariants. The authors highlight current methods, potential benefits for CPS applications, and a roadmap of future work, including scalability, probabilistic guarantees, and expanded tooling.

Abstract

This informal contribution presents an ongoing line of research that is pursuing a new approach to the construction of sound proofs for the formal verification and control of complex stochastic models of dynamical systems, of reactive programs and, more generally, of models of Cyber-Physical Systems. Neural proofs are made up of two key components: 1) proof rules encode requirements entailing the verification of general temporal specifications over the models of interest; and 2) certificates that discharge such rules, namely they are constructed from said proof rules with an inductive (that is, cyclic, repetitive) approach; this inductive approach involves: 2a) accessing samples from the model's dynamics and accordingly training neural networks, whilst 2b) generalising such networks via SAT-modulo-theory (SMT) queries that leverage the full knowledge of the models. In the context of sequential decision making problems over complex stochastic models, it is possible to additionally generate provably-correct policies/strategies/controllers, namely state-feedback functions that, in conjunction with neural certificates, formally attain the given specifications for the models of interest.

Paper Structure

This paper contains 8 sections, 1 figure.

Table of Contents

  1. Models of Cyber-Physical Systems
  2. Model Analysis: Verification and Control Synthesis
  3. Lateral discussion - Formal Abstractions for Verification and Control Synthesis
  4. Neural Proofs
  5. Proof Rules
  6. Construction of Proof Certificates
  7. Neural Proofs and Certificates for Models of CPS
  8. Desiderata for Future Work on Neural Proofs

Figures (1)

  • Figure 1: An inductive synthesis architecture, including a Learner (top block) and a Verifier (bottom), which in particular can be implemented as the known counterexample-guided inductive synthesis (CEGIS).