Compiling High-Level Neural Network Specifications into VNN-LIB Queries

The formal verification of traditional software has been revolutionised by verification-orientated languages such as Dafny and F* which enable developers to write high-level specifications that are automatically compiled down to low-level SMT-LIB queries. In contrast, neural network verification currently lacks such infrastructure, often requiring users to express requirements in formats close to the low-level VNN-LIB query format. This gap persists because targeting VNN-LIB presents unique algorithmic challenges when compared to targeting SMT-LIB: VNN-LIB is restricted to a fixed finite set of variables representing the input and outputs of the network, and even toy neural network specifications have an extremely large number of variables. In this paper, we present the first algorithm for compiling high-level neural network specifications into optimised VNN-LIB queries. Our algorithm is numerically sound and supports a far rich logical fragment than existing tools, including transformations of variables, first-class quantifiers, and specifications involving multiple networks or multiple applications of the same network. We implement this algorithm within the Vehicle framework and demonstrate that its performance is asymptotically optimal for benchmark specifications.