Verifying Numerical Methods with Isabelle/HOL

TL;DR

This paper introduces a framework in Isabelle/HOL for verifying numerical algorithms, enabling formal correctness proofs and code generation for reliable scientific computing.

Contribution

It presents a user-friendly specification language, automated proof support, and extensions to formal mathematics libraries for verifying numerical methods.

Findings

Successfully verified bisection and fixed-point iteration methods.

Generated executable code from verified specifications.

Enhanced Isabelle/HOL libraries with derivatives and Taylor's theorem.

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.