Programming News and Articles
8 subscribers
5 photos
3 files
241 links
Download Telegram
Forwarded from Блог*
#prog #math #article

Написано на удивление доходчиво.

High Performance Correctly Rounded Math Libraries for 32-bit Floating Point Representations

Everyone uses math libraries (i.e., libm), which provide approximations for elementary functions. Surprisingly (or not), mainstream math libraries (i.e., Intel’s and GCC’s libm) do not produce correct results for several thousands of inputs! Developers of modern software systems are seldom aware of them, which affects the reproducibility and portability of software systems. This blog post describes our new method for synthesizing elementary functions that produces correct results for all inputs but is also significantly faster than the state of the art libraries, which have been optimized for decades.

<...>

The overall goal of our RLIBM project is to make correctly rounded elementary functions mandatory rather than a recommendation by the standards (at least for 32 bits or lower). In our RLIBM project, we have been making a case for generating polynomials that approximate the correctly rounded result of f(x) rather than the real value of f(x) because our goal is to generate correct, yet efficient implementations. By approximating the correctly rounded result, we consider both approximation errors (i.e., polynomial approximation) and rounding errors (i.e., with polynomial evaluation with finite precision representations), which enables the generation of correct results. One can use existing high-precision libraries, which are slow, to generate oracle correctly rounded results. Now our goal is to generate efficient polynomials that produce these correctly rounded results for all inputs. Given a correctly rounded result, there is an interval of real values around the correct result that the polynomial can produce, which still rounds to the correct result. This interval is the amount of freedom available that our polynomial generator has for a given input. Using this interval, our idea is to structure the problem of polynomial generation that produces correct results for all inputs as a linear programming (LP) problem. To scale to representations with a large number of inputs, we propose counterexample guided polynomial generation, generate piecewise polynomials rather than a single polynomial, and develop techniques that support various complex range reductions.