nach oben

Journal of Automated Reasoning

Erschienen in:

01.10.2016

Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq

verfasst von: Érik Martin-Dorel, Guillaume Melquiond

Erschienen in: Journal of Automated Reasoning | Ausgabe 3/2016

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

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.

Nächster Artikel A Learning-Based Fact Selector for Isabelle/HOL

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

http://lipforge.ens-lyon.fr/www/crlibm/.

Binary64 is the name of the IEEE 754–2008 floating-point format that was formerly known as the “double precision” format.

https://code.google.com/p/flyspeck/.

The author of NLCertify is considering relying on CoqInterval to check the quadratic forms that bound elementary functions. This would be a step further in getting completely verified results with NLCertify.

An interval function \(\mathbf {f}\) is isotone if, for any pair of intervals \((\mathbf {x},\mathbf {x'})\), we have \(\mathbf {x}\subseteq \mathbf {x'}\implies \mathbf {f}(\mathbf {x})\subseteq \mathbf {f}(\mathbf {x'})\) (see also [11, Definition 4.8.10]).

http://www.jhauser.us/arithmetic/SoftFloat.html.

http://www.mpfr.org/.

The unit in the last place of a real number x is the gap between the two floating-point numbers enclosing x in a given format (see also [22, p. 32]).

i.e. in the univariate case, P is considered as \(P(x)=\sum \nolimits _{i=0}^n P_i\cdot (x-x_0)^i\) for a given expansion point \(x_0\).

Namely, we use this simple algorithm when computing a Taylor model for identity or constant functions, as the estimation of the Taylor–Lagrange remainder is already sharp in this case.

https://code.google.com/p/hol-light/.

https://code.google.com/p/flyspeck/source/browse/#svn/trunk/formal_ineqs.

http://forge.ocamlcore.org/projects/nl-certify.

https://metitarski.googlecode.com/hg-history/V2_4/tptp/Problems/atan-problem-1-sqrt.tptp.

Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175–205 (2010). doi:10.1007/s10817-009-9149-2 MathSciNetMATHCrossRef

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

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

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

Ceberio, M., Granvilliers, L.: Horner’s rule for interval evaluation revisited. Computing 69(1), 51–81 (2002). doi:10.1007/s00607-002-1448-y MathSciNetMATHCrossRef

Chevillard, S., Harrison, J., Joldeş, M., Lauter, C.: Efficient and accurate computation of upper bounds of approximation errors. J. Theor. Comput. Sci. 412(16), 1523–1543 (2011). doi:10.1016/j.tcs.2010.11.052 MathSciNetMATHCrossRef

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)

Daumas, M., Lester, D., Muñoz, C.: Verified real number calculations: a library for interval arithmetic. IEEE Trans. Comput. 58(2), 226–237 (2009)MathSciNetCrossRef

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

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)

14.

Joldeş, M.: Rigorous Polynomial Approximations and Applications. Ph.D. thesis, ENS de Lyon, France (2011). http://tel.archives-ouvertes.fr/tel-00657843/en/

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(4), 379–456 (2003)MathSciNetMATH

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

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)

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

20.

Melquiond, G.: Floating-point arithmetic in the Coq system. Inf. Comput. 216, 14–23 (2012). doi:10.1016/j.ic.2011.09.005 MathSciNetMATHCrossRef

21.

Moore, R.E.: Interval Analysis. Prentice-Hall, Englewood Cliffs (1966)MATH

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 MATHCrossRef

23.

Muñoz, C., Narkawicz, A.: Formalization of a representation of Bernstein polynomials and applications to global optimization. J. Autom. Reason. 51(2), 151–196 (2013). doi:10.1007/s10817-012-9256-3 MATHCrossRef

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, P.T.P.: Table-driven implementation of the exponential function in IEEE floating-point arithmetic. ACM Trans. Math. Softw. 15(2), 144–157 (1989). doi:10.1145/63522.214389 MATHCrossRef

27.

Ziv, A.: Fast evaluation of elementary mathematical functions with correctly rounded last bit. ACM Trans. Math. Softw. 17(3), 410–423 (1991). doi:10.1145/114697.116813 MATHCrossRef

28.

Zumkeller, R.: Global Optimization in Type Theory. Ph.D. thesis, École polytechnique, France (2008). http://alacave.net/~roland/FormalGlobalOpt.pdf

Titel: Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
verfasst von: Érik Martin-Dorel
Guillaume Melquiond
Publikationsdatum: 01.10.2016
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 3/2016
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-015-9350-4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Premium Partner