Skip to content

The Evolution of Proofs

September 18, 2012
by

Let me start by saying that I have never read any blog posts, let alone written one, until today.  You are probably asking yourself, why am I blogging then? Well, the truth is that the only reason is that I couldn’t resist Omer’s charm when he asked me to join the blog.

I decided to write about one of my favorite topics in theoretical computer science: The evolution of proofs. It is really remarkable how our understanding of the concept of proofs has changed over the last 30 years. In this post I will give a (too) brief overview of some of this progress, and end with the problem that I have been obsessed with for a few years now:  The problem of delegating (or outsourcing) computation.

Let me warn you that this is not meant to be a survey,  and my apologies in advance for all the missing references.

Before the seminal work of Goldwasser, Micali and Rackoff [GMR85], we thought of proofs as being mathematical proofs (as initially defined by Euclid in 300 BCE), where a set of axioms and deductive logic is used to prove mathematical statements.  In 1985,  the breakthrough work of [GMR85] proposed to diverge from this classical view of proofs, and introduced the notion of interactive proofs, where the verifier verifies the correctness of a statement, by interacting with the prover and by using randomness.   As was shown later by Lund, Fortnow, Karloff, Nisan, and Shamir [LFKN90, S90], interactive proofs seem to be much more powerful than standard proofs, as every language in PSPACE can be verified efficiently via an interactive proof, whereas only languages in NP can be verified efficiently via a standard proof.  More specifically, [LFKN90, S90] showed that any language that can be computed in space s has an interactive proof where the verifier runs in time poly(s,n), where n is the instance size.  Unfortunately, the running time of the prover in such proofs is exponential in s.   (In these original works the running time was 2^{O(s^2)}, and this was later improved to be 2^{O(s)} by [GKR08]).

As a side remark, here is a problem that I am obsessed with, and I would love for someone to solve it (ideally, me):  Does the prover really need to run in time exponential in s? In other words, for languages that are computable in time t and space s, does there exist an interactive proof for proving membership in L, where the prover runs in time poly(t(n)) and the verifier runs in time poly(s(n),n), where n is the instance size?  Stated more philosophically:  Is proving really harder than computing?

A few years after interactive proofs were introduced, Ben-Or, Goldwasser, Kilian, and Wigderson [BGKW88] introduced the notion of multi-prover interactive proofs (MIPs).  In this model, there are several provers that are proving a statement to a single polynomial time verifier, and the assumption is that these provers do not communicate with each other during the proof.  [BGKW88] showed that whatever can be proved with k provers can also be proved with only two provers.  Shortly after, Babai, Fortnow and Lund [BFL90] showed that this proof model is extremely powerful, by proving that any language in NEXP has a 2-prover interactive proof.  Moreover, there is no blowup in the runtime of the provers.  Namely, if the language is computable in time t(n) then the provers in the MIP proof run in time poly(t(n)), and the verifier runs in time that depends only on the input size (independent of t). Soon after the model of MIP was introduced, Fortnow, Rompel and Sipser [FRS94] noticed that MIPs can be converted into probabilistically checkable proofs (PCPs).  (We note that the work of [FRS94] was done before the notion of PCPs was formally defined.  However, they notice that the provers can be replaced with an oracle, and that given this oracle, a probabilistic verifier can efficiently decide the language.)

PCPs are proofs which can be verified by a probabilistic verifier by reading only a few bits of the proof. In my opinion, PCPs are one of the most amazing successes of theoretical computer science. There has been a long series of remarkable works trying to improve the parameters of the PCP (the query complexity, the randomness complexity, and the size of the PCP). For those interested to learn more about PCPs, there is a fantastic survey by Madhu Sudan.

All this progress is really amazing!  Moreover, these results seem to be extremely useful in today’s world of cloud computing.  Suppose I wish to compute a (polynomial time computable) function f on some input x, but I don’t have the computational resources to do the computation.  The idea would be to send f and x to the cloud, and the cloud should send back f(x) together with a proof of correctness.  Of course, we require that verifying the proof should be significantly easier than computing f.  Moreover, we require that proving should not be too much harder than computing, since the cloud is powerful, but not all powerful.  Namely, if f is computable in time t, then we require that the proof can be computed in time poly(t).  This problem is known as the problem of delegating (or outsourcing) computation. The question is:   Can we use a scale down version of the above results (IP=PSPACE, MIP=NEXP, or PCP=NEXP) to solve the problem of delegation?

Well… using interactive proofs results with a prover who runs in time that is exponential in the space, and hence can only be applied to LOG SPACE languages.  (Actually, this can be boosted to any LOGSPACE uniform circuit of low depth [GKR08]).  In addition, the resulting proof has many rounds of interaction (proportional to the space of the computation, or to the depth of the function), and hence is not very practical. Using PCPs requires the verifier to store the entire PCP, and in many settings the verifier is space bounded and cannot store such a long string. Using MIPs requires the existence of two clouds that do not interact with each other, and we prefer not to make such an assumption, since our starting point is that we do not trust the cloud, and hence do not trust that the clouds will not interact.

So, a priori it is not clear how to use these results to solve the (practical) problem computation delegation.   However, here cryptography comes to the rescue!  It turns out that if we rely on cryptographic assumptions then we can use the results above to obtain delegation schemes for any (polynomial time computable) function f, where the runtime of the verifier depends only on the input length, independent of the running time of f, and the runtime of the prover is polynomially related to the running time of f. However, the resulting protocols are not (interactive) proofs, as they do not satisfy the usual soundness condition, but rather satisfy a weakened version:  The requirement is that only computationally bounded cheating provers cannot convince the verifier of the validity of incorrect statements (whereas an all powerful adversary may be able to cheat).  A protocol that satisfies such a computational soundness condition is called an interactive argument (as opposed to an interactive proof), a notion that was introduced by Brassard, Chaum and Crepeau [BCC88]. The motivation behind such a definition is the belief that in real life adversaries are not all powerful.

In my next blog post, I will tell you about some exciting works, which use the results above (IP=PSACE, MIP=NEXP) to construct delegating schemes — stay tuned!

References:

[BCC88] Gilles Brassard, David Chaum, Claude Crépeau: Minimum Disclosure Proofs of Knowledge. J. Comput. Syst. Sci. 37(2): 156-189 (1988).

[BFL90] László Babai, Lance Fortnow, Carsten Lund: Non-Deterministic Exponential Time Has Two-Prover Interactive Protocols FOCS 1990: 16-25.

[BGKW88] Michael Ben-Or, Shafi Goldwasser, Joe Kilian, Avi Wigderson: Multi-Prover Interactive Proofs: How to Remove Intractability Assumptions STOC 1988: 113-131.

[FRS94] Lance Fortnow, John Rompel, Michael Sipser: On the Power of Multi-Prover Interactive Protocols. Theor. Comput. Sci. 134(2): 545-557 (1994).

[GKR08] Shafi Goldwasser, Yael Tauman Kalai, Guy N. Rothblum: Delegating computation: interactive proofs for muggles. STOC 2008: 113-122.

[GMR85] Shafi Goldwasser, Silvio Micali, Charles Rackoff: The Knowledge Complexity of Interactive Proof-Systems (Extended Abstract) STOC 1985: 291-304.

[LFKN90] Carsten Lund, Lance Fortnow, Howard J. Karloff, Noam Nisan: Algebraic Methods for Interactive Proof Systems FOCS 1990: 2-10.

[S90] Adi Shamir: IP=PSPACE FOCS 1990: 11-15.

5 Comments leave one →
  1. September 18, 2012 4:24 pm

    Great post. Minor comment, the link people.csail.mit.edu/madhu/pcp/pcp.ps points to https://windowsontheory.org/2012/09/18/the-evolution-of-proofs/people.csail.mit.edu/madhu/pcp/pcp.ps

    • yaelism permalink
      September 19, 2012 1:02 pm

      Thanks so much, corrected.

  2. September 19, 2012 1:24 am

    Welcome on board Yael! Looking forward to your next post 🙂

    • yaelism permalink
      September 19, 2012 1:02 pm

      Thanks Omer — don’t hold your breath 🙂

  3. September 21, 2012 7:26 pm

    Great post, Yael and an exciting story indeed. I remember the interactive proofs story from its early days, but was not aware of the new applications to delegation. So I plan to stay tuned and hold my breath for your next post.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: