VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification

TL;DR

VNN-LIB 2.0 establishes a rigorous theoretical foundation for neural network verification, addressing previous limitations by defining a formal syntax, semantics, and type system, and ensuring consistency through mechanization in Agda.

Contribution

It introduces the concept of network theory to abstractly define a semantic interface, enabling VNN-LIB to be independent of specific model formats and compatible with evolving representations.

Findings

Developed a formal syntax and semantics for VNN-LIB 2.0

Introduced network theory as an abstraction layer

Mechanized the standard in Agda for internal consistency

Abstract

Neural network verification is an active and rapidly maturing research area, with a growing ecosystem of solvers and tools. The VNN-LIB standard was introduced to support interoperability in this ecosystem, but Version~1.0 has several serious short-comings as a formal foundation: it lacks a precise syntax, semantics, and type system, offers limited expressivity, and relies on externally defined ONNX models whose semantics are informal and constantly evolving. The latter distinguishes VNN-LIB from established standards such as SMT-LIB, where queries are self-contained and have fixed semantics. In this paper we address these challenges by developing the theoretical foundations of VNN-LIB~2.0. Our key contribution is the introduction of the notion of a \emph{network theory}, which abstractly characterises the minimal semantic interface required from a neural network model format. This abstraction enables VNN-LIB to be defined independently of any specific ONNX version while remaining compatible with evolving model representations. Building on this foundation, we present a formal syntax for a more expressive query language, a type system for it over the numeric domains provided by the network theory, and finally a formal semantics. To ensure internal consistency, the standard is mechanised in the Agda theorem prover. VNN-LIB~2.0 therefore provides robust and rigorous foundations for trustworthy neural network verification.