Richard J. Lipton - Program Checking

Program Checking

Lipton showed that randomized testing can be provably useful, given the problem satisfied certain properties. Proving correctness of a program is one of the most important problems presented in computer science. Typically in randomized testing, in order to attain a 1/1000 chance of an error, 1000 tests must be run. However Lipton shows that if a problem has "easy" sub-parts, repeated black-box testing can attain cr error rate, with c a constant less than 1 and r being the number of tests. Therefore, the probability of error goes to zero exponentially fast as r grows.

This technique is useful to check the correctness of many types of problems.

• Signal processing: fast Fourier transform (FFT) and other highly parallelizable functions are difficult to manually check results when written in code such as FORTRAN, so a way to quickly check correctness is greatly desired.
• Functions over finite fields and the permanent: Suppose that is a polynomial over a finite field of size q with q > deg(ƒ) + 1. Then ƒ is randomly testable of order deg(ƒ) + 1 over the function basis that includes just addition. Perhaps the most important application from this is the ability to efficiently check the correctness of the permanent. Cosmetically similar to the determinant, the permanent is very difficult to check correctness, but even this type of problem satisfies the constraints. This result even led to the breakthroughs of interactive proof systems Karloff-Nisan and Shamir, including the result IP = PSPACE.