Harley's example

Average Error: 4.2 → 0.5

Time: 58.6s

Precision: binary64

• could not determine a ground truth for program body

  1. c_p = 7.760534679590852e-135
  2. c_n = 1.591454800408899e-273
  3. t = -2.051473706622546e-53
  4. s = -2.0463886271292852e+48

\[\]

Math

\[\]

↓

\[\]

Error

Bits error versus c_p

Bits error versus c_n

Bits error versus t

Bits error versus s

Target

Original	4.2
Target	2.1
Herbie	0.5

\[\]

Derivation

1. Split input into 2 regimes

2. if s < -735106654.81811118

   1. Initial program 3.7

      \[\]
   2. Using strategy rm

   3. Applied add-exp-log 3.7

      \[\leadsto \]

   4. Applied pow-exp 3.7

      \[\leadsto \]

   5. Applied add-exp-log 3.7

      \[\leadsto \]

   6. Applied add-exp-log 3.7

      \[\leadsto \]

   7. Applied div-exp 3.7

      \[\leadsto \]

   8. Applied pow-exp 3.7

      \[\leadsto \]

   9. Applied prod-exp 3.7

      \[\leadsto \]

   10. Applied add-exp-log 3.7

       \[\leadsto \]

   11. Applied pow-exp 3.7

       \[\leadsto \]

   12. Applied add-exp-log 3.7

       \[\leadsto \]

   13. Applied add-exp-log 3.7

       \[\leadsto \]

   14. Applied div-exp 3.7

       \[\leadsto \]

   15. Applied pow-exp 3.7

       \[\leadsto \]

   16. Applied prod-exp 3.7

       \[\leadsto \]

   17. Applied div-exp 1.1

       \[\leadsto \]

   18. Simplified 1.1

       \[\leadsto \]

   19. Taylor expanded around 0 0.9

       \[\leadsto \]

   20. Simplified 0.9

       \[\leadsto \]

   if -735106654.81811118 < s

   1. Initial program 4.4

      \[\]
   2. Using strategy rm

   3. Applied add-exp-log 4.4

      \[\leadsto \]

   4. Applied pow-exp 4.4

      \[\leadsto \]

   5. Applied add-exp-log 4.4

      \[\leadsto \]

   6. Applied add-exp-log 4.4

      \[\leadsto \]

   7. Applied div-exp 4.4

      \[\leadsto \]

   8. Applied pow-exp 4.4

      \[\leadsto \]

   9. Applied prod-exp 4.4

      \[\leadsto \]

   10. Applied add-exp-log 4.4

       \[\leadsto \]

   11. Applied pow-exp 4.4

       \[\leadsto \]

   12. Applied add-exp-log 4.4

       \[\leadsto \]

   13. Applied add-exp-log 4.4

       \[\leadsto \]

   14. Applied div-exp 4.4

       \[\leadsto \]

   15. Applied pow-exp 4.4

       \[\leadsto \]

   16. Applied prod-exp 4.4

       \[\leadsto \]

   17. Applied div-exp 1.9

       \[\leadsto \]

   18. Simplified 1.9

       \[\leadsto \]

   19. Taylor expanded around 0 0.4

       \[\leadsto \]

   20. Simplified 0.4

       \[\leadsto \]
3. Recombined 2 regimes into one program.

4. Final simplification 0.5

   \[\leadsto \]

Reproduce

herbie shell --seed 2020191 
(FPCore (c_p c_n t s)
  :name "Harley's example"
  :precision binary64
  :pre (and (< 0.0 c_p) (< 0.0 c_n))

  :herbie-target
  (* (pow (/ (+ 1.0 (exp (neg t))) (+ 1.0 (exp (neg s)))) c_p) (pow (/ (+ 1.0 (exp t)) (+ 1.0 (exp s))) c_n))

  (/ (* (pow (/ 1.0 (+ 1.0 (exp (neg s)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (neg s))))) c_n)) (* (pow (/ 1.0 (+ 1.0 (exp (neg t)))) c_p) (pow (- 1.0 (/ 1.0 (+ 1.0 (exp (neg t))))) c_n))))