Dandelion: Certified Approximations of Elementary Functions

TL;DR

Dandelion is a verified tool that certifies polynomial approximations of elementary functions, ensuring they meet specified error bounds across input domains, thereby improving reliability and automation in function approximation verification.

Contribution

It introduces Dandelion, the first fully verified certificate checker for polynomial approximations of elementary functions using HOL4, automating and formalizing the verification process.

Findings

Dandelion successfully verifies polynomial approximations within specified error bounds.

The tool automates the certification process, reducing manual effort.

Verified certificates can be efficiently validated with extracted binaries.

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.