Document Open Access Logo

Dandelion: Certified Approximations of Elementary Functions

Authors Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, Jean-Baptiste Jeannin

PDF
Thumbnail PDF

File

LIPIcs.ITP.2022.6.pdf
  • Filesize: 0.76 MB
  • 19 pages

Document Identifiers

Author Details

Heiko Becker
  • MPI-SWS, Saarland Informatics Campus (SIC), Germany
Mohit Tekriwal
  • University of Michigan, Ann Arbor, MI, USA
Eva Darulova
  • Uppsala University, Sweden
Anastasia Volkova
  • Nantes Université, France
Jean-Baptiste Jeannin
  • University of Michigan, Ann Arbor, MI, USA

Funding

This work was supported in part by the University of Michigan.

Acknowledgements

The authors would like to thank John Harrison for the insightful discussion and for providing the source code for his paper that inspired the Dandelion work. Further, we thank Magnus Myreen and Michael Norrish for their help with improving the HOL4 implementation of Dandelion. We also thank Samuel Coward for helping us with the MetiTarski evaluation. Finally, we thank the anonymous ITP reviewers for their feedback on the paper. {}

Cite AsGet BibTex

Heiko Becker, Mohit Tekriwal, Eva Darulova, Anastasia Volkova, and Jean-Baptiste Jeannin. Dandelion: Certified Approximations of Elementary Functions. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 6:1-6:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITP.2022.6

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • elementary functions
  • approximation
  • certificate checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Oskar Abrahamsson, Son Ho, Hrutvik Kanabar, Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Yong Kiam Tan. Proof-Producing Synthesis of CakeML from Monadic HOL Functions. Journal of Automated Reasoning (JAR), 64(7), 2020. URL: https://doi.org/10.1007/s10817-020-09559-8.
  2. Behzad Akbarpour, Amr Abdel-Hamid, Sofiène Tahar, and John Harrison. Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. The Computer Journal, 53:465-488, May 2010. URL: https://doi.org/10.1093/comjnl/bxp023.
  3. Behzad Akbarpour and Lawrence Charles Paulson. MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. Journal of Automated Reasoning (JAR), 44(3):175-205, 2010. URL: https://doi.org/10.1007/s10817-009-9149-2.
  4. Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O Myreen, and Anthony Fox. A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4. In Formal Methods in Computer Aided Design (FMCAD), 2018. URL: https://doi.org/10.23919/FMCAD.2018.8603019.
  5. Hans-J. Boehm. Towards an API for the Real Numbers. In Programming Language Design and Implementation (PLDI), 2020. URL: https://doi.org/10.1145/3385412.3386037.
  6. Florent Bréhard, Assia Mahboubi, and Damien Pous. A Certificate-Based Approach to Formally Verified Approximations. In Interactive Theorem Proving (ITP), 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.8.
  7. Nicolas Brisebarre and Sylvain Chevillard. Efficient polynomial L-approximations. In IEEE Symposium on Computer Arithmetic (ARITH), 2007. URL: https://doi.org/10.1109/ARITH.2007.17.
  8. S. Chevillard, M. Joldeş, and C. Lauter. Sollya: An Environment for the Development of Numerical Codes. In International Congress on Mathematical Software (ICMS), 2010. URL: https://doi.org/10.1007/978-3-642-15582-6_5.
  9. Sylvain Chevillard, John Harrison, Mioara Joldeş, and Ch Lauter. Efficient and accurate computation of upper bounds of approximation errors. Theoretical Computer Science, 412(16):1523-1543, 2011. URL: https://doi.org/10.1016/j.tcs.2010.11.052.
  10. The Coq Proof Assistant. URL: https://coq.inria.fr.
  11. Samuel Coward, Lawrence Paulson, Theo Drane, and Emiliano Morini. Formal Verification of Transcendental Fixed and Floating Point Algorithms using an Automatic Theorem Prover. Formal Aspects of Computing (in press), 2022. Google Scholar
  12. Nasrine Damouche, Matthieu Martel, Pavel Panchekha, Chen Qiu, Alexander Sanchez-Stern, and Zachary Tatlock. Toward a Standard Benchmark Format and Suite for Floating-Point Analysis. In Numerical Software Verification (NSV), 2016. URL: https://doi.org/10.1007/978-3-319-54292-8_6.
  13. Catherine Daramy, David Defour, Florent de Dinechin, and Jean-Michel Muller. CR-LIBM: a correctly rounded elementary function library. In Advanced Signal Processing Algorithms, Architectures, and Implementations, volume 5205, pages 458-464. International Society for Optics and Photonics, 2003. Google Scholar
  14. Eva Darulova and Anastasia Volkova. Sound Approximation of Programs with Elementary Functions. In Computer Aided Verification (CAV), 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_11.
  15. Manuel Eberl. A Decision Procedure for Univariate Real Polynomials in Isabelle/HOL. In Certified Programs and Proofs (CPP), 2015. URL: https://doi.org/10.1145/2676724.2693166.
  16. Sicun Gao, Soonho Kong, and Edmund M Clarke. dReal: An SMT solver for nonlinear theories over the reals. In Conference on Automated Deduction (CADE), 2013. URL: https://doi.org/10.1007/978-3-642-38574-2_14.
  17. John Harrison. "floating point verification in hol light: The exponential function". In Algebraic Methodology and Software Technology (AMAST), 1997. URL: https://doi.org/10.1007/BFb0000475.
  18. John Harrison. Verifying the accuracy of polynomial approximations in HOL. In Theorem Proving in Higher Order Logics (TPHOLs), 1997. URL: https://doi.org/10.1007/BFb0028391.
  19. John Harrison. Verifying nonlinear real formulas via sums of squares. In Theorem Proving in Higher Order Logics (TPHOLs), 2007. URL: https://doi.org/10.1007/978-3-540-74591-4_9.
  20. The HOL-Light Proof Assistant. URL: https://www.cl.cam.ac.uk/~jrh13/hol-light/.
  21. Johannes Hölzl. Proving inequalities over reals with computation in isabelle/hol. In Programming Languages for Mechanized Mathematics Systems, 2009. Google Scholar
  22. Joe Hurd. First-Order Proof Tactics in Higher-Order Logic Theorem Provers. In Design and Application of Strategies/Tactics in Higher Order Logics, number NASA/CP-2003-212448 in NASA Technical Reports, 2003. Google Scholar
  23. The Isabelle/HOL Proof Assistant. URL: https://isabelle.in.tum.de/.
  24. Anastasiia Izycheva, Eva Darulova, and Helmut Seidl. Synthesizing Efficient Low-Precision Kernels. In Automated Technology for Verification and Analysis (ATVA), 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_17.
  25. Olga Kupriianova and Christoph Lauter. Metalibm: A Mathematical Functions Code Generator. In International Congress on Mathematical Software (ICMS), 2014. URL: https://doi.org/10.1007/978-3-662-44199-2_106.
  26. Wenda Li, Grant Olney Passmore, and Lawrence C Paulson. Deciding univariate polynomial problems using untrusted certificates in isabelle/hol. Journal of Automated Reasoning, 62(1):69-91, 2019. URL: https://doi.org/10.1007/s10817-017-9424-6.
  27. Jay P Lim and Santosh Nagarakatte. One Polynomial Approximation to Produce Correctly Rounded Results of an Elementary Function for Multiple Representations and Rounding Modes. Principles of Programming Languages (POPL), 2022. URL: https://doi.org/10.1145/3498664.
  28. Érik Martin-Dorel and Guillaume Melquiond. CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq. In Conference on Effective Analysis: Foundations, Implementations, Certification, 2016. Google Scholar
  29. Érik Martin-Dorel and Guillaume Melquiond. Proving tight bounds on univariate expressions with elementary functions in Coq. Journal of Automated Reasoning (JAR), 57(3):187-217, 2016. URL: https://doi.org/10.1007/s10817-015-9350-4.
  30. R.E. Moore. Interval Analysis. Prentice-Hall, 1966. Google Scholar
  31. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  32. Jean-Michel Muller. Elementary Functions. Springer, 2006. Google Scholar
  33. César Muñoz, Anthony Narkawicz, George Hagen, Jason Upchurch, Aaron Dutle, María Consiglio, and James Chamberlain. DAIDALUS: detect and avoid alerting logic for unmanned systems. In Digital Avionics Systems Conference (DASC), 2015. Google Scholar
  34. Anthony Narkawicz, César Munoz, and Aaron Dutle. Formally-Verified Decision Procedures for Univariate Polynomial Computation Based on Sturm’s and Tarski’s theorems. Journal of Automated Reasoning (JAR), 54(4):285-326, 2015. URL: https://doi.org/10.1007/s10817-015-9320-x.
  35. Anthony Narkawicz, Cesar Munoz, and Aaron Dutle. A decision procedure for univariate polynomial systems based on root counting and interval subdivision. Journal of Formalized Reasoning, 11(1):19, 2018. URL: https://doi.org/10.6092/issn.1972-5787/8212.
  36. Ricardo Pachón and Lloyd N Trefethen. Barycentric-Remez Algorithms for Best Polynomial Approximation in the Chebfun System. BIT Numerical Mathematics, 49(4):721, 2009. Google Scholar
  37. Konrad Slind and Michael Norrish. A Brief Overview of HOL4. In Theorem Proving in Higher Order Logics (TPHOLs), 2008. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  38. Geoff Sutcliffe, Jürgen Zimmer, and Stephan Schulz. Tstp data-exchange formats for automated theorem proving tools. Distributed Constraint Problem Solving and Reasoning in Multi-Agent Systems, 112:201-215, 2004. Google Scholar
  39. Yong Kiam Tan, Magnus O. Myreen, Ramana Kumar, Anthony Fox, Scott Owens, and Michael Norrish. The Verified CakeML Compiler Backend. Journal of Functional Programming (JFP), 29, 2019. URL: https://doi.org/10.1017/S0956796818000229.
  40. Ping-Tak Peter Tang. Table-driven implementation of the exponential function in IEEE floating-point arithmetic. ACM Transactions on Mathematical Software (TOMS), 15(2):144-157, 1989. URL: https://doi.org/10.1145/63522.214389.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact