Neural Network Verification is a Programming Language Challenge

TL;DR

This work reframes neural network verification as a programming-language challenge, arguing that robust properties cannot be guaranteed without language-level specifications and integrated backends. It surveys the current state, including ONNX-based representations and VNN-LIB-style queries, and highlights critical gaps: the Embedding Gap between problem-space and embedding-space, and the Implementation Gap arising from architecture translation, numerical types, non-determinism, and quantisation. The authors discuss prototypes like CAISAR and Vehicle that advance higher-level specification languages and emphasize the need for a unified dependently-typed language and formal interfaces to connect ML pipelines with verification tooling. The paper envisions a future where a single expressive language can encode training, specification, and verification, with proof-carrying modules and certified checkers, significantly impacting safety-critical ML systems and cyber-physical systems through rigorous, machine-checked guarantees.

Abstract

Neural network verification is a new and rapidly developing field of research. So far, the main priority has been establishing efficient verification algorithms and tools, while proper support from the programming language perspective has been considered secondary or unimportant. Yet, there is mounting evidence that insights from the programming language community may make a difference in the future development of this domain. In this paper, we formulate neural network verification challenges as programming language challenges and suggest possible future solutions.

Figures (8)

• Figure 1: Schematic representation of the state of the art in training and verifying neural networks for properties. Solid lines denote methods widely accepted by the research communities, dashed lines mean "some experimental prototypes exist", dotted arrows mean the connection is desired but not established.
• Figure 2: Schematic representation of the neural network verification pipeline.
• Figure 3: Snippet of robustness specification in VNN-Lib for an image data set that has input of dimension $792$ and $10$ classes. The specification assumes an external definition of $f^*: \mathbb{R}^{792} \to \mathbb{R}^{10}$.
• Figure 4: An extract from a local robustness specification in CAISAR and Vehicle's input languages for the same image dataset described in Fig. \ref{['fig:spec']}. Note the ability to reuse predicates and definitions, the conciseness of vector-based operations, and the explicit data set bindings.
• Figure 5: Schematic representation of the embedding gap.