Herbie automatically rewrites floating point expressions to make them more accurate. Floating point arithmetic is inaccurate; hence the jokes that 0.1 + 0.2 ≠ 0.3 for a computer. But it is hard to understand and fix these inaccuracies, creating mysterious and hard-to-fix bugs. Herbie is a tool to help.

To get started, download and install Herbie. With Herbie installed, you're ready to begin using it.

Now that Herbie is installed, start it with:

herbie web

After a brief wait, this ought to open a web browser to a page with Herbie's results. The most important part of the page is this bit:

Go ahead and type `(1 + x) - x` into this box and press
enter. You should see the entry box gray out, then some additional
text appear on the screen describing the various steps Herbie is
doing. Eventually (after a few seconds) you'll be redirected to a
page with Herbie's results. The most important part of that page is
the large gray box in the middle:

This shows both the input `(1 + x) - x`

that you gave
Herbie, and also Herbie's idea of a more accurate way to evaluate
that expression: `1`

. Here, Herbie did a good job,
which you can double check using the statistics above that box:

Here, Herbie reports that the improved the program has 0 bits of
error, on average, whereas the original program had 29.4. That's
because, when `x`

is really big, `x + 1 = x`

in floating-point arithmetic, so `(x + 1) - x = 0`

.

There's lots more information on this results web page to help explain both what the accuracy is on different inputs and to describe how Herbie derived its result.

Now that you've run Herbie and know how to read its results, let's work through applying Herbie to a realistic program.

When you're working on a numerical program, it's best to keep Herbie open in a browser tab so you can run it easily. That way, when you're writing a complex floating-point expression, you can run Herbie to make sure you use the most accurate version of that expression that you can. Herbie has options to log all the expressions you enter, so that you can refer to them later.

However, if you're tracking down a bug that you think is caused by floating-point error, you'll need to identify the problematic floating-point expression before you can use Herbie on it.

As an example, let's use math.js, an extensive math library for JavaScript, and walk through bug 208, which found an inaccuracy in the implementation of complex square root. (For a full write-up of the bug itself, check out a blog post by one of the Herbie authors.)

Before using Herbie you need to know what floating-point expressions to feed it. In most programs, there's a small core that does the mathematical computations, while the rest of the program sets up parameters, handles control flow, visualizes or print results, and so on. The mathematical core is what Herbie will be interested in.

For example, in the case of math.js, the mathematical core
is in `lib/function/`

.
Each file in each subdirectory contains a collection of mathematical functions.
The bug we're interested in is about complex square root, so let's look at the file
`arithmetic/sqrt.js`

,
which contains real and complex square roots.

The code handles argument checks, five different number types, and
error handling. None of that is of interest to Herbie; we want to
extract just the mathematical computation. So let's look at
the `isComplex(x)`

case:

var r = Math.sqrt(x.re * x.re + x.im * x.im); if (x.im >= 0) { return new Complex( 0.5 * Math.sqrt(2.0 * (r + x.re)), 0.5 * Math.sqrt(2.0 * (r - x.re)) ); } else { return new Complex( 0.5 * Math.sqrt(2.0 * (r + x.re)), -0.5 * Math.sqrt(2.0 * (r - x.re)) ); }

This code contains a branch: one option for non-negative `x.im`

,
and one for positive `x.im`

.
While Herbie supports an `if`

construct,
it's usually better to send each branch to Herbie separately.

Also, in this code, `x`

is of
type `Complex`

, a data structure with multiple fields.
Herbie only deals with floating-point numbers, not data
structures, so we will treat the input `x`

as two
separate inputs to Herbie: `xre`

and `xim`

.
We'll also pass each field of the output to Herbie separately.

Finally, each field of the final output uses the
variable `r`

, which is defined in the first line of the
code snippet. When you're using Herbie, you want to expand or
inline intermediate variables like this, because the definition of
that variable contains important information that Herbie can use
to improve accuracy.

Putting this all together, let's do the first field of the
non-negative `x.im`

case first. It looks like this:

0.5 * sqrt(2.0 * (sqrt(xre * xre + xim * xim) + xre))

Before running Herbie on this expression, click the “Additional
options” link. You should see a box where you can enter a
precondition; enter `xim <= 0`. This makes sure that
Herbie only considers the points this expression will actually be
run on when improving the accuracy of this expression.

Herbie will churn for a few seconds and produce an output, perhaps something like this:

Herbie's algorithm is randomized, so you likely won't see the
exact same thing. For example, the branch expression ```
xre ≤
6.68107529348e-308
```

will probably have some other really small
number. And perhaps Herbie will choose slightly different
expressions. But the result should be recognizably similar. In this
case, Herbie reports that the initial expression had 38.7 bits of
error, and that the output has 29.4.

It's a little harder to describe what Herbie found wrong with the original expression, and why its new version is better—it is due to a floating-point phenomenon called “cancellation”. But you can get some insight from the error plot just below the program block:

There's a lot going on here. Along the horizontal axis, you have
the various input values (of `xim`

). Note that the graph
is log-scale, and includes only negative values (thanks to our
precondition). So in the middle is the value -1, to the left you have
values with large exponents approaching infinity, and to the right
you have values with small exponents approaching 0.

On the vertical axis, you have Herbie's error measure (bits of
error), from 0 to 64. There are two lines drawn: a red one for your
input expression and a blue one for Herbie's output. Lower is
better. You can see from the plot that as `xim`

gets
larger (toward the right, closer to zero), Herbie's improvement
becomes more and more important. Below the plot, there is a list of
the argument names, with `xim`

highlighted. If you switch
it to `xre`

, you will see that the two expressions are
the same for positive `xre`

, and that Herbie's output is
better for negative `xre`

. You can also see that the
difference is quite large, with Herbie's output expression being
much more accurate than its input.

Note again that Herbie is randomized, and you may see somewhat different output than the screenshots and descriptions here. The overall gist should be similar, however.

Now that you have the more accurate version of this expression, all you need to do is insert it back into the program:

var r = Math.sqrt(x.re * x.re + x.im * x.im); // Herbie version of 0.5 * Math.sqrt(2.0 * (r + x.re)) var re; if (x.re <= 0) { re = Math.abs(x.im) * Math.sqrt(0.5) / Math.sqrt(r - x.re); } else { re = 0.5 * Math.sqrt(2.0 * (r + x.re)); } if (x.im >= 0) { return new Complex( re, 0.5 * Math.sqrt(2.0 * (r - x.re)) ); } else { return new Complex( 0.5 * Math.sqrt(2.0 * (r + x.re)), -0.5 * Math.sqrt(2.0 * (r - x.re)) ); }

Note that I've left the original code in place in a comment. That's because the original code is a bit more readable, and it also means that as Herbie gets better, we can re-run it to get future improvements in accuracy.

By the way, for some languages, like C, you can use the drop-down in the top-right corner of the gray program block to see Herbie's output in that language. You'll probably need to clean up the resulting program a bit, though.

With this change, we've made this part of the complex square root function much more accurate, and we could repeat the same steps for the other branches and other fields in this program. You now have a pretty good understanding of Herbie and how to use it. Please let us know if Herbie has helped you, and check out the documentation to learn more about Herbie's various options and outputs.