Optimize floating-point expressions for accuracy

For this line of the tutorial:

https://github.com/uwplse/herbie/blob/master/www/doc/1.2/tutorial.html#L82

the image tutorial-report-image.png is not in the repo.

Also, the tutorial link from page http://herbie.uwplse.org/doc/latest/installing.html leads to the non-existent page http://herbie.uwplse.org/doc/latest/doc/1.0/tutorial.html

Debian sid, commit 1162a7e05c63bf4374171ababb3c0ad43d186570

racket ~/src/herbie/src/reports/run.rkt --fuel 4 /tmp/test.rkt

Starting Herbie on 1 problems...
Seed: #(3729278177 3588225692 2076616249 3282344076 1976024238 1618906825)
  1/1   [   CRASH   ]   2

1. mk-pcontext in /home/lebedevri/src/herbie/src/points.rkt:22:0
2. for-loop in /home/lebedevri/src/herbie/src/core/alt-table.rkt:75:2
3. split-atab in /home/lebedevri/src/herbie/src/core/alt-table.rkt:74:0
4. #f in /usr/share/racket/collects/racket/contract/private/arrow-val-first.rkt:357:18
5. split-table in /home/lebedevri/src/herbie/src/glue.rkt:171:0
6. get-final-combination in /home/lebedevri/src/herbie/src/mainloop.rkt:264:0
7. run-improve50 in /home/lebedevri/src/herbie/src/mainloop.rkt:237:0
8. .../more-scheme.rkt:261:28 in ???

/tmp/test.rkt:

(herbie-test (alt mu vx vy)
  "2"
  (sqrt (/ (+ (- (+ (* (pow alt 2) (pow vx 4)) (* (* (pow alt 2) (pow vx 2)) (pow vy 2))) (* (* (* 2 alt) mu) (pow vx 2))) (pow mu 2)) (pow mu 2)))
)

debug.txt

Results for naive hypot function are pretty strange.

https://herbie.uwplse.org/demo/beffe884b924ebd9b2264b60006ab037dded11c5.b9fb4a99a678c42719f1af4df2435bfd560a1c86/graph.html#reproduce

The same applies to hypot with 3 parameters: sqrt(xx+yy+z*z).

https://herbie.uwplse.org/demo/92fcb878d8333bea9340b8c6ad6e0dfc5d1ef52f.b9fb4a99a678c42719f1af4df2435bfd560a1c86/graph.html#reproduce

Herbie failed on the following input:

(-((az - dz) - (vz/vx) * (ax - dx)) - ((bz - az) - ((vz/vx) * (bx - ax)))*gz) / (((dz - cz) - (bz - az)) - (vz/vx) * ((dx - cx) - (bx - ax)))*gz + ((cz - az) - (vz/vx) * (cx - ax))

which resulted in the following command

$ herbie shell --seed 2042407083
(FPCore (az dz vz vx ax dx bz bx gz cz cx)
  :name "(-((az - dz) - (vz/vx) * (ax - dx)) - ((bz - az) - ((vz/vx) * (bx - ax)))*gz) / (((dz - cz) - (bz - az)) - (vz/vx) * ((dx - cx) - (bx - ax)))*gz + ((cz - az) - (vz/vx) * (cx - ax))"
  (+ (* (/ (- (- (- (- az dz) (* (/ vz vx) (- ax dx)))) (* (- (- bz az) (* (/ vz vx) (- bx ax))) gz)) (- (- (- dz cz) (- bz az)) (* (/ vz vx) (- (- dx cx) (- bx ax))))) gz) (- (- cz az) (* (/ vz vx) (- cx ax)))))

with the following backtrace:

flonum->ordinal: contract violation expected: Float given: +inf.f in: the 1st argument of (-> Float any) contract from: <pkgs>/math-lib/math/private/flonum/flonum-bits.rkt blaming: <pkgs>/herbie/interface.rkt (assuming the contract is correct) at: <pkgs>/math-lib/math/private/flonum/flonum-bits.rkt:9.9 | L | C
-- | -- | --

the best approximation is too far from the herbie solutions

the claim by herbie that Average Error: 9.9 → 0.5 Time:20.5s Precision:64 Internal precision: 1152

(x - sin(x))  x = 0.5
the best approximation is      0.020574461395796998
the two herbie solutions
      with numerics disabled:   0.020574466765873017
      with numerics enabled:    0.020574466765873014

herbie shell --seed '#(3879704165 3744610602 266041085 3070558684 3536960646 1218547627)' (FPCore (x) :name "x - sin(x)" (- x (sin x)))

Defines only surface syntax and error checking. A #lang herbie/input program does nothing but check that herbie tests are well formed and print out some messages. The following conditions are checked:

• Duplicate variables
• Unused variables
• Undefined variables

Additionally, the general structure of test cases is checked. A test case is an s-expression containing herbie-test, a string description, a variable list, and an equation. Malformed test cases produce syntax errors highlighting the cause.

This PR attempts to cleanup the rule instantiation mess created by multi-precision expressions. As a refresher, rules are expanded so that each implementation is desugared into a real op + precision name. Every N-ary op becomes an (N+1)-ary op. This would work if not for expansive rules of the form ?x => f(?x) where we cannot infer the precision type. The solution was duplicating every rule for all "necessary" representations. Definitely a bad idea.

This has been only partially fixed. Rule duplication has been removed so most of Herbie (except for a slight caveat) will only see the rules exactly as they are defined internally or in plugins. The slight caveat is in src/core/egg-herbie.rkt where all egraph-related code is now nicely contained. Only here, specifically when make-ffi-rules is run, are the rules desugared into patterns usable by egg and possibly duplicated in the case of a few expansive rules.

Overall, I think it's a win. I think it could be argued that I just moved the ugliness around. But it's now concentrated into a place that already has to deal with messy expression translation.

This is a different problem that #402. With a clean, manual install of Racket 8.2 and Herbie 1.5 on top of Ubuntu 20.04, herbie improve prints [CRASH], and herbie shell prints an error:

herbie>  (FPCore (x) (- (sqrt (+ x 1)) (sqrt x)))
hash-ref: no value found for key
  key: 'NAN.f64
  context...:
   /usr/local/share/racket/pkgs/herbie/programs.rkt:231:0: eval-application
   /usr/local/share/racket/pkgs/regraph/main.rkt:104:0: set-precompute!
   /usr/local/share/racket/pkgs/regraph/main.rkt:79:0
   /usr/local/share/racket/pkgs/herbie/core/simplify.rkt:92:0
   /usr/local/share/racket/pkgs/herbie/core/simplify.rkt:68:0
   /usr/local/share/racket/pkgs/herbie/mainloop.rkt:347:0: simplify!
   /usr/local/share/racket/pkgs/herbie/mainloop.rkt:472:0: run-iter!
   /usr/local/share/racket/pkgs/herbie/mainloop.rkt:503:0: run-improve
   /usr/local/share/racket/pkgs/herbie/sandbox.rkt:62:6
   /usr/local/share/racket/collects/racket/engine.rkt:42:24

I passed herbie test ((35000000.0 + ((0.401 * (1000.0 / x)) * (1000.0 / x))) * (x - (1000.0 * 4.27e-5))) - ((1.3806503e-23 * 1000.0) * 300.0) expression, the maximum error given is 6.6bits, the test interval is [0.01, 100000], the corresponding input x to find this point is 13809681318699300000, I speculate that x here should be decimal, convert it to hexadecimal The hexadecimal number is 0xbfa5d7fe166b74a0. When converting the hexadecimal number to the corresponding floating-point number, it is -0.042663517224107. Why is the corresponding negative number here? My test range is obviously a positive number. I would like to know how each point of herbie's 8000 sampling points is converted into a corresponding floating point number, or whether herbie can give the input corresponding to the maximum error in a given interval. Maybe I didn't understand what 13809681318699300000 is here, I hope to get your reply, thank you

For us newbies, there's a bit of a gap with the documentation in various places. I hope you'll find my points of confusion as springboards for ideas on how to make things a bit clearer. This will help new users give Herbie a try, vs. getting a bit lost.

On the home page https://github.com/uwplse/herbie it says:

Herbie has unit tests for basic functionality, though coverage is far from complete. You can run the test suite with:

raco test src/

It's a minor point, but you might want to let the user know they need to go to Github\herbie or whatever directory they've downloaded the package. All the other commands on this page up to this point can be executed from whatever directory you want.

When I actually run this command, I get the baffling:

C:\Users\ehaines\Documents\Github\herbie>raco test src/ raco test: "src/alternative.rkt" raco test: (submod "src/bigcomplex.rkt" test) raco test: (submod "src/biginterval.rkt" test) raco test: (submod "src/common.rkt" test) raco test: "src/config.rkt" standard-module-name-resolver: collection not found for module path: fpbench collection: "fpbench" in collection directories: C:\Users\ehaines\AppData\Roaming\Racket\7.3\collects C:\Program Files\Racket\collects ... [167 additional linked and package directories]

Does that "collection not found" mean something is broken? I honestly don't know. I definitely ran something, but don't know what I've done or how to check whether things ran properly.

The test you then later suggest:

herbie report bench/hamming/ graphs/

looks like it's running properly. I do see the warning at the start:

Warning: could not determine a ground truth for program body x = 5.02679018721975e+286 See https://herbie.uwplse.org/doc/1.3/faq.html#ground-truth for more.

which is a little worrisome. It happens on a number of tests. That URL says "If you see this warning, you should add a restrictive precondition" - so it seems like you would want to do so, too. Or, explain in the docs that this is normal.

I'm done with this page - the installation page is next. My goal's to make Herbie as easy to use and professional-looking as possible. If I didn't care, I wouldn't file this bug. :)

Hello,

I just tried to install herbie on Ubuntu 18.10 (somehow, the very first expression I tried is too complex for the web demo and times out). I installed racket 7.1 from the indicated ppa:

racket -v
Welcome to Racket v7.1.

When running the tests, all failed:

~/.racket/7.1/bin/herbie report bench/tutorial.fpcore graphs/
Starting Herbie on 3 problems (seed: 1537437092)...
  1/3   [   CRASH   ]   Expanding a square
  2/3   [   CRASH   ]   Commute and associate
  3/3   [   CRASH   ]   Cancel like terms

I also tried to install from sources, but with similar results:

git clone https://github.com/uwplse/herbie
cd herbie/
racket src/herbie.rkt report bench/tutorial.fpcore graphs/
Starting Herbie on 3 problems (seed: 1855190789)...
  1/3   [   CRASH   ]   Expanding a square
  2/3   [   CRASH   ]   Commute and associate
  3/3   [   CRASH   ]   Cancel like terms

See below the infos from the report.html:

herbie shell --seed 1855190789 
(FPCore (x)
  :name "Expanding a square"
  (- (* (+ x 1) (+ x 1)) 1))

herbie shell --seed 1855190789 
(FPCore (x y z)
  :name "Commute and associate"
  (- (+ (+ x y) z) (+ x (+ y z))))

herbie shell --seed 1855190789 
(FPCore (x)
  :name "Cancel like terms"
  (- (+ 1 x) x))

and the backtrace from the first one:

mpfr_set_nan: implementation not found; arguments: #<_mpfr> | L | C
-- | -- | --
new-mpfr | /usr/share/racket/pkgs/math-lib/math/private/bigfloat/mpfr.rkt | 335 | 0
bf | /usr/share/racket/pkgs/math-lib/math/private/bigfloat/mpfr.rkt | 601 | 2
(unnamed) | /usr/share/racket/collects/racket/contract/private/arrow-higher-order.rkt | 357 | 33
f140 | unknown
f140 | unknown
f140 | unknown
eval-prog | /home/myhome/softs/herbie/src/programs.rkt | 150 | 0
make-exacts* | /home/myhome/softs/herbie/src/points.rkt | 138 | 0
loop | /home/myhome/softs/herbie/src/points.rkt | 158 | 2
prepare-points | /home/myhome/softs/herbie/src/points.rkt | 214 | 0
setup-prog!32 | /home/myhome/softs/herbie/src/mainloop.rkt | 72 | 0
run-improve41 | /home/myhome/softs/herbie/src/mainloop.rkt | 234 | 0
.../more-scheme.rkt:261:28 | unknown
(unnamed) | /usr/share/racket/collects/racket/private/more-scheme.rkt | 261 | 28

Do not hesitate to ask for more tests...

This PR adds the first API endpoint (/api/sample) as well as documentation and a basic test for the endpoint. Affected files are summarized below, and a copy of the documentation is shown. @pavpanchekha should probably double-check my resolution of the conflict in sandbox.rkt, though I think it was trivial.

affected files

Testing: .github/workflows/api-endpoint.yml infra/testApi.mjs

Code: In src/web/demo.rkt, adds a URL matcher: [("api" (string-arg)) #:method (or "post" "get" "put") call-api-fn]

call-api-fn routes requests to an appropriate function. Currently, the only function is sample, which runs get-sample from src/sandbox.rkt.

Modifies www/doc.html and adds copies of api-endpoint.html to www/doc/1.6 and 1.7, since latest currently points to 1.6.

documentation

Documentation text is copied below:

Format for all endpoints

All the endpoints listed below respond to POST requests unless otherwise specified. A typical example of sending a POST request to a running Herbie server is:

/api/sample

Call sample on an input like:

Output from that example, in an unordered array of pairs of the point and exact output calculated:

/api/analyze

Forthcoming.

/api/alternatives

Forthcoming.

/api/local-error

Forthcoming.

This PR replaces the existing "arrow plot" with a more compact pair of plots: a standard x/y plot showing accuracy improvement and a narrower pareto plot showing cost vs accuracy. Here's an example on the tutorial (so, few points):

I know this is controversial: we know and love the arrow plot from when @wilcoxjay invented it for the PLDI'15 paper. But our reports are now much larger and it's totally infeasible to take in the arrow plot at once. Instead, I just find myself scrolling past it. This PR accomplishes two goals:

1. It shrinks the arrow plot down into something small, which can be taken in at once and doesn't need to be scrolled past;
2. Highlights the importance of program cost by making that easy to see at the top of the page.

The page covers:

• What is rounding
• What bits of error means
• What average error means
• Which inputs are valid
• How inputs are distributed / sampled

In the process, it has strengthened my convictions:

• Infinite points should be considered valid
• Average error should be replaced with percent accurate
• There should be a pop-up when you write an input range that spans 0, and there should be a button to add a minimum magnitude.

But anyway, the page describes things as they are; hopefully we can simplify it as we change stuff.

I was looking at the output of herbie for the example listed on the website, sqrt(x+1) - sqrt(x), and for the input range -1000 to +1000, the website test page output (x + (1 - x)) / (sqrt(x+1) + sqrt(x)

Herbie chose not to pursue the free optimization of (x + (1 - x) to 1 because the input range was too small, which does seem reasonable for a trial based algorithm. However herbie also lists alternatives, which sacrifice accuracy for speed. I do feel that herbie should have pursued optimizing the numerator to 1 in the alternatives.

Also, I think the cost numbers for expressions are a bit off. Looking at the code in cost.rkt, it says that mul and add are a cost of 1, div is a cost of 1, and transcendentals are a cost of 100. From my experience and consulting the intel intrinsics guide (check entries for mul_sd, sqrt_sd, and div_sd), I think that a more reasonable estimate would be to have div's cost increased from 1 to 8 and transcendentals like sqrt and sin decreased from 100 to 15.

These estimates aren't strictly tied x86 in particular: floating point division is in general significantly more expensive than multiplication. On many platforms, and fairly commonly on gpus, x / y is approximated as x * rcp(y) for speed

This PR redesigns the header for the Herbie website to look like this:

The hope is that a similar header, with different right-hand options, could work for the future Herbie browser UI (Odyssey).

This PR adds a simple rule. This branch has been kicking around for a long time, and I figure let's just test if this is useful and if it is let's merge it.