Probabilistic Checking of Proofs

Eli Ben-Sasson, Prahladh Harsha & Madhu Sudan

What

This research project explores formats for writing proofs that are very sensitive to errors. True theorems should have totally valid proofs, while false statements should have an abundance of innaccuracies.

Why

The notion of proving theorems and verifying them is at the heart of computer science. Verifying a proof of a theorem  ought to be easy, and this notion is best expressed by saying that a computer program can verify the proof. Finding a proof for a given theorem (i.e., proving a theorem) ought to be hard, or else one may well replace mathematicians with computer programs! Indeed, the assumption that proving theorems is harder than verifying them is  equivalent to the famed conjecture that P does not equal NP.

A natural question that emerges in the context of verifying proofs is whether there is an efficient way to do gain confidence about the correctness of a proof. Specifically, one would like a verifier to sample small pieces of the proof looking for any "obvious" inaccuracies, and if none is found to conclude that the proof may be right. Such a verifier would need to be probabilistic and may accept invalid proofs with some probability, but hopefully, this probability is small for every theorem and every proof. The centrality of the task of verifying proofs makes this a task of fundamental importance to computer science. For instance,  efficient transformations achieving this would allow us to print transcripts of computations that take much less time to audit for correctness than to generate.

Such transformations are now known and the focus is on the efficiency of the transformations with respect to some key parameters: (1) We would like the verifier to be as efficient as possible in its computation time, and the number of probes it makes into the probabiilistically checkable proof. (2) We would like the transformation of proofs to be as efficient as possible. In particular the probabilisitically checkable proofs should not be much longer than standard  (error-hiding) proofs.

How

By now a vast variety of techniques are known to convert proofs into probabilistically checkable ones. They rely on analysis of functions over finite domains, on a spectrum of techniques in probabilistic algorithms, and on the theory of correcting errors in data.

Progress

Early results in this field [1,2] have shown how to verify proofs probing just a constant number of bits in the proof while rejecting every  false assertion with probablity at least, say, 50%.  Furthermore the probabilistically checkable proofs are only a polynomial factor larger than classical proofs. Our current research [3,4,5] has been focussiing on the question of making the proofs even shorter and simpler. In [3,4,5] we show how to make the length of the proofs only slightly longer (by poly-logarithmic factors) than the length of the classical proofs. Furthermore the new verifier runs in time polylogarithmic in the length of the proof.

Future

The main challenge in this area is to either get linear sized proofs that are probabilistically checkable or to prove that such proofs can't exist. 

Research Support

This research was supported in part by NSF grant CCR-0312575.

References

[1] S. Arora and S. Safra. Probabilistic checking of Proofs. JACM 45(1): 70--122 (1998).

[2] S. Arora, C. Lund, R. Motwani, M. Sudan, and M. Szegedy. Proof verification and the hardness of approximation problems. J. ACM  45(3): 501-555, May 1998.

[3] E. Ben-Sasson, O.Goldreich, P. Harsha, M. Sudan, and S. Vadhan. Robust PCPs of proximity, shorter PCPs, and applications to coding. Proceedings of the Thirty Sixth Annual ACM Symposium on Theory of Computing , pages 1-10, Chicago, Illinois, June 13-15, 2004.

[4] E. Ben-Sasson and M. Sudan.   Simple PCPs with poly-logarithmic rate and query complexity. Proceedings of the Thirty Seventh Annual ACM Symposium on Theory of Computing, (to appear), Baltimore, Maryland, May 22-24, 2005.

[5] E. Ben-Sasson, O.Goldreich, P. Harsha, M. Sudan, and S. Vadhan. Short PCPs verifiable in poly-logarithmic time.  Proceedings of the Twelfth Annual IEEE Conference on Computational Complexity , (to appear), San Jose, California, June 12-15, 2005.