Formal verification of dynamical models via neural synthesis

Thesis

Dynamical models are a mathematical tool for representing, understanding, and analysing complex systems that are ubiquitous across science and engineering. Complexity and nonlinearity in these systems result in a lack of analytical solutions and challenging, or even intractable, analysis in view of safety-critical applications. Effective methodologies for the verification of behaviours of dynamical models are therefore of great importance, and their effectiveness is often determined by their ability to handle nonlinearity. This thesis studies two alternative approaches to verifying continuous-time nonlinear dynamical models: abstraction, which directly disregards nonlinearity, and indirect certificate-based approaches, which indirectly handle nonlinearity. The strength of neural networks as universal approximators has seen widespread interest from the formal verification community. Commonly, this is in the context of verifying machine learning models themselves. Conversely, this thesis explores the use of neural networks as a tool for verification, in particular for dynamical models. In particular, we introduce a novel approach for abstracting nonlinear dynamical models via neural networks, and contribute to growing literature which leverages neural networks as certificates for specifications of dynamical models. For the former, we demonstrate that these abstractions, which we call neural abstractions, can be used to verify safety properties of nonlinear dynamical models. For the latter, we demonstrate that neural networks may be used in conjunction with neural-based controllers to ensure controlled dynamical models satisfy a range of specifications. Both approaches require a formal synthesis procedure to construct neural networks which satisfy required properties. We utilise counterexample-guided inductive synthesis (CEGIS) to this end, in which neural networks are employed as approximators alongside solvers for satisfiability modulo theories to provide formal guarantees of correctness. We demonstrate that this synthesis approach is effective for both abstractions and certificates. Through a range of experimental case studies, we demonstrate that the use of neural networks in both abstraction and certificate function synthesis is a flexible, effective approach to verifying nonlinear dynamical models.

Authors: Edwards, A

• DOI: 10.5287/ora-j1m8g9jvw
• Type of award: DPhil
• Level of award: Doctoral
• Awarding institution: University of Oxford
• Language: English
• Keywords: dynamical models; formal verification; machine learning; neural networks; SMT-solvers
• Subjects: Machine learning; Differentiable dynamical systems; Formal methods (computer science)