Title: IsaGrad: Verified Automatic Differentiation over Computational Graphs in Imperative HOL
Speakers: Alex Hyman
Abstract:

We present IsaGrad, a formalisation of scalar reverse automatic differentiation (RAD) over mutable reference-based computational graphs using the Imperative HOL library of Isabelle, and verify its functional correctness by an interactive separation-logic proof. We use IsaGrad as the differentiation engine for two machine learning case studies: training a multi-layer perceptron and a recurrent neural network. Leveraging Isabelle’s code generation, we extract imperative-style Haskell programs where the training process is backed by our verified algorithm. To our knowledge, our implementation is the first of its kind to prove the functional correctness of an imperative, heap-based RAD algorithm. Beyond showcasing Imperative HOL’s expressiveness, this work demonstrates how formal verification increases confidence in computational graphs used for gradient-based optimisation, including neural network training.