Hey! Some people in my lab work on that! I also did some work on analyzing floating point exceptions, so I learned a bit about this stuff. AMA, and I’ll do my best to answer. :)

(For clarification, I work at the University of Utah, so Pavel is the head honcho over Herbie here.)

This is very cool, and I think would have been useful in a project I worked on a couple of years ago where scaling the units in a tool by 1000X surfaced a whole litany of FP accuracy problems. For that application, it would have been really useful to have even just the part of Herbie that reports the accuracy of an expression.

I was interested in how the percentage accuracy metric is computed, but the link from the tutorial was dead. I was wondering if it could be useful to supply a bit more information. The example I was thinking of is linked from the math.js complex sqrt example, where the fastest version is rated more accurate than the original, because it avoids some catastrophic cancellation, but does not even use all the inputs to the problem. (Maybe that's not as bad as it sounds? I didn't get deep into the FP semantics but on the surface it sounded like something you'd be unhappy about if you blindly copy-and-pasted it into your product or library.) It seemed like % accuracy was hiding an important property that you might want to know about, which once you got into the details, you'd have an "aha, but no thanks" moment about. I'm not sure what metrics would make that clearer at an earlier point, but it's sort of an interesting problem.

Another question -- I see that you can restrict the ranges of the inputs to get improved answers. Another very common fact you might know about an expression is that one input is expected to be much larger than the other. Could Herbie take that as another assumption, and could it help? Maybe as a suggestion as to what ratios between inputs are most important when evaluating accuracy, or as a runtime test to break it into cases? Which it looks like you are already doing for ranges of specific variables (I guess the search space increases pretty fast when you start considering relationships between the inputs.)

Very cool work -- both esoteric and practical all at once!

Can Herbie also look at expressions that are part of summing floating point numbers, or similar operations, to minimize the error of doing so?

I think Herbie only works on a closed-form expression. Besides from that though, if you are indeed summing numbers there should be some library to do that accurately, for example C++ Summation Toolkit [1] or the `accurate` crate in Rust [2].

[1] https://www.partow.net/programming/sumtk/index.html

[2] https://docs.rs/accurate/latest/accurate/

I tried 1/sqrt(9x-6) from .7 to 1e308, and got as one alternative

sqrt(-.16666…)

It did correctly mark this as 0% accurate, but I’m kinda curious as to where it came from.

It does have a 1.1x speedup apparently. None of the other (more accurate) options provide a speedup. Maybe there aren’t any value options that provide a speedup, but the tool allows increasingly reduced accuracy (down to zero) until it finds a speedup?

You can click "derivation" to see the exact process it was derived. It's the first term of a taylor series expansion around x = 0, which is indeed f(0) = 1/sqrt(9*0-6) = sqrt(-1/6). I'm not sure why x was chosen outside of its input domain though.

----

ADDED LATER: I think I have the answer. Herbie seems to always assume x = 0, but there are a fixed set of transformations to get around that fact. Currently it only tries f(x), 1/f(x) and 1/-f(x) [1].

[1] https://github.com/herbie-fp/herbie/blob/b4a4bb4c61749912a64...

> Maybe there aren’t any value options that provide a speedup, but the tool allows increasingly reduced accuracy (down to zero) until it finds a speedup?

AFAIK Herbie works by trying a bunch of transformations to get candidate expressions and evaluate them to get the pareto frontier. So if there is a single constant expression generated, it will always be available as the worst alternative.

Aside from the alternative, there's not much room to optimize that function. 1/sqrt(x) has pretty good approximations (e.g. fast inverse sqrt, reciprocal sqrt instructions) and 9x-6 is just FMA. A quick test with compiler explorer [1] shows 4 instructions, and you could probably do 3 with judicious instruction set choice and/or no regard for performance. Even a lookup table could be slower in practice, depending on what the rest of the program looks like.

[1] https://godbolt.org/z/86P86xTvx

Those are four long instructions, and there's a chance that you could do better within your desired accuracy bounds by using one of the inverse square root instructions and a round of Newton-Raphson iteration.

It does have an FMA command that it can suggest, but it paired it with pow.

double code(double x) { return pow(fma(x, 9.0, -6.0), -0.5); }

It labeled this as having a slowdown.

Very cool! I've run into some of these kinds of issues myself in my daily work and it took a long time to both discover the other and a solution. I'll definitely try this out to see if it can help me find and fix these kinds of issues faster.

Where do you work? Not many people run into fp accuracy issues.

Well, chances are if you think you don't, you already do.

There is a reason a big part of numerics (the mathematical disciplíne) is about dealing with it.

Most people don't realize they have them. For instance in most BI/ETL tools the expression below returns false:

    0.1 + 0.2 = 0.3

In Excel and Google Sheets, this returns false:

   2.03 - 0.03 - 2 = 0

In both of those cases the problem is not problem with floating point arithmetic but the parsing of floating point literals, or rather how systems take input and then substitute it with something different quietly behind the scenes. None of 0.1, 0.2, 0.3 are true (binary) fp values. Nobody would be surprised that

    0.1000000000000000056 + 0.2000000000000000111 != 0.2999999999999999889

You won't believe it, but Excel users are actually surprised. As do users of many other applications.

Somebody pointed me at "Towards an API for the Real Numbers" which explains why these calculations work how you expect in the Android default Calculator.

It's really nice, as they explain you can't drop this in instead of the floating point arithmetic in a serious language because the performance isn't what you want. However in human terms, for a product like the calculator - it's easily fine.

That's a very different kind of accuracy, though.

This tool is about improving the number of digits that are correct.

Trying to use exact equality is going to fail on most equations even if you have millions of correct digits.

This would be very cool for simulation programming space, where it can find derivations without too much performance hit with better accuracy.

Esp., where subnormal numbers come into play.

Are you guys able to offer any guidance on numerical stability of linear algebra problems? For example, the Woodbury matrix identity's stability seems uncertain based on https://mathoverflow.net/questions/80340/special-considerati...

I think it depends on the nature of the matrices; it doesn’t make sense to use if your A matrix is just some general dense matrix for example.

Why doesn't it make sense to use in that case?

The dimensions of (A-UBU’) are the same as the dimensions of A. After you apply Woodbury, you have

inv(A) - (other stuff)

So, it only makes sense if A is much easier to solve than (A-UBU’).

This is cool! I'm now wondering if it's possible to shell out to it from a Roslyn Analyzer (= C# compiler plugin). At the very least I'm sure I could automatically generate FPCore expressions from C# ASTs.

Long ago I integrated Herbie with the Clang Static Analyzer to process floating point expressions and warn about avoidable accuracy loss. The neat thing was that it could deal with loops, calculations split across multiple assignments, etc. But I never came up with a heuristic for knowing when the calculation was "complete" so it generated too many intermediate warnings.

Some kind of escape analysis would give you a notion of a complete calculation.

Excellent demo! It cool to see egraph transforms supported in producing alternative equations with different numerical stability properties. Nice end to end work!