×

zbMATH — the first resource for mathematics

Proving tight bounds on univariate expressions with elementary functions in Coq. (English) Zbl 1386.68151
Summary: The verification of floating-point mathematical libraries requires computing numerical bounds on approximation errors. Due to the tightness of these bounds and the peculiar structure of approximation errors, such a verification is out of the reach of generic tools such as computer algebra systems. In fact, the inherent difficulty of computing such bounds often mandates a formal proof of them. In this paper, we present a tactic for the Coq proof assistant that is designed to automatically and formally prove bounds on univariate expressions. It is based on a formalization of floating-point and interval arithmetic, associated with an on-the-fly computation of Taylor expansions. All the computations are performed inside Coq’s logic, in a reflexive setting. This paper also compares our tactic with various existing tools on a large set of examples.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
41A58 Series expansions (e.g., Taylor, Lidstone series, but not Fourier series)
65G50 Roundoff error
Software:
Coq; Flocq; MetiTarski; PVS; Sollya
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Akbarpour, B; Paulson, LC, Metitarski: an automatic theorem prover for real-valued special functions, J. Autom. Reason., 44, 175-205, (2010) · Zbl 1215.68206
[2] Allamigeon, X., Gaubert, S., Magron, V., Werner, B.: Certification of bounds of non-linear functions: the templates method. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) Intelligent Computer Mathematics—MKM, Calculemus, DML, and Systems and Projects. Lecture Notes in Computer Science, vol. 7961, pp. 51-65 (2013). doi:10.1007/978-3-642-39320-4_4 · Zbl 1390.68570
[3] Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: Antelo, E., Hough, D., Ienne, P. (eds.) Proceedings of the 20th IEEE Symposium on Computer Arithmetic, pp. 243-252. Tübingen, Germany (2011). doi:10.1109/ARITH.2011.40
[4] Brisebarre, N., Joldeş, M., Martin-Dorel, É., Mayero, M., Muller, J.M., Paşca, I., Rideau, L., Théry, L.: Rigorous polynomial approximation using Taylor models in Coq. In: Goodloe, A., Person, S. (eds.) Proceedings of 4th International Symposium on NASA Formal Methods. Lecture Notes in Computer Science, vol. 7226, pp. 85-99. Springer, Norfolk (2012). doi:10.1007/978-3-642-28891-3_9 · Zbl 1314.68286
[5] Ceberio, M; Granvilliers, L, Horner’s rule for interval evaluation revisited, Computing, 69, 51-81, (2002) · Zbl 1017.65013
[6] Chevillard, S; Harrison, J; Joldeş, M; Lauter, C, Efficient and accurate computation of upper bounds of approximation errors, J. Theor. Comput. Sci., 412, 1523-1543, (2011) · Zbl 1211.65025
[7] Chevillard, S., Joldeş, M., Lauter, C.: Sollya: an environment for the development of numerical codes. In: Fukuda, K., van der Hoeven, J., Joswig, M., Takayama, N. (eds.) Proceedings of the 3rd International Congress on Mathematical Software, Lecture Notes in Computer Science, vol. 6327, pp. 28-31. Heidelberg (2010) · Zbl 1295.65143
[8] Daumas, M; Lester, D; Muñoz, C, Verified real number calculations: a library for interval arithmetic, IEEE Trans. Comput., 58, 226-237, (2009) · Zbl 1367.65213
[9] Daumas, M., Melquiond, G., Muñoz, C.: Guaranteed proofs using interval arithmetic. In: Montuschi, P., Schwarz, E. (eds.) Proceedings of the 17th IEEE Symposium on Computer Arithmetic, pp. 188-195. Cape Cod, MA (2005). doi:10.1109/ARITH.2005.25
[10] Denman, W., Muñoz, C.: Automated real proving in PVS via MetiTarski. In: Jones, C.B., Pihlajasaari, P., Sun, J. (eds.) FM, Lecture Notes in Computer Science, vol. 8442, pp. 194-199. Springer (2014). doi:10.1007/978-3-319-06410-9_14 · Zbl 1022.65051
[11] Hansen, E., Walster, G.: Global Optimization Using Interval Analysis: Revised and Expanded. Monographs and Textbooks in Pure and Applied Mathematics. CRC Press, Boca Raton (2003)
[12] Harrison, J.: Verifying the accuracy of polynomial approximations in HOL. In: Gunter, E.L., Felty, A.P. (eds.) Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 1275, pp. 137-152. Murray Hill, NJ, USA (1997). doi:10.1007/BFb0028391
[13] Harrison, J.: Verifying nonlinear real formulas via sums of squares. In: Schneider, K., Brandt, J. (eds.) Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics. Lecture Notes in Computer Science, vol. 4732, pp. 102-118. Kaiserslautern, Germany (2007) · Zbl 1144.68357
[14] Joldeş, M.: Rigorous Polynomial Approximations and Applications. Ph.D. thesis, ENS de Lyon, France (2011). http://tel.archives-ouvertes.fr/tel-00657843/en/ · Zbl 1017.65013
[15] Makino, K.: Rigorous Analysis of Nonlinear Motion in Particle Accelerators. Ph.D. thesis, Michigan State University, East Lansing, Michigan, USA (1998)
[16] Makino, K; Berz, M, Taylor models and other validated functional inclusion methods, Int. J. Pure Appl. Math., 4, 379-456, (2003) · Zbl 1022.65051
[17] Martin-Dorel, É., Mayero, M., Paşca, I., Rideau, L., Théry, L.: Certified, efficient and sharp univariate Taylor models in Coq. In: IEEE, SYNASC 2013, pp. 193-200. Timişoara, Romania (2013). doi:10.1109/SYNASC.2013.33 · Zbl 1367.65213
[18] Melquiond, G.: Floating-point arithmetic in the Coq system. In: Proceedings of the 8th Conference on Real Numbers and Computers, pp. 93-102. Santiago de Compostela, Spain (2008) · Zbl 1215.68206
[19] Melquiond, G.: Proving bounds on real-valued functions with computations. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) Proceedings of the 4th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence, vol. 5195, pp. 2-17. Sydney, Australia (2008). doi:10.1007/978-3-540-71070-7_2 · Zbl 1165.68464
[20] Melquiond, G, Floating-point arithmetic in the coq system, Inf. Comput., 216, 14-23, (2012) · Zbl 1257.68131
[21] Moore, R.E.: Interval Analysis. Prentice-Hall, Englewood Cliffs (1966) · Zbl 0176.13301
[22] Muller, J.M., Brisebarre, N., de Dinechin, F., Jeannerod, C.P., Lefèvre, V., Melquiond, G., Revol, N., Stehlé, D., Torres, S.: Handbook of Floating-Point Arithmetic. Birkhäuser, Boston (2010). doi:10.1007/978-0-8176-4705-6 · Zbl 1197.65001
[23] Muñoz, C; Narkawicz, A, Formalization of a representation of Bernstein polynomials and applications to global optimization, J. Autom. Reason., 51, 151-196, (2013) · Zbl 1314.68286
[24] Narkawicz, A., Muñoz, C.: A formally verified generic branching algorithm for global optimization. In: Cohen, E., Rybalchenko, A. (eds.) Proceedings of the 5th International Conference on Verified Software: Theories, Tools, Experiments. Lecture Notes in Computer Science, vol. 8164, pp. 326-343. Menlo Park, CA, USA (2013). doi:10.1007/978-3-642-54108-7_17
[25] Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: Brat, G., Rungta, N., Venet, A. (eds.) Proceedings of the 5th International Symposium on NASA Formal Methods. Lecture Notes in Computer Science, vol. 7871, pp. 383-397. Moffett Field, CA, USA (2013). doi:10.1007/978-3-642-38088-4_26
[26] Tang, PTP, Table-driven implementation of the exponential function in IEEE floating-point arithmetic, ACM Trans. Math. Softw., 15, 144-157, (1989) · Zbl 0900.65047
[27] Ziv, A, Fast evaluation of elementary mathematical functions with correctly rounded last bit, ACM Trans. Math. Softw., 17, 410-423, (1991) · Zbl 0900.65038
[28] Zumkeller, R.: Global Optimization in Type Theory. Ph.D. thesis, École polytechnique, France (2008). http://alacave.net/ roland/FormalGlobalOpt.pdf · Zbl 0900.65047
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.