pith. sign in

arxiv: 1907.01297 · v1 · pith:DXVJJRN6new · submitted 2019-07-02 · 💻 cs.AI · cs.PL

Neural Network Verification for the Masses (of AI graduates)

Ekaterina Komendantskaya , Rob Stewart , Kirsy Duncan , Daniel Kienitz , Pierre Le Hen , Pascal Bacchus This is my paper

Pith reviewed 2026-05-25 11:22 UTC · model grok-4.3

classification 💻 cs.AI cs.PL
keywords neural network verificationAI MSc degreesverification toolsprogramming language limitationsstudent projectsAI safetyadversarial attacksteaching materials
0
0 comments X

The pith

Shortage of verification tools and language limitations hinder teaching safe AI in MSc programs.

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

The paper establishes that rapid growth in AI applications and MSc degrees has outpaced the availability of accessible verification tools and teaching materials, even as safety concerns like adversarial attacks on neural networks become prominent. It describes how one lab addresses the gap by involving MSc students in verification projects as dissertation work. The main obstacles encountered trace back to limitations in existing programming languages for verification. The authors outline successes alongside these difficulties and point to future directions for better integration of verification into AI education.

Core claim

The paper claims there is a noticeable shortage of accessible tools, methods and teaching materials for incorporating verification into AI programs. A lab engages AI and Robotics MSc students in verification projects as part of dissertation work, reporting both successes and unexpected difficulties that arise from limitations of existing programming languages used for verification, while discussing future directions for incorporating verification into AI degrees.

What carries the argument

Student verification projects in an AI MSc program, used to surface and illustrate programming language limitations as the core practical barrier.

If this is right

  • Verification can be introduced into AI MSc degrees through student dissertation projects.
  • Overcoming programming language limitations is required before verification becomes routine in AI teaching.
  • New methods and tools will be needed to make verification accessible to AI graduates.
  • Wider adoption of verification in education would help address safety vulnerabilities in neural networks.

Where Pith is reading between the lines

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

  • Labs using similar student-project models at other universities could test whether language limitations remain the dominant obstacle once curriculum changes are tried.
  • Resolving language barriers for education might also accelerate verified neural network use in deployed AI systems.
  • Prioritizing neural network verification in teaching suggests that deep learning safety problems are seen as more urgent than verification for other AI techniques.

Load-bearing premise

The primary barriers to incorporating verification into AI degrees are limitations in existing programming languages used for verification, rather than other factors such as curriculum design, student background, or availability of suitable verification problems.

What would settle it

A survey of multiple AI MSc programs showing that curriculum design or student background explains the lack of verification teaching more than language limitations do.

Figures

Figures reproduced from arXiv: 1907.01297 by Daniel Kienitz, Ekaterina Komendantskaya, Kirsy Duncan, Pascal Bacchus, Pierre Le Hen, Rob Stewart.

Figure 1
Figure 1. Figure 1: Given a trained neural network and a correctly classified image of “0” on the left, we can create a perturbation η (middle) to the original image so that the same neural network predicts a “3” with 92% confidence for the modified image (right). The second kind of verification projects usually uses Python for the machine learning part and SMT solvers (such as Z3 [13]) for verification component, and often r… view at source ↗
Figure 2
Figure 2. Figure 2: Left: An example of a neuron in the last hidden layer L: Its potential is z 2 L = (Pn i=1 w (i) L−1 z (i) L−1 ) + bL−1. Right: A multi-layer feed-forward neural network for a two class classification problem. Yellow: input layer; Blue: hidden layers; Red: biases; Green: output layer. 2 Background: Neural Networks and their Robustness The standard feed-forward neural network (also called multi-layer percept… view at source ↗
Figure 3
Figure 3. Figure 3: Toy running example. Left: Perceptron computing the logical connective and. Right: The “training data set” for and. neural network. For example, in the setting of image classification, this is done by adding a vector r ∈ R n to the input x ∈ R n of the neural network, while keeping ||r||p as small as possible with respect to a user specified p-norm5 : min ||r||p such that y = f(x) 6= f(x + r), (4) where y … view at source ↗
Figure 4
Figure 4. Figure 4: A snippet of Python code implementing a Perceptron. can be used irrespective of the Python library in which the students implement their networks. The Python/Z3 verification workflow will generally comprise of the following steps: – Implement the neural network in Python. Example 3. We define in Python the Perceptron given in [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: A snippet of Python code implementing the and-gate Perceptron verification. course of Data Mining and Machine Learning for MSc students with AI spe￾cialisms at Heriot-Watt University. Simplicity of use is thus the first benefit of choosing Z3 Python API. This methodology has been used in complex extensions, including e.g. [6,17]. There, deep convolutional neural networks were verified via Z3 Python API, an… view at source ↗
Figure 6
Figure 6. Figure 6: Coq record type defining a Perceptron. 4 ITP Approach to Neural Network Verification An alternative approach, that would resolve all three shortcomings identified in the previous section, is the ITP approach, as advocated in e.g. [1,2]. It amounts to first defining neural networks directly in Coq, and then proving properties about these definitions directly, thus avoiding programming in Python at the verif… view at source ↗
Figure 7
Figure 7. Figure 7: Coq function that computes neuron’s potential; formal definition of the notion of the “next output”, cf. [2]. any concrete Perceptron). For example, one may want to prove that, feeding any input of the correct type to a Perceptron, we always get the next output within a permissible range [PITH_FULL_IMAGE:figures/full_fig_p010_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: A snippet of Coq’s output computing function Pp. 5 F ∗ : A Hybrid Approach to Neural Net Verification In this section we investigate whether new hybrid languages, such as Microsoft’s F ∗ [11], bear promise to resolve major drawbacks of the two approaches we surveyed so far. F ∗ is a general-purpose functional programming language with effects, that combines the automation of an SMT solver Z3 with dependent… view at source ↗
Figure 9
Figure 9. Figure 9: F ∗ record type defining a Perceptron. 1 val perceptron : neuron 2 let perceptron = MakeNeuron [1] [0.194R ; 0.195R] 0.184R 1.0R Compare this with Example 6, in which we used Coq’s rational numbers to approximate floating point numbers of Python. Proofs of properties that were impossible in Coq due to the Coq’s implemen￾tation of function evaluation, now come fully automated via Z3’s theory of linear real … view at source ↗
read the original abstract

Rapid development of AI applications has stimulated demand for, and has given rise to, the rapidly growing number and diversity of AI MSc degrees. AI and Robotics research communities, industries and students are becoming increasingly aware of the problems caused by unsafe or insecure AI applications. Among them, perhaps the most famous example is vulnerability of deep neural networks to ``adversarial attacks''. Owing to wide-spread use of neural networks in all areas of AI, this problem is seen as particularly acute and pervasive. Despite of the growing number of research papers about safety and security vulnerabilities of AI applications, there is a noticeable shortage of accessible tools, methods and teaching materials for incorporating verification into AI programs. LAIV -- the Lab for AI and Verification -- is a newly opened research lab at Heriot-Watt university that engages AI and Robotics MSc students in verification projects, as part of their MSc dissertation work. In this paper, we will report on successes and unexpected difficulties LAIV faces, many of which arise from limitations of existing programming languages used for verification. We will discuss future directions for incorporating verification into AI degrees.

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

1 major / 2 minor

Summary. The manuscript is an experience report describing the LAIV lab at Heriot-Watt University and its efforts to involve AI and Robotics MSc students in neural network verification projects as part of dissertation work. It asserts a noticeable shortage of accessible tools, methods and teaching materials for verification in AI programs, reports on project successes and difficulties (many attributed to limitations of existing programming languages), and outlines future directions for incorporating verification into AI degrees.

Significance. As an observational account of lab activities, the paper could usefully inform educators seeking to add verification content to AI curricula by surfacing concrete implementation obstacles. Its significance remains modest because the central observations rest on author experience without supporting measurements, surveys or external references.

major comments (1)
  1. [Abstract] Abstract: the assertion of a 'noticeable shortage of accessible tools, methods and teaching materials for incorporating verification into AI programs' is presented as fact but is unsupported by any data, statistics, citations to existing tool surveys, or references to AI degree curricula; this claim is load-bearing for the motivation of both the lab and the paper.
minor comments (2)
  1. [Abstract] Abstract: 'Despite of the growing number' is grammatically incorrect and should read 'Despite the growing number'.
  2. [Abstract] Abstract: the repeated use of future tense ('we will report', 'We will discuss') is atypical for a completed manuscript; rephrase to present tense to match the reporting style of an experience report.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the review and the suggestion to strengthen the motivation section. We address the major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the assertion of a 'noticeable shortage of accessible tools, methods and teaching materials for incorporating verification into AI programs' is presented as fact but is unsupported by any data, statistics, citations to existing tool surveys, or references to AI degree curricula; this claim is load-bearing for the motivation of both the lab and the paper.

    Authors: We agree that the statement is presented without external supporting data, surveys or citations. As this is an experience report grounded in the LAIV lab's direct work with AI and Robotics MSc students, the observation arises from repeated practical difficulties encountered when assigning verification-related dissertation projects. To address the concern we will revise the abstract to frame the claim explicitly as an observation from our lab activities rather than an unsubstantiated general assertion. We will also add a small number of references to existing AI-safety and verification literature where they help contextualise the shortage without changing the paper's observational character. revision: partial

Circularity Check

0 steps flagged

No significant circularity: purely descriptive experience report

full rationale

The paper is an experience report describing LAIV lab activities, MSc student projects, observed shortages of tools, and practical difficulties with existing programming languages. It contains no equations, derivations, predictions, fitted parameters, or formal claims whose validity depends on hidden assumptions. All content is observational narrative with no load-bearing technical steps, self-citations, or reductions to inputs by construction. The central narrative is presented as direct reporting rather than a derived result, making the paper self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No technical derivations, parameters, or entities are introduced; the paper is an experience report on education.

pith-pipeline@v0.9.0 · 5732 in / 941 out tokens · 18216 ms · 2026-05-25T11:22:15.245952+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

19 extracted references · 19 canonical work pages · 4 internal anchors

  1. [1]

    AAAI (2019)

    Bagnall, A., Stewart, G.: Certifying the true error: Machine learning in Coq with verified generalisation guarantees. AAAI (2019)

    work page 2019

  2. [2]

    In: CSBio 2018 Proceedings of the 9th Interna- tional Conference on Computational Systems-Biology and Bioinformatics (2018)

    Bahrami, A., de Maria, E., A.Felty: Modelling and verifying dynamic properties of biological neural networks in Coq. In: CSBio 2018 Proceedings of the 9th Interna- tional Conference on Computational Systems-Biology and Bioinformatics (2018)

    work page 2018

  3. [3]

    In: Beringer, L., Felty, A.P

    Cohen, C.: Construction of real algebraic numbers in coq. In: Beringer, L., Felty, A.P. (eds.) Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings. Lecture Notes in Computer Science, vol. 7406, pp. 67–82. Springer (2012)

    work page 2012

  4. [4]

    Coq Development Team: Coq reference manual (2015), https://coq.inria.fr/ Neural Network Verification for the Masses (of AI graduates) 15

    work page 2015

  5. [5]

    Hinton, G., Deng, L., Yu, D., Dahl, G.E., rahman Mohamed, A., Jaitly, N., Senior, A., Vanhoucke, V., Nguyen, P., Sainath, T.N., Kingsbury, B.: Deep neural networks for acoustic modeling in speech recognition: The shared views of four research groups 29, 82 – 97 (2012), https://ieeexplore.ieee.org/document/6296526

    work page arXiv 2012

  6. [6]

    In: Majumdar, R., Kuncak, V

    Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10426, pp. 3–29. Springer (2017), https://doi.org/10.1007/978...

    work page doi:10.1007/978-3-319-63387-9 2017

  7. [7]

    Human-level performance in first-person multiplayer games with population-based deep reinforcement learning

    Jaderberg, M., Czarnecki, W.M., Dunning, I., Marris, L., Lever, G., Casta˜ neda, A.G., Beattie, C., Rabinowitz, N.C., Morcos, A.S., Ruderman, A., Sonnerat, N., Green, T., Deason, L., Leibo, J.Z., Silver, D., Hassabis, D., Kavukcuoglu, K., Graepel, T.: Human-level performance in first-person multiplayer games with population-based deep reinforcement learnin...

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  8. [8]

    Komendantskaya

    Kientiz, D.: Verification of evolved neural networks: MSc progress report (2019), Heriot-Watt University, Supervisor E. Komendantskaya

    work page 2019

  9. [9]

    Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep con- volutional neural networks. Commun. ACM 60(6), 84–90 (2017)

    work page 2017

  10. [10]

    Komendantskaya

    LeHen, P.: Verification of neural networks: MSc progress report (2019), Heriot- Watt University, Supervisor E. Komendantskaya

    work page 2019

  11. [11]

    In: Caires, L

    Mart´ ınez, G., Ahman, D., Dumitrescu, V., Giannarakis, N., Hawblitzel, C., Hritcu, C., Narasimhamurthy, M., Paraskevopoulou, Z., Pit-Claudel, C., Protzenko, J., Ramananandro, T., Rastogi, A., Swamy, N.: Meta-fstar : Proof automation with smt, tactics, and metaprograms. In: Caires, L. (ed.) Programming Languages and Systems - 28th European Symposium on Pr...

    work page 2019

  12. [12]

    Bulletin of Math

    McCulloch, W., Pitts, W.: A logical calculus of the ideas immanent in nervous activity. Bulletin of Math. Bio. 5, 115–133 (1943)

    work page 1943

  13. [13]

    In: TACAS’08

    de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS’08. LNCS, vol. 4963, pp. 337–340 (2008)

    work page 2008

  14. [14]

    In: Brand, J., Valenti, M.C., Ak- inpelu, A., Doshi, B.T., Gorsic, B.L

    Papernot, N., McDaniel, P.D., Swami, A., Harang, R.E.: Crafting adversarial in- put sequences for recurrent neural networks. In: Brand, J., Valenti, M.C., Ak- inpelu, A., Doshi, B.T., Gorsic, B.L. (eds.) 2016 IEEE Military Communica- tions Conference, MILCOM 2016, Baltimore, MD, USA, November 1-3, 2016. pp. 49–54. IEEE (2016), http://ieeexplore.ieee.org/x...

    work page 2016

  15. [15]

    Detecting Adversarial Examples in Convolutional Neural Networks

    Pertigkiozoglou, S., Maragos, P.: Detecting adversarial examples in convolutional neural networks. CoRR abs/1812.03303 (2018), http://arxiv.org/abs/1812. 03303

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  16. [16]

    Adversarial Examples - A Complete Characterisation of the Phenomenon

    Serban, A.C., Poll, E.: Adversarial examples - A complete characterisation of the phenomenon. CoRR abs/1810.01185 (2018), http://arxiv.org/abs/1810. 01185

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  17. [17]

    PACMPL 3(POPL), 41:1–41:30 (2019), https://doi.org/10

    Singh, G., Gehr, T., P¨ uschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. PACMPL 3(POPL), 41:1–41:30 (2019), https://doi.org/10. 1145/3290354

    work page 2019

  18. [18]

    Intriguing properties of neural networks

    Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fer- gus, R.: Intriguing properties of neural networks. CoRR abs/1312.6199 (2014), https://arxiv.org/abs/1312.6199

    work page internal anchor Pith review Pith/arXiv arXiv 2014

  19. [19]

    Yann LeCun, Corinna Cortes, C.J.B.: The mnist datbase of handwritten digits” http://yann.lecun.com/exdb/mnist/

    work page