Herbie Tutorial

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.

Giving Herbie expressions

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.

Programming with Herbie

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.)

Finding the problematic expression

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))
  );
}

Converting problematic code to Herbie input

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.

Using Herbie's results

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.

Next steps

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.