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.

翻译：传统软件的形式化验证已因Dafny和F*等面向验证的语言而发生革命性变化，这些语言使开发者能够编写可自动编译为底层SMT-LIB查询的高级规范。相比之下，神经网络验证目前缺乏此类基础设施，用户通常需要以接近底层VNN-LIB查询格式的形式表达需求。这一差距持续存在是因为相较于面向SMT-LIB，面向VNN-LIB存在独特的算法挑战：VNN-LIB仅限于表示网络输入输出的固定有限变量集，且即使是玩具神经网络规范也包含极大量的变量。本文提出首个将高级神经网络规范编译为优化VNN-LIB查询的算法。该算法具有数值可靠性，并支持比现有工具更丰富的逻辑片段，包括变量变换、一阶量词，以及涉及多个网络或同一网络多次应用的规范。我们在Vehicle框架内实现了该算法，并证明其对基准规范具有渐进最优性能。