基本函数的证明近似
Dandelion: Certified Approximations of Elementary Functions
摘要：
像sin和exp这样的初等函数运算一般不能在今天的数字计算机上精确计算，因此必须近似计算。库函数中的标准近似通常只提供有限的精度集，并且对于许多应用程序来说效率太低。为有限的输入域和输出精度定制的多项式近似可以提供卓越的性能。事实上，Remez算法计算给定多项式次数的最佳可能近似，但迄今为止尚未得到正式验证。本文介绍了Daneclit，一个自动证书检查器的多项式近似的基本函数计算与Remez类算法，充分验证了HOL4定理证明。Danvet检查多项式近似与其目标参考初等函数之间的差异是否保持低于给定约束中所有输入的给定误差范围。通过使用CakeML编译器提取经过验证的二进制文件，Danvet可以在合理的时间内验证证书，完全自动化以前的手动验证近似值。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
