The Input Format

Herbie uses the FPCore format to specify an input program, and has extensive options for precisely describing its context.

Math format

The Herbie web shell takes input in a subset of the math.js syntax. The web shell automatically checks for syntax errors, and provides a graphical user interface for specifying the input domain. The web shell converts the mathematical expression and input ranges into FPCore before sending it to Herbie.

FPCore format

Herbie's command-line and batch-mode tools use FPCore format to describe mathematical expressions. FPCore looks like this:

(FPCore (inputs ...) properties ... expression)

(FPCore name (inputs ...) properties ... expression)

Each input is a variable name, like x, used in the expression. Properties are used to specify additional information about the expression's context. If name is specified, the function can be referenced in subsequent FPCore declarations in the file.

The expression is written in prefix form, with every function call parenthesized, as in Lisp. For example, the formula for the hypotenuse of a triangle with legs a and b is:

(FPCore (a b) (sqrt (+ (* a a) (* b b))))

The semicolon (;) character introduces a line comment. We recommend the .fpcore file extension for Herbie input files.

Supported functions

Herbie supports all functions from math.h with floating-point-only inputs and outputs. The best supported functions include:

+, -, *, /, fabs: The usual arithmetic functions
sqrt, cbrt: Square and cube roots
pow, exp, log: Various exponentiations and logarithms
sin, cos, tan: The trigonometric functions
asin, acos, atan, atan2: The inverse trigonometric functions
sinh, cosh, tanh: The hyperbolic functions
asinh, acosh, atanh: The inverse hyperbolic functions
fma, expm1, log1p, hypot: Specialized numeric functions

Herbie also supports the constants PI and E. Use - for both subtraction and negation.

Herbie links against your computer's libm to evaluate these functions. So, each function has the same behavior in Herbie as in your code. You can instead use the racket precision if you instead want reproducible behavior.

Conditionals

FPCore uses if for conditional expressions:

(if cond if-true if-false)

The conditional cond may use:

==, !=, <, >, <=, >=: The usual comparison operators
and, or, not: The usual logical operators
TRUE, FALSE: The two boolean values

The comparison functions support chained comparisons with more than two arguments.

Intermediate variables

Intermediate variables can be defined using let and let*:

(let ([variable value] ...) body)

(let* ([variable value] ...) body)

In both let and let*, each variable is bound to its value and can be used in the body. The difference between let and let* is what order the values are evaluated in:

let expressions: In a let expression, all the values are evaluated in parallel, before they are bound to their variables. This means that later values can't refer to earlier variables in the same let block.
let* expressions: A let* block looks the same as a let block, except the values are evaluated one at a time, and later values can refer to earlier variables.

Unless you have a lot of Lisp experience, you'll probably find let* more intuitive.

Internally, Herbie treats intermediate values only as a notational convenience, and inlines their values before improving the formula's accuracy. Using intermediate variables will therefore not produce a more accurate result or help Herbie run faster.

Specifications

In some cases, your input program is an approximation of some more complex mathematical expression. The :spec (for “specification”) lets you specify the more complex ideal case. Herbie will then try to modify the input program to make it more accurately evaluate the specification.

For example, suppose you want to evaluate sin(1/x) via a series expansion. Write:

(FPCore (x)
  :spec (sin (/ 1 x))
  (+ (/ 1 x) (/ 1 (* 6 (pow x 3)))))

Herbie will only use the :spec expression to evaluate error, not to search for accurate expressions.

Preconditions

By default, the arguments to formulas are assumed to be arbitrarily large or small floating-point numbers. However, in most programs a smaller range of argument values is possible. The :pre property (for “precondition”) describes this smaller range.

Preconditions use comparison and boolean operators, just like conditional statements:

(FPCore (x) :pre (< 1 x 10) (/ 1 (- x 1)))

Herbie is particularly efficient when when the precondition is an and of ranges for each variable, but more complex preconditions also work.

Precisions

Herbie supports both single- and double-precision values; you can specify the precision with the :precision property:

binary32: Single-precision IEEE-754 floating point
binary64: Double-precision IEEE-754 floating point
racket: Like binary64, but using Racket math functions rather than your computer's libm.

By default, binary64 is assumed. Herbie also has a plugin system to load additional precisions.

Herbie won't produce mixed-precision code unless you allow it to do so, using the :herbie-conversions property:

:herbie-conversions ([prec1 prec2] ...): Expressions in precision prec1, can be rewriten to use precision prec2, and vice versa.

All conversions are assumed to be bidirectional. For example, if you specify :herbie-conversions ([binary64 binary32]), Herbie will be able to add conversions between single- and double-precision floating-point.

Miscellaneous Input Properties

Herbie uses the :name property to name FPCores in its UI. Its value ought to be a string.

Herbie allows :alt properties to specify additional "developer targets"; these might be other alternatives you've tried that you want to compare against.

Additional Output Metadata

Herbie's output provides additional information in custom properties:

:herbie-status status: status describes whether Herbie worked: it is one of success, timeout, error, or crash.
:herbie-time ms: The time, in milliseconds, used by Herbie to find a more accurate formula.
:herbie-error-input ([pts err] ...): The average error of the input program at pts points. Multiple entries correspond to Herbie's training and test sets.
:herbie-error-output ([pts err] ...): The computed average error of the output program, similar to :herbie-error-input.

Herbie's benchmark suite also uses properties for continuous integration, but these are not officially supported and their use is discouraged.