Verifying Numerical Methods with Isabelle/HOL

Abstract

Modern machine learning pipelines and ODE solvers are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-physical systems. We evaluate a framework designed for verifying imperative programs and the Isabelle proof assistant as tools for proving the total correctness of four numerical algorithms: the bisection method, the fixed-point method, the perceptron, and the gradient descent algorithm. Our verifications required subtle extensions and generalisations to Isabelle's version of Taylor's theorem and higher-order derivatives. Finally, we reflect on the framework's automation, friendly syntax, and on further requirements to turn it into a verification tool for numerical methods.

arXiv commentThis paper has been accepted for presentation at SEFM 2026; it is 18 pages and has 16 listings, for accompanying formalisation, see https://doi.org/10.5281/zenodo.17679525