From: "Thiemann, René" <cl-isabelle-users@lists.cam.ac.uk>
Dear all,
I’m happy to announce a new AFP entry.
Formalizing Neural Networks
by Achim D. Brucker and Amy Stell
Abstract
Deep learning, i.e., machine learning using neural networks, is used
successfully in many application areas. Still, their use in safety-critical or
security-critical applications is limited, due to the lack of testing and
verification techniques. We address this problem by formalizing an important
class of neural networks, feed-forward neural networks, in Isabelle/HOL. We
present two different approaches of formalizing feed-forward networks and show
their equivalence as well as demonstrate their use in verifying certain safety
and correctness properties of various example. Moreover, we do not only provide
a formal model that allows to reason over feed-forward neural networks, we also
provide a datatype package for Isabelle/HOL that supports importing models from
TensorFlow.js.
https://www.isa-afp.org/entries/Neural_Networks.html
Enjoy,
René
Last updated: Dec 02 2025 at 16:32 UTC