Pith. sign in

REVIEW 3 major objections 5 minor 129 references

Neural Network Verification is a Programming Language Challenge

T0 review · 3 major / 5 minor · reviewed 2026-08-10 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper argues that neural network verification is increasingly a programming language challenge, with rigorous specification semantics, verified translations, and proof-carrying interfaces as the decisive missing pieces.

desk verdict A well-argued position paper that correctly identifies PL infrastructure as a bottleneck in NN verification, but overstates its own table and offers a roadmap that is more aspiration than validated plan. read the letter →

arxiv 2501.05867 v2 pith:FD4XMO7Y submitted 2025-01-10 cs.PL cs.LGcs.LO

Lucas C. Cordeiro , Matthew L. Daggitt , Julien Girard-Satabin , Omri Isac , Taylor T. Johnson , Guy Katz , Ekaterina Komendantskaya , Augustin Lemesle
show 3 more authors
Edoardo Manino Artjoms Šinkarovs Haoze Wu
This is my paper · ORCID
classification cs.PLcs.LGcs.LO
keywords neuralnetworkverificationprogramminglanguagedesigndependentlytypedlanguagesspecificationembeddinggapimplementationproofcertificatesVNN-LIB
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper argues that the hardest remaining obstacles to trustworthy neural network verification are not solver algorithms but programming language design. It claims that verification tools currently check an idealized version of the network expressed in the ONNX exchange format, not the actual trained program, and that property languages lack formal semantics, conciseness, dataset bindings, and the ability to express multi-network or hyper-properties. It identifies two named gaps: the embedding gap between high-level problem data and low-level real vectors, and the implementation gap between real-valued verification and floating-point, non-deterministic execution. The paper concludes that neural network verification is increasingly a programming language challenge and proposes a roadmap centered on a single expressively typed language, with types that can depend on values, with formal interfaces as a fallback.

What carries the argument

The load-bearing machinery is the three-lemma decomposition that turns a network-level certificate into a whole-program guarantee by threading it through explicit embedding and unembedding functions $e : P \to \mathbb{R}^m$ and $u : \mathbb{R}^n \to R$. This decomposition exposes the two gaps the paper names: the embedding gap, where problem-space values like discrete switches or image semantics are crudely approximated by real-valued intervals, and the implementation gap, where the verified object $f^*$ differs from the trained network $f$ due to ONNX conversion, floating-point arithmetic, parallel execution, and compiler optimizations. Around this decomposition, the paper also identifies five programming language features no current tool combines: rigorous semantics, embedding-gap support, implementation-gap support, proof certificates, and support for property-guided training.

What would settle it

A concrete way to test the central claim is to build a prototype of the unified language and run a standard robustness certification for a small convolutional network end to end, with training, conversion, and proof all inside the language and no unverified external library calls; if the type-checker cannot finish in practical time, or if any step silently falls back to an unverified backend, the practical version of the claim fails.

Watch

Extended reading notes

Core claim

On the paper's own terms, the central claim is that a safety guarantee for a neural network is only meaningful when it is connected by formally specified transformations to the network's actual implementation and to the larger system around it. The paper decomposes this into three lemmas: the network satisfies a network property $\Xi(f)$; any network satisfying $\Xi$ yields a lifted solution $u \circ g \circ e$ satisfying a solution property $\Phi$; and any such solution makes the full neuro-symbolic program $s(u \circ f \circ e)$ satisfy the program property $\Psi$. Currently, verifiers check $\Xi(f^*)$ where $f^*$ is an ONNX conversion of $f$, and neither the conversion nor the surrounding embedding is formally accounted for. The paper's proposed remedy is a single language whose types can depend on values, expressing the training pipeline, the properties, the embedding and unembedding functions, and proof certificates, with type-checking acting as proof checking; failing that, it argues for rigorously specified formal interfaces between existing components.

Load-bearing premise

The paper's proposal rests on the belief that a single language with very expressive types can express the whole training-to-verification pipeline and still be efficient enough for real tools; the paper itself acknowledges that type-checking such specifications is a hard open problem and offers no implementation or scaling evidence.

Editorial extensions

If this is right

  • Verification standards like VNN-LIB and ONNX need formally defined syntax and semantics before sound tools can be built around them.
  • New specification languages should be high-level and typed, with dataset bindings, multi-network properties, and hyper-properties, so that a single specification compiles to multiple solvers.
  • Property-guided training and verification should be viewed as two backends of the same specification compiler, not separate activities.
  • Verifiers must either verify the actual floating-point implementation or produce certificates that survive a formally justified translation, with quantized networks getting dedicated theories.
  • In a unified dependently typed language, proof certificates and proof checkers disappear as separate artifacts because terms are certificates and the type-checker is the checker.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the thesis is right, near-term progress is more likely through formal interface contracts for existing ONNX operators and verifier backends than through one unified language, since tool adoption is the bottleneck.
  • A testable extension would be a benchmark that scores verification tools not only on solver speed but on how many specification errors, conversion mismatches, and unverified library assumptions they catch.
  • The embedding gap suggests specification languages should treat the data manifold as a first-class citizen, possibly connecting to probabilistic or distributional specifications of the input space.
  • The paper's argument implies that safety certification of learned systems will eventually require the same infrastructure as compiler correctness: verified translation, proof-carrying code, and contract-based specifications for libraries.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. This paper is a position piece arguing that neural network verification is, at its core, a programming language challenge. It surveys the state of the art in NN verification from the perspective of five PL challenges: rigorous specification semantics, the embedding gap (between high-level problem-space properties and real-vector network properties), the implementation gap (between verified ONNX models and actual trained implementations), proof certificate production, and property-guided training. The paper traces each of these through the existing pipeline (VNN-LIB, ONNX, verifiers such as Marabou and αβ-CROWN, and prototypes such as CAISAR and Vehicle), and then proposes a roadmap featuring a unified dependently typed language (§4.1) and, more pragmatically, formal interfaces with behavioral specifications (§4.2). The central claim is that no current tool satisfies all five challenges, and that a PL-centered approach offers a path forward.

Significance. If the thesis is accepted, it would redirect research effort toward specification languages with formal semantics, compiler support for embedding and unembedding, proof certificates, and tight integration of training and verification. The paper's main strengths are its synthesis of known but scattered problems (ONNX's lack of formal semantics, floating-point mismatch, nondeterminism, the VNN-LIB limitations) and its clear articulation of the embedding and implementation gaps, with concrete code snippets and a useful decomposition of the decomposition of the proof obligations (Eqs. 2–4). The paper is honest about its limitations: it disclaims bibliographic completeness and acknowledges (§4.2) that a wholly unified language faces major efficiency and adoption hurdles. It also gives credit to existing partial solutions (CAISAR, Vehicle, Marabou's proof production, Imandra-based checkers). The paper is a valuable agenda-setting contribution, provided its empirical claims are stated precisely.

major comments (3)
  1. [§4, Table 1 (§3.5)] The claim that "some tools considered leaders in the neural network verification market do not satisfy any" is not supported by Table 1 as printed. Section 3.5 explicitly describes a proof-production mechanism implemented on top of Marabou, and the footnote to Table 1 states that the Farkas witness for neural-network UNSAT problems is available in Marabou, implying a checkmark in the Proof Certificates row for Marabou. The table's row/column alignment is ambiguous in the text, and no inclusion criterion for "satisfy" is provided. The paper should make the alignment explicit, define precisely what a checkmark means, and weaken or qualify the "do not satisfy any" sentence to reflect the actual evidence.
  2. [§4.1, item 3] The statement that the implementation gap "will be resolved" in a unified dependently typed language is stronger than the argument supports. The paragraph itself concedes that external libraries such as XLA and OpenBLAS would need to be formally verified or synthesized type-preservingly, which is exactly the difficult work of the implementation gap, not a consequence of the language design. No complexity or scalability argument is offered. The roadmap is plausible as a research vision, but this should be phrased as a conditional research target ("would need to be addressed by...") rather than as a resolution.
  3. [Table 1 (§3.2, §3.4)] The table mixes different notions of the five challenges across tool categories. For instance, CBMC/ESBMC's "Implementation Gap" checkmark refers to direct verification of low-level C code, which is a different kind of gap from the ONNX-translation gap addressed (or not addressed) by neural-network verifiers. Likewise, the "Rigorous Semantics" checkmarks for CAISAR and Vehicle are asserted without a citation or a definition of the formal semantics they provide. The table needs a precise legend stating what each checkmark means for each category, and the caption should explain the distinction between the generic proof production of CBMC/ESBMC and the Farkas-witness certificates of Marabou.
minor comments (5)
  1. [Author affiliations] The affiliation line contains a typo: "Heriot-Watt Univerwsity" should be "Heriot-Watt University".
  2. [Throughout] The name of the tool is written inconsistently as "αβ-Crown" and "αβ-CROWN"; please standardize.
  3. [Table 1] The header "F uture" appears to have a missing character; it should read "Future".
  4. [References] References [20] and [21] both point to the same Brix et al. paper "First three years of the international verification of neural networks competition"; one should be removed or they should be cross-referenced.
  5. [§3.1, item 4] The proposal to dynamically bind datasets in a specification language would benefit from a discussion of the formal status of such bound data (e.g., as axioms, finite constraints, or probabilistic models); the paper only mentions the mechanism without addressing how it interacts with soundness of the verification pipeline.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation; the paper is a perspective piece whose self-cited prototypes and roadmap are not used as fitted predictions or definitional equivalences.

full rationale

The paper does not derive a quantitative result from data or fit parameters, so the fitted-input and self-definition patterns do not apply. Its central thesis—that neural network verification should be understood as a programming-language challenge—is supported by independent evidence (Szegedy et al. [112]; Jia and Rinard [71]) and by a gap analysis of VNN-LIB and ONNX that does not depend on the authors' own tools. The authors' tools (Vehicle, CAISAR, Marabou) appear as motivating examples, but the argument does not reduce to their correctness; the paper explicitly notes their limitations, e.g. 'it can be argued that the composability of WhyML is limited' (Section 3.2) and 'we are not naive as to the difficulty of implementating such a unified framework' (Section 4.2). The unified dependently typed language is presented as a research agenda ('we believe the idealised solution to be'), not as an established result, and Section 4.2 cites Kokke et al. [77] for the acknowledged efficiency obstacle. No uniqueness theorem or ansatz is imported from prior author work. Table 1's classification is open to internal criticism—Marabou and αβ-CROWN receive proof-certificate checkmarks while the text says some leaders 'do not satisfy any'—but this is an evidentiary inconsistency, not circularity: the claim is not true by construction. Therefore the circularity score is 0.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper introduces no free parameters or invented entities. Its diagnosis rests on qualitative assessments of existing formats and tools, and its prescription is an unimplemented roadmap.

assumptions (3)
  • domain assumption The de facto formats VNN-LIB and ONNX lack formally defined semantics.
    Section 3.1 makes this the basis of the lack-of-rigour critique, supported by examples such as the single-sentence ONNX convolution description rather than by a formal analysis.
  • ad hoc to paper A single dependently typed language is the ideal way to integrate training, verification, and proof checking.
    Proposed in Section 4.1 as the idealised solution; no implementation exists, so it functions as an unverified design belief.
  • domain assumption Community practice often assumes verification guarantees about the ONNX model f* transfer to the original implementation f, and this assumption is unsafe.
    Section 3.4 motivates the implementation gap with this claim, citing evidence from Jia and Rinard [71] and Zombori et al. [129].

how reviews work

0 comments
Cite this review

Pith. "Pith review of Neural Network Verification is a Programming Language Challenge." pith.science (2026). https://pith.science/paper/FD4XMO7Y

@misc{pith2026250105867,
  author       = {Pith},
  title        = {Pith review of: Neural Network Verification is a Programming Language Challenge},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FD4XMO7Y}},
  note         = {Machine review of arXiv:2501.05867}
}
read the original 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

Figures reproduced from arXiv: 2501.05867 by the authors.

Figure 1
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. sway the neural network’s classification decisions. This lack of robustness can have safety and security implications:… view at source ↗
Figure 2
Figure 2. Schematic representation of the neural network verification pipeline. assume using a special format — ONNX (standing for Open Neural Network Exchange) [1] — to represent the neural networks. Thus, in reality, we verify Ξ(f ∗ ), where f ∗ is obtained from f by ONNX translation. The verifiers typically consider properties defining a precondition on the network inputs and a postcondition on its outputs. Both conditions… view at source ↗
Figure 3
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 ∗ : R 792 → R 10 . at a time, which makes encoding specifications where one needs to express properties on several neural networks at once impossible. Similarly, hyper￾properties [8,28] cannot be specified in VNN-LIB without special tooling, and ne… view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: An extract from a local robustness specification in CAISAR and Vehicle’s input languages for the same image dataset described in [PITH_FULL_IMAGE:figures/full_fig_p008_4.png]
Figure 5
Figure 5. Figure 5: Schematic representation of the embedding gap. existing pipelines: in Figs. 1 and 2, this is depicted by a dashed “Specification” box towards the left side. Other specification languages exist, like NeSAL [123] (which has no implementation) or DNNP [107] (lacking quant…
Figure 6
Figure 6. Figure 6: Outline of Vehicle compiler backends, bridging the Embedding Gap [33,32]. Dashed lines indicate information flow and solid lines automatic compilation. Ξ, all values must be represented as continuous real vectors (in actuality, at the training phase, floating-point vec…
Figure 7
Figure 7. Figure 7: Schematic representation of the implementation gap. this section, we outline a range of problems caused by this and thus trace the right-most section of the diagram illustrated in Figs. 1 and 7. Poor support for neural architecture conversion to ONNX. ONNX re-implement…
Figure 8
Figure 8. Figure 8: Schematic representation of the neural network training pipeline. Proof production mechanism, supporting several piecewise-linear activation functions, was implemented on top of Marabou [66,120]. The proofs produced by Marabou are checked by a proof checker implemented…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

129 extracted references · 40 canonical work pages

  1. [1]

    Open Neural Network Exchange format, https://onnx.ai/, accessed on 30.01.2022

    2022

  2. [2]

    In: Interactive Theorem Provers (ITP) 2024 (2024) 20 L

    Affeldt, R., Bruni, A., Komendantskaya, E., Slusarz, N., Stark, K.: Taming Dif- ferentiable Logics with Coq Formalisation. In: Interactive Theorem Provers (ITP) 2024 (2024) 20 L. C. Cordeiro et al

    2024

  3. [3]

    In: International Conference on Autonomous Agents and Multiagent Systems, AAMAS

    Akintunde, M.E., Botoeva, E., Kouvaros, P., Lomuscio, A.: Formal verification of neural agents in non-deterministic environments. In: International Conference on Autonomous Agents and Multiagent Systems, AAMAS. pp. 25–33 (2020)

    2020

  4. [4]

    Albarghouthi, A.: Introduction to neural network verification (2021),https:// arxiv.org/abs/2109.10317

    arXiv 2021

  5. [5]

    In: 15th International NASA Symposium on Formal Methods (NFM 2023), Houston, TX, USA, May 16–18, 2023

    Aleksandrov, A., Völlinger, K.: Formalizing piecewise affine activation functions of neural networks in Coq. In: 15th International NASA Symposium on Formal Methods (NFM 2023), Houston, TX, USA, May 16–18, 2023. Lecture Notes in Computer Science, vol. 13903, pp. 62–78. Springer (2023).https://doi.org/10. 1007/978-3-031-33170-1_4, https://doi.org/10.1007/9...

    work page doi:10.1007/978-3-031-33170-1_4 2023

  6. [6]

    In: Groote, J.F., Larsen, K.G

    Amir, G., Wu, H., Barrett, C., Katz, G.: An smt-based approach for verifying binarized neural networks. In: Groote, J.F., Larsen, K.G. (eds.) Tools and Al- gorithms for the Construction and Analysis of Systems. pp. 203–222. Springer International Publishing, Cham (2021)

    2021

  7. [7]

    Astorga, A., Hsieh, C., Madhusudan, P., Mitra, S.: Perception contracts for safety of ml-enabled systems. Proc. ACM Program. Lang. 7(OOPSLA2) (Oct 2023). https://doi.org/10.1145/3622875

    doi:10.1145/3622875 2023

  8. [8]

    Athavale, A., Bartocci, E., Christakis, M., Maffei, M., Nickovic, D., Weis- senbacher, G.: Verifying global two-safety properties in neural networks with con- fidence (2024), https://arxiv.org/abs/2405.14400

    work page Pith review arXiv 2024

Show all 129 references
  1. [9]

    Atkey, R., Daggitt, M.L., Kokke, W.: Vehicle formalisation (2024), https:// github.com/vehicle-lang/vehicle-formalisation

    2024

  2. [10]

    In: Proceedings of the AAAI Conference on Artificial Intelligence

    Bagnall, A., Stewart, G.: Certifying the true error: Machine learning in Coq with verified generalization guarantees. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 33, pp. 2662–2669 (2019)

    2019

  3. [11]

    http://arxiv.org/abs/2109.00498

    Bak, S., Liu, C., Johnson, T.: The Second International Verification of Neural Net- works Competition (VNN-COMP 2021): Summary and Results (2021), technical Report. http://arxiv.org/abs/2109.00498

    2021 arXiv

  4. [12]

    In: Peltier, N., Sofronie-Stokkermans, V

    Baranowski, M., He, S., Lechner, M., Nguyen, T.S., Rakamarić, Z.: An smt theory of fixed-point arithmetic. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Auto- mated Reasoning. pp. 13–31. Springer International Publishing, Cham (2020)

    2020

  5. [13]

    www.SMT-LIB.org (2016)

    Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)

    2016

  6. [14]

    ACM Trans

    Baskin, C., Liss, N., Schwartz, E., Zheltonozhskii, E., Giryes, R., Bronstein, A.M., Mendelson, A.: Uniq: Uniform noise injection for non-uniform quantization of neural networks. ACM Trans. Comput. Syst.37(1–4) (mar 2021).https://doi. org/10.1145/3444943, https://doi.org/10.11...

    2021 doi

  7. [15]

    Beyer, D.: Competition on software verification and witness validation: Sv-comp

  8. [17]

    science/hal-04474530/document

    Brisebarre, N., Hanrot, G., Muller, J.M., Zimmermann, P.: Correctly-rounded evaluation of a function: why, how, and at what cost? (2024), https://hal. science/hal-04474530/document

    2024

  9. [18]

    Brix, C., Bak, S., Johnson, T.T., Wu, H.: The fifth international verification of neural networks competition (vnn-comp 2024): Summary and results (2024), https://arxiv.org/abs/2412.19985 NN Verification is a PL Challenge 21

    2024 arXiv

  10. [19]

    CoRRabs/2312.16760 (2023)

    Brix, C., Bak, S., Liu, C., Johnson, T.T.: The Fourth International Verifica- tion of Neural Networks Competition (VNN-COMP 2023): Summary and Re- sults. CoRRabs/2312.16760 (2023). https://doi.org/10.48550/ARXIV.2312. 16760, https://doi.org/10.48550/arXiv.2312.16760

    2023 doi arXiv

  11. [20]

    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). Int. J. Softw. Tools Technol. Transf.25(3), 329–339 (2023).https://doi.org/10.1007/ S10009-023-00703-4, https://doi.org/10.10...

    2023 doi

  12. [21]

    International Journal on Software Tools for Technology Transfer25(3), 329–339 (2023)

    Brix, C., Müller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the in- ternational verification of neural networks competition (vnn-comp). International Journal on Software Tools for Technology Transfer25(3), 329–339 (2023)

    2023

  13. [22]

    In: 25th International Symposium on Formal Methods (FM 2023), Lübeck, Germany, March 6–10, 2023

    Brucker, A.D., Stell, A.: Verifying feedforward neural networks for classifica- tion in Isabelle/HOL. In: 25th International Symposium on Formal Methods (FM 2023), Lübeck, Germany, March 6–10, 2023. Lecture Notes in Computer Science, vol. 14000, pp. 427–444. Springer (2023). h...

    2023 doi

  14. [23]

    In: 2019 IEEE 26th Symposium on Com- puter Arithmetic (ARITH)

    Burgess, N., Milanovic, J., Stephens, N., Monachopoulos, K., Mansell, D.: Bfloat16 processing for neural networks. In: 2019 IEEE 26th Symposium on Com- puter Arithmetic (ARITH). pp. 88–91 (2019).https://doi.org/10.1109/ARITH. 2019.00022

    2019

  15. [24]

    IEEE Transactions on Software Engineering 50(6), 1374–1395 (2024).https://doi.org/10.1109/TSE.2024.3385378

    Calinescu, R., Imrie, C., Mangal, R., Rodrigues, G.N., Păsăreanu, C., Santana, M.A., Vázquez, G.: Controller synthesis for autonomous systems with deep- learning perception components. IEEE Transactions on Software Engineering 50(6), 1374–1395 (2024).https://doi.org/10.1109/TS...

    2024

  16. [25]

    Carlini, N.: A complete list of all (arxiv) adversarial example papers (2019)

    2019

  17. [27]

    In: Computer Aided Verification (CAV 2022)

    Casadio, M., Komendantskaya, E., Daggitt, M.L., Kokke, W., Katz, G., Amir, G., Refaeli, I.: Neural network robustness as a verification property: A principled case study. In: Computer Aided Verification (CAV 2022). Lecture Notes in Computer Science, Springer (2022)

    2022

  18. [28]

    Christakis, M., Eniser, H.F., Hoffmann, J., Singla, A., Wüstholz, V.: Specify- ing and testing k-safety properties for machine-learning models (2022),https: //arxiv.org/abs/2206.06054

    2022 arXiv

  19. [29]

    In: Smola, A., Dimakis, A., Sto- ica, I

    Cidon, E., Pergament, E., Asgar, Z., Cidon, A., Katti, S.: Characterizing and taming model instability across edge devices. In: Smola, A., Dimakis, A., Sto- ica, I. (eds.) Proceedings of Machine Learning and Systems. vol. 3, pp. 624– 636 (2021), https://proceedings.mlsys.org/p...

    2021

  20. [30]

    Coquand, T., Huet, G.: The calculus of constructions. Ph.D. thesis, Inria (1986)

    1986

  21. [31]

    https://doi.org/10.48550/ARXIV.2202.05207, https://arxiv.org/ abs/2202.05207

    Daggitt, M.L., Kokke, W., Atkey, R., Arnaboldi, L., Komendantskya, E.: Ve- hicle: Interfacing neural network verifiers with interactive theorem provers (2022). https://doi.org/10.48550/ARXIV.2202.05207, https://arxiv.org/ abs/2202.05207

    2022 doi arXiv

  22. [32]

    CoRR abs/2401.06379 (2024)

    Daggitt, M.L.,Kokke, W.,Atkey, R.,Slusarz, N.,Arnaboldi,L., Komendantskaya, E.: Vehicle: Bridging the embedding gap in the verification of neuro-symbolic programs. CoRR abs/2401.06379 (2024). https://doi.org/10.48550/ARXIV. 2401.06379, https://doi.org/10.48550/arXiv.2401.06379...

    2024 doi arXiv

  23. [33]

    In: Narodytska, N., Amir, G., Katz, G., Isac, O

    Daggitt, M.L., Kokke, W., Komendantskaya, E., Atkey, R., Arnaboldi, L., Slusarz, N.,Casadio,M.,Coke,B.,Lee,J.:Thevehicletutorial:Neuralnetworkverification with vehicle. In: Narodytska, N., Amir, G., Katz, G., Isac, O. (eds.) Proceedings of the 6th Workshop on Formal Methods fo...

    2023 doi

  24. [34]

    Frontiers of Computer Science16(3), 1–22 (2022)

    De Maria, E., Bahrami, A., l’Yvonnet, T., Felty, A., Gaffé, D., Ressouche, A., Grammont, F.: On the use of formal methods to model and verify neuronal archetypes. Frontiers of Computer Science16(3), 1–22 (2022)

    2022

  25. [35]

    In: 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems (Jul 2023)

    Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A.: Supporting standardization of neural networks verification with vnn-lib and coconet. In: 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems (Jul 2023)

    2023

  26. [36]

    In: 32nd USENIX Security Symposium (USENIX Security 23)

    Deng, Z., Meng, G., Chen, K., Liu, T., Xiang, L., Chen, C.: Differential testing of cross deep learning framework APIs: Revealing inconsistencies and vulnerabili- ties. In: 32nd USENIX Security Symposium (USENIX Security 23). pp. 7393–

  27. [37]

    In: https://arxiv.org/abs/2405.10611 (2024)

    Desmartin, R., Isac, O., Komendantskaya, E., Stark, K., Passmore, G., Katz, G.: A Certified Proof Checker for Deep Neural Network Verification. In: https://arxiv.org/abs/2405.10611 (2024)

    2024 arXiv

  28. [38]

    In: Glück, R., Kafle, B

    Desmartin, R., Isac, O., Passmore, G.O., Stark, K., Komendantskaya, E., Katz, G.: Towards a Certified Proof Checker for Deep Neural Network Verification. In: Glück, R., Kafle, B. (eds.) Logic-Based Program Synthesis and Transformation - 33rd International Symposium, LOPSTR 202...

    2023 doi

  29. [39]

    In: PPDP 2022: 24th International SymposiumonPrinciplesandPracticeofDeclarativeProgramming,Tbilisi,Geor- gia, September 20 - 22, 2022

    Desmartin,R.,Passmore,G.O.,Komendantskaya,E.,Daggit,M.:Checkinn:Wide range neural network verification in imandra. In: PPDP 2022: 24th International SymposiumonPrinciplesandPracticeofDeclarativeProgramming,Tbilisi,Geor- gia, September 20 - 22, 2022. pp. 3:1–3:14. ACM (2022).ht...

    2022

  30. [41]

    IFAC-PapersOnLine 51(16), 151 – 156 (2018)

    Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Learning and verification of feedback control systems using feedforward neural networks. IFAC-PapersOnLine 51(16), 151 – 156 (2018). https://doi.org/10.1016/j.ifacol.2018.08.026, iFAC Conference on Analysis and Design of Hy...

    2018 doi

  31. [42]

    In: Dutle, A., Muñoz, C., Narkawicz, A

    Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NASA Formal Methods. pp. 121–138. Springer International Publishing, Cham (2018)

    2018

  32. [43]

    In:D’Souza,D.,NarayanKumar,K.(eds.)AutomatedTechnologyforVerification and Analysis

    Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In:D’Souza,D.,NarayanKumar,K.(eds.)AutomatedTechnologyforVerification and Analysis. pp. 269–286. Springer International Publishing, Cham (2017)

    2017

  33. [44]

    In: International Symposium on Automated Technology for Verification and Analysis (ATVA) (2020) NN Verification is a PL Challenge 23

    Fan, J., Huang, C., Li, W., Chen, X., Zhu, Q.: Reachnn*: A tool for reachabil- ity analysis ofneural-network controlled systems. In: International Symposium on Automated Technology for Verification and Analysis (ATVA) (2020) NN Verification is a PL Challenge 23

    2020

  34. [45]

    In: Felleisen, M., Gardner, P

    Filliâtre, J.C., Paskevich, A.: Why3 - Where Programs Meet Provers. In: Felleisen, M., Gardner, P. (eds.) Programming Languages and Systems. pp. 125–128. Lec- ture Notes in Computer Science, Springer, Berlin, Heidelberg (2013). https: //doi.org/10.1007/978-3-642-37036-6_8

    2013 doi

  35. [46]

    In: Chaudhuri, K., Salakhutdinov, R

    Fischer, M., Balunovic, M., Drachsler-Cohen, D., Gehr, T., Zhang, C., Vechev, M.T.: DL2: training and querying neural networks with logic. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 201...

    2019

  36. [47]

    Flinkow, T., Pearlmutter, B.A., Monahan, R.: Comparing differentiable logics for learning with logical constraints (2024),https://arxiv.org/abs/2407.03847

    2024 arXiv

  37. [48]

    In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation

    Fremont, D.J., Dreossi, T., Ghosh, S., Yue, X., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Scenic: a language for scenario specification and scene generation. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 63–78. PLDI...

    2019 doi

  38. [49]

    In: Low-Power Computer Vision, pp

    Gholami, A., Kim, S., Dong, Z., Yao, Z., Mahoney, M.W., Keutzer, K.: A survey of quantization methods for efficient neural network inference. In: Low-Power Computer Vision, pp. 291–326. Chapman and Hall/CRC (2022)

    2022

  39. [50]

    (eds.) Tools and Algorithms for the Construction and Analysis of Systems

    Giacobbe, M., Henzinger, T.A., Lechner, M.: How many bits does it take to quan- tize your neural network? In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 79–97. Springer International Publishing, Cham (2020)

    2020

  40. [51]

    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

    2022

  41. [52]

    In: Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22)

    Giunchiglia, E., Stoian, M.C., Lukasiewicz, T.: Deep learning with logical con- straints. In: Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22). pp. 5478–5485. International Joint Conferences on Artificial In- telligence Organization (7 2022). h...

    2022 doi

  42. [53]

    In: Raedt, L.D

    Giunchiglia, E., Stoian, M.C., Lukasiewicz, T.: Deep learning with logical con- straints. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23-29 July

    2022

  43. [54]

    Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples (2015)

    2015

  44. [55]

    In: Proceedings of the IEEE/CVF International Conference on Computer Vision

    Gowal, S., Dvijotham, K.D., Stanforth, R., Bunel, R., Qin, C., Uesato, J., Arand- jelovic, R., Mann, T., Kohli, P.: Scalable verified training for provably robust image classification. In: Proceedings of the IEEE/CVF International Conference on Computer Vision. pp. 4842–4851 (2019)

    2019

  45. [57]

    ACM Comput

    Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3) (Jun 2012). https://doi.org/10.1145/2187671.2187678, https://doi.org/ 10.1145/2187671.2187678

    2012

  46. [58]

    In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR) (June 2019)

    He, Z., Fan, D.: Simultaneously optimizing weight and quantizer of ternary neural network using truncated gaussian approximation. In: Proceedings of the IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR) (June 2019)

    2019

  47. [59]

    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)

    2021

  48. [60]

    IOS Press (2022)

    Hitzler, P., Sarker, M.: Neuro-symbolic Artificial Intelligence: The State of the Art. IOS Press (2022)

    2022

  49. [61]

    In: International Sym- posium on Automated Technology for Verification and Analysis (ATVA) (2022)

    Huang, C., Fan, J., Chen, X., Li, W., Zhu, Q.: POLAR: A polynomial arithmetic framework for verifying neural-network controlled systems. In: International Sym- posium on Automated Technology for Verification and Analysis (ATVA) (2022)

    2022

  50. [62]

    ACM Transactions on Embedded Computing Systems (TECS) 18(5s), 1–22 (2019)

    Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: Reachability analysis of neural-network controlled systems. ACM Transactions on Embedded Computing Systems (TECS) 18(5s), 1–22 (2019)

    2019

  51. [63]

    In: Proceedings of the AAAI Conference on Artificial Intelligence

    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 AAAI Conference on Artificial Intelligence. vol. 38, pp. 21152–21160 (2024)

    2024

  52. [64]

    Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks (2017)

    2017

  53. [65]

    IEEE Std 754-2019 (Revision of IEEE 754-2008) pp

    IEEE: Ieee standard for floating-point arithmetic. IEEE Std 754-2019 (Revision of IEEE 754-2008) pp. 1–84 (2019).https://doi.org/10.1109/IEEESTD.2019. 8766229

    2019 doi

  54. [66]

    In: Proc

    Isac, O., Barrett, C., Zhang, M., Katz, G.: Neural Network Verification with Proof Production. In: Proc. 22nd Int. Conf. on Formal Methods in Computer-Aided Design (FMCAD). pp. 38–48 (2022)

    2022

  55. [67]

    In: International Conference on Computer-Aided Verification (2021)

    Ivanov, R., Carpenter, T., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig 2.0: Verification of neural network controllers using taylor model preconditioning. In: International Conference on Computer-Aided Verification (2021)

    2021

  56. [68]

    ACM Trans

    Ivanov, R., Carpenter, T.J., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verifying the safety of autonomous systems with neural network controllers. ACM Trans. Embed. Comput. Syst.20(1) (Dec 2020).https://doi.org/10.1145/3419742

    2020 doi

  57. [69]

    In: 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: International Conference on Hybrid Systems: Computation and Control. p. 169–178. HSCC, ACM (2019). https://doi.org/10.1145/33025...

    2019

  58. [70]

    In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H

    Jia, K., Rinard, M.: Efficient exact verification of binarized neural networks. In: Larochelle, H., Ranzato, M., Hadsell, R., Balcan, M., Lin, H. (eds.) Ad- vances in Neural Information Processing Systems. vol. 33, pp. 1782–1795. Curran Associates,Inc.(2020), https://proceedin...

    2020

  59. [71]

    In: Drăgoi, C., Mukherjee, S., Namjoshi, K

    Jia, K., Rinard, M.: Exploiting verified neural networks via floating point numer- ical error. In: Drăgoi, C., Mukherjee, S., Namjoshi, K. (eds.) Static Analysis. pp. 191–205. Springer International Publishing, Cham (2021)

    2021

  60. [72]

    In: Frehse, G., Althoff, M

    Johnson, T.T., Lopez, D.M., Benet, L., Forets, M., Guadalupe, S., Schilling, C., Ivanov, R., Carpenter, T.J., Weimer, J., Lee, I.: Arch-comp21 category report: NN Verification is a PL Challenge 25 Artificial intelligence and neural network control systems (ainncs) for continuo...

    2021

  61. [73]

    In: Frehse, G., Althoff, M

    Johnson, T.T., Lopez, D.M., Musau, P., Tran, H.D., Botoeva, E., Leofante, F., Maleki, A., Sidrane, C., Fan, J., Huang, C.: Arch-comp20 category report: Artificial intelligence and neural network control systems (ainncs) for contin- uous and hybrid systems plants. In: Frehse, G...

    2020 doi

  62. [74]

    In: International conference on computer aided verification

    Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient smt solver for verifying deep neural networks. In: International conference on computer aided verification. pp. 97–117. Springer (2017)

    2017

  63. [75]

    443–452 (07 2019)

    Katz, G., Huang, D., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., Dill, D., Kochenderfer, M., Barrett, C.: The Marabou Framework for Verification and Analysis of Deep Neural Networks, pp. 443–452 (07 2019)

    2019

  64. [76]

    In: NASA Formal Methods

    Kochdumper, N., Schilling, C., Althoff, M., Bak, S.: Open- and closed-loop neural network verification using polynomial zonotopes. In: NASA Formal Methods. pp. 16–36. Springer (2023)

    2023

  65. [77]

    Kokke, W., Komendantskaya, E., Kienitz, D., Atkey, R., Aspinall, D.: Neu- ral networks, secure by construction - an exploration of refinement types. In: d. S. Oliveira, B.C. (ed.) Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30...

    2020

  66. [78]

    NeurIPS 2018 tutorial (2018), available athttps://adversarial-ml-tutorial.org/

    Kolter, Z., Madry, A.: Adversarial robustness—theory and practice. NeurIPS 2018 tutorial (2018), available athttps://adversarial-ml-tutorial.org/

    2018

  67. [79]

    Tutorial at NeurIPS p

    Kolter, Z., Madry, A.: Adversarial robustness: Theory and practice. Tutorial at NeurIPS p. 3 (2018)

    2018

  68. [80]

    In: Interna- tional Conference on Tools and Algorithms for the Construction and Analysis of Systems

    Kroening, D., Tautschnig, M.: CBMC–C bounded model checker. In: Interna- tional Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 389–391. Springer (2014)

    2014

  69. [81]

    In: International Confer- ence on Learning Representations (2020),https://openreview.net/forum?id= BkgXT24tDS

    Li, Y., Dong, X., Wang, W.: Additive powers-of-two quantization: An effi- cient non-uniform discretization for neural networks. In: International Confer- ence on Learning Representations (2020),https://openreview.net/forum?id= BkgXT24tDS

    2020

  70. [82]

    ACM Trans

    Lohar, D., Jeangoudoux, C., Volkova, A., Darulova, E.: Sound mixed fixed-point quantization of neural networks. ACM Trans. Embed. Comput. Syst.22(5s) (sep 2023). https://doi.org/10.1145/3609118, https://doi.org/10.1145/3609118

    2023 doi

  71. [83]

    In: Frehse, G., Althoff, M., Schoitsch, E., Guiochet, J

    Lopez, D.M., Althoff, M., Benet, L., Chen, X., Fan, J., Forets, M., Huang, C., Johnson, T.T., Ladner, T., Li, W., Schilling, C., Zhu, Q.: Arch-comp22 cate- gory report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants...

    2022

  72. [84]

    In: Frehse, G., Althoff, M

    Lopez, D.M., Althoff, M., Forets, M., Johnson, T.T., Ladner, T., Schilling, C.: Arch-comp23 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) Proceedings of 10th Int...

    2023 doi

  73. [85]

    https://doi.org/10.1007/978-3-030-64437-6_4 , https: //doi.org/10.1007/978-3-030-64437-6_4

    Springer (2020). https://doi.org/10.1007/978-3-030-64437-6_4 , https: //doi.org/10.1007/978-3-030-64437-6_4

    2020 doi

  74. [86]

    In: Frehse, G., Althoff, M

    Lopez, D.M., Musau, P., Tran, H.D., Dutta, S., Carpenter, T.J., Ivanov, R., Johnson, T.T.: Arch-comp19 category report: Artificial intelligence and neural network control systems (ainncs) for continuous and hybrid systems plants. In: Frehse, G., Althoff, M. (eds.) ARCH19. 6th ...

    2019 doi

  75. [87]

    In: International Conference on Learn- ing Representations (2018)

    Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learn- ing models resistant to adversarial attacks. In: International Conference on Learn- ing Representations (2018)

    2018

  76. [88]

    In: Proceedings of the 22nd ACM SIGPLAN Inter- national Conference on Generative Programming: Concepts and Experiences

    Magalhães, J.W.d.S., Woodruff, J., Polgreen, E., O’Boyle, M.F.P.: C2taco: Lift- ing tensor code to taco. In: Proceedings of the 22nd ACM SIGPLAN Inter- national Conference on Generative Programming: Concepts and Experiences. p. 42–56. GPCE 2023, Association for Computing Machi...

    2023

  77. [89]

    In: Enea, C., Lal, A

    Lopez, D.M., Choi, S.W., Tran, H.D., Johnson, T.T.: NNV 2.0: The neural net- work verification tool. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 397–412. Springer Nature Switzerland, Cham (2023)

    2023

  78. [90]

    Artificial Intelli- gence 298, 103504 (2021)

    Manhaeve, R., Dumančić, S., Kimmig, A., Demeester, T., De Raedt, L.: Neural probabilistic logic programming in deepproblog. Artificial Intelli- gence 298, 103504 (2021). https://doi.org/https://doi.org/10.1016/j. artint.2021.103504, https://www.sciencedirect.com/science/articl...

    2021

  79. [91]

    In: Workshop on Automated Formal Reasoning for Trustworthy AI Systems (2023)

    Manino, E., Menezes, R.S., Shmarov, F., Cordeiro, L.C.: NeuroCodeBench: a Plain C Neural Network Benchmark for Software Verification. In: Workshop on Automated Formal Reasoning for Trustworthy AI Systems (2023)

    2023

  80. [92]

    IEEE Transac- tions on Computer-Aided Design of Integrated Circuits and Systems43(4), 1121– 1134 (2024)

    Matos,J.B.P.,deLimaFilho,E.B.,Bessa,I.,Manino,E.,Song,X.,Cordeiro,L.C.: Counterexample guided neural network quantization refinement. IEEE Transac- tions on Computer-Aided Design of Integrated Circuits and Systems43(4), 1121– 1134 (2024). https://doi.org/10.1109/TCAD.2023.3335313

    2024

  81. [93]

    https://doi.org/10.48550/ARXIV.2405

    Mandal, U., Amir, G., Wu, H., Daukantas, I., Newell, F.L., Ravaioli, U.J., Meng, B., Durling, M., Ganai, M., Shim, T., Katz, G., Barrett, C.W.: Formally verifying deep reinforcement learning controllers with lyapunov barrier certifi- cates.CoRR abs/2405.14058(2024). https://do...

    2024 doi arXiv

  82. [94]

    IEEE Transactions on Computer-Aided Design of In- tegrated Circuits and Systems41(11), 4445–4456 (2022)

    Mistry, S., Saha, I., Biswas, S.: An milp encoding for efficient verification of quan- tized deep neural networks. IEEE Transactions on Computer-Aided Design of In- tegrated Circuits and Systems41(11), 4445–4456 (2022). https://doi.org/10. 1109/TCAD.2022.3197697

    2022

  83. [95]

    In: Proceedings of the 1st ACM SIGPLAN International Workshop on Machine Learning and Programming Languages

    Murphy, C., Gray, P., Stewart, G.: Verified perceptron convergence theorem. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Machine Learning and Programming Languages. pp. 43–50 (2017)

    2017

  84. [96]

    Müller, M.N., Eckert, F., Fischer, M., Vechev, M.: Certified training: Small boxes are all you need (2023)

    2023

  85. [97]

    In: Finkbeiner, B., Kovács, L

    Menezes, R.S., Aldughaim, M., Farias, B., Li, X., Manino, E., Shmarov, F., Song, K., Brauße, F., Gadelha, M.R., Tihanyi, N., Korovin, K., Cordeiro, L.C.: Esbmc v7.4: Harnessing the power of intervals. In: Finkbeiner, B., Kovács, L. (eds.) Tools and Algorithms for the Construct...

    2024

  86. [98]

    In: Chaudhuri, K., Salakhutdinov, R

    Odena, A., Olsson, C., Andersen, D., Goodfellow, I.: TensorFuzz: Debugging neu- ral networks with coverage-guided fuzzing. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning. Proceedings of Machine Learning Research...

    2019

  87. [99]

    Payani,A.,Fekri,F.:InductiveLogicProgrammingviaDifferentiableDeepNeural Logic Networks. Tech. rep. (Jun 2019).https://doi.org/10.48550/arXiv.1906. 03523, http://arxiv.org/abs/1906.03523,zSCC:0000039arXiv:1906.03523[cs] type: article

    2019 doi arXiv

  88. [100]

    In: Proceedings of the 35th IEEE/ACM Inter- national Conference on Automated Software Engineering

    Pham, H.V., Qian, S., Wang, J., Lutellier, T., Rosenthal, J., Tan, L., Yu, Y., Nagappan, N.: Problems and opportunities in training deep learning software systems: an analysis of variance. In: Proceedings of the 35th IEEE/ACM Inter- national Conference on Automated Software En...

    2021

  89. [101]

    In: Proceedings of the AAAI Conference on Artificial Intelligence

    Narodytska, N., Kasiviswanathan, S., Ryzhyk, L., Sagiv, M., Walsh, T.: Verify- ing properties of binarized deep neural networks. In: Proceedings of the AAAI Conference on Artificial Intelligence. vol. 32 (2018)

    2018

  90. [102]

    In: Touili, T., Cook, B., Jackson, P

    Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. pp. 243–257. Springer Berlin Heidelberg, Berlin, Heidelberg (2010)

    2010

  91. [103]

    Pattern Recognition 105, 107281 (2020)

    Qin, H., Gong, R., Liu, X., Bai, X., Song, J., Sebe, N.: Binary neu- ral networks: A survey. Pattern Recognition 105, 107281 (2020). https://doi.org/https://doi.org/10.1016/j.patcog.2020.107281, https://www.sciencedirect.com/science/article/pii/S0031320320300856

    2020

  92. [104]

    In: Proc

    Sälzer, M., Lange, M.: Reachability Is NP-Complete Even for the Simplest Neural Networks. In: Proc. 15th Int. Conf. on Reachability Problems (RP). pp. 149–164 (2021)

    2021

  93. [105]

    In: Proceedings of the IEEE/CVF Con- ference on Computer Vision and Pattern Recognition (CVPR)

    Prach, B., Brau, F., Buttazzo, G., Lampert, C.H.: 1-lipschitz layers compared: Memory speed and certifiable robustness. In: Proceedings of the IEEE/CVF Con- ference on Computer Vision and Pattern Recognition (CVPR). pp. 24574–24583 (June 2024)

    2024

  94. [106]

    Com- mun

    Seshia, S.A., Sadigh, D., Sastry, S.S.: Toward verified artificial intelligence. Com- mun. ACM 65(7), 46–55 (Jun 2022).https://doi.org/10.1145/3503914 28 L. C. Cordeiro et al

    2022 doi

  95. [107]

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

    Shriver, D., Elbaum, S., Dwyer, M.B.: DNNV: A framework for deep neural net- work verification. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification. pp. 137–150. Springer International Publishing, Cham (2021)

    2021

  96. [108]

    In: 2022 IEEE 29th Symposium on Computer Arithmetic (ARITH)

    Sibidanov, A., Zimmermann, P., Glondu, S.: The core-math project. In: 2022 IEEE 29th Symposium on Computer Arithmetic (ARITH). pp. 26–34 (2022). https://doi.org/10.1109/ARITH54963.2022.00014

    2022

  97. [109]

    In: Oh, A., Nau- mann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S

    Schlögl, A., Hofer, N., Böhme, R.: Causes and effects of unanticipated nu- merical deviations in neural network inference frameworks. In: Oh, A., Nau- mann, T., Globerson, A., Saenko, K., Hardt, M., Levine, S. (eds.) Advances in Neural Information Processing Systems. vol. 36, ...

    2023

  98. [110]

    Proceedings of the ACM on Programming Languages3(POPL), 1–30 (2019)

    Singh, G., Gehr, T., Püschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages3(POPL), 1–30 (2019)

    2019

  99. [111]

    In: Piskac, R., Voronkov, A

    Slusarz, N., Komendantskaya, E., Daggitt, M.L., Stewart, R.J., Stark, K.: Logic of differentiable logics: Towards a uniform semantics of DL. In: Piskac, R., Voronkov, A. (eds.) LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelli...

    2023 doi

  100. [112]

    Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks (2014)

    2014

  101. [113]

    Safe Machine Learning workshop at ICLR (2019)

    Sidrane, C., Kochenderfer, M.J.: OVERT: Verification of nonlinear dynamical systems with neural network controllers via overapproximation. Safe Machine Learning workshop at ICLR (2019)

    2019

  102. [114]

    In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI)

    Teuber, S., Büning, M.K., Kern, P., Sinz, C.: Geometric path enumeration for equivalence verification of neural networks. In: 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI). pp. 200–208 (2021). https://doi.org/10.1109/ICTAI52525.2021.00035

    2021

  103. [115]

    https://doi.org/10

    Teuber, S., Mitsch, S., Platzer, A.: Provably safe neural network controllers via differentialdynamiclogic.CoRR abs/2402.10998(2024). https://doi.org/10. 48550/ARXIV.2402.10998, https://doi.org/10.48550/arXiv.2402.10998

    2024 doi arXiv

  104. [116]

    IEEE Design & Test39(1), 24–34 (2022)

    Tran, H.D., Xiang, W., Johnson, T.T.: Verification approaches for learning- enabled autonomous cyber–physical systems. IEEE Design & Test39(1), 24–34 (2022). https://doi.org/10.1109/MDAT.2020.3015712

    2022

  105. [117]

    Tassarotti, J., Tristan, J.B.: Verified density compilation for a probabilistic pro- gramming language. Proc. ACM Program. Lang. 7(PLDI) (Jun 2023). https: //doi.org/10.1145/3591245, https://doi.org/10.1145/3591245

    2023 doi

  106. [118]

    In: Bengio, S., Wal- lach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R

    Wang, N., Choi, J., Brand, D., Chen, C.Y., Gopalakrishnan, K.: Training deep neural networks with 8-bit floating point numbers. In: Bengio, S., Wal- lach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems. v...

    2018

  107. [119]

    Advances in Neural Information Processing Sys- tems 34, 29909–29921 (2021)

    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 neural network robustness verification. Advances in Neural Information Processing Sys- tems 34, 29909–29921 (2021)

    2021

  108. [120]

    In: Computer Aided Verification (CAV) (2024) NN Verification is a PL Challenge 29

    Wu, H., Isac, O., Zeljic, A., Tagomori, T., Daggitt, M.L., Kokke, W., Refaeli, I., Amir, G., Julian, K., Bassan, S., Huang, P., Lahav, O., Wu, M., Zhang, M., Komendantskaya, E., Katz, G., Barrett, C.W.: Marabou 2.0: A Versatile Formal Analyzer of Neural Networks. In: Computer ...

    2024

  109. [121]

    In: 32nd International Con- ference on Computer-Aided Verification (CAV’20) (7 2020)

    Tran, H.D., Yang, X., Lopez, D.M., Musau, P., Nguyen, L.V., Xiang, W., Bak, S., Johnson, T.T.: NNV: The neural network verification tool for deep neural net- works and learning-enabled cyber-physical systems. In: 32nd International Con- ference on Computer-Aided Verification (...

    2020

  110. [122]

    IEEE transactions on neural networks and learning systems29(11), 5777–5783 (2018)

    Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and ver- ification for multilayer neural networks. IEEE transactions on neural networks and learning systems29(11), 5777–5783 (2018)

    2018

  111. [123]

    In: Raedt, L.D

    Xie, X., Kersting, K., Neider, D.: Neuro-symbolic verification of deep neural net- works. In: Raedt, L.D. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI-22. pp. 3622–3628. International Joint Conferences on Artificial Int...

    2022 doi

  112. [124]

    Nature 577(7792), 641–646 (2020)

    Yao, P., Wu, H., Gao, B., Tang, J., Zhang, Q., Zhang, W., Yang, J.J., Qian, H.: Fully hardware-implemented memristor convolutional neural network. Nature 577(7792), 641–646 (2020)

    2020

  113. [125]

    In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems

    Wu, H., Zeljić, A., Katz, G., Barrett, C.: Efficient neural network analysis with sum-of-infeasibilities. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 143–163. Springer (2022)

    2022

  114. [126]

    In: Enea, C., Lal, A

    Zhang, Y., Song, F., Sun, J.: Qebverif: Quantization error bound verification of neural networks. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. pp. 413–437. Springer Nature Switzerland, Cham (2023)

    2023

  115. [127]

    In: Proceedings of the 37th International Conference on Machine Learning

    Zhang, Y., Albarghouthi, A., D’Antoni, L.: Robustness to programmable string transformations via augmented abstract training. In: Proceedings of the 37th International Conference on Machine Learning. pp. 11023–11032 (2020)

    2020

  116. [128]

    In: Marculescu, D., Chi, Y., Wu, C

    Zhuang, D., Zhang, X., Song, S., Hooker, S.: Randomness in neural network training: Characterizing the impact of tooling. In: Marculescu, D., Chi, Y., Wu, C. (eds.) Proceedings of Machine Learning and Systems. vol. 4, pp. 316– 336 (2022), https://proceedings.mlsys.org/paper_fi...

    2022

  117. [129]

    In: 8th International Conference on Learning Representations, ICLR 2020 (2020)

    Zhang, H., Chen, H., Xiao, C., Gowal, S., Stanforth, R., Li, B., Boning, D., Hsieh, C.J.: Towards stable and efficient training of verifiably robust neural networks. In: 8th International Conference on Learning Representations, ICLR 2020 (2020)

    2020

  118. [133]

    In: International Conference on Learning Represen- tations (2021), https://openreview.net/forum?id=4IwieFS44l

    Zombori, D., Bánhelyi, B., Csendes, T., Megyeri, I., Jelasity, M.: Fooling a com- plete neural network verifier. In: International Conference on Learning Represen- tations (2021), https://openreview.net/forum?id=4IwieFS44l

    2021

  119. [2022]

    5478–5485

    pp. 5478–5485. ijcai.org (2022).https://doi.org/10.24963/ijcai.2022/ 767, https://doi.org/10.24963/ijcai.2022/767

    2022 doi

  120. [2023]

    (eds.) Tools and Algorithms for the Construction and Analysis of Systems

    In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 495–522. Springer Nature Switzerland, Cham (2023)

    2023

  121. [7410]

    org/conference/usenixsecurity23/presentation/deng-zizhuang

    USENIX Association, Anaheim, CA (Aug 2023), https://www.usenix. org/conference/usenixsecurity23/presentation/deng-zizhuang

    2023

Pith tools

Reviewed August 10, 2026 · model on record in the stance chip above.