VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification

• URL: http://arxiv.org/abs/2605.07451v1
• Date: Fri, 08 May 2026 08:56:59 GMT
• Title: VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification
• Abstract summary: We introduce the notion of a emphnetwork theory, which abstractly characterises the minimal semantic interface required from a neural network model format.<n>We then 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.<n>VNN-LIB2.0 therefore provides robust and rigorous foundations for trustworthy neural network verification.
• Score: 1.0499611180329804
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• SABER: A Semantic-Aligned Brain Network Analysis Framework via Multi-scale Hypergraphs [2.525239819116781]
  Brain disease diagnosis requires synergy of brain connectivity patterns and high-level semantic knowledge.<n>Existing methods treat semantics from large language models (LLMs) as auxiliary features or supervision.<n>We propose a semantic-aligned brain network framework that actively integrates LLM-derived semantics into the prediction process.
  arXiv  Detail & Related papers  (2026-07-02T08:58:47Z)
• Native Explainability for Bayesian Confidence Propagation Neural Networks: A Framework for Trusted Brain-Like AI [0.3013679260442808]
  No systematic framework exists for explaining BCPNN decisions.<n>BCPNN is an inherently transparent model whose architectural primitives map directly onto established explainable-AI (XAI) families.<n>We propose the first XAI taxonomy for BCPNN. It maps weights, biases, hypercolumn posteriors, structural-plasticity usage scores, attractor dynamics, and input-reconstruction populations onto attribution, prototype, concept, counterfactual, and mechanistic explanation modalities.
  arXiv  Detail & Related papers  (2026-05-12T06:21:19Z)
• Talking with Verifiers: Automatic Specification Generation for Neural Network Verification [5.883923958146327]
  We introduce a novel component to the verification pipeline, making existing verification tools applicable to a broader range of domains and specification styles.<n>Our framework enables users to formulate specifications in natural language, which are then automatically analyzed and translated into formal verification queries compatible with state-of-the-art neural network verifiers.<n>Our results show that this translation process maintains high fidelity to user intent while incurring low computational overhead, thereby substantially extending the applicability of formal verification to real-world, high-level requirements.
  arXiv  Detail & Related papers  (2026-02-13T09:36:40Z)
• A Constructive Framework for Nondeterministic Automata via Time-Shared, Depth-Unrolled Feedforward Networks [0.0]
  We present a formal and constructive simulation framework for nondeterministic finite automata (NFAs) using time-shared, depth-unrolled feedforward networks (TS-FFNs)<n>Our formulation symbolically encodes automaton states as binary vectors, transitions as sparse matrix transformations, and nondeterministic branching-including $varepsilon$-closures-as compositions of shared thresholded updates.
  arXiv  Detail & Related papers  (2025-05-30T01:18:35Z)
• Noise Sensitivity and Stability of Deep Neural Networks for Binary Classification [0.9438207505148947]
  We ask if certain sequences of Boolean functions represented by common DNN models are noise sensitive or noise stable. Due to the natural randomness in DNN models, these concepts are extended to annealed and quenched versions. We investigate the properties of two standard DNN architectures, the fully connected and convolutional models, when initiated with Gaussian weights.
  arXiv  Detail & Related papers  (2023-08-18T08:09:31Z)
• Robust Training and Verification of Implicit Neural Networks: A Non-Euclidean Contractive Approach [64.23331120621118]
  This paper proposes a theoretical and computational framework for training and robustness verification of implicit neural networks. We introduce a related embedded network and show that the embedded network can be used to provide an $ell_infty$-norm box over-approximation of the reachable sets of the original network. We apply our algorithms to train implicit neural networks on the MNIST dataset and compare the robustness of our models with the models trained via existing approaches in the literature.
  arXiv  Detail & Related papers  (2022-08-08T03:13:24Z)
• Neuro-Symbolic Artificial Intelligence (AI) for Intent based Semantic Communication [85.06664206117088]
  6G networks must consider semantics and effectiveness (at end-user) of the data transmission. NeSy AI is proposed as a pillar for learning causal structure behind the observed data. GFlowNet is leveraged for the first time in a wireless system to learn the probabilistic structure which generates the data.
  arXiv  Detail & Related papers  (2022-05-22T07:11:57Z)
• Interpretable part-whole hierarchies and conceptual-semantic relationships in neural networks [4.153804257347222]
  We present Agglomerator, a framework capable of providing a representation of part-whole hierarchies from visual cues. We evaluate our method on common datasets, such as SmallNORB, MNIST, FashionMNIST, CIFAR-10, and CIFAR-100.
  arXiv  Detail & Related papers  (2022-03-07T10:56:13Z)
• Self-Ensembling GAN for Cross-Domain Semantic Segmentation [107.27377745720243]
  This paper proposes a self-ensembling generative adversarial network (SE-GAN) exploiting cross-domain data for semantic segmentation. In SE-GAN, a teacher network and a student network constitute a self-ensembling model for generating semantic segmentation maps, which together with a discriminator, forms a GAN. Despite its simplicity, we find SE-GAN can significantly boost the performance of adversarial training and enhance the stability of the model.
  arXiv  Detail & Related papers  (2021-12-15T09:50:25Z)
• On Recurrent Neural Networks for learning-based control: recent results and ideas for future developments [1.1031750359996124]
  This paper aims to discuss and analyze the potentialities of Recurrent Neural Networks (RNN) in control design. Main families of RNN are considered, namely Neural AutoRegressive eXo, NNARX, Echo State Networks (ESN), Long Short Term Memory (LSTM), and Gated Recurrent Units (GRU)
  arXiv  Detail & Related papers  (2021-11-26T15:52:52Z)
• Compiling ONNX Neural Network Models Using MLIR [51.903932262028235]
  We present a preliminary report on our onnx-mlir compiler, which generates code for the inference of deep neural network models. Onnx-mlir relies on the Multi-Level Intermediate Representation (MLIR) infrastructure recently integrated in the LLVM project.
  arXiv  Detail & Related papers  (2020-08-19T05:28:08Z)
• Modeling from Features: a Mean-field Framework for Over-parameterized Deep Neural Networks [54.27962244835622]
  This paper proposes a new mean-field framework for over- parameterized deep neural networks (DNNs) In this framework, a DNN is represented by probability measures and functions over its features in the continuous limit. We illustrate the framework via the standard DNN and the Residual Network (Res-Net) architectures.
  arXiv  Detail & Related papers  (2020-07-03T01:37:16Z)
• Obtaining Faithful Interpretations from Compositional Neural Networks [72.41100663462191]
  We evaluate the intermediate outputs of NMNs on NLVR2 and DROP datasets. We find that the intermediate outputs differ from the expected output, illustrating that the network structure does not provide a faithful explanation of model behaviour.
  arXiv  Detail & Related papers  (2020-05-02T06:50:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.