Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice

TL;DR

This paper introduces a compositional methodology and a framework called Vehicle for verifying neuro-symbolic cyber-physical systems in various interactive theorem provers, enabling complex safety guarantees.

Contribution

It extends Vehicle to integrate with multiple theorem provers, facilitating the verification of neural components and infinite time-horizon safety proofs in a unified manner.

Findings

Successfully integrated Vehicle with Rocq, Isabelle/HOL, Agda, and Imandra.

Demonstrated infinite time-horizon safety proof for a cyber-physical system with neural controllers.

Verified safety of a medical device modeled as a continuous cyber-physical system.

Abstract

Formal verification of neuro-symbolic cyber-physical systems, such as drones, medical devices and robots, is complicated. Neural components must be trained to be optimal with respect to the available data as well as the safety specifications, and then verified using specialised solvers. Symbolic models of the "cyber" and "physical" behaviour of the system must be constructed and verified in interactive theorem provers (ITPs), often requiring mature mathematical libraries to reason about the interplay of discrete and continuous dynamics, preferably obtaining infinite time-horizon guarantees. Finally, the results of the two already challenging verification tasks need to be integrated into a single proof in a coherent and consistent way, whilst preserving deployability of the resulting model. In this paper we present a compositional methodology for constructing such proofs. The Vehicle framework provides a functional, domain-specific language for specifying, training, and verifying neural components. We extend Vehicle to allow integration with any ITP with minimal effort. First, we describe how Vehicle's standard bidirectional type checker can be reused to transpile neural specifications into an intermediate representation targeting multiple theorem provers. Second, we integrate Vehicle with Rocq, Isabelle/HOL, Agda and the industrial prover Imandra; and showcase a generic infinite time-horizon safety proof of a discrete cyber-physical system with a neural network controller in each ITP. Finally, we use the Mathematical Components libraries in Rocq to verify infinite time-horizon safety of a medical device, modelled as a continuous cyber-physical system with a neural controller. To our knowledge, this is the first result of this kind in a general purpose ITP; and a result that was only feasible thanks to the compositionality provided by Vehicle's functional interface.