Verifying Numerical Methods with Isabelle/HOL

TL;DR

The paper tackles the challenging problem of formally verifying numerical methods used in machine learning and cyber-physical systems by building an Isabelle/HOL framework based on ITrees. It introduces a verification condition generator with Hoare-style reasoning, enabling end-to-end verification and code extraction for real-valued algorithms. The authors formalise and verify two core methods, the bisection method and the fixed-point iteration, and extend the mathematical toolkit with higher-order differentiation and Taylor's theorem in Peano form to support rigorous proofs, including contraction-based convergence. Empirically, the framework demonstrates automation via Sledgehammer and vcg, achieving substantial automatic proof work while enabling precise, machine-checked guarantees that can be exported as executable sources, with potential impact on reliable ML and control systems.

Abstract

Modern machine learning pipelines are built on numerical algorithms. Reliable numerical methods are thus a prerequisite for trustworthy machine learning and cyber-physical systems. Therefore, we contribute a framework for verified numerical methods in Isabelle/HOL based on ITrees. Our user-friendly specification language enables the direct declaration of numerical programs that can be annotated with variants and invariants for reasoning about correctness specifications. The generated verification conditions can be discharged via automated proof methods and lemmas from the HOL-Analysis library. The ITrees foundation interacts with Isabelle's code generator to export source code. This provides an end-to-end path from formal specifications with machine-checked guarantees to executable sources. We illustrate the process of modelling numerical methods and demonstrate the effectiveness of the verification by focusing on two well-known methods, the bisection method and the fixed-point iteration method. We also contribute crucial extensions to the libraries of formalised mathematics required for this objective: higher-order derivatives and Taylor's theorem in Peano form. Finally, we qualitatively evaluate the use of the framework for verifying numerical methods.