Herbie is a tool that automatically rewrites floating point expressions to make them more accurate. It's well-known that floating point arithmetic is inaccurate; hence the jokes that 0.1 + 0.2 ≠ 0.3 for a computer. But to understand the inaccuracies and reduce them is a much harder task. Usually, programs that use floating point arithmetic are just written with the hope that these inaccuracies will not cause bugs, and when they do, these bugs are mysterious and hard to fix.
To get started using Herbie, download and install it, including running the test suite (as described in the installation instructions) to ensure that you have Herbie working properly. Now that Herbie is installed, you're ready to begin using it.
Herbie is a stand-alone tool, which accepts floating point expressions as inputs
and produces floating point expressions as output.
These floating point expressions are written in Herbie's custom input language,
which is approximately a subset of Racket.
For an example, open up
You'll see three blocks of code, the first of which is
(herbie-test (x) "Cancel like terms" (- (+ 1 x) x))
Each of these blocks describes a single input to Herbie;
the block has a list of variables:
"Cancel like terms";
and the expression itself:
(- (+ 1 x) x).
Inputs can also have an optional "target"—an equivalent expression
for Herbie to compare its results to.
That's used for tests, but isn't that useful to you.
Take a look at the three test cases in the file. If you're not
familiar with Lisp syntax, it might take a bit to get used to the
way expressions are written. As you can see, Herbie has common
mathematical operators built in, from arithmetic to more
complicated functions like as
Now run the tutorial file through Herbie by running
racket src/herbie.rkt report bench/tutorial.fpcore graphs/
from the base Herbie directory.
graphs directory should appear
(if it already existed, its contents will be replaced),
which contains a detailed description of Herbie's results and how it got them.
graphs/report.html with your web browser to view these results.
There's a lot going on in this page, so let's break it down. On top, you see a quick summary of the results: the running time, the number of expressions improved, the total number of expressions run on, and the starting/ending bits of accuracy. You should see that Herbie considers itself to have improved 2/2 expressions, even though it ran on three. The reason is that Herbie doesn't consider itself to have “improved” an expression until it improves it accuracy by at least one bit. Since one of the expressions was pretty accurate to start (less than a bit of error), it isn't even a contender, and the improved version doesn't count as an improvement.
Next, there's a graph summarizing the test results. Each horizontal row is a single expression, and the line stretches from the original accuracy of that expression to the accuracy of Herbie's output. You should see one long arrow (for the expression (x + 1)2 - 1), one short arrow (for the expression (1 + x) - x) and one bare arrowhead (for the expression ((x + y) + z) - (x + (y + z))). This corresponds to the fact that the first expression is pretty inaccurate (for small x), the second is also inaccurate (for large x), and the last one is pretty accurate (though not exactly so).
Next to the graph is a grid of blocks, each one listing the bits improved for a test case. These are in the same order as the arrows; mouse over one to see the associated arrow light up. The colors describe how Herbie scores itself: white for already accurate, green for improved, orange for not improved, and red for made worse. You won't be seeing the last one (if you do, report it as a bug).
Below that, you have a lot of information about Herbie's internal configuration.
You can usually skip it, but many of these parameters are configurable from the command line.
The most useful one is the seed.
Herbie uses random sampling internally, so different runs can yield slightly different results.
and can be set with the
--seed flag to Herbie.
Finally, the page has a table of each expression, with the starting error, final error, runtime, and a link to details.
Click on the last row, for the expression (x + 1)2 - 1. This page explains what Herbie did to that expression, including how the error is distributed for that expression, the final expression Herbie came up with, and how it derived that expression.
At the top, like before, you see some run-specific data, which probably isn't that useful to you. (The debug output, and profiling data, could all help the developers track down any problems you have). On the right, there is a plot. This plot shows where the original expression, and Herbie's result, have error. The horizontal axis is the input; in this case, it is the value of x, and if your expression has multiple input variables, you'll see several plots, one for each input variable. Note that this axis is logarithmic; one is about halfway between zero and infinity. The vertical axis is the error, in number of bits; it ranges from 0 at the bottom to 64 at the top. In this example, you can see that the error of the original program (in red) is large near zero and small far from zero. On the other hand, Herbie's output (barely visible in blue) is approximately 0 for all inputs.
Finally, on the left, you have Herbie's derivation of its result.
Usually you skip to the bottom of this and look at the result:
(λ (x) (+ (* x x) (* x 2))), or x2 + 2 x.
But sometimes it is useful to look at the derivation.
In my case, the derivation uses simplification
to expand the expression into (2 + x) x,
then uses Taylor expansion to expand this into 1 x2 + 2 x,
and then simplifies again to get rid of the unnecessary multiplication by 1.
Again, you usually don't care about this derivation,
but when a result seems strange, it can be helpful to look at the derivation.
If you've made it this far, you've now run Herbie and know how to read its output. The next step is to use it on some more realistic programs. Pick a floating point expression you care about and try it out, or check out Part 2 of the tutorial, which walks through a more-realistic example.