Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs
It addresses the verification problem for developers of neuro-symbolic programs, offering a general methodology to ensure safety, though it appears incremental as it builds on existing verification tools.
The paper tackles the challenge of verifying neuro-symbolic programs by introducing Vehicle, an intermediate language that bridges the embedding gap between neural and symbolic components, enabling formal verification of safety properties, as demonstrated by verifying a neural network-controlled autonomous car in a stochastic environment.
Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodology for verifying such programs is challenging due to both the number of different tools involved and the intricate interface between the ``neural'' and ``symbolic'' program components. In this paper we present a general decomposition of the neuro-symbolic verification problem into parts, and examine the problem of the embedding gap that occurs when one tries to combine proofs about the neural and symbolic components. To address this problem we then introduce Vehicle -- standing as an abbreviation for a ``verification condition language'' -- an intermediate programming language interface between machine learning frameworks, automated theorem provers, and dependently-typed formalisations of neuro-symbolic programs. Vehicle allows users to specify the properties of the neural components of neuro-symbolic programs once, and then safely compile the specification to each interface using a tailored typing and compilation procedure. We give a high-level overview of Vehicle's overall design, its interfaces and compilation & type-checking procedures, and then demonstrate its utility by formally verifying the safety of a simple autonomous car controlled by a neural network, operating in a stochastic environment with imperfect information.