Neural Proofs for Sound Verification and Control of Complex Systems

TL;DR

This paper introduces neural proofs as a novel method for sound verification and control of complex stochastic models, combining proof rules, neural network training, and SMT-based generalization to ensure formal correctness.

Contribution

It proposes a new neural proof framework that integrates inductive neural network training and SMT queries for formal verification and control of complex systems.

Findings

Neural proofs enable formal verification of complex stochastic models.

The approach can generate provably-correct policies for decision-making.

Combines neural network training with logical reasoning for sound proofs.

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.