pith. machine review for the scientific record. sign in

arxiv: 2605.07451 · v1 · submitted 2026-05-08 · 💻 cs.LG

Recognition: no theorem link

VNN-LIB 2.0: Rigorous Foundations for Neural Network Verification

Allen Antony, Andrea Gimelli, Ann Roy, Matthew L. Daggitt

Authors on Pith no claims yet

Pith reviewed 2026-05-11 02:07 UTC · model grok-4.3

classification 💻 cs.LG
keywords networkvnn-libneuralsemanticsformalfoundationsverificationdefined
0
0 comments X

The pith

VNN-LIB 2.0 uses a network theory abstraction to supply precise syntax, type systems, and semantics for neural network verification queries independent of external model formats.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes rigorous foundations for VNN-LIB 2.0 by addressing gaps in the prior version, including imprecise definitions and dependence on informal, evolving external model representations. It introduces the network theory as an abstract minimal semantic interface that any compatible neural network model format must satisfy. This separation permits a self-contained formal syntax for more expressive queries, a type system defined over the numeric domains supplied by the network theory, and an accompanying formal semantics. The entire construction is mechanized in a theorem prover to confirm internal consistency. A reader would care because the result yields verification standards whose meaning no longer drifts with changes in supporting model formats.

Core claim

The central claim is that a network theory abstraction characterises the minimal semantic interface required from a neural network model format. This interface enables VNN-LIB to be defined independently of any specific version of external model representations while preserving compatibility as those representations evolve. Building on the abstraction, the paper supplies a formal syntax for an expressive query language, a type system for that language over the numeric domains provided by the network theory, and a formal semantics for the queries, all of which are mechanized to guarantee consistency.

What carries the argument

The network theory, an abstract characterisation of the minimal semantic interface required from any neural network model format, which decouples the verification query language from concrete model implementations.

If this is right

  • Verification queries acquire fixed, self-contained semantics that do not change with updates to external model formats.
  • The query language supports greater expressivity while remaining type-safe with respect to the numeric domains of the network theory.
  • Compatibility with new or revised model representations is maintained without introducing soundness gaps in the verification process.
  • Mechanization of the syntax, type system, and semantics ensures that the definitions contain no internal contradictions.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Verification tools built on this standard could remain stable even as underlying model formats continue to change.
  • The same abstraction pattern could be reused for other verification or certification standards that must interface with rapidly evolving external data representations.
  • Developers could test the abstraction by attempting to encode existing neural network models and queries strictly within the network theory boundaries and checking for completeness.
  • keywords:[
  • neural network verification
  • formal semantics
  • type system
  • query language

Load-bearing premise

The network theory abstraction is sufficient to capture every necessary semantic detail of neural network models while preserving full expressivity and soundness when interfacing with external formats.

What would settle it

An observation that a real neural network model exhibits observable behaviors or constraints that cannot be expressed through the network theory interface without either omitting information or producing unsound verification outcomes would falsify the claim.

Figures

Figures reproduced from arXiv: 2605.07451 by Allen Antony, Andrea Gimelli, Ann Roy, Matthew L. Daggitt.

Figure 1
Figure 1. Figure 1: A simple VNN-LIB 1.0 query and accompanying neural network model. In VNN [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The definition of a network theory, i.e. the minimal signature for an abstract [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The syntax of VNN-LIB queries. The superscript [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: A simple VNN-LIB query which declares a network with a single input and [PITH_FULL_IMAGE:figures/full_fig_p008_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: A VNN-LIB network declaration with multiple inputs/outputs. [PITH_FULL_IMAGE:figures/full_fig_p009_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: A VNN-LIB network declaration that declares a hidden node [PITH_FULL_IMAGE:figures/full_fig_p009_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: VNN-LIB network declarations allowing the referencing of multiple networks. [PITH_FULL_IMAGE:figures/full_fig_p010_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: A pair of VNN-LIB network declarations that reference the same ONNX model. [PITH_FULL_IMAGE:figures/full_fig_p011_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: A pair of VNN-LIB network declarations referencing isomorphic ONNX models. [PITH_FULL_IMAGE:figures/full_fig_p011_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: An example of a real-valued VNN-LIB query. This explicitly gives the solver [PITH_FULL_IMAGE:figures/full_fig_p017_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Constructing a real-valued network theory [PITH_FULL_IMAGE:figures/full_fig_p018_11.png] view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 3 minor

Summary. The paper introduces VNN-LIB 2.0 by defining a network theory as an abstract minimal semantic interface for neural network models. This enables a self-contained formal syntax for an expressive query language, a type system over numeric domains supplied by the network theory, formal semantics, and full mechanization in Agda. The development directly targets the shortcomings of VNN-LIB 1.0 (imprecise syntax/semantics, limited expressivity, and dependence on informal, evolving ONNX semantics) and aims to deliver rigorous, trustworthy foundations for neural network verification.

Significance. If the network theory abstraction succeeds in capturing required semantics while preserving compatibility, the work would establish a self-contained standard comparable to SMT-LIB, substantially improving interoperability and soundness guarantees across verification tools. The Agda mechanization supplies independent, machine-checked evidence of internal consistency for the syntax, type system, and semantics, which is a notable strength.

major comments (2)
  1. [§3] §3 (Network Theory definition): the claim that the abstraction is sufficient to capture all necessary semantic details of neural network models (including those required for full ONNX compatibility) is load-bearing for the central contribution, yet the paper provides only high-level interface requirements without a concrete mapping or expressivity proof for representative ONNX operators.
  2. [§5] §5 (Semantics and mechanization): while the Agda development demonstrates consistency of the core definitions, the paper does not state which edge cases (e.g., non-standard numeric domains, higher-order network constructs, or partial functions) are covered by the mechanized theorems versus left as informal assumptions.
minor comments (3)
  1. [Abstract and §1] The abstract and introduction repeatedly contrast VNN-LIB with SMT-LIB; a short table summarizing the corresponding features (self-contained queries, fixed semantics, etc.) would improve clarity.
  2. [§4] Notation for the numeric domains supplied by the network theory is introduced without an explicit summary table; adding one would aid readers when following the type-system rules.
  3. [§4 and §5] A few forward references to later mechanization lemmas appear before the relevant definitions are fully stated; reordering or adding brief forward pointers would reduce reader effort.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading, positive assessment of the contribution, and recommendation for minor revision. We address each major comment below.

read point-by-point responses

  1. Referee: [§3] §3 (Network Theory definition): the claim that the abstraction is sufficient to capture all necessary semantic details of neural network models (including those required for full ONNX compatibility) is load-bearing for the central contribution, yet the paper provides only high-level interface requirements without a concrete mapping or expressivity proof for representative ONNX operators.

    Authors: The network theory is intentionally defined as a minimal abstract interface that characterises the semantic requirements any concrete model format must satisfy, thereby decoupling VNN-LIB from the informal and evolving semantics of ONNX. The formal syntax, type system, and semantics are then built parametrically over this interface, and the Agda mechanisation establishes their internal consistency. We agree, however, that an explicit illustration of how representative ONNX operators are captured would strengthen the load-bearing claim. In the revised manuscript we will add an appendix that supplies concrete mappings for a representative set of ONNX operators (e.g., Gemm, Conv, Relu, and element-wise arithmetic) together with a brief discussion of how their semantics are expressed through the network-theory interface. revision: yes

  2. Referee: [§5] §5 (Semantics and mechanization): while the Agda development demonstrates consistency of the core definitions, the paper does not state which edge cases (e.g., non-standard numeric domains, higher-order network constructs, or partial functions) are covered by the mechanized theorems versus left as informal assumptions.

    Authors: We appreciate the request for greater precision regarding the scope of the mechanisation. The Agda development covers the syntax, typing rules, and denotational semantics for the core query language over the standard numeric domains (reals, integers, and finite-precision floating-point) and first-order network constructs supplied by the network theory. Non-standard numeric domains, higher-order network constructs, and partial functions fall outside this fragment and are treated as informal assumptions, as already indicated in the paper’s limitations discussion. In the revision we will add a short subsection (or table) in §5 that explicitly enumerates the mechanised cases and the informal assumptions that remain. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper introduces a network theory as an abstract minimal semantic interface for neural network models, then defines a formal syntax, type system, and semantics on top of it, with the full development mechanized in Agda. This chain is purely definitional and foundational: the abstraction enables independence from evolving ONNX while the mechanization supplies independent evidence of internal consistency. No equations reduce to prior inputs by construction, no parameters are fitted then relabeled as predictions, and no load-bearing claims rest on self-citations or uniqueness theorems imported from the authors' prior work. The contribution addresses VNN-LIB 1.0 shortcomings through new definitions rather than circular derivation.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

This is a definitional and formalization paper; it introduces new constructs rather than empirical fits or data-driven parameters.

axioms (1)
  • standard math Standard mathematical foundations of syntax, semantics, and type theory
    The formalization relies on basic set theory, type theory, and inductive definitions as background.
invented entities (1)
  • Network theory no independent evidence
    purpose: Abstract characterization of the minimal semantic interface required from any neural network model format
    New concept introduced to decouple VNN-LIB from specific ONNX versions while remaining compatible.

pith-pipeline@v0.9.0 · 5550 in / 1338 out tokens · 39185 ms · 2026-05-11T02:07:43.954355+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

28 extracted references · 28 canonical work pages

  1. [1]

    In: Proceedings of 60 the 29th ACM International Conference on Architectural Support for Program- ming Languages and Operating Systems, Volume 2

    Ansel, J., Yang, E., He, H., Gimelshein, N., Jain, A., Voznesensky, M., Bao, B., Bell, P., et al.: PyTorch 2: Faster Machine Learning Through Dynamic Python Bytecode Transformation and Graph Compilation. In: 29th International Confer- ence on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’24). ACM (Apr 2024).https://doi.org...

    work page doi:10.1145/3620665.3640366 2024

  2. [2]

    In: International Conference on Computer Aided Verification

    Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Nickovic, D., Weissenbacher, G.: Verifying global two-safety properties in neural networks with confidence. In: International Conference on Computer Aided Verification. pp. 329–351. Springer (2024).https://doi.org/10.1007/978-3-031-65630-9_17

    work page doi:10.1007/978-3-031-65630-9_17 2024

  3. [3]

    In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK)

    Barrett, C., Stump, A., Tinelli, C., et al.: The SMT-LIB standard: Version 2.0. In: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK). vol. 13, p. 14 (2010)

    work page 2010

  4. [4]

    First Three Years of the International Verification of Neural Networks Competition (

    Brix, C., Müller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the international verification of neural networks competition (VNN-COMP). Interna- tional Journal on Software Tools for Technology Transfer25(3), 329–339 (2023). https://doi.org/10.1007/s10009-023-00703-4

    work page doi:10.1007/s10009-023-00703-4 2023

  5. [5]

    In: European Symposium on Programming

    Cordeiro, L.C., Daggitt, M.L., Girard-Satabin, J., Isac, O., Johnson, T.T., Katz, G., Komendantskaya, E., Lemesle, A., Manino, E., Šinkarovs, A., et al.: Neural net- work verification is a programming language challenge. In: European Symposium on Programming. pp. 206–235. Springer (2025)

    work page 2025

  6. [6]

    Journal of Open Source Software10(116), 9241 (2025).https://doi

    Daggitt, M.L., Allais, G., McKinna, J., Abel, A., Doorn, V., Wood, J., Norell, U., Kidney, D.O., Meshveliani, S., Stucki, S., et al.: The Agda standard library: Version 2.0. Journal of Open Source Software10(116), 9241 (2025).https://doi. org/10.21105/joss.09241

    work page doi:10.21105/joss.09241 2025

  7. [7]

    and Kokke, Wen and Atkey, Robert and Komendantskaya, Ekaterina and Slusarz, Natalia and Arnaboldi, Luca , editor =

    Daggitt, M.L., Kokke, W., Atkey, R., Komendantskaya, E., Slusarz, N., Arnaboldi, L.: Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs. In: International Conference on Formal Structures for Computation and Deduction (FSCD 2025). vol. 337, pp. 2:1–2:20. Dagstuhl, Germany (2025). https://doi.org/10.4230/LIPIcs.FSCD.2025.2 VN...

    work page doi:10.4230/lipics.fscd.2025.2 2025

  8. [8]

    In: FoMLAS@ CAV

    Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A., Narodytska, N., Amir, G., Katz, G., Isac, O.: Supporting Standardization of Neural Networks Verification with VNNLIB and CoCoNet. In: FoMLAS@ CAV. pp. 47–58 (2023)

    work page 2023

  9. [9]

    developers, O.R.: ONNX Runtime.https://onnxruntime.ai/(2021)

    work page 2021

  10. [10]

    In: International Sympo- sium on AI Verification

    Elboher, Y.Y., Isac, O., Katz, G., Ladner, T., Wu, H.: Abstraction-based proof production in formal verification of neural networks. In: International Sympo- sium on AI Verification. pp. 203–220. Springer (2025).https://doi.org/10.1007/ 978-3-031-99991-8_10

    work page 2025

  11. [11]

    In: AISafety

    Girard-Satabin, J., Alberti, M., Bobot, F., Chihani, Z., Lemesle, A.: CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness. In: AISafety. CEUR-Workshop Proceedings, Vienne, Austria (Jul 2022),https:// hal.archives-ouvertes.fr/hal-03687211

    work page 2022

  12. [12]

    In: Proceedings of the AAAI conference on Artificial Intelligence

    Henzinger, T.A., Lechner, M., Žikelić, Ð.: Scalable verification of quantized neural networks. In: Proceedings of the AAAI conference on Artificial Intelligence. vol. 35, pp. 3787–3795 (2021)

    work page 2021

  13. [13]

    In: Proceedings of the AAAIConferenceonArtificialIntelligence.vol.38,pp.21152–21160(2024).https: //doi.org/10.1609/aaai.v38i19.30108

    Huang, P., Wu, H., Yang, Y., Daukantas, I., Wu, M., Zhang, Y., Barrett, C.: Towards efficient verification of quantized neural networks. In: Proceedings of the AAAIConferenceonArtificialIntelligence.vol.38,pp.21152–21160(2024).https: //doi.org/10.1609/aaai.v38i19.30108

    work page doi:10.1609/aaai.v38i19.30108 2024

  14. [14]

    In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control

    Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. pp. 169–178 (2019).https://doi.org/10.1145/3302504.3311806

    work page doi:10.1145/3302504.3311806 2019

  15. [15]

    In: International Static Analysis Symposium

    Jia, K., Rinard, M.: Exploiting verified neural networks via floatingpoint numerical error. In: International Static Analysis Symposium. pp. 191–205. Springer (2021). https://doi.org/10.1007/978-3-030-88806-0_9

    work page doi:10.1007/978-3-030-88806-0_9 2021

  16. [16]

    Allerton Conference on Communication, Control, and Computing (2025)

    Johnson, T.T.: Is neural network verification useful and what is next? In: 2025 61st Allerton Conference on Communication, Control, and Computing Proceedings. Allerton Conference on Communication, Control, and Computing (2025)

    work page 2025

  17. [17]

    Pro- ceedings of the ACM on Programming Languages8(OOPSLA), 1010–1039 (2024)

    Kabaha, A., Cohen, D.D.: Verification of neural networks’ global robustness. Pro- ceedings of the ACM on Programming Languages8(OOPSLA), 1010–1039 (2024). https://doi.org/10.1145/3649847

    work page doi:10.1145/3649847 2024

  18. [18]

    arXiv preprint arXiv:2512.19007 (2025)

    Kaulen, K., Ladner, T., Bak, S., Brix, C., Duong, H., Flinkow, T., Johnson, T.T., Koller, L., Manino, E., Nguyen, T.H., et al.: The 6th International Verifica- tion of Neural Networks Competition (VNN-COMP 2025): Summary and Results. arXiv:2512.19007 (2025).https://doi.org/10.48550/arXiv.2512.19007

    work page doi:10.48550/arxiv.2512.19007 2025

  19. [19]

    Ad- vances in Neural Information Processing Systems33, 15427–15438 (2020)

    Liu, X., Han, X., Zhang, N., Liu, Q.: Certified monotonic neural networks. Ad- vances in Neural Information Processing Systems33, 15427–15438 (2020)

    work page 2020

  20. [20]

    , year =

    Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: NNV 2.0: The neural network verification tool. In: International Conference on Computer Aided Verification. pp. 397–412. Springer (2023).https://doi.org/10.1007/978-3-031-37703-7_19

    work page doi:10.1007/978-3-031-37703-7_19 2023

  21. [21]

    Proceedings of the ACM on Programming Languages6(POPL), 1–33 (2022)

    Müller, M.N., Makarchuk, G., Singh, G., Püschel, M., Vechev, M.: PRIMA: gen- eral and precise neural network certification via scalable convex hull approxima- tions. Proceedings of the ACM on Programming Languages6(POPL), 1–33 (2022). https://doi.org/10.1145/3498704

    work page doi:10.1145/3498704 2022

  22. [22]

    In: Proceedings of the 4th international workshop on Types in language design and implementation

    Norell, U.: Dependently typed programming in Agda. In: Proceedings of the 4th international workshop on Types in language design and implementation. pp. 1–2 (2009).https://doi.org/10.1145/1481861.1481862

    work page doi:10.1145/1481861.1481862 2009

  23. [23]

    In: Proceedings of the ACM/IEEE 42nd International Conference on 22 Roy et al

    Paulsen, B., Wang, J., Wang, C.: Reludiff: Differential verification of deep neural networks. In: Proceedings of the ACM/IEEE 42nd International Conference on 22 Roy et al. Software Engineering. pp. 714–726 (2020).https://doi.org/10.1145/3377811. 3380337

    work page doi:10.1145/3377811 2020

  24. [24]

    In: Silva, A., Leino, K.R.M

    Shriver, D., Elbaum, S., Dwyer, M.B.: DNNV: A Framework for Deep Neural Network Verification. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Ver- ification. pp. 137–150. Springer International Publishing, Cham (2021).https: //doi.org/10.1007/978-3-030-81685-8_6

    work page doi:10.1007/978-3-030-81685-8_6 2021

  25. [25]

    In: Globerson, A., Mackey, L., Fan, A., Zhang, C., Bel- grave, D., Tomczak, J., Paquet, U

    Teuber, S., Mitsch, S., Platzer, A.: Provably safe neural network controllers via differential dynamic logic. In: Globerson, A., Mackey, L., Fan, A., Zhang, C., Bel- grave, D., Tomczak, J., Paquet, U. (eds.) Advances in Neural Information Process- ing Systems. Curran Associates, Inc. (2024).https://doi.org/10.5555/3737916. 3737967

    work page doi:10.5555/3737916 2024

  26. [26]

    Advances in Neural Information Processing Systems34(2021).https://doi.org/10.5555/3540261.3542550

    Wang, S., Zhang, H., Xu, K., Lin, X., Jana, S., Hsieh, C.J., Kolter, J.Z.: Beta- CROWN: Efficient bound propagation with per-neuron split constraints for com- plete and incomplete neural network verification. Advances in Neural Information Processing Systems34(2021).https://doi.org/10.5555/3540261.3542550

    work page doi:10.5555/3540261.3542550 2021

  27. [27]

    ACM Transactions on Multimedia Computing, Communications, and Ap- plications (TOMM)17(1s), 1–25 (2021).https://doi.org/10.1145/3408317

    Wang, Y.: Survey on deep multi-modal data analytics: Collaboration, rivalry, and fusion. ACM Transactions on Multimedia Computing, Communications, and Ap- plications (TOMM)17(1s), 1–25 (2021).https://doi.org/10.1145/3408317

    work page doi:10.1145/3408317 2021

  28. [28]

    In: International Conference on Computer Aided Verification

    Wu, H., Isac, O., Zeljić, A., Tagomori, T., Daggitt, M., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., et al.: Marabou 2.0: a versatile formal analyzer of neural networks. In: International Conference on Computer Aided Verification. pp. 249–264. Springer (2024).https://doi.org/10.1007/978-3-031-65630-9_13

    work page doi:10.1007/978-3-031-65630-9_13 2024