Item

Abstract

Elementary function operations such as sin and exp cannot in general be
computed exactly on today's digital computers, and thus have to be
approximated. The standard approximations in library functions typically
provide only a limited set of precisions, and are too inefficient for many
applications. Polynomial approximations that are customized to a limited input
domain and output accuracy can provide superior performance. In fact, the Remez
algorithm computes the best possible approximation for a given polynomial
degree, but has so far not been formally verified.
This paper presents Dandelion, an automated certificate checker for
polynomial approximations of elementary functions computed with Remez-like
algorithms that is fully verified in the HOL4 theorem prover. Dandelion checks
whether the difference between a polynomial approximation and its target
reference elementary function remains below a given error bound for all inputs
in a given constraint. By extracting a verified binary with the CakeML
compiler, Dandelion can validate certificates within a reasonable time, fully
automating previous manually verified approximations.