Proving Without Explaining, and Verifying Without Understanding
Last Friday, I was at a “Symposium on the Nature of Proof” at UPenn, to give a popular talk about theoretical computer scientists’ expansions of the notion of mathematical proof (to encompass things like probabilistic, interactive, zero-knowledge, and quantum proofs). This really is some of the easiest, best, and most fun material in all of CS theory to popularize. Here are iTunes videos of my talk and the three others in the symposium: I’m video #2, logician Solomon Feferman is #3, attorney David Rudovsky is #4, and mathematician Dennis DeTurck is #5. Also, here are my PowerPoint slides. Thanks very much to Scott Weinstein at Penn for organizing the symposium.
In other news, the Complexity Zoo went down yet again this week, in a disaster that left vulnerable communities without access to vital resources like nondeterminism and multi-prover interaction. Luckily, computational power has since been restored: with help from some volunteers, I managed to get the Zoo up and running again on my BlueHost account. But while the content is there, it looks horrendously ugly; all the formatting seems to be gone. And the day I agreed to let the Zoo be ported to MediaWiki was the day I lost the ability to fix such problems. What I really need, going forward, is for someone else simply to take charge of maintaining the Zoo: it’s become painfully apparent both that it needs to be done and that I lack the requisite IT skills. If you want to take a crack at it, here’s an XML dump of the Zoo from a few months ago (I don’t think it’s really changed since then). You don’t even need to ask my permission: just get something running, and if it looks good, I’ll anoint you the next Zookeeper and redirect complexityzoo.com to point to your URL.
Update (Nov. 18): The Zoo is back up with the old formatting and graphics!! Thanks so much to Charles Fu for setting up the new complexity-zoo.net (as well as Ethan, who set up a slower site that tided us over). I’ve redirected complexityzoo.com to point to complexity-zoo.net, though it might take some time for your browser cache to clear.
Follow
Comment #1 November 17th, 2012 at 6:24 pm
Scott, in regard to slide #9 of your talk (namely, the slide that provides a Merlin-Arthur definition the attributes “completeness” and “soundness” of mathematical claims), it is a striking aspect of complexity theory, that when we restrict the class of claims to “claims of membership in classes of the Complexity Zoo”, we obtain the following:
It seems plausible (to me) that many folks (well, me anyway) would be very interested in a slide discussing this remarkable aspect of Complexity-Zoo membership claims.
Comment #2 November 17th, 2012 at 6:59 pm
Proving, verifying, explaining and understanding were all once acts that only a conscious being could perform. We now have machine emulations or imitations of the first two, and no doubt the progress of cognitive science will eventually give us strictly mechanistic or functional analogues of the latter two as well.
But at some point we need to come to terms with the original concepts, and that means understanding them as acts of conscious cognition (or unconscious cognition with a conscious manifestation). There are at least two central problems of consciousness. One is to understand how mind relates to matter, the other is just to understand consciousness in itself. I recommend Husserl for the latter. (The former will in my opinion require quantum neurobiology plus a new ontology of quantum theory in which large tensor factors in entangled systems are special ontological wholes, but that’s just me.)
Comment #3 November 17th, 2012 at 7:42 pm
John Sidles #1: I’m afraid your “Proposition” doesn’t make sense, at least until you explain which set of “Complexity-Zoo membership-claims” you mean, and compared to what the set is incomplete. Do you mean the (finite) set of such claims that have been made? The set of all provable claims? (Provable in which formal system?) The set of all Platonically-true claims?
Comment #4 November 17th, 2012 at 7:48 pm
Are non-iTunes versions of the videos available for those of us that don’t live in Apple-land?
Comment #5 November 17th, 2012 at 8:13 pm
Matt #4: Sorry, it doesn’t look like it! Yeah, if it were up to me, I would’ve just uploaded the videos to YouTube. But you can get them for free from iTunes, can’t you?
Comment #6 November 17th, 2012 at 8:27 pm
Scott,
How about renaming Complexity Zoo to Complexity Museum? It seems only fossils remain there, given where the field is going — don’t you think?
Comment #7 November 17th, 2012 at 9:40 pm
bitter #6: No, really I don’t think so! Assuming that by “the field,” you mean computational complexity theory, we can get a rough sense by looking at the list of abstracts from this summer’s CCC conference. By my count, 13 of the abstracts directly involve complexity classes, compared to 21 that don’t. (And even if a paper was all about, say, circuit lower bounds, I didn’t count it as “directly involving complexity classes” if the connection wasn’t explicit!)
It’s true that complexity theory has branched off into lots of wonderful directions only indirectly related to complexity classes — coding theory, extractors, property testing, proof complexity, etc. — but that was already true when I created the Zoo back in 2002! The Zoo is a specific resource for a specific purpose, and nothing would make me happier than if other people were inspired by it to create a proof system zoo, a cryptographic primitive zoo, etc. (Indeed, I’ve been trying to interest students in the latter project for a while.) Even so, I’d say that even as the field evolves, complexity classes remain roughly as fundamental to complexity theory as the chemical elements do to chemistry.
Could you elaborate on where you think the field is going?
Comment #8 November 17th, 2012 at 9:53 pm
I’ve put up a complexity zoo mirror at:
http://complexityzoo.helpfulcloud.com
It may take a day or two for the DNS records to propagate everywhere. There also seems to be a number of broken links, perhaps from the import/export process somehow.
Comment #9 November 17th, 2012 at 9:59 pm
Ethan #8: Wow, thank you so much!!! I just redirected complexityzoo.com to point to your site. The site is slow, but I’ll leave it pointed there until something better comes along. Again, thank you.
Comment #10 November 17th, 2012 at 10:09 pm
Scott, here is the Merlin-Arthur game that your slide #9 (as I understand it) naturally suggests:
The interpolations “[]” point to:
Is this how it works?
Comment #11 November 17th, 2012 at 10:22 pm
http://complexity-zoo.net/
Took a bit more time to set up a special domain name. Should be all good to go. (as Ethan said, propogation takes a while.)
Comment #12 November 18th, 2012 at 12:02 am
Scott, great talk and exciting ending!
About the PCP theorem, are there caveats which in practice prevent checking formal proofs? Also, you indicate this theorem implies finding an approximate solution is hard for many NP problems. Why not all? Is it an actual possibility that two kinds of NP-complete problems exist, some hard to approximate and some not, or i’m just overinterpreting?
Comment #13 November 18th, 2012 at 1:12 am
Matt #4: If you’re on Linux (and presumably BSD, etc), you can install and use the “tunesviewer” program to download videos that are in iTunes U.
Comment #14 November 18th, 2012 at 5:20 am
Hmmm … on further reflection, it appears that the players in the Merlin-Arthur/Zoo Classification game can always specify inference rules that are sufficiently restrictive as to ensure the game’s soundness (in retrospect this is obvious) , and yet any such sound set of inference rules necessarily is incomplete in respect to the general Zoo Classification problem.
Does this incompleteness suggest, for example, that separating “P” from “NP” may be comparably hard to separating “true” from “false” in ZFC?
These questions seem to be generically tough … or is some key point eluding me?
Comment #15 November 18th, 2012 at 8:16 am
Scott #5: Not if you are running an OS that does not have iTunes, e.g. Linux. I suppose I could try to install it in Wine, but, with all due respect, that seems like a lot of effort for a popular talk. Generally, I think that academic institutions should make some effort not to lock their content into proprietary formats.
Comment #16 November 18th, 2012 at 9:30 am
Scott #5: If Matt Leifer is running Linux, as I am, the answer would be yes, in principle, just out of Turing-Completeness, but it is certainly not easy to do so.
Comment #17 November 18th, 2012 at 12:21 pm
Linux users: Sorry! To clarify, I had nothing whatsoever to do with these videos, except for giving one of the talks. 🙂 Complain to Penn if you want.
Comment #18 November 18th, 2012 at 12:38 pm
Jay #12:
About the PCP theorem, are there caveats which in practice prevent checking formal proofs?
Yes, there are several issues that severely limit the direct, practical applicability of the PCP theorem.
Most obviously, your proof needs to be in a machine-checkable format before the PCP theorem can be applied. The vast majority of proofs are not in such a format.
But even more importantly, once the proof is in machine-checkable format, you need to apply a further conversion to get it into probabilistically-checkable format. That conversion will require at least linear time (and will also blow up the proof size by substantial polylogarithmic and constant factors). So in practice, it’s much faster and easier just to feed the machine-checkable proof directly into a conventional proof-checking program.
Also, you indicate this theorem implies finding an approximate solution is hard for many NP problems. Why not all? Is it an actual possibility that two kinds of NP-complete problems exist, some hard to approximate and some not, or i’m just overinterpreting?
No, you’re not overinterpreting! What you write is not merely a “possibility” but the known reality (assuming P≠NP). To give two famous examples, it’s known to be NP-hard to solve 3SAT within a 7/8+ε factor of optimal, for any ε>0. By contrast, the Traveling Salesman Problem in the Euclidean plane is solvable to within a 1+ε factor of optimal, for any ε>0, in time polynomial in n and 1/ε. For more examples, see the excellent Compendium of NP Optimization Problems.
For the past two decades, there’s been an enormous field that studies the approximability or non-approximability of various NP-hard problems; I’d say it now accounts for something like a third of theoretical computer science. But to answer your question in a paragraph, the reason the PCP theorem doesn’t imply that all NP-complete problems are hard to approximate is that only some NP-hardness reductions, and not others, are “approximation-preserving.” In other words, many NP-hardness reductions will map an exact solution of problem A to an exact solution of problem B, but could map an approximate solution of problem A to a terrible solution of problem B, one that isn’t even close to optimal. So, all such reductions need to be redone in the PCP setting, and sometimes the PCP-ification succeeds and sometimes it doesn’t. And sometimes fast approximation algorithms are actually discovered (like for Euclidean TSP), and then we understand exactly why the NP-hardness reductions for those problems must have failed to preserve approximation: because otherwise, we would’ve solved an NP-hard approximation problem in polynomial time and thereby gotten P=NP!
Comment #19 November 18th, 2012 at 3:15 pm
Philip #13’s suggestion worked for me.
I found it very cool the idea of someone proving that P != NP but only sharing with the world a zero-knowledge proof. In a sense, it would be precisely the opposite situation of what happened in the Deolalikar affair, when everybody had access to the proof but couldn’t know whether it was correct (ok, most people found it very unlikely to be correct, but actually checking it is a bitch). But even if the prover were evil enough to want to do this, it would probably be too hard to formalize the proof to be worth it.
Comment #20 November 18th, 2012 at 3:49 pm
Thx 🙂
Comment #21 November 25th, 2012 at 12:45 pm
[…] Shtetl-Optimized,Proving Without Explaining, and Verifying Without Understanding, here. So wait a minute, Aaronson is the TIBCO Career Development Prof of EE and CS. When did that […]
Comment #22 November 25th, 2012 at 8:30 pm
Your example of the two Merlins proving they know how to 3-color a certain graph (slide 14) is confusing.
I understand the version in which a single prover convinces a verifier that a graph is 3-colorable, as you describe here:
http://www.scottaaronson.com/democritus/lec12.html
In the case in your slides, you seem to assume that the two Merlins have synchronized their colorations, so that one is not a color permutation of the other. But then if the protocol is repeated for greater confidence, the two Merlins are permitted to communicate before each trial so that they both employ the same permutation of colors?
It seems you gave this example rather than the single prover in order to highlight the possibility of entanglement in the multi-prover context. But how exactly would the two Merlins use entangled particles in this case? Are they told before answering whether they’re both being asked for the color of the same node, or for the colors of adjacent nodes? (If not, then how can they use the entanglement — it’s easy to see how they could measure the entangled particles and make use of a protocol to permit them to provide the same or different color according to the question asked, but they could also do this via a pre-agreed classical protocol).
Finally, once you’ve filled in the details of the protocol, and explained how entanglement can be used, then how does the Ito/Vidick result you mention (arXiv:1207.0550 ?) override the use of entanglement?
Comment #23 November 26th, 2012 at 12:42 am
I know very little complexity theory, so the following question is probably explaining without understanding, but
Can one define quantum proofs very generally so that probabilistic, interactive and zero knowledge proofs are special cases of quantum proofs? Classical probability is a limit of quantum mechanics, interactive depends on what observables one is allowed to measure, zero knowledge sounds like the least number of observables are allowed to be measured
Comment #24 November 26th, 2012 at 5:54 am
Just thought you should see this since it was related to the Lego Turing machine. Made me cringe a little. http://www.google.com/hostednews/afp/article/ALeqM5jfvsy2G44S1zgbkMgubhgKUEEPuQ?docId=CNG.93856f85727197789905422507423546.1131&index=0
Comment #25 November 26th, 2012 at 11:28 pm
Slipper.Mystery #22: Yeah, some people complained about that after the talk as well, so I guess it was confusing (in my defense, I probably would’ve explained it better, but I was running out of time). In complexity theory, it’s always assumed that the two Merlins can agree on a strategy—which in this case, means a 3-coloring—before the protocol starts. And yes, they could meet again to agree on a new 3-coloring in between every two challenges from Arthur; that would make no difference to the protocol’s completeness and soundness.
The answers to your other two questions are much more complicated. I’m not sure if I’ve ever seen a good popular exposition of how entanglement lets Merlins cheat (let alone how to overcome that problem, which is a few-months’-old result!) An excellent starting point, however, is this paper by Cleve, Hoyer, Toner, and Watrous.
Comment #26 November 26th, 2012 at 11:45 pm
rrtucci #23: You can have pretty much any combination you want! People have defined and studied quantum interactive proofs, quantum zero-knowledge proofs, etc. However, I don’t think there’s any sense in which “quantum” is some sort of umbrella notion that captures everything. For one thing, you can certainly have non-interactive and non-zero-knowledge quantum proofs. Even more important, no matter how you chose to define “quantum proofs,” I bet I could find a classical notion of proof that wasn’t encompassed by your notion! (By simply adding more Merlins, making their messages longer, giving Arthur more time to verify them, etc.)
Adding quantum seems to make many kinds of proof more powerful than they would be otherwise: for example, it’s conjectured that QMA strictly contains MA (where MA = Merlin-Arthur), and that QSZK strictly contains SZK (where SZK = Statistical Zero Knowledge). (Though on the other hand, we now know that QIP=IP=PSPACE, meaning that quantum does not increase the power of poly(n)-round interactive proofs!) On the other hand, quantum is not a panacea whose addition makes a given proof notion “leapfrog” over every other proof notion that could ever be defined: to give one example, no one knows whether QSZK contains classical MA, and they might well be incomparable.
In other words: as far as complexity theory knows or cares, quantumness is basically “just another interesting resource to add to the mix,” similar to nondeterminism, multiple provers, etc. Of course, the fact that the actual physical universe seems to provide quantumness makes that resource extremely special! But then we’re talking physics, not complexity theory. 🙂
(Incidentally, I think your comment stopped making sense at “interactive depends on what observables one is allowed to measure.” I don’t know how to define interactive proofs by talking only about “measuring observables,” without making reference to a hypothetical entity that implements a strategy with the goal of maximizing the verifier’s acceptance probability.)
Comment #27 November 27th, 2012 at 10:27 am
Scott #25: re the two Merlin’s cheating, for a graph with N vertices I’m willing to believe this can be done with an entangled state of 2N qubits, each Merlin holding N of them, one for each vertex, with the entanglement such that the qubits corresponding to the same vertex always measure the same, and qubits corresponding to neighboring vertices always measure different.
I even suspect this can be done with 2logN qubits, such that each vertex is associated to applying a specific binary pattern of Hadamards before measurement, again such that same and neighboring patterns measure same and different.
But do you happen to know the minimum number of qubits necessary for this case of cheating, specifically whether constant or how it scales with N?
Comment #28 November 27th, 2012 at 8:15 pm
p.s. scott #25: An excellent starting point, however, is this paper [arXiv:quant-ph/0404076] by Cleve, Hoyer, Toner, and Watrous
OK I have looked. In 3.2 they discuss convincing a ref that an odd cycle of length n is 2-colorable, using a single Bell pair. The optimal strategy is correct with probability cos^2(pi/4n): better than the classical 1-1/2n, but not a perfect quantum strategy. (So now it’s not clear if your two Merlin’s were just beating the classical odds, or always successful.)
In 4.1, they discuss the graph coloring proof system, with k colors, where there is a perfect quantum strategy for a class of graphs G_n, but the smallest number of colors for which one of these is uncolorable (and hence would require the quantum strategy) is k=n=16, so inapplicable to the k=3 case.
So still slightly unclear as to whether there’s a perfect quantum strategy for two Merlins purporting to 3-color, or just one that beats the classical odds (i.e., does better than 1-1/(V+E) ), and in either case how may qubits are used.
(Sorry if this takes your talk too literally)
Comment #29 December 3rd, 2012 at 7:01 pm
Re: Hamiltonian path proof: Sorry, there’s one part of this presentation that I’m stuck on. Could a bad Merlin fake knowledge of a Hamiltonian path? For example, could he always send back the Arthur graph with “clever” edge encryption such that: (1) If Arthur asks Merlin to reveal the whole graph, then Merlin could do so (decrypt all) and (2) If Arthur asks Merlin to show the Hamiltonian path, Merlin could just reveal |V| fake edges?
In other words, how does Arthur know that the boxes can only be decrypted one way and Merlin isn’t just picking a decryption key based on Arthur’s question? Do you need some kind of signature scheme to keep Merlin honest (in addition to encryption)? Or does your encryption scheme make it hard to fake the true contents of a message?
[I don’t think the question changes much if Merlin is only allowed to send back one key for all |V| Hamiltonian edge boxes. Maybe that just means he needs each box to have 2^|V| hidden compartments, rather than 2].
Comment #30 December 3rd, 2012 at 11:38 pm
Slipper.Mystery #28: Yes, sorry, I’d forgotten that their examples with perfect entangled cheating strategies are for k-coloring rather than 3-coloring specifically. Would be interesting to know whether it can be done for 3-coloring (or maybe it’s already known).
For other similar examples, see the Mermin Magic Square Game and Pentagram Game.
Comment #31 December 3rd, 2012 at 11:43 pm
ngm #29: To make it work, you need an encryption scheme where every message has a unique decryption (also known as a commitment scheme). But those exist under pretty minimal cryptographic assumptions. As the simplest example, Merlin could encrypt a 0 with a product of 2 huge primes and a 1 with a product of 3 huge primes, then factor the products to reveal the bits he commited to. (Note that Arthur can check in polynomial time that a given number is prime.)
Comment #32 December 4th, 2012 at 10:02 am
Great explanation! Thanks!
Comment #33 December 5th, 2012 at 9:53 am
Scott #30: Would be interesting to know whether it can be done for 3-coloring (or maybe it’s already known).
Yes, the Magic Square and Pentagram games are described in Mermin’s ’93 article http://link.aps.org/doi/10.1103/RevModPhys.65.803 , but the 3-color case still requires more thought. It is conceivable that Arkhipov the author of http://arxiv.org/abs/1209.3819 would already know the answer (though the problem is slightly different from his generalization of Mermin-Peres).
Comment #34 December 11th, 2012 at 12:02 am
Slipper.Mystery December 5th, 2012 at 9:53 am Says: Your comment is awaiting moderation.
(The AI underlying the blog moderation appears to be running on an Atari 2600 these days)
If we’re to believe that the refs in http://arxiv.org/abs/1212.1724 (Graph Homomorphisms for Quantum Players) are up to date (it just appeared today), then (a) the object in question is called the quantum chromatic number of a graph (the minimum c such that there exists a perfect quantum strategy, i.e., winning every time despite the lack of a classical c-coloring), and (b) currently there are no known graphs with c=3.
If this interpretation is correct, this small part of the talk may need to be modified next time around.
Comment #35 December 16th, 2012 at 10:00 pm
Slipper #34: I don’t think the paper you refer to claims that there are no known graphs with quantum chromatic number 3 and chromatic number greater than 3. In fact, Imai, Le Gall, and Fukawa describe such a graph. To achieve this (3 vs >3) kind of separations, quantum provers *must* use measurements with projectors of rank higher than one (i.e. full basis measurements are not sufficient).
Unfortunately, the paper “Quantum Coloring Games via Symmetric SAT Games” by Imai, Le Gall, Fukawa that I refer to above, can only be found in the conference proceedings of AQIS 11.
Comment #36 October 16th, 2013 at 12:19 am
ヴィトン バッグ トート