Trustworthy Computations (Thesis)

Abstract:

The reliability of computations has always been an issue, even before
these days when computers and computing machinery run our lives.
The task of ensuring that computations are trustworthy needs to be
approached from many angles. The theoretical approach provides
evaluation of the reliability of a given computation. Once finding
flaws, this approach may provide schemes and (hopefully) proofs of
their effectiveness. However, correctness, reliability and
trustworthiness need to be the property of computations performed in
reality, and not be provided just in theory.
In this work, we address several aspects of this problem.
In the first part, we address theoretical aspects of reliability. We
study one of the central problems in the areas of algebraic
computations, coding theory, program checking and others. This is the
problem of obtaining explicit (or implicit, but correct)
representation for a function given by an unreliable black box oracle.
Solutions to such problems may be thought of as ``smart''
interpolation algorithms.
In the second part, we study the checking of approximate numerical
computations over subsets of the reals. We indicate why approximate
checking is much more challenging than exact checking of similar
computational tasks, and present a variety of checkers for linear
algebra computations. We do not leave checking in the realm of
theory. We provide an implementation, a package of checkers for
linear algebra computations manipulating matrices.
Last, we consider the issue of trust in the people executing
computations, by addressing the correctness of benchmark computation
results and their time reports.We consider the task of designing
benchmarks that are uncheatable in the following sense. First, the
customer has a way to check the accuracy of the output of the
computations of a benchmark run by the vendor; second, when asked to
run the benchmark the vendor has to perform some {em specific/}
computation, in order to get the correct results. We suggest a
benchmark and give the theoretical justification for its being
uncheatable, in addition to providing an implementation demonstrating
its usefulness and reliability.