research-article

Automatically improving accuracy for floating point expressions

Authors:

Pavel Panchekha,

Alex Sanchez-Stern,

James R. Wilcox,

Zachary TatlockAuthors Info & Claims

ACM SIGPLAN Notices, Volume 50, Issue 6

Pages 1 - 11

https://doi.org/10.1145/2813885.2737959

Published: 03 June 2015 Publication History

Abstract

Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate to produce unacceptable results. While the numerical methods literature provides techniques to mitigate rounding error, applying these techniques requires manually rearranging expressions and understanding the finer details of floating point arithmetic. We introduce Herbie, a tool which automatically discovers the rewrites experts perform to improve accuracy. Herbie's heuristic search estimates and localizes rounding error using sampled points (rather than static error analysis), applies a database of rules to generate improvements, takes series expansions, and combines improvements for different input regions. We evaluated Herbie on examples from a classic numerical methods textbook, and found that Herbie was able to improve accuracy on each example, some by up to 60 bits, while imposing a median performance overhead of 40%. Colleagues in machine learning have used Herbie to significantly improve the results of a clustering algorithm, and a mathematical library has accepted two patches generated using Herbie.

References

[1]

M. Altman and M. McDonald. The robustness of statistical abstractions. Political Methodology, 1999.

[2]

M. Altman and M. P. McDonald. Replication with attention to numerical accuracy. Political Analysis, 11(3):302–307, 2003. URL http: //pan.oxfordjournals.org/content/11/3/302.abstract.

[3]

M. Altman, J. Gill, and M. P. McDonald. Numerical Issues in Statistical Computing for the Social Scientist. Springer-Verlag, 2003.

Digital Library

[4]

E. T. Barr, T. Vo, V. Le, and Z. Su. Automatic detection of floating-point exceptions. POPL ’13, 2013.

Digital Library

[5]

F. Benz, A. Hildebrandt, and S. Hack. A dynamic program analysis to find floating-point accuracy problems. PLDI ’12, pages 453–462, New York, NY, USA, 2012. ACM. ISBN 978-1-4503-1205-9. URL http://doi.acm.org/10.1145/2254064.2254118.

Digital Library

[6]

S. Boldo. Kahan’s algorithm for a correct discriminant computation at last formally proven. IEEE Transactions on Computers, 58(2):220–225, Feb. 2009. URL http://hal.inria.fr/inria-00171497/.

Digital Library

[7]

S. Boldo, F. Clément, J.-C. Filliâtre, M. Mayero, G. Melquiond, and P. Weis. Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program. Journal of Automated Reasoning, 50(4): 423–456, Apr. 2013. URL http://hal.inria.fr/hal-00649240/ en/.

Digital Library

[8]

W.-F. Chiang, G. Gopalakrishnan, Z. Rakamari´c, and A. Solovyev. Efficient search for inputs causing high floating-point errors. pages 43–52. ACM, 2014.

Digital Library

[9]

V. Chvatal. A greedy heuristic for the set-covering problem. Mathematics of Operations Research, 4(3):pp. 233–235, 1979. URL http://www.jstor.org/stable/3689577.

Digital Library

[10]

E. Darulova and V. Kuncak. Sound compilation of reals. POPL ’14, pages 235–248, New York, NY, USA, 2014. ACM. ISBN 978- 1-4503-2544-8. URL http://doi.acm.org/10.1145/2535838.

Digital Library

[11]

2535874.

[12]

E. Darulova, V. Kuncak, R. Majumdar, and I. Saha. Synthesis of fixed-point programs. EMSOFT ’13, pages 22:1–22:10, Piscataway, NJ, USA, 2013. IEEE Press. ISBN 978-1-4799-1443-2. URL http: //dl.acm.org/citation.cfm?id=2555754.2555776.

Digital Library

[13]

M. Daumas and G. Melquiond. Certification of bounds on expressions involving rounded operators. ACM Trans. Math. Softw., 37(1):2:1–2:20, Jan. 2010. http://gappa.gforge.inria.fr/.

Digital Library

[14]

J. de Jong. math.js: An extensive math library for JavaScript and Node.js, 2013. URL http://mathjs.org/.

[15]

H. Eldib and C. Wang. An SMT based method for optimizing arithmetic computations in embedded software code. FMCAD ’13, 2013.

[16]

European Commission. The introduction of the euro and the rounding of currency amounts. Euro papers. European Commission, Directorate General II Economic and Financial Affairs, 1998.

[17]

L. Fousse, G. Hanrot, V. Lefèvre, P. Pélissier, and P. Zimmermann. MPFR: A multiple-precision binary floating-point library with correct rounding. ACM Transactions on Mathematical Software, 33(2):13:1– 13:15, June 2007. URL http://doi.acm.org/10.1145/1236463.

Digital Library

[18]

1236468.

[19]

D. Goldberg. What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv., 23(1):5–48, Mar. 1991. URL http://doi.acm.org/10.1145/103162.103163.

Digital Library

[20]

E. Goubault and S. Putot. Static analysis of finite precision computations. VMCAI’11, pages 232–247, Berlin, Heidelberg, 2011. Springer-Verlag. ISBN 978-3-642-18274-7. URL http://dl.acm. org/citation.cfm?id=1946284.1946301.

Digital Library

[21]

R. Hamming. Numerical Methods for Scientists and Engineers. Dover Publications, 2nd edition, 1987.

Digital Library

[22]

N. J. Higham. Accuracy and Stability of Numerical Algorithms. Society for Industrial and Applied Mathematics, Philadelphia, PA, USA, 2nd edition, 2002. ISBN 0898715210.

[23]

IEEE. IEEE standard for binary floating-point arithmetic. IEEE Std. 754-2008, 2008.

[24]

A. Ioualalen and M. Martel. Synthesizing accurate floating-point formulas. ASAP ’13, pages 113–116, June 2013.

Digital Library

[25]

W. Kahan. A Survey of Error Analysis. Defense Technical Information Center, 1971. URL http://books.google.com/books?id= dkW7tgAACAAJ.

[26]

W. Kahan. Miscalculating area and angles of a needle-like triangle. Technical report, University of California, Berkeley, Mar. 2000. URL http://www.cs.berkeley.edu/~wkahan/Triangle.pdf.

[27]

W. Kahan and J. D. Darcy. How Java’s floating-point hurts everyone everywhere. Technical report, University of California, Berkeley, June 1998. URL http://www.cs.berkeley.edu/~wkahan/JAVAhurt. pdf.

[28]

J. Kleinberg and E. Tard˝os. Algorithm Design. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2005.

Digital Library

[29]

ISBN 0321295358.

[30]

V. Lefévre and J.-M. Muller. The table maker’s dilemma: our search for worst cases. Technical report, Ecole Normale Supérieure de Lyon, Oct. 2003. URL http://perso.ens-lyon.fr/jean-michel. muller/Intro-to-TMD.htm.

[31]

M. Martel. Program transformation for numerical precision. PEPM ’09, pages 101–110, New York, NY, USA, 2009. ACM. ISBN 978-1-60558- 327-3. URL http://doi.acm.org/10.1145/1480945.1480960.

Digital Library

[32]

B. D. McCullough and H. D. Vinod. The numerical reliability of econometric software. Journal of Economic Literature, 37(2):633–665, 1999.

[33]

D. Monniaux. The pitfalls of verifying floating-point computations. ACM Trans. Program. Lang. Syst., 30(3):12:1–12:41, May 2008. URL http://doi.acm.org/10.1145/1353445.1353446.

Digital Library

[34]

C. G. Nelson. Techniques for Program Verification. PhD thesis, Stanford University, 1979.

Digital Library

[35]

P. Panchekha. Numerical imprecision in complex square root, 2014. URL https://github.com/josdejong/mathjs/pull/208.

[36]

P. Panchekha. Accuracy of sinh and complex cos/sin, 2014. URL https://github.com/josdejong/mathjs/pull/247.

[37]

K. Quinn. Ever had problems rounding off figures? This stock exchange has. The Wall Street Journal, page 37, November 8, 1983.

[38]

C. Rubio-González, C. Nguyen, H. D. Nguyen, J. Demmel, W. Kahan, K. Sen, D. H. Bailey, C. Iancu, and D. Hough. Precimonious: Tuning assistant for floating-point precision. SC ’13, 2013.

Digital Library

[39]

E. Schkufza, R. Sharma, and A. Aiken. Stochastic optimization of floating point programs using tunable precision. PLDI ’14, 2014.

Digital Library

[40]

A. Solovyev, C. Jacobsen, Z. Rakamaric, and G. Gopalakrishnan. Rigorous estimation of floating-point round-off errors with symbolic taylor expansions. FM’15. Springer, June 2015.

[41]

N. Toronto and J. McCarthy. Practically accurate floating-point math. Computing in Science Engineering, 16(4):80–95, July 2014.

Cited By

Saiki BBrough JRegehr JPonce JPradeep VAkhileshwaran ATatlock ZPanchekha PEeckhout LSmaragdakis GLiang KSampson AKim MRossbach C(2025)Target-Aware Implementation of Real ExpressionsProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3669940.3707277(1069-1083)Online publication date: 30-Mar-2025
https://dl.acm.org/doi/10.1145/3669940.3707277
Krahl MGüdemann MWallentowitz S(2025)SafeFloatZone: Identify Safe Domains for Elementary FunctionsEmbedded Computer Systems: Architectures, Modeling, and Simulation10.1007/978-3-031-78377-7_9(122-137)Online publication date: 28-Jan-2025
https://doi.org/10.1007/978-3-031-78377-7_9
Appel AKellison ATimany ATraytel DPientka BBlazy S(2024)VCFloat2: Floating-Point Error Analysis in CoqProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636953(14-29)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636953
Show More Cited By

Index Terms

Automatically improving accuracy for floating point expressions
1. Mathematics of computing
  1. Mathematical analysis
    1. Numerical analysis

Recommendations

Automatically improving accuracy for floating point expressions
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation

Scientific and engineering applications depend on floating point arithmetic to approximate real arithmetic. This approximation introduces rounding error, which can accumulate to produce unacceptable results. While the numerical methods literature ...
Accelerating Accuracy Improvement for Floating Point Programs via Memory Based Pruning
Internetware '20: Proceedings of the 12th Asia-Pacific Symposium on Internetware

Floating point programs are widely used in science and engineering. These programs approximate real arithmetic with floating point arithmetic, which introduces rounding errors and leads to inaccurate results. In life-critical software systems, ...
Decimal Floating-Point Multiplication

Decimal multiplication is important in many commercial applications including financial analysis, banking, tax calculation, currency conversion, insurance, and accounting. This paper presents the design of two decimal floating-point multipliers: one ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 50, Issue 6

PLDI '15

June 2015

630 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2813885

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2015
630 pages
ISBN:9781450334686
DOI:10.1145/2737924
General Chair:
David Grove
IBM Research, USA
,
Program Chair:
Steve Blackburn
Australian National University, Australia

Copyright © 2015 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 June 2015

Published in SIGPLAN Volume 50, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

169
Total Citations
View Citations
1,426
Total Downloads

Downloads (Last 12 months)203
Downloads (Last 6 weeks)26

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Saiki BBrough JRegehr JPonce JPradeep VAkhileshwaran ATatlock ZPanchekha PEeckhout LSmaragdakis GLiang KSampson AKim MRossbach C(2025)Target-Aware Implementation of Real ExpressionsProceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 110.1145/3669940.3707277(1069-1083)Online publication date: 30-Mar-2025
https://dl.acm.org/doi/10.1145/3669940.3707277
Krahl MGüdemann MWallentowitz S(2025)SafeFloatZone: Identify Safe Domains for Elementary FunctionsEmbedded Computer Systems: Architectures, Modeling, and Simulation10.1007/978-3-031-78377-7_9(122-137)Online publication date: 28-Jan-2025
https://doi.org/10.1007/978-3-031-78377-7_9
Appel AKellison ATimany ATraytel DPientka BBlazy S(2024)VCFloat2: Floating-Point Error Analysis in CoqProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636953(14-29)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636953
Cheng JCoward SChelini LBarbalho RDrane TTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)SEER: Super-Optimization Explorer for High-Level Synthesis using E-graph RewritingProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640392(1029-1044)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620665.3640392
Coward SDrane TConstantinides G(2024)ROVER: RTL Optimization via Verified E-Graph RewritingIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.341015443:12(4687-4700)Online publication date: Dec-2024
https://doi.org/10.1109/TCAD.2024.3410154
Helal STao ZRubio-González CGygi FThakur A(2024)Towards Verifying Exact Conditions for Implementations of Density Functional ApproximationsSC24-W: Workshops of the International Conference for High Performance Computing, Networking, Storage and Analysis10.1109/SCW63240.2024.00027(160-169)Online publication date: 17-Nov-2024
https://doi.org/10.1109/SCW63240.2024.00027
Xia ZChen YNie PWang Z(2024)Detecting Numerical Deviations in Deep Learning Models Introduced by the TVM Compiler2024 IEEE 35th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE62328.2024.00018(73-83)Online publication date: 28-Oct-2024
https://doi.org/10.1109/ISSRE62328.2024.00018
Coward SDrane TMorini EConstantinides G(2024)Combining Power and Arithmetic Optimization via Datapath Rewriting2024 IEEE 31st Symposium on Computer Arithmetic (ARITH)10.1109/ARITH61463.2024.00014(24-31)Online publication date: 10-Jun-2024
https://doi.org/10.1109/ARITH61463.2024.00014
Kneusel RKneusel R(2024)Pitfalls of Floating-Point Numbers (And How To Avoid Them)Numbers and Computers10.1007/978-3-031-67482-2_4(115-133)Online publication date: 4-Dec-2024
https://doi.org/10.1007/978-3-031-67482-2_4
Fernández Mir RJackson PBhat SGoens AGrosser T(2024)Transforming Optimization Problems into Disciplined Convex Programming FormIntelligent Computer Mathematics10.1007/978-3-031-66997-2_11(183-202)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-3-031-66997-2_11
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Issue’s Table of Contents