License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2022.6
URN: urn:nbn:de:0030-drops-167155
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16715/
Becker, Heiko ;
Tekriwal, Mohit ;
Darulova, Eva ;
Volkova, Anastasia ;
Jeannin, Jean-Baptiste
Dandelion: Certified Approximations of Elementary Functions
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.
BibTeX - Entry
@InProceedings{becker_et_al:LIPIcs.ITP.2022.6,
author = {Becker, Heiko and Tekriwal, Mohit and Darulova, Eva and Volkova, Anastasia and Jeannin, Jean-Baptiste},
title = {{Dandelion: Certified Approximations of Elementary Functions}},
booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
pages = {6:1--6:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-252-5},
ISSN = {1868-8969},
year = {2022},
volume = {237},
editor = {Andronick, June and de Moura, Leonardo},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16715},
URN = {urn:nbn:de:0030-drops-167155},
doi = {10.4230/LIPIcs.ITP.2022.6},
annote = {Keywords: elementary functions, approximation, certificate checking}
}
