6
$\begingroup$

I use interval arithmetic for reliable computing. Now, a procedure coded in a good implementation of interval arithmetic takes perhaps about eight times as much as the same procedure carried out without interval arithmetic (if the lion's share of runtime is taken by floating-point computations). I have sometimes been asked why I don't do rounding-error analysis by hand instead. To me, that does not look like a good option: it amounts to saving computer time at the expense of human time, and creates one more occasion for human error.

Now, what would make sense for me would be for there to be a system for bounding rounding errors with the help of a computer. It might not be realistic to expect a computer to analyse the total error in fairly complex procedures, but a human and a computer might be able to do a quicker and more reliable job than a human working alone, and produce a certificate of correctness to boot. Cf. how it is much easier to produce a formal proof with computer assistance.

(In particular: I would be interested in how error analysis in the sense of e.g. Wilkinson could be used in the context of a rigorous proof. I could see how it might be possible to implement it by means of a system for the computer-aided production of formal proofs. Has such a thing been done in practice?)

Note: perhaps it shows, but -- I am a pure mathematician; feel free to tell me if what I say seems a little naïve.

Improve this question
$\endgroup$
10
  • 4
    $\begingroup$ Interval arithmetic is a method for bounding rounding errors with the help of a computer. Are you asking for something different? $\endgroup$
    – Federico Poloni
    Aug 26, 2018 at 17:02
  • 3
    $\begingroup$ There are plenty of automated systems that ensure that certain computations and their floating point errors are bounded and safe. Many of them these days use semidefinite optimization to write down an optimization problem for the worst case. Search the literature for some papers on this! $\endgroup$
    – Wolfgang Bangerth
    Aug 26, 2018 at 21:23
  • 1
    $\begingroup$ Federico Poloni: yes, but it is a posteriori method; each time a computation is carried out, the maximal error is, if you wish, computed afresh, with a substantial overhead. The alternative is to estimate what the maximal error in the output of an operation can be, given a relative error size in the input. Say we have a loop running 10^9 times. We should be able to bound the maximal error in the final output of the loop without having to compute intervals or error bounds 10^9 times. $\endgroup$
    – H A Helfgott
    Aug 27, 2018 at 3:40
  • $\begingroup$ Wolfgang Bangerth: any references to the literature would be very welcome; as I should have said, I work in number theory, and this area is relatively unfamiliar to me. Just to be clear - I know (or think I know) that what e.g. matrix multiplication does to errors is well-understood. Are there systems that - presumably with some human help - can bound the error the result from iterating a loop 10^9 times, say, without having to go through the loop 10^9 times and seeing how the error changes with every operation? $\endgroup$
    – H A Helfgott
    Aug 27, 2018 at 4:16
  • 1
    $\begingroup$ I suggest that you use a @ before name when replying, that way the person will receive a notification. $\endgroup$
    – nicoguaro ♦
    Aug 27, 2018 at 13:20

1 Answer 1

Reset to default
2
$\begingroup$

I find an 8 times overhead a bit surprising, the most intense operation i have in mind is 4 times overhead, namely multiplication. The rest could be due to an inefficient library though.

I am using JuliaIntervals and never has such a slow down.

About your question, Interval Arithmetics computes the error along the path of computation you took you can then reject the solution or continue working with it. The resulting interval is basically is a proof for a certain set of inputs.

Formally verifying that an Interval for a certain input has an acceptable range is as expensive as performing the interval arithmetic. Formally verifying that for all input of a certain set the range is acceptable is an hard problem. As you either have to try all combinations (finitely many for floating point) or use a more clever proof system. Sadly verifying properties of multipliers on their own is still an active research area not to speak of generic non-linear functions.

Summary:

  • Look for a better library
  • If you know an upper estimate for the error given input intervals, you can always get upper and lower bounds from the inputs, do your short cut calculations and make a new interval.
  • Interval arithmetic is like derivatives, simple rules that can be applied quickly by a computer. Formal verification requires search and i wouldn't be surprised if such a problem falls into some NP complexity class for certain functions.
Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.