Why Herbie uses Rival, not Arb

Before I talk about the results, let me give you a quick overview of how Herbie works.

When a user types in an expression, Herbie begins by defining the permissible inputs for the expression based on the user's input ranges and the domains of the functions in the expression. For example, if there is a square root in the expression, its domain might be [0, +inf), and that intersects with the user's input range of, say, [-1, 1e20], to define the valid inputs to be [0, 1e20]. Herbie then samples about 8,000 permissible input points to evaluate the accuracy of the user's input. It does this by first computing the output at each input at a high precision (we call that the ground truth) and then looking at the difference between the ground truth and the results computed at lower precision.

Then the main part of Herbie kicks in, modifying the original expression using rewriting rules and measuring the accuracy of these changes to find a more accurate expression. This mutation process is repeated several times, resulting in a refined expression with reduced error across the 8,000 data points.

Here's the key point: the key steps establishing ground truth and assessing accuracy are performed using the Rival interval arithmetic library, often at precisions as high as 10,000 bits. These interval operations are time-intensive, accounting for about 40% of the overall runtime. Put simply, 40% of Herbie's runtime is spent in Rival.

Rival is a relatively thin wrapper around the MPFR arbitrary-precision library. But the MPFR documentation itself suggests that Arb is faster than MPFR, and Arb also supports an interval mode like Rival, so we figured Arb should be much faster than Rival. Switching to Arb could therefore make Herbie much faster, without making the results any less accurate.

Rival uses an interval representation: two arbitrary-precision endpoints. Arb uses a ball representation: an arbitrary-precision mid-point and a single-precision floating-point radius. The difference in representations is at the core of both why Arb is faster and also why switching to it didn't work.

Typically, 30 bits are enough to represent the radius of an interval, but not always in all contexts. For example, consider the interval [1e10, 2e20]. Rival can represent [1e10, 2e20] with no serious problems at any precision. But using arb_set_interval_mpfr in Arb, the final interval will look like [+/- 2.01e+20] meaning [-212381339136, 200000000222381339136] when converting back to endpoints.

This happens because the real radius of the interval [1e10, 2e20] is 9.9999999995e19. To represent that in single precision, it must be rounded up to 1.00000000217e20. The absolute difference between the true and rounded radius is 222,381,339,136—relatively small compared to the midpoint, but much bigger than our lower endpoint 1e10. So the left endpoint—the midpoint minus the radius—ends up negative. That leads to problems. If Herbie next does, for example, a comparison between [1e10, 2e20] and [0, 1], then in Rival the comparison is exact but in Arb the intervals overlap.

These very wide intervals are common during the stage where Herbie determines the valid input range, and with Arb Herbie’s logic would sometimes crash or define the whole input expression as “illegal”, with no permissible inputs. We therefore decided that we couldn't allow comparisons like this to happen.

By the way, it is no secret that ball arithmetic is less accurate. In many cases, that's okay: losing some accuracy in the ball arithmetic is fine. But for us, these very "unbalanced" intervals occur often and it is important not to lose much accuracy, so Rival’s interval representation fits Herbie better.

The second reason that Arb didn't work for Herbie was a difference in the representation of intervals that contain infinity. This problem arises from the original idea of representation. Again, Rival uses two endpoints and there’s nothing wrong with the interval [2, +inf). Arb, meanwhile, needs a midpoint and radius, which infinite intervals don’t have: to represent [2, +inf), the radius would have to be (inf-2)/2 and the midpoint to (inf+2)/2, which can't be represented precisely. Arb does specially support the interval [0, +inf), represented with a midpoint and radius of infinity, and symmetrically for (-inf, 0], but Herbie needs other infinite intervals as well.

For example, consider computing the exponential function of the interval [2, +inf) in 200 bits of precision. In Rival, this produces a result that is close to the real one: [e7.3890560989306502…, +inf). In Arb, the result is much wider: [-inf, +inf].[fn:: It's not clear why this doesn't at least return [0, +inf).]

It's worth noting another advantage for Rival: error intervals and movability flags. These extensions to interval arithmetic allow us to track domain errors, which Herbie’s core uses to speed up sampling. These extensions can be added to Arb but, unfortunately, they require more comparison operations which, as already discussed, are less accurate in Arb. In any case, the issues above suggested that ball representations wouldn’t work for Herbie.

The measured performance increase with Arb was indeed impressive for us. Nothing we saw invalidated the claim that Arb is faster. Nevertheless, for Herbie, Arb is not suitable because of the reasons above, and this is why we use Rival instead of Arb in Herbie.