11
$\begingroup$

I, like many people, am a keen user of mathematical software such as Mathematica and Maple. However, I have become increasingly frustrated by the many cases where such software simply gives you the wrong answer without warning. This can occur when performing all sorts of operations from simple sums to optimization amongst many other examples.

I have been wondering what could be done about this serious problem. What is needed is some way to allow the user to verify the correctness of an answer that is given so that they have some confidence in what they are being told. If you were to get a solution from a math colleague she/he might just sit down and show you their working. However this is not feasible for a computer to do in most cases. Could the computer instead give you a simple and easily checkable witness of the correctness of their answer? Checking may have to be done by computer but hopefully checking the checking algorithm will be much easier than checking the algorithm to produce the witness in the first place. When would this be feasible and how exactly could this be formalized

So in summary, my question is the following.

Could it be possible at least in theory for mathematical software to provide a short checkable proof along with the answer you have asked for?

A trivial case where we can do this immediately is for factorization of integers of course or many of the classic NP-complete problems (e.g. Hamiltonian circuit etc.).

Improve this question
$\endgroup$
6
  • $\begingroup$ Can you give an example where the produced answer is wrong? It is of course possible to generate a verifiable proof of the correctness of computations, but such a proof need not be easy to check by hand, simply because the software typically uses highly non-trivial algorithms that are more efficient than the most intuitive ones. $\endgroup$
    – Mahdi Cheraghchi
    Apr 9, 2013 at 19:14
  • $\begingroup$ I gave two examples in the question but the link colors might not be easy to see. Click on "sums" or "optimization". $\endgroup$
    – user15587
    Apr 9, 2013 at 19:15
  • 1
    $\begingroup$ Sort of what Manuel Blum and Sampath Kannan did in dl.acm.org/citation.cfm?id=200880? $\endgroup$
    – Andrej Bauer
    Apr 9, 2013 at 21:02
  • $\begingroup$ You might want to take a look at Certifying Algorithms. $\endgroup$
    – Pratik Deoghare
    Apr 10, 2013 at 1:00
  • $\begingroup$ yes too many symbolic software systems are treated as "black boxes" and this is also a corporate strategy to protect trade secrets. (1) try open source alternatives (2) consider the software engineering "best practice" of "unit testing". briefly the idea would be to create "sanity checks" of the results, eg by substituting known values, other manipulations, inverses, etc. for well constructed tests it is unlikely that both the formula and the test would fail in a way that would give a "false positive". $\endgroup$
    – vzn
    Apr 10, 2013 at 2:09

1 Answer 1

Reset to default
5
$\begingroup$

  1. The concept of "witnesses" or "checkable proofs" is not totally new: as mentioned in the comments, look for the concept of "certificate". Three examples came to mind, there are more (in the comments and elsewhere):

    • Kurt Mehlhorn described in 1999 a similar problem in computational geometry algorithms (e.g. minor errors in coordinates can yield big errors in the results of some algorithm), solved in a similar way in the library Leda, by insisting that each algorithm produces a "certificate" of its answer in addition of the answer itself.

    • Demaine, Lopez-Ortiz and Munro in 2000 used the concepts of certificates (they call them "proofs") to show adaptive lower bounds on the computation of the union and intersection (and difference, but this one is trivial) of sorted sets. Don't exclude their work because they did not use certiticates to protect against computing errors: they showed that even though the certificate can be linear in the size of the instance in the worst case, it is often shorter, and hence can be "checked" in sublinear time (given random access to the input as a sorted array or a B-Tree), and in particular in time less than required to compute such a certificate.

    • I have been using the concept of certificates on various other problems since seeing Ian Munro presenting their implementation at Alenex 2001, and in particular for permutations (apologies for the shameless plug, another one is coming), where the certificate is shorter in the best case than in the worst or average case, which yields a compressed data structure for permutations. Here again, checking the certificate (i.e. the order) takes at most linear time, less than computing it (i.e. sorting).

  2. The concept is not always usefull for error checking: there are problems where checking the certificate takes as much time as producing it (or simply producing the result). Two examples come to mind, one trivial and one complicated, Blum and Kannan (mentioned in the comments) give others.

    • The certificate for proving that an element is not in an unsorted array of $n$ elements is obtained in $n$ comparisons and checked in the same time.
    • The certificate for the convex hull in two and three dimensions, if the points are given in random order, takes as much bits to encode as comparisons to compute [FOCS 2009] (other shameless plug).

The library Leda is the most general effort (that I know of) toward making deterministic certificate-producing algorithms the norm in practice. Blum and Kannan's paper is the best effort I saw to make it the norm in theory, but they do show the limits of this approach.

Hope it helps...

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thank you that is very interesting. With respect to your point 2. I think I am talking about something a little different. The problem is not bugs in the code but rather algorithms that we know may give the wrong answer. Also, at a mundane level I don't even know what a useful certificate for many mathematical functions would look like. For example for an infinite sum or, say, the minimization of a function. $\endgroup$
    – user15587
    Apr 10, 2013 at 12:54
  • $\begingroup$ To be slightly clearer. It seems that is very hard to devise provably correct algorithms for many math problems. However we live with algorithms that may make mistake without warning us (and in fact are provably incorrect) for practical reasons. The hope that it is not (as) hard to devise provably correct correctness checkers for the same set of problems. $\endgroup$
    – user15587
    Apr 10, 2013 at 13:02
  • $\begingroup$ I am getting far from my expertise, but I thought the computation errors were generally caused by rounding errors with intermediate results (it was clearly the case in the examples motivating Leda) on basic operations (multiplications, divisions, etc..) rather than errors in the algorithms. I would have thought that algebraic systems such as maple and matlab avoided those :( $\endgroup$
    – J..y B..y
    Apr 11, 2013 at 9:18
  • $\begingroup$ It's an interesting question and maybe someone here knows for sure.. however many of the incorrect answers I am talking about are not for numerical calculations so this implies at least prima facie that the problems are more than you describe. I don't know the complexity of computing limits/infinite sums etc. but I assume that in general they are intractable in the worst case and so heuristics which sometimes give the wrong answer are needed/useful. mathematica.stackexchange.com/questions/tagged/bugs is not uninformative to get a feeling for the things that go wrong. $\endgroup$
    – user15587
    Apr 11, 2013 at 14:02
  • $\begingroup$ Theoretical CS has the concept of self-testing, which applies to many problems in linear algebra. One of the basic ideas is that for many problems, the solution can be checked (perhaps with a little extra information) more easily than it can be computed. See e.g. https://doi.org/10.1016/0022-0000(93)90044-W. $\endgroup$
    – Neal Young
    Jul 3, 2018 at 2:49

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.