Introducing some British people to P vs. NP
Here’s a 5-minute interview that I did with The Naked Scientists (a radio show syndicated by the BBC, and no, I’m not sure why it’s called that), explaining the P vs. NP problem. For readers of this blog, there won’t be anything new here, but, well … you might enjoy the rest of the hour-long programme [sic], which also includes segments about a few other Clay Millennium problems (the Riemann Hypothesis, Navier-Stokes, and Poincaré), as well as a segment about fat fish that live in caves and gorge themselves on food on the rare occasions when it becomes available, and which turn out to share a gene variant with humans with similar tendencies.
Follow
Comment #1 July 22nd, 2015 at 1:47 pm
I expect the name of the show is a reference to “The Naked Chef”, which was a cooking show in which the titular chef (Jamie Oliver) wasn’t naked either.
Comment #2 July 22nd, 2015 at 3:08 pm
When I saw the title of the post, I thought you were going to talk about this nice preprint 🙂
http://arxiv.org/abs/1507.05061
Comment #3 July 22nd, 2015 at 3:17 pm
Sorry, did you mean Cat fish?
Comment #4 July 22nd, 2015 at 4:20 pm
“The Naked Chef” was called that because Jamie Oliver intended to strip everything down to the basics of cooking, instead of making things gratuitously fancy and elaborate as many other cookery programmes of the time did. The intention was to simplify the process of cooking so that anyone could do it. Presumably “The Naked Scientists” has a similar philosophy.
Comment #5 July 22nd, 2015 at 6:29 pm
Saul #3: No, fat fish. Listen to the segment!
Comment #6 July 22nd, 2015 at 6:32 pm
Rachel #4: ah, OK, thanks. They certainly did strip my segment down to the bare essentials! Based on my incorrect understanding of what they explained to me, I was ready to speak for an hour, field call-in questions, etc., but then they only wanted 5 minutes, and then even that was edited down for length.
Comment #7 July 22nd, 2015 at 6:52 pm
Shtetl Optimized readers may enjoy reading the case for the opposite view, per some brand-new references that were supplied by this week’s Calvin Café essay “Don Knuth on SAT“ (note: Calvin Café is hosted by the Simons Institute for the Theory of Computing at UC/Berkeley).
Here are excerpts from what Knuth has to say:
(the closing brackets are Knuth’s)
Affirmation of Knuth’s view that “the subject is not fully explored”, appears in last week’s Ahmed Younes and Jonathan Rowe preprint “A Polynomial Time Bounded-error Quantum Algorithm for Boolean Satisfiability” (arXiv:1507.05061, see comment #2): their proposed SAT-solving algorithm depends crucially upon ancillary qubits that supply precisely the Tseytin-style extended resolution that Knuth’s concluding paragraph commends.
Younes and Rowe’s claimed proof may be correct or it may be flawed — a safe bet is that it is flawed — but at least their proof strategy does exhibit some elements of the Tseytin/Knuth-level ingenuity that any successful proof plausibly would require.
Conclusion To borrow some felicitous phrases from a recent Shtetl Optimized essay, Donald Knuth’s 310-page “truly epic” exposition on satisfiability “has not a single word of filler: it is just pure beef.”
PS A sure-to-be-tasty follow-on course to Knuth’s “pure beef” is this fall’s Simons Institute Program (Aug. 19 – Dec. 18 2015) “Fine-Grained Complexity and Algorithm Design”, which no doubt will serve-up a banquet of Tseytin/Knuth extended-resolution methods — and many other tasty mathematical dishes too — to algorithm-famished attendees.
Comment #8 July 22nd, 2015 at 7:18 pm
Re: Anthony #2
Um, yeah, if you would care to weigh in on that pre-print Scott, I would really be interested to read your thoughts. 🙂 🙂 🙂
Comment #9 July 22nd, 2015 at 8:48 pm
Scott, do you really believe that if P=NP, then current cryptography is necessarily broken or that computers can be programmed to (efficiently?) solve Millennium Problems? I would appreciate if you could elaborate on that since I’m guessing that these statements were oversimplifications necessitated by shortness of your interview. Or, if you wrote about it elsewhere could you post a link?
Comment #10 July 22nd, 2015 at 9:08 pm
great to see the popsci promulgation efforts.
did you comment yet on the STOC2015 Backurs/ Indyk strong exponential time hypothesis vs edit distance in quadratic time result? more here
re this
this reminds me of fortnows recent book. there are all kinds of extravagant, wild claims about what would be possible if P=NP. agreed it would be wild, but have never found any scientific ref where these are actually laid out in detail, nobody ever cites any. am well aware many elite scientists claiming this, but its all close to enthusiastic handwaving if you ask me.
moreover, automated thm proving is all based on undecidable problems which P vs NP has little bearing on. so, whaddya say? you of all paper are highly qualified to write such a paper. could someone explain in more detail why P=NP leads to massive real world implications outside of math? (other than the quite verifiable crypto case?) thx in advance!
Comment #11 July 22nd, 2015 at 11:21 pm
Ian #8: As I say in my FAQ, normally I blog about such things only after they get so much attention that silence on my part would amount to complicity.
Comment #12 July 22nd, 2015 at 11:33 pm
Bobby #9 and vzn #10: There are potential implications of P=NP that are more speculative, but speeding up the finding of proofs of theorems is a completely obvious, straightforward, and uncontroversial one, which (for example) Gödel already discussed in his 1956 letter to von Neumann, reprinted in Sipser’s 1992 survey. All you need to notice is that, given any conjecture S expressible (say) in the language of ZF set theory, the statement
“There exists a ZF proof of S at most n bits long”
is an NP statement, with n as the parameter—not “is vaguely analogous to an NP statement,” but is one. So if P=NP, that immediately implies that there exists an algorithm that takes n and S as input, and in time polynomial in n and |S|, decides whether such a proof exists, and if so, finds one.
It’s true that deciding whether a given conjecture has a ZF proof is an undecidable problem, if you put no upper bound on the length of the proof, and don’t allow its length to enter into the running time. But if P=NP, that would mean you could always find formal proofs in time polynomial in the length of the proofs (i.e., in the time needed to write the proofs down at all), rather than exponential in the length. That’s the implication that I was talking about.
Obviously, whenever we talk about practical implications of P=NP, we’re always making the implicit assumption that the algorithm takes (say) n2 or n3 time, rather than n1000000 time or something absurd like that. But even if an n1000000 algorithm were discovered, that would still have world-changing importance, precisely because it would mean there was no longer any barrier to an n2 or n3 algorithm except for lowering one arbitrary-seeming exponent.
Comment #13 July 22nd, 2015 at 11:36 pm
vzn #10: Yes. I commented on the Backurs/Indyk breakthrough here.
Comment #14 July 23rd, 2015 at 12:26 am
There is a sequel to the Naked Chef with a naked chef…
Comment #15 July 23rd, 2015 at 9:29 am
Scott, yes I’m sorry I thought it was a typo since I explore caves in Central America and we do have troglobite versions of Cat Fish, but wow this is very interesting! Perhaps this is the fish they are talking about:
https://en.wikipedia.org/wiki/Mexican_tetra
Comment #16 July 23rd, 2015 at 10:24 am
Scott #12:
““There exists a ZF proof of S at most n bits long”
is an NP statement, with n as the parameter—not “is vaguely analogous to an NP statement,” but is one.”
Is there a way to transform an instance of such a proof searching problem into a statisfiability problem (in poly time)?
If not, does it matter?
Comment #17 July 23rd, 2015 at 11:06 am
#12 ok, agreed auto thm proving might get a dramatic boost from P=NP, but we already have massive supercomputers and cloud resources to search for proofs (if its really somewhat an NP complete problem rather than undecidable, then its “embarrassingly parallel” like other NP complete problem eg SAT, and massive parallelization should have a significant effect on it), but very few to “nobody” seems to be doing it. why not? is this a collective bias against “experimental” work or is there something else more fundamental at play? so agreed that P=NP seems to lead to some magical-like scenarios (much of this concept seems to go back to Impagliazzo’s Worlds), but as complexity theory teaches us, there are different levels of magic so to speak, and just feel that some of the assertions about real world implications of P=NP go too far and verge on “magical thinking”…. it seems hard for ppl to wrap their brains around the fact that either P=NP or P!=NP is “counterfactual” and analysis of its contrary aspect is literally based on a fallacy. therefore think scientists should be conservative in their claims about implications esp in the Real World™ either way…
Comment #18 July 23rd, 2015 at 1:11 pm
Donald Knuth’s remarks (quoted in #7) pullback to the second-order (Gödelian?) observation
Broader perspectives Donald Knuth’s views in regard to PvsNP may be right or may be wrong, but perhaps more relevantly — in regard to Scott’s FAQ (of #11) — it is assuredly the case that Knuth’s views are rational and their implications are profound for complexity theory (both foundational and applied).
At least, Luca Trevisan thought so (as the author of the Simons Institute/Calvin Café essay “Don Knuth on SAT“ cited in #7).
Conclusion The careful study of Knuth’s graceful writings and effective research methods is near-universally commended to young researchers in complexity theory … and every other STEAM discipline too.
Comment #19 July 23rd, 2015 at 1:36 pm
VZN, what kind of massive parallelization do you have in mind? Assuming you set the upper bounds at, say, a 10 page proof, further assuming a page can hold about 2,000 characters, and further assuming that there are 100 possible, distinct characters in a proof (which is definitely an underestimate with the English language, numerals, math symbols, Greek letters, etc. one can use), you’d need to check over 100^2000 or 10^4000 proofs. Even if you had a billion computers (that’s US billion, 10^9), each one would have to check 10^3991 proofs. If one computer could check a million proofs a second, you’d need 10^3985 seconds, or 3.171×10^3977 years. Parallelization isn’t enough.
Comment #20 July 23rd, 2015 at 1:38 pm
Err, I’m sorry, the numbers in my comment above are for a one page (2,000 character) proof. It gets much worse for 10 pages.
Comment #21 July 23rd, 2015 at 1:56 pm
vzn #17: People have tried automated proof search; in fact it’s a major research area. Probably the most famous success of the field was the proof, in 1996, of the Robbins Conjecture, which was a longstanding open problem in logic. In that case, the proof was only 13 lines, but searching for it took several weeks with fast workstations of the time (as well as lots of clever pruning strategies). For the Riemann Hypothesis, you could imagine that the shortest ZF proof might be hundreds of megabytes, in which case this sort of approach would be completely hopeless, even if you filled the entire galaxy with workstations (as Vadim #19 correctly points out).
The reason P=NP would be incredible is precisely that it would completely change this situation.
If you find the consequences of P=NP too “magical” for your taste, then there’s a very simple way out: namely, just accept that almost certainly P≠NP, like I do, and like you probably do already for the Riemann Hypothesis and most other famous unsolved math problems. Try it; I recommend it! 😉
Comment #22 July 23rd, 2015 at 4:14 pm
#19/#21. yes am a big fan of auto thm proving myself, a favorite area & have researched the area heavily, and there are very notable successes over the years (have cited many myself on blog), but (to me at least) they seem quite unusual/ isolated/ somewhat anomalous. if thm proving of important thms was indeed “subject to search”, seems like more results would be around for “low to medium” level complexity and significance of proofs (yes many thms have been computer-proven ie verified with human guidance, am talking about finding original proofs.) from long analysis of this area, think there is something more fundamental in play. ie theorems are fundamentally not amenable to search the way NP problems are, and think this is an independent fact of P≠NP so to speak, and shorthand discussion/ soundbites on that even by expert scientists seems to gloss over this. & think this is related to the relationship between thm proving and undecidability. so think that the common shorthand of talking about NP problems in the same breath as “proofs” is something of a misnomer….
Comment #23 July 23rd, 2015 at 4:24 pm
Scott #21
But can’t we flip the argument around and ask:
How come the brain of a mathematician (a physical structure using way less resources than a universe filled with computers) was able to find the proof for Fermat’s last Theorem?
“Intuition”, “Genius” really mean “magic” given our current understanding of the human brain.
Or just declaring in hindsight that “Fermat’s last theorem” was relatively easy to prove?
Comment #24 July 23rd, 2015 at 4:58 pm
Fred,
In the case of the FLT proof, humans (or one human) found a solution for a particular problem instance; they didn’t find a general algorithm for a problem (given a theorem, find a proof). FLT may have some structure in it that makes it easier to find a proof (actually, it must, since Andrew Wiles didn’t find the proof by brute forcing as our galaxy filled with computers would), but the technique he used to do it isn’t general.
Comment #25 July 23rd, 2015 at 5:08 pm
vzn #22: Formal proofs are subject to search (though the search might, of course, be infeasible in practice), because the problem of whether a given statement has a formal proof of length n is an NP problem. This is a mathematical fact. It follows from the definition of NP. It’s not a question of how you feel about it.
And the fact you point out, that automated theorem proving has had only a few isolated successes in solving famous open problems, is exactly what you would expect if P≠NP, and if proofs of most interesting theorems were sufficiently long that brute-force search was an infeasible way of looking for them! You keep wanting to accuse TCS people of intellectual dishonesty and of asking the wrong questions, but then, ironically, you base your case on phenomena that are perfectly clearly explained by the P≠NP hypothesis.
Comment #26 July 23rd, 2015 at 6:10 pm
LOL! “relatively easy”! it took over 3½ centuries by worlds top math minds! anyway this example seems to further the idea that there is something nonalgorithmic about theorem proving in the same way human intelligence is (apparently so far!) nonalgorithmic….
whoa! objection your honor! let the record show, innocent as charged!
searching for a solution to SAT involves assignment to a finite set of binary variables. searching for a mathematical proof involves axioms, existential logic, substitution rules, parsing, etc….! isnt there some major glossing over going on here? who has reduced general math theorem proving to SAT? (leaving aside the question of whether it is solvable, where is the reduction? somehow missed that bulletin/ ref!
Comment #27 July 23rd, 2015 at 6:11 pm
Vadim #24,
sure, but that still doesn’t explain how his brain came up with that proof.
“FLT may have some structure in it that makes it easier to find a proof”
But doesn’t the same argument hold for NP=P using problem structure?
It could also be that mathematician brains have a general method to come up with rather successful average-case NP solutions (given the finite resources of a human brain).
It also goes back to what Scott asked recently about the class of math theorems humans happen to find relevant/interesting. By definition our brains only “see”/”understand”/”like” problems that can map to their internal structures (and we’re just blind to the rest).
All I’m saying is that saying P!=NP because too much “magic” would be happening is kinda “short changing” the fact that there’s plenty of magic already going on with the human brain, as a computing machine. I’m not claiming that the human brain is a proof that P==NP, but that we may not have yet fully understood the richness of “classical” optimization algorithms.
Comment #28 July 23rd, 2015 at 8:03 pm
@fred #16: That’s a good and observant question. Answer is that it heavily depends on what ‘S’ is. If it is something that can be converted (hopefully efficiently) to something written in the language of propositional logic, then it is straight forward.
Unfortunately, many statements of theorems are not written out this way and most cannot be simplified down efficiently. A lot that you see make use of fragments of first order logic with richer usages of quantification or have additional ‘features’. For example, it is definitely useful for us to be able to prove theorems expressed in variants of linear temporal logic (LTL) or prove some special security properties of sophisticated cryptographic protocols. The equivalent formulations of these statements in the language of SAT could be exponential in size or worse. So even if P=NP, the combined running time would be on the order of O(poly(>=exp(n’))). When it comes to being able to efficiently prove interesting theorems automagically, knowing that P=NP makes a much smaller dent on the problem than some people make it out to be.
Comment #29 July 23rd, 2015 at 9:11 pm
Stupid question obviously coming from a guy who doesn’t read many proofs, but can proofs (in FOL or however they’re normally done in practice) have anything analogous to loops and conditionals? In other words, are proofs programs? If so, doesn’t that prevent us from verifying a proof in polynomial time in the worst case? To avoid that, in addition to the upper bound on proof size, we’d need an upper bound on the number of recursions.
Comment #30 July 23rd, 2015 at 9:45 pm
vzn #26:
who has reduced general math theorem proving to SAT? (leaving aside the question of whether it is solvable, where is the reduction? somehow missed that bulletin/ ref!
Err, that particular reduction was done by Stephen Cook in 1971 (paper title: “The Complexity of Theorem-Proving Procedures”), and independently by Leonid Levin around the same time. Maybe you’ve heard of them? 😉 (Also, did you really think I’d say what I said in the previous comments, if the needed reduction weren’t merely known, but one of the most fundamental things in TCS?)
To answer your question, all you need is
(1) a polynomial-time algorithm to verify the proof of a theorem in ZF or some other formal system (which is easy; theorem-provers like Coq and Mizar and HOL Light actually implement such algorithms), and then
(2) the Cook-Levin Theorem, which uses that algorithm to convert the problem of finding a proof of size n into a size-nO(1) 3SAT instance.
Look, until you’ve worked through an intro complexity textbook (even Sipser’s would be fine), it probably won’t be a good use of time for either of us to continue arguing about these things.
Comment #31 July 23rd, 2015 at 9:58 pm
Vadim #29: No, if you’re talking just about a standard proof in first-order logic, then it has no analogues of loops or conditionals. It’s more like a “straight-line program”; every statement in the proof needs to follow from previous statements and/or axioms by one of a few allowed rules of inference. So such a proof can actually be verified in close to linear time.
With more general notions of “proof,” things can get more complicated—e.g., you could have one step in the proof be, “run this program and verify that indeed it terminates after n100 steps.” And people might or might not deal with such things in program verification; I’m not sure. But in any case, for first-order proofs, it’s really as simple as I said.
Comment #32 July 23rd, 2015 at 10:26 pm
fred #27: I liked how Stephen Hawking once put it, in response to Roger Penrose’s question of how human mathematicians could possibly be so good at proving theorems if the brain just obeyed the known, mechanistic laws of physics. “It’s a very hit-or-miss business,” he wrote. “We certainly don’t have a knowably sound procedure.” Here he meant: a knowably sound procedure for guessing new axioms of set theory consistent with the previous ones. But one could likewise say: we humans certainly don’t have a general procedure for proving arbitrary theorems in time polynomial in the proof length! If so, we could exploit that procedure in our heads to, e.g., factor huge numbers and break RSA.
How humans manage to find proofs of particular assertions lile FLT is an extremely fascinating question—but it’s safe to say that it has something to do with “chunking,” or moving up to higher and higher levels of abstraction, and something to do with the human ability to find analogies and connections between seemingly-unrelated parts of math. It also has to do with the fact that are such connections to be found, and that chunking and abstraction actually work for many of the questions (like FLT) that humans care about—that such questions turn out to form a supercontinent, rather than a bunch of disconnected islands, as they could have been a priori. As I wrote in this essay, this is something that I still find mysterious, but at least it’s a mystery that mathematicians have had many centuries of experience with.
Comment #33 July 24th, 2015 at 12:24 am
#30, am quite familiar with cooks proof from undergrad CS, thx much for that (fyi we used ancient hopcroft/ ullman… maybe not acceptable nowadays with all the new thinking/ results in complexity theory?).
what is the proof that thm provers such as those you mention run in “P-time” for problem verifications? what does that even mean for individual thm instances? doesnt actual run time tend to depend on the problem? think this stuff is glossed over/ handwaved off by many. to refer to it as “dishonesty” is putting words in someones mouth. “slippery”, maybe. ps not sure if any actual/ real arguing is going on. it takes two to tango.
Comment #34 July 24th, 2015 at 1:09 am
Re #12: I disagree about “But even if an n1000000 algorithm were discovered, that would still have world-changing importance, precisely because it would mean there was no longer any barrier to an n2 or n3 algorithm except for lowering one arbitrary-seeming exponent.”
There is no reason to think it could be lowered to even n^999999, other than the fact in some cases it has happened.
So, it might have world changing theoretical importance, but it will continue to have zero practical importance.
Pretty much everyone agrees that P = NP is the top TCS question. We are all on board with that. But why are so many unwilling to let it just be a great theoretical problem? Claiming it has practical significance is irresponsible BS.
Comment #35 July 24th, 2015 at 8:30 am
vzn #33: All it means for these provers to run in polynomial time is that they verify a proof of length n, in time polynomial in n. In fact the time is close to linear in n, since as I explained in comment #31, all the checker needs to do is check that each line of the proof follows from previous lines (or from axioms). And no, the running time does not depend on the particular proof or statement being proved.
Comment #36 July 24th, 2015 at 8:51 am
Scott #31
” It’s more like a “straight-line program”; every statement in the proof needs to follow from previous statements and/or axioms by one of a few allowed rules of inference.”
.
So this system is powerful enough to also come up with a classic proof by induction (i.e. show the base case holds, then the induction step) without being stuck in just showing the relation holds for i=0,1,2,… (infinity)?
I’m having a tough time imagining how that could work (but I guess it’s one of those “few allowed rules of inference” you’re talking about).
.
Scott #30 “Cook-Levin Theorem”
Hah, that answers my question in #17. There’s no need to look for an explicit transformation from a proving problem to SAT, we always know that one must exist.
Thanks!
Comment #37 July 24th, 2015 at 9:03 am
Observation The comments here on Shtetl Optimized, and Don Knuth’s fascicle 7.2.2.2 Satisfiability (per comment #7) too, are grappling with the mysterious reality, which is both individual and social, that solving tough NP-complete problems is a crucial task of ordinary human life.
Tensions, appreciations, and relaxations The following Shtetl Optimized passages vividly illustrate three canonical tensions, appreciations, and relaxations that are associated to NP-solving.
In regard to “tensions” It’s an admirable trait of Shtetl Optimized commenters that, in the present comments, there have been no “accusations of intellectual dishonesty”, and neither have any substantial reasons been set forth that commenters are “asking the wrong questions.” Indeed, Don Knuth’s fascicle takes pains to document that so many PvsNP questions are presently open, that no one person or group can reasonably tackle more than an near-infinitesimal portion of them … and so the possibility of “asking the wrong question” is essentially moot.
In regard to “appreciations” Shtetl Optimized readers who wonder “How does reduction-to-SAT work exactly?” and “What cognitive strategies are humans using for problems that reduce to SAT?” will are encouraged to consult Knuth’s index for discussions of Stephen Arthur Cook’s works (on pages 61, 62, 130-131, 154, 229, and 237). It was news (to me) that Cook’s research strategies were so intimately focused upon concrete SAT-solving methods, and that so many of Cook’s research questions remain open — and even unpublished! — even today. We all owe a great debt to Don Knuth for his sustained labors in gently illuminating these crucial pages of TCS history.
In regard to “relaxation” As with Knuth, we all owe a great debt to Scott, for his sustained labors in “a spirit of transcending backgrounds and ‘building a global shtetl'”. The process of building STEAM-shtetls surely ain’t simple, easy, or quick … the joke of “two STEAM-workers, three opinions” definitely applies.
Chess-fans (I am one) appreciate the dislocations attendant to “the rise of the machines”, which has been so pronounced that nowadays inarguably the best chess-players are centaurs, which is to say, humans who conceive chess strategies partnered with machines that work out the details.
Similar “centaurian syntheses” are becoming increasingly dominant in pretty much every STEAM discipline. Are we to infer that someday — perhaps even someday soon — the Riemann postulate may be settled by the publication of a human-conceived/human-understandable ten-page proof-strategy, accompanied by a machine-generated certificate that SAT-solving algorithms have successfully expanded this proof-strategy into a rigorous proof (whose details plausibly will be of more-than-human length).
As to the feasibility and/or desirability of a mathematical centaurian synthesis, Michael Harris’ admirable (as it seems to me) weblog Mathematics Without Apologies has been hosting in recent weeks a high-level “shtetl-building” discussion on this topic, in regard to Harris’ essay Univalent Foundations: “No Comment.” (of May 13, 2015).
More broadly, Harris’ weblog, and his recent book of the same title, make an outstanding complement to Knuth’s fascicle and to the discussions here on Shtetl Optimized
Fundamental to any background-transcending shtetl is a shared appreciation that it is neither necessary, nor feasible, nor even desirable that everyone think alike. So let’s give Donald Knuth the last word:
Conclusion The Knuthian process of teaching computers to think more diversely yet rigorously, may assist people in learning to think more diversely yet rigorously … and thereby foster the evolution of a more vigorous, more diverse, more background-transcending global STEAM-shtetl.
Comment #38 July 24th, 2015 at 11:06 am
ok! re #28 have heard/ read in misc cases that some proofs that are “not that big” in human readable format/ papers tend to “blow up” in size when converted to ATP formats. many ATP workers have attested to this. and this might be closer to real complexity of proofs hinted in #31. not claiming it is impossibly, only think the details need to be filled in (eg in a paper) & havent seen it done. have not seen papers that do so. how many proofs utilized by mathematicians are actually 1st order logic? it seems that there is not much study of the actual theoretical complexity of ATP & real world packages, it is more of an applied field….
not an expert! is ZFC considered entirely 1st order logic? how many modern proofs can be expressed in it? if proofs can be verified in P time then why are so few important modern proofs converted to ATP formats? there is a new/ recent sciam article on attempting to eg streamline the classification of finite simple groups, spanning thousands of pages, and afaik, nobody is talking about (what might seem somewhat obvious) mounting an ATP effort on that…. also, seems like russell/ whitehead book principia mathematica is a relevant yet cautionary tale in this area… hundreds of pages to prove 1+1=2!
Comment #39 July 24th, 2015 at 2:13 pm
Regarding the Rowe-Younes paper (ad #7, #8), the part of their algorithm sketched most clearly in Figure 3 at the top of page 7 seems to be doing post-selection on a measurement result of 1 (the NOT gate is not present if the result is 0). Scott showed Postselected-BQP = PP, and of course NP is in PP. At least this seems to be the most likely error, not taking time to plumb it further. There is a Hacker News thread at https://news.ycombinator.com/item?id=9928657 but not with a mention of post-selection.
Comment #40 July 24th, 2015 at 2:30 pm
Actually the deferred-measurement analysis of Strilanc at the bottom amounts to the same thing as what I said; the 2–10 loop in the algorithm on page 9 is the same juncture, and the blowup seems to be the same as what you get if you try to eliminate post-selection.
Comment #41 July 24th, 2015 at 3:05 pm
A on-line white paper that at least begins to address the various questions/concerns of vzn’s comment #38 is Homotopy Type Theory: Unified Foundations of Mathematics and Computation (MURI Proposal), by a team that includes multiple mathematical luminaries and numerous top-ranked research institutions.
Is there anything like a consensus view regarding the future prospects of the HoTT/UF program? No.
Conclusion Plausibly it is no harder to create the outcome of emerging mathematical enterprises like HoTT/UF, than to predict that outcome.
Comment #42 July 24th, 2015 at 6:06 pm
Is it possible to prove an $n^4$ time space lower on SAT by using randomness?
Comment #43 July 24th, 2015 at 6:29 pm
vzn #33, #38: Proof length has been investigated, at least with respect to cut-elimination and higher-order logic:
From the wikipedia article on the Cut-elimination theorem
In “A Curious Inference”, Boolos shows a similar phenomenon for first-order logic vs. higher order logic, see for example the article “A Lost Proof” by C. Benzmüller and M. Kerber.
The rant “A term of length 4,523,659,424,929” by ARD Mathias is also famous.
ZFC can be considered entirely 1st order logic. However, you may also consider ZFC to be the “backport” of NBG to Zermelo set theory, and NBG can be considered both as 1st order and as 2nd order, whichever you prefer. I probably won’t count as an expert either from an academic point of view, but I worked through an intro logic textbook (Ebbinghaus…) and intermediate logic, type theory and set theory material (SEP, R. Holmes, ARD Mathias, Boolos, Shapiro, Quine, Girard, …), so maybe I have a chance to pass Scott’s “good use of time” test, if he doesn’t find out that I have trouble following Girard.
Comment #44 July 24th, 2015 at 6:45 pm
Scott #30: The suggestion to work through intro textbooks doesn’t help with the real problems a passionate amateur scientist like vzn might face. After publishing one or two real articles, you learn that it is a huge amount of work, and that the feedback you get is not significantly more than if you had just published your ideas unpolished on your own blog. And if you behave slightly off (but not too much) and overuse words like “breakthrough” or “revolution”, then you might even get a decent amount of feedback.
Comment #45 July 24th, 2015 at 6:46 pm
Instead of conjecturing P≠NP, my preference goes to the following, stronger hypothesis: “it’s impossible to factor large integers efficiently, using a method that’s actually feasible.”
Unfeasibility without logical impossibility has indeed a great explanatory power. It accounts very well for not finding an algorithm, while not being able to prove that there’s none. So I expect the following breakthrough in a near future: a galactic, classic, polynomial algorithm for integer factoring. Do you think it’s possible?
Comment #46 July 24th, 2015 at 6:55 pm
Scott #35: vzn’s defense might have been weak, but your reply “All it means for these provers to run in polynomial time is that they verify a proof of length n, in time polynomial in n.” is worse. A proof can be interpreted as a certificate for a non-deterministic computation, and the length of the certificate has to be bounded by a polynomial in the length of the statement it purports to prove, if you want to claim that the problem is in NP (i.e. reducible to SAT). As vzn correctly points out, this doesn’t even make sense for a single statement.
But if we would consider the set of all statements provable in a given formal system, then hell breaks lose, and we are thrown far outside of NP (and even NEXP). Then even padding of the statement cannot bring it back into NP. What one can do instead is to include the allowed length of a proof as part of the statement. However, then the statement is no longer independent from the formal system used to prove it. Because the length of the shortest proof of a given statement varies widely between logically equivalent formal systems (as pointed out in reply to vzn #38), this is a serious limitation of this approach, and not just a minor detail.
Comment #47 July 24th, 2015 at 7:56 pm
Essentially by showing even if $NP\subseteq P/Poly$, then we need $n^4$ time-space lower bound?
Comment #48 July 24th, 2015 at 9:59 pm
RE: #38
Well, mathematicians aren’t really going to be explicit about the logic they’re using. Some statements may naturally sound like higher-order logic. But if you try to be explicit about the theory and logic you’re using, all proofs easily convert to 1st order logic.
Yes.
Most proofs can be directly written in ZFC, although there’s a fair amount of usage of Grothendieck Universes (which is stronger than ZFC) in some modern areas of math.
There are interesting debates in the logic community whether such strong theories are required, or if the proofs can be lowered to weaker systems, such as second order arithmetic (which, despite the name, uses first order logic).
I think the simple answer is, mathemeticians have better things to do with their time. I hope some day ATPs are nearly as easy to use as LaTeX, at which point everyone will use ATP to guantee they have made no errors. But today, formalizing proofs in ATP is a difficult and low-reward activity.
I think I read a similar article a while ago too. It’s really amazing what a feat the proof is, involving so many mathematicians and so many pages!
The highest priority is to have a self-contained, complete human-readable proof first, before we proceed to ATP. ATP could be done any time in the future, since it’s just translation of what’s already been written. But streamlining the proof ideally needs to be done while the experts in the proof are still alive.
From wikipedia, I see that the Feit-Thompson theorem, one of the first steps in the classification proof, has been formalized.
Comment #49 July 24th, 2015 at 11:18 pm
Luke #48: Thanks so much for explaining all that, and thereby saving me the need to!
The one thing to add is that, while converting an informal proof to a formal language like ZFC does incur a blowup, the blowup will be by a constant factor—it won’t be by an exponential, as can happen, for example, when converting from ZFC to resolution (for a proof of the unsatisfiability of a propositional formula). That’s just a different way of saying that ZFC is powerful enough to capture all ordinary mathematical reasoning. (Indeed, even if you wanted more powerful principles than ZFC, like Grothendieck universes, you could just tack them on as additional axioms—what’s really important for this discussion isn’t the ZFC axioms, but just the language and inference rules of first-order logic.)
Comment #50 July 24th, 2015 at 11:37 pm
Raoul #34:
There is no reason to think it could be lowered to even n^999999, other than the fact in some cases it has happened.
So, it might have world changing theoretical importance, but it will continue to have zero practical importance.
Pretty much everyone agrees that P = NP is the top TCS question. We are all on board with that. But why are so many unwilling to let it just be a great theoretical problem? Claiming it has practical significance is irresponsible BS.
Suppose someone built a controlled nuclear fusion generator, which put out way more power than was needed to run it, but the one caveat was that the current model cost ten billion dollars per day to operate, making it completely economically impractical.
By your standards of argument, we would need to say: this discovery is purely theoretical; it has zero practical significance (and claiming that it does is irresponsible BS). We can’t say that the cost will probably come down, since logically, no one can prove that the cost will come down by even a cent.
But I think the most hardheaded businessperson would say that’s completely absurd. If we’re talking about practical significance at all, then ipso facto we’ve left the realm of proof and entered the realm of Bayesian likelihood. And all of our experience in theoretical computer science tells us that exponents, particularly huge exponents, are a lot like prices. I.e., they’re numbers whose hugeness is way more likely to reflect the messy compromises of a proof than some Platonic reality, and that (like the cost of a brand-new technology) can come down dramatically if people care enough about bringing them down, and invest enough blood and sweat into optimizing them.
Must that always be the case? Of course not. And believe me that I’m perfectly capable of distinguishing what we can prove from what’s merely in keeping with all our previous experience. But if I’m asked to speculate about the likely practical implications of such-and-such a result (as opposed to the logically provable implications), then why on earth should I ignore previous experience? It’s not what people do in any other domain, making the insistence on it in theoretical computer science an isolated demand for rigor.
Comment #51 July 25th, 2015 at 12:14 am
gentzen #46: If you really want to be pedantic, the point I was trying over and over to explain to vzn boils down to saying that the language
L = {⟨S,0n⟩ : S has a ZF proof ≤n symbols long}
is in NP. Which, I hope you’ll agree, is a true statement, and which suffices for the conceptual point I was trying to make (that if P=NP, proofs of length n could be searched for in poly(n) time).
I think what’s going on here, honestly, is what SMBC once labeled the “Mount Stupid” phenomenon. If you know almost nothing about complexity theory, you can just accept that the P vs. NP question asks whether there’s a general way to avoid the brute-force enumeration of exponentially many possibilities when searching for short proofs of theorems—as Gödel put it in 1956, and as Cook put it again in 1971. If you know more about complexity theory, but still not enough, you can think of objections to that view (“who says searching for proofs is even an NP problem? what’s the exact problem statement, anyway—how is the upper bound on proof length encoded?” etc). If you know still more, then you immediately know how to answer those objections, thereby returning you to the original, “naïve” view of what P vs. NP was asking about.
For this reason, I think my suggestion to vzn, to read or reread a complexity textbook, is fine. There are plenty of questions that completely stump experts, or that are philosophical in nature, with the expert’s feeling or hunch barely better than the layperson’s. But, not just here but in previous discussions (e.g. about quantum computing), vzn has had a bad habit of raising as devastating objections to an entire field things that he doesn’t know are completely, totally, 100% addressed in the standard textbooks, and then continuing to treat those objections as profound and under-studied even after this is pointed out to him—refusing to accept “like seriously, RTFTB” as an answer.
Comment #52 July 25th, 2015 at 1:02 am
With respect to quantum …, vzn’s views are indeed questionable, but his TCS background is solid (in my opinion).
On a general note, I like the fact that you criticize “isolated demand for rigor”. How else could we distinguish between the facts that we know for sure, like that PA is consistent, that fact we could declare as dogmas like N != NP, and facts like that consistency of ZFC is a totally open question, which we will probably never be able to answer?
Comment #53 July 25th, 2015 at 2:04 am
The Fall 2015 Simons Institute/Berkeley program Fine-Grained Complexity and Algorithm Design (FGCAD, Aug 19 – Dec 18, 2015) shows that a marvelous program in cutting-edge complexity research can be advanced that doesn’t directly tackle the vexatious \(\mathsf{P}\overset{\scriptscriptstyle\mathsf{?}}{=}\mathsf{NP}\) question.
Rather, the focus of FGCAD’s four (star-studded) complexity theory workshops is less to solve \(\mathsf{P}\overset{\scriptscriptstyle\mathsf{?}}{=}\mathsf{NP}\) than to dissolve it — or dissolve at least some edge cases of it — in the “universal solvent” of fine-grained class-structure (as the FGCAD logo ingeniously depicts).
Safe prediction The proceedings of the FGCAD workshops will be read with avid enjoyment by fans (well, me at least) of practical “Knuthian” algorithms for attacking NP-complete (and harder) problems.
One hopes that the FGCAD organizers have extended a special invitation to Donald Knuth to attend at least some of the FGCAD workshops. To borrow Raoul’s phrase “we are all on-board with that.”
Comment #54 July 25th, 2015 at 6:31 am
Scott:
Do you think a ST lower bound on SAT assuming NP is in P/Poly is useful?
Comment #55 July 25th, 2015 at 6:41 am
a #54: What’s an “ST lower bound”? A space/time tradeoff?
In general, conditional results are useful, not always directly, but for helping to clarify the space of possibilities.
Comment #56 July 25th, 2015 at 2:50 pm
JS that univalent foundations stuff/ HoTT is very intriguing & thx much for the ref, shows some of the state-of-the-art research in the area.
lol G thx for the “support”. some useful/ applicable stuff/ refs. kinda. “damned by faint praise”
am not able to easily articulate my objections but basically think the concept of complexity of theorem proving is not a very well nailed down area “yet”. research continues. it seems to cross cut fields and sit in a sort of limbo area of research. ATP research tends to be very applied & not look at complexity. complexity theory tends to be more theoretical. P=?NP does maybe both effectively and ineffectively capture some of this crosscutting.
my big objection might be boiled down to “blowup”. there seem to be unexamined basic “blowups” in converting what we consider human-readable proofs into machine readable ones, before even the issue of verification is considered. and then there seem to be other “blowups” lurking in verification that make the idea of linear time verification a verging-on-naive simplification. but do believe these issues will be examined and addressed in years ahead based on current research trends.
re blowup also along lines quoted by G, here is a semifamous paper maybe relevant
Cosmological Lower Bound on the Circuit Complexity of a Small Problem in Logic Stockmeyer/ Meyer
would luv to engage in a further “free for all no holds barred” discussion on this topic but feel scott hits below the intellectual belt sometimes, think veers outside of collegial/ respectful boundaries, & have suffered consequences in the past for expressing too much free speech on this blog, & every comment here is moderated etc.; invite others to drop by stackexchange chat rooms for more freewheeling/ uninhibited chats.
Comment #57 July 26th, 2015 at 8:02 am
As a follow-up to my comment #45, I don’t know the relationship between BQP and NP but I’d love to see a highly nonconstructive proof that P=BQP… a breakthrough suggesting that the power of ZFC might be equivalent to the non-feasibility of quantum computing…
Regarding univalent foundations, they look like a nice way to build computerized versions of proofs first imagined within a set theoretical context. I doubt we’ll have soon mathematicians who think only in HoTT. Too restrictive…
Comment #58 July 26th, 2015 at 4:45 pm
Has anyone ever even formalized the statement of P=NP or other millenium questions in coq, hol light, or other proof assistants? Even with a miraculous SAT solver this would still need to be done and agreed upon by humans, and might be nontrivial since computer formalized proofs make rigorous delta epsilon proofs look like flaky hand waving. As far as I can tell there are formalizations of the correctness of Cook-Levin reduction and AKS primality test, but not of polynomial running time, which is apparently hard to formalize. If I’m overstating the difficulty then just paste the coq code for the the Poincaré conjecture in the comments.
Comment #59 July 26th, 2015 at 6:59 pm
The connection between NP=!P and between proving vs verification of mathematical theorem in real life mathematics is quite fascinating. Boaz Barak and I had discussed it on a previous blog post by Boaz (from this comment down). Certainly, we are talking about related phenomena but perhaps the following can help clarifying the connection in more precise terms.
Consider the following three statements:
1) In mathematics, as practiced in real-life, it is easier to verify a mathematical proof than to find a proof.
2) It is easier to verify that a certain collection of edges in a graph forms a perfect matching than to find a perfect matching.
3) It is easier to verify that a certain collection of edges in a graph forms a Hamiltonian cycle than to find a Hamiltonian cycle.
All these three statements are very plausible, and they all part of some general phenomenon. The question is if when we zoom in, is statement 1) closer to statement 2) or to statement 3)? In real-life mathematics, is the gap between finding a proof and verifying it closer to the gap between finding a matching and verifying a matching, or to the gap between finding a Hamiltonian cycle and verifying one?
(Of course, when it comes to general mathematical statements and not to real-life mathematical theorems, the gap between proving and verifying a proof manifests P =! NP. But the interesting issue is about real-life mathematical theorems.)
Comment #60 July 27th, 2015 at 12:36 am
Here is a natural question (which is not addressed in any CT textbooks familiar to me), that is so constructed as to blend two recent remarks of Donald Knuth and Gil Kalai:
Alice’s Claim There exists a Turing machine \(\mathsf{TM}\) that runs in PTIME (but not necessarily provably so) that infallibly separates mortal matrices from non-mortal matrices (but the separation is not necessarily provably infallible).
Which of the following responses by Bob is correct?
Bob’s response A Existing complexity theory theorems suffice to prove that Alice’s claim is false.
Bob’s response B Existing complexity theory conjectures (if true) suffice to prove that Alice’s claim is false.
Bob’s response C Complexity theory, as presently conceived, has nothing to say in regard to Alice’s claim.
Question Is separating PTIME \(\mathsf{TM}\)s from the set of all \(\mathsf{TM}\)s any easier than than separating mortal matrix-sets from the set of all matrix-sets?
Comment #61 July 27th, 2015 at 4:03 am
Scott #51: I’m not sure how pedantic I really want to be, or more precisely how pedantic I should strive to be.
You have omitted the used proof calculus here. Possible choices include natural deduction, sequent calculus, Hilbert systems, semantic tableaux methods, … You also were not explicit about the fact that only systems for first-order should be used. But I have to agree that if you had been explicit about those details, then described language would have been in NP.
My own feeling is that I should be at least a bit pedantic here. The shortest proofs using ZF with an appropriate formulation of a semantic tableaux method for 1st order logic will often be more than exponentially longer than the shortest proofs using the 2nd order variant of NGB together with an appropriate formulation of a sequent calculus for 2nd order logic.
Please note that formal systems behave different than machine models (like single-tape single-head Turing machines vs. multi-head multi-tape Turing machines), where the resource usage for one (reasonable) machine model is polynomially related to the resource usage of any other (reasonable) machine model.
Comment #62 July 27th, 2015 at 9:33 am
Following Scott’s excellent suggestion (in regard to past Shtetl Optimized comments), I’ve posted #60 as a TCS StackExchange question “The Mortal Matrix problem: how hard is deciding class membership?“
If the answers are illuminating — as I hope they will be — then two days from now I’ll award a bounty to the best answer, in grateful appreciation of the creative collegial effort that is required to write good answers.
Comment #63 July 27th, 2015 at 11:39 am
@Dewey 58: “Has anyone ever even formalized the statement of P=NP or other millenium questions in coq, hol light, or other proof assistants?”
Inspired by this question, I decided to write a formalization of the P vs. NP statement in Agda. It may be found here:
http://pastebin.com/nCE92XUd
The whole thing is only 173 lines, and includes basic definitions such as the definition of the natural numbers. However, I suspect the Millenium problems would be longer to define, as P vs. NP is the only problem whose statement does not involve the real numbers, and those can be finicky to define and manipulate.
Comment #64 July 27th, 2015 at 7:39 pm
Dewey #58: You might look at my cstheory.se question (click my name for the link). As far as I can tell, there is no commonly accepted formalization even of Turing machines in Coq.
Where did you find the formalizations of the validity of the Cook-Levin reduction and the AKS primality test? After a sort-of serious search a few years ago, I wasn’t even able to find a Coq-formalization of the halting problem. Maybe someone has built one recently though.
There are a few attempted formalizations of Turing machines in Coq on the internet; e.g., type ‘ “turing.v” coq ‘ into Google (without the single quotes, with the double quotes). I’m not sure if any of them are correct.
Comment #65 July 27th, 2015 at 7:43 pm
Well, I think we can avoid the use of the real numbers in the Riemann Hypothesis and the Birch and Swinnerton-Dyer conjectures as well. Some appropriate reformulation would be needed, but I think it should be doable.
The Riemann hypothesis for instance is (as shown by Jeff Lagarias) equivalent to the statement σ(n) ≤ H_n + e^(H_n) * log(H_n) for every n, where H_n is the n’th harmonic number. The exponential function and the logarithm are both transcendental concepts, of course, but I bet you could define the function ⌊ H_n + e^(H_n) * log(H_n) ⌋ in purely rational terms.
Meanwhile for BSD, at least if we stick to just the minimal form of BSD proper (like, not including the leading coefficient — maybe it’s possible to get that too, this is not my area), instead of phrasing it in terms of L-functions you can phrase it in terms of the asymptotics of the number of points on the curve mod p for every prime p. That shouldn’t be a problem using only rational numbers — well, OK, the log part might be a problem, but A. good chance that’s doable anyway and B. even if not, it should definitely don’t worry about the coefficient, as then any log would work, and you could just use floor of log base 2 instead of anything with the natural log, and that you could definitely do without invoking real numbers.
Comment #66 July 28th, 2015 at 12:02 am
Scott, blog post request:
Can you do a post about what’s been happening with Boson Sampling. What’s the latest news from the front there?
Any success in scaling to larger setups?
Comment #67 July 28th, 2015 at 1:32 am
Now that I remember it, there’s more on this theme over on this MathOverflow question[0]. The question — at least as interpreted by most people — is about where on the arithmetic hierarchy each of the Millenium Prize problems is (after suitable refomulation, of course). But of course if such a problem is anywhere on the arithmetical hierarchy, I assume that means it can be expressed in Agda!
Poincare conjecture is now known to be true, so in that sense it’s trivially Δ_0. (I’m going to omit the superscript 0s as implicit; I did say it’s the arithmetical hierarchy I’m talking about.) Alex Gavrilov points out that before that, it was known to be Π_1 due to Rubinstein’s algorithm.
Riemann Hypothesis is Π_1. P vs NP is Π_2.
BSD, says Gavrilov, is not known to be Π_1, but it certainly looks like I’m right that you can express it without reference to real numbers.
Terry Tao says that the torus version of Navier-Stokes is Π_2, but doesn’t say anything about the R^3 version. (Note that you can get the prize by solving either the torus or the R^3 version.)
So that leaves Hodge and Yang-Mills as possibly not expressible, and possibly the R^3 version of Navier-Stokes, if you want to count that. Hodge and Yang-Mills like I said I know nothing about. But I would expect that if torus Navier-Stokes is OK then so is the R^3 version!
[0]It’s not really relevant here, but to lessen confusion, I should perhaps mention that Harry Altman is me.
Comment #68 July 28th, 2015 at 10:04 am
Rahul #66: I actually don’t understand the majority of papers with “BosonSampling” in the title or abstract these days—I haven’t, since the physicists took over the subject. But yes, the next time there’s some dramatic advance that I do understand, I’ll be sure to blog about it.
On the experimental side, I know that Paul Kwiat and other optics people have been thinking hard about how to scale up to ~10 photons. Meanwhile, the ion trap and cold atom people have also been thinking about how to scale up using a completely different setup. To date, though, the record for BosonSampling remains 4 photons (from the Oxford group).
On the theoretical side, maybe the most important problem right now is to get a clear understanding of what happens to the computational complexity when a large fraction of photons are lost. I’ve been talking with Daniel Brod and others about this, and we hope to have a paper about it before too long.
I’m actually in Santiago, Chile right now, for the International Congress on Mathematical Physics, where I’m giving an invited talk tomorrow afternoon entitled simply “BosonSampling.” Because of the audience, the majority of the talk will be basic stuff, as well as mathematically-interesting questions about the permanent not directly related to experiments. But I’ll certainly spend some time on the lost-photons issue.
Comment #69 July 28th, 2015 at 11:07 am
Sniffnoy, the Yang-Mills problem is not formal. Part of the problem is simply to state the question precisely.
Comment #70 July 28th, 2015 at 1:13 pm
Lol … to show that a planet with seven billion people on it can none-the-less compose “a small world,” I should perhaps mention that the author of that particular MathOverflow question (“For which Millennium Problems does undecidable -> true?”) was me.
It is a mystery why similar questions and answers (as asked/answered by me anyway) commonly receive contrasting up-ratings on MathOverflow and down-ratings on TCS StackExchange (and vice-versa).
One illuminating reference in this regard is Joseph Landsberg’s essay “Clash of Cultures”, which appears as Section 0.3 in Landsberg’s Tensors: Geometry and Applications (2012)
Another gracefully illuminating reference is Donald Knuth’s YouTube video “Wrong Turn on the Dragon” (2014), in which Knuth admiringly quotes Piet Hein’s grook:
Conclusion We all take “wrong turns on the dragon.”
PS The nature and magnitude of photon-loss dynamics strongly affects the practical computational complexity, not only of BosonSampling simulation, but of simulating many other quantum dynamical processes too. That is why occasional Shtetl Optimized updates/discussions of work in this area would be welcomed by many (including me).
Comment #71 July 28th, 2015 at 2:00 pm
Sniffnoy, the Yang-Mills problem is not formal. Part of the problem is simply to state the question precisely.
Yikes, really? Well, we can certainly strike that one then!
Comment #72 July 28th, 2015 at 5:06 pm
In #40 on Rowe-Younes I meant to say Strilanc’s points were at the bottom of the Hacker News thread. Now I notice David Bacon also weighed in there: https://news.ycombinator.com/item?id=9929917. It seems to be another ramification of the same way of fudging between c_0,…,c_{m-1} and the last register in Fig. 3.
Comment #73 July 29th, 2015 at 12:35 am
Do you think the truth of P=NP is encoded in a solution to a diophantine equation which is solvable but hard to solve and once solved everything becomes easy (that is P=NP is possible)?
Comment #74 July 29th, 2015 at 1:43 am
Also why are false proofs of P=NP easily checkable. That is why are no instances of “Is this a proof of P=NP?” easily checkable? Does it imply proof of this question is in coNP system. Note that typically mathematical proof systems are in NP.
Comment #75 July 29th, 2015 at 9:22 am
a #73, #74: I don’t really understand your questions, but:
No, I don’t think that P=NP. But if that were the case, then one could certainly encode the algorithm for SAT as the solution of a Diophantine equation, so in that case, what you want would trivially be possible. 🙂
In principle, all proofs are easily checkable, once the proofs are written out in a suitable formal system. In practice, false proofs of both P=NP and P≠NP tend to be pretty easy to reject, because the same basic errors recur over and over—these proofs are never as original as their authors think.
Comment #76 July 29th, 2015 at 1:12 pm
a few other thoughts on feasibility of automated theorem proving vs moores law/ supercomputers etc occurred to me.
fluid dynamics and molecular simulations were two areas where decades ago, almost nothing was feasible on computers. supercomputers have nearly revolutionized both areas & now very large, sophisticated simulations are quite feasible and run routinely. this is due to both software and hardware advances (esp parallelization which crosscuts both). also though, the complexity of these “algorithms” is apparently not so well studied (so are they even P-time or Exptime? not sure exactly. maybe a case can be made that despite all their complexity they are still in P-time).
theorem proving does not seem to fit this pattern at all. definitely there has been a rise of a lot of software for ATP and increasing use of it, but it seems like supercomputers have not made any “dent” in this overall field. there seem to be no large supercomputer ATP projects anywhere! is it because it hasnt been tried, or it isnt really possible? seems, this is not as expected if ATP really is at heart a “low-to-moderate-complexity” “NP” type problem (again, NP problems are whats known as “embarrassingly parallel” meaning that parallel implementations are easy to create).
so it seems there is some kind of gap, something missing, some kind of disconnect. somehow ATP seems to be harder than the theory acknowledges. there does not seem to be an “increasing encroaching” of ATP technology into theorem proving. despite imagination apparently theorem searching/ proving is not exactly an “applied problem” in the way that other applied physics problems are like fluid dynamics or molecular simulations etc….
also, afaict, there are many NP-complete type problems (other than ATP!) run on supercomputers, but not sure of a list. does anyone know of the complexity classification of supercomputer type problems? are they mostly P? are some NP? cannot even think of a reference that would address this basic question. (maybe will ask it myself on stackexchange sometime.)
Comment #77 July 29th, 2015 at 2:17 pm
Scott #68:
Thanks for the update!
And for a change, you ought to actually do a post on stuff you *don’t* understand! 🙂
So, we’d not complain about a Scott post on the Experimental parts of Boson Sampling. After all, the BS theory has been racing ahead of the experiments for a while. So the “bottleneck” or rate determining step or whatever you’d call it resides in the experiments so far as I can tell. Hence the interest in knowing what’s happening in those parts.
Comment #78 July 29th, 2015 at 5:10 pm
vzn #76: Once again, I find it bizarre to regard it as a “gap” in complexity theory that automated theorem proving is hard, because complexity theory predicts that ATP should be hard in general! Indeed, it predicts that ATP, being NP-complete, should be “harder” in some sense than either fluid dynamics (which is in P for any reasonable formalization), or molecular simulation (which is in BQP, so almost certainly not NP-hard). All this is consistent with what’s observed.
So at some point it’s like, when will you take a successful theoretical prediction for an answer? And what could complexity theory possibly have said about this, that you wouldn’t regard as a failure?
Comment #79 July 29th, 2015 at 6:14 pm
By the nature of their disciplines, scientists greatly prize experiments that affirm (or disprove) theoretical predictions, and similarly for engineers in respect to feasible technologies, chemists in respect to feasible molecular reactions, physicians in respect to feasible medical treatments (etc.)
For the sake of argument, let’s suppose that all of the standard postulates of complexity theory are true, including the separation of P from NP, the integrity of the polynomial hierarchy … all the postulates set forth so ably in Arora and Barak’s Computational Complexity: A Modern Approach () for example.
Then we can classify hopes for complexity theory as associated alternatively to global complexity theory (of Arora and Barak) versus fine-grained complexity theory (of this fall’s Simons Institute Program, as cited in #7).
Hopes for global complexity theory
• Public key cryptography provably outside of P
• Scalable quantum computers in the laboratory
• Scalable (non-simulable) BosonSampline
Hopes for fine-grained complexity theory
• Sustained “more-than-Moore” progress
in SAT-solving capability (per #7)
• […] in proof-checking capability
• […] in materials science capability
• […] in biomedical imaging capability
• […] in thermodynamic simulation capability
• […] in fluid dynamical simulation capability
Reason for celebration Without any disparagement intended to the hopes that are traditionally associated to global complexity theory, it is entirely reasonable — for young researchers especially — to celebrate too the amazing progress of fine-grained complexity theory in recent decades (amazing to many, including Donald Knuth)
Reason for inspiration And it is reasonable too, to wonder whether at least some of the postulates that are traditionally associated to global complexity theory in general (and to quantum computing theory in particular) might be amended so as to similarly accelerate progress in the global domain.
Conclusion The following “grook” is inspired by the works of Donald Knuth, Piet Hein, and Gil Kalai:
The complexity-theoretic insight that this grook attempts to capture, which first was formally proved in the context of fundamental research in global complexity theory, is proving to be fundamental to sustained “more-than-Moore” progress in fine-grained complexity theory.
And so the aspirations of each branch — global versus fine-grained — are inspired and nourished by the advances of the other branch. To borrow a phrase from Moby Dick: “On that we can all splice hands!”
Comment #80 July 29th, 2015 at 7:37 pm
vzn #76: Synopsys (an electronic design automation vendor) acquired Coverity (a static code analysis vendor) in 2014. As far as I know, Coverity takes full advantage of current hardware. Instead of trying to prove the source code correct, it tries to find suspicious code which might be incorrect. So it is a sort of automatic theorem disprover, with the caveat the it just identifies potential errors, and only can identify certain types of errors. Similar to fluid dynamics and molecular simulations, this stuff is commercially important. Semiconductor companies also use ATP technology for proving specific source code correct, but I have less direct experience with this. So in the areas where it made commercial sense, your large supercomputer ATP projects have happened indeed.
Comment #81 July 29th, 2015 at 7:48 pm
Scott #78: You say that automatic theorem proving is NP-complete. Does this mean that the automatic theorem disproving of the sort Coverity tries to do is coNP-complete? But shouldn’t disproving be easier than proving? If I want to disprove Fermat’s last theorem, then I just need 4 natural numbers x,y,z and n such that x^n+y^n = z^n. But for proving it, I need a formal system, axioms, and quite a bit more technology which might even be inconsistent. On the other hand, disproving Fermat’s last theorem should be equivalent to proving the negation of Fermat’s last theorem.
So the important distinction cannot be between proving or disproving. It’s rather the “forall” quantor in Fermat’s last theorem which makes disproving seemingly easier than proving. But this indicates to me that ATP for formulas with arbitrary nesting of quantors might be rather PSPACE complete instead of NP complete.
Comment #82 July 29th, 2015 at 8:19 pm
Scott #68,
Is there somewhere you or someone else has made a list of open problems related to the permanent and that emphasizes which ones are relevant to further understanding of BS?
Comment #83 July 29th, 2015 at 9:29 pm
gentzen #81: No, I wasn’t talking about searching for direct counterexamples (which, in any case, is only relevant for Π1-sentences). I was only talking about searching for proofs or disproofs in some formal axiomatic theory like ZF (though of course, such a proof might involve constructing a counterexample). As I said in comment 51, the relevant problem that’s in NP is to decide whether a statement S has (say) a ZF proof at most n symbols long, given S and 0n as input.
And yes, this is an NP problem. The form of S—e.g., whether it has one universal quantifier, one existential quantifier, or some other number of quantifiers—is irrelevant to that. The problem is also easily seen to be NP-complete, for example by reducing 3SAT to it. (Well, technically, the problem is NP-complete assuming ZF is consistent. If ZF is inconsistent, then the problem is in P, since for sufficiently large n, every statement then has a proof of length n (!!).) The corresponding coNP problem is to decide whether S has no proof at most n symbols long.
Comment #84 July 29th, 2015 at 9:57 pm
Joshua #82:
Is there somewhere you or someone else has made a list of open problems related to the permanent and that emphasizes which ones are relevant to further understanding of BS?
That’s an extremely fair request. No, I don’t know of any such list: while I’ve listed a bunch of such problems, they’re scattered across multiple papers about BS. Just for you, though, I’ll now make a list of what I consider to be the 5 most important BS-related open problems about the permanent. (Of course, any partial progress in the direction of these problems would also be of interest.)
(1) The Permanent-of-Gaussians Conjecture. Is there a fast algorithm to approximate |Per(X)|2, where X is an n-by-n matrix of N(0,1) complex Gaussians? Say, one that runs in time poly(n,1/ε,1/δ), where ε is the desired multiplicative error in the approximation, and 1-δ is the fraction of X’s for which that error should be achieved? Is this problem at least in BPPNP (i.e., can it be reduced to a nonnegative sum)? Or is it #P-complete?
This question has obvious, central importance to the entire BosonSampling program.
(2) The Permanent Anti-Concentration Conjecture. Can we show that, if X is an n-by-n matrix of i.i.d. N(0,1) Gaussians, then as n gets large, |Per(X)|2 converges to a lognormal random variable? (See our paper for a more quantitative statement of what we need.)
Based on numerical evidence, we’re confident that this question has a positive answer, but proving it might be a prerequisite to answering question (1). It also fits in naturally with the program started by Tao and Vu, to understand the anti-concentration of random permanents. (Unfortunately, while Tao and Vu’s results are the strongest known, they’re not nearly strong enough for us.)
(3) The Permuted Diagonal Conjecture. Is it the case that, if X is an n-by-n matrix with norm at most 1, and |Per(X)|≥1/nO(1), then X is “close” to a permuted diagonal matrix (say, it has a diagonal whose product is ≥1/nO(1) in absolute value)?
If this conjecture holds, then there’s no hope of “smuggling” a submatrix with a huge permanent into a BosonSampling unitary, in such a way that a linear-optical experiment can efficiently find that submatrix but a classical computer can’t. But if the conjecture fails, then there might still be hope for that. See my paper with Nguyen for details and related results.
(4) Approximating Permanents of Hermitian psds. Let X be an n-by-n Hermitian psd matrix. Is there a polynomial-time randomized algorithm to approximate Per(X)? (One can show that Per(X) is nonnegative, and indeed that it can be written as a nonnegative integral, whence it can be approximated in BPPNP, so presumably the problem isn’t #P-complete.)
If such an algorithm exists, it would imply that BS output probabilities given thermal initial states could be approximated in classical polynomial time. Though honestly, I think the non-BS importance of such a result would exceed its BS importance. I regard it as entirely plausible that such an algorithm exists.
(5) Sums of Squares of Permanents. Given an n-by-(n+k) matrix A of i.i.d. N(0,1) complex Gaussians, let Φ(A) equal the sum of |Per(X)|2, over all n-by-n submatrices X of A. How large does k have to be compared to n, before Φ(A) becomes approximable in classical polynomial time (or at least in BPPNP), with high probability over A?
The answer to this question basically determines how many photons can be randomly lost in a BosonSampling experiment, before sampling the resulting distribution becomes easy for a classical computer. Daniel Brod and I have been thinking about it and have some partial results, though still very far from what we want.
Let me mention one last trio of questions, which I don’t think have any direct relevance to BosonSampling, but which still would be nice to answer, and which amazingly might not have been.
(1) Is computing Per(X), for X unitary, a #P-complete problem?
(2) What about if X is Hermitian psd?
(3) Can Gurvits’s randomized algorithm, for approximating the permanent of a bounded-norm matrix, be derandomized? (See my paper with Hance for details and partial results.)
Comment #85 July 30th, 2015 at 10:46 am
Scott, thanks. That seems like a nice list.
Comment #86 July 30th, 2015 at 12:00 pm
Sorry, this may come across as either bewildering out of the blue, or totally trivial, I’m not sure which.
I just realized there is an incredibly deep connection between the theory of Turing Machines and the theory of Stochastic Processes. Specifically a Turing Machine is process adapted to the filtration of the sequence of realized states in the computation. More exactly: let Z be the integers, representing the current position of the tape, S be the possible internal states, and W be the allowed symbols, then the observable measure space is E=Z*S*W. Our filtration on E is indexed by the time step of the computation t, so that F_t is the sigma algebra on all sequences of length t of elements of E. A Turing Machine is then a Markov Process adapted to F_T, giving the probability of the next state E_{n+1} given the current state E_n as P[E_n+1| E_n].
The incredible thing is that statements about P vs NP, and the halting problem then become statements about stopping time random variables, which gives us access to the powerful machinery of generators, resolvents, Hille-Yosida theorem, Feller-Dynkin theorem, and conservation theorems like Feynmann-Kac, Chapman-Kolomogorov. In a way it allows us to define the logarithm of the transition function of the Turing Machine.
Actually now that I think about it we could just let E=Z^3, and then let the probability measure P take care of restricting the symbols and the internal states.
…or I’m completely out to lunch and have been spending too much time reading probability theory.
Comment #87 July 30th, 2015 at 12:40 pm
…sorry I slipped the wording Markov Process in there, when really its more general, because the transition function looks back to the last symbol written to the current tape position. Nevertheless this is still a process adapted to the filtration.
Comment #88 July 30th, 2015 at 1:31 pm
Scott #84:
With all due respect to your list I think the single most important BS issue that intrigues me is why are people having so much trouble scaling beyond the 4 photon case. I do realize Jushua intended theoretical problems but still I find this part so relevant yet so under-blogged about.
I’m sure the experimentalists are very smart people and that makes the situation even more intriguing.
I wish there was a Scott analog for the experimental side of things who could have educated us on what’s actually going on out there on the experimental front.
Maybe I am just naive but then I’d love some insights into what’s hampering the attempts to even get to 10 photons. Because from what I remember even at 20 photons or so you are already at the limit where you’d be sampling faster than you could calculate and that’d be one fantastic result.
Comment #89 July 30th, 2015 at 2:25 pm
…actually this can be reduced to a Markov Process on E=Z*Q*Z, where the first set of integers represents the tape positions, the second set of rationals is the current state of the whole tape (lexicographic encoding in the power of the tape position), and the last set of integers is the internal state of the machine. The transition rules then place bounds are the largest steps that can occur, namely that the first integer can change in increments of 1 (drunken sailors walk), the second rational can change only as much as the power of the first integer, and the last integer is bounded.
So the question is, given that Q is dense in R, what is the generator of this process (logarithm of the transition function) and resolvent this process (Laplace transform of the transition function)?
Comment #90 July 30th, 2015 at 2:36 pm
…and how about this, we can densify the time step t of computation by making it an exponential random variable. Essentially we can make the process fully Lévy by introducing uncertainty as to when the next computation will take place. Then we can apply the Lévy–Khintchine theorem of the Fourier transform of the process to reason about the harmonics of the Turing machine.
Maybe this is old hat to everyone else, but this sure seems really cool.
Comment #91 July 30th, 2015 at 2:58 pm
@Scott #78:
fluid dynamics (which is in P for any reasonable formalization)
I almost want to do a King of the Hill: “You’re not proving fluid dynamics easier, you’re proving P harder!”
Comment #92 July 30th, 2015 at 4:53 pm
Rahul #88: I listed mathematical questions about the permanent because that’s what Joshua asked for. (Though note that my question 5, about photon losses, is directly related to scalability.)
The central reason why scaling is hard is actually extremely simple, and was understood from the very beginning. It’s that sufficiently reliable single-photon sources don’t yet exist. If your sources are unreliable, then the probability of an n-photon coincidence falls off exponentially with n. And that’s exactly what happens in the existing experiments, putting a hard cap on how large n can be if you want to finish taking data this century and within a reasonable budget.
In principle, this problem ought to be addressable through the development of optical multiplexing, or other technologies that could yield much better single-photon sources — in combination with scattershot, and theoretical results about how many losses you can tolerate and still be sampling from an asymptotically hard distribution. And it’s reasonable to hope for further progress in all these directions within the next decade, and to be disappointed if it doesn’t happen (in which case, of course, one will want to understand why). But these things don’t happen at blog speed, and I don’t think there’s any great mystery about why not.
Comment #93 July 30th, 2015 at 9:31 pm
BS = Boson Sampling (not bullshit) – can posters try to use only well-established acronyms so novices like me can follow the discussion – in direct response to a post which expands the acronym this is not necessary, but flooding the comments section with acronyms which aren’t defined earlier is not good.
(Sniffnoy #65 earlier uses BSD for Birch-Swinnerton-Dyer for example, so later uses of the acronym BS may be confusing for some folks)
Comment #94 July 31st, 2015 at 12:37 am
Scott #92:
Is this inability to scale in Boson Sampling Experiments different qualitatively from the de-coherence on scaling up that has been plaguing the more conventional Quantum Computing experiments?
i.e. Should this problem be easier to surmount than that one? Is one a “mere” practical issue and the other a fundamental barrier?
My reading of the original BS papers was that BS offered a neat way to obviate the de-coherence-on-scaling issues affecting all conventional QC attempts and yet get to a point where a problem was big enough that it could be Boson sampled faster than it could be computed in any other conventional way.
That’s a target that any conventional QC is not even close. i.e. to solve something much faster than could be via a conventional computer.
Comment #95 July 31st, 2015 at 12:41 am
In the context of Boson Sampling how reliable is a sufficiently reliable single photon source?
Is there a metric to quantify the reliability of a photon source. In order to access, say, a n=25 Boson Sampling Experiment how reliable a single photon source do we think we need?
And in terms of the improvement in reliability of single photon sources what has been the trajectory of improvement in the past decade.
Is there a mathematical way to quantitate the past, present and required reliability of single photon sources?
My goal is to get an idea of whether this is an Engineering / Technology problem that just needs some time to go away or are we looking at a massive technological miracle to get there.
Comment #96 July 31st, 2015 at 9:24 am
Rahul,
Gil Kalai would probably say that they are related, but I don’t want to put words in his mouth. So instead let’s talk about GK, which is Josh’s mental model of Gil. GK says that they are both barriers created by the same fundamental principles that keep the polynomial time version of the Church-Turing thesis practically true for our universe. GK would have similar remarks about question 5 and how it relates to how many photons we can practically avoid losing, which would essentially amount to saying that whatever the fraction that it is computationally hard if we lose less than that, is not going to be practically doable in an experiment.
Comment #97 July 31st, 2015 at 9:39 am
Sniffnoy #65,
Yes, we can define ⌊ H_n + e^(H_n) * log(H_n) ⌋ in purely rational terms. It isn’t that hard to work out how far one needs to go in the Taylor series approximations for both e^x and the log such that the resulting quantity is close enough to H_n + e^(H_n) * log(H_n) . I haven’t worked out the details, but the only issue seems to be that log x doesn’t have a Taylor series that converges for big x, but that can be handled by using the Taylor series for log (x /(x-1)) which does converge for all x>1.
(For James, RH= Riemann Hypothesis, PNT= Prime Number Theorem)
However, this does bring up another issues: actually showing that these statements are equivalent to what we care about seems to be non-trivial since they require going through the zeta function and its analytic continuation. Therefore, I wonder is there any way to say prove that Lagarias’s version of RH is equivalent to the statement of RH involving the error in the PNT by purely rational means? The Chebyshev functions are rationally definable using the same log x/(x-1) trick but beyond that I’m not sure. Lagarias’s proof seems morally to involve the idea that if RH is false then one should get unusually dense bunches of primes together along with long stretches with unusually few primes. That might be something one can express purely in terms of the error term in the various forms of PNT?
Comment #98 July 31st, 2015 at 12:51 pm
Joshua #96:
Agree with you. And knowing whether your hypothetical “GK” is right or not about the fundamental BS-scaling constraints would be very interesting.
So far as I can tell, the real Gil Kalai has made the point (speculation?) often about conventional QC but I’m not sure he has commented about BS-scaling. In any case, it’d be interesting to hear his thoughts. Gil are you reading this? 🙂
At the same time, the empirical data from the experiments would also be very interesting to see. I haven’t seen quantitative metrics about the photon losses reported much.
Also questions like: How fast are photon sources improving? Is the curve of the improvement in the lossiness of photon sources still moving fast or saturating to some asymptotic loss limit?
Are the practically observed loss in the BS runs commensurate with what we’d expect from measurements with single, independent sources?
Comment #99 July 31st, 2015 at 6:11 pm
Consider the proposition that Black has a force win in chess. This is almost certainly false. Also it is checkable by a simple finite procedure, whose only problem is that it’s too lengthy for today’s computers.
Would a linear time SAT solver help with this?
Comment #100 July 31st, 2015 at 7:22 pm
asdf #99: No, for games like chess (assuming a polynomial upper bound on the game length) you’d want P=PSPACE, and a linear-time quantified SAT (QBF) algorithm. Note that, if the game can last for exponential time, and the starting configuration can be arbitrary, then chess is known to be EXP-complete, and hence not in P.
Comment #101 August 1st, 2015 at 6:59 am
vzn #76:
Re ATPs not running on supercomputers, note that some special-purpose provers are run on large computer clusters, for example GIMPS which consistently finds new largest-known prime numbers.
Also, the flyspeck project used an Amazon computer cluster for the formalization and verification of the proof for a pure math problem (Kepler’s sphere packing conjecture). A large part of a proof verifier is an ATP which connects one lemma to the others.
Comment #102 August 1st, 2015 at 8:40 am
I have the feeling that, whenever a problem is hard, it’s not possible to tell which complexity measure makes it hard. Thus you can’t separate P from PSPACE, from BQP, from NP, and so on. There must be a physical notion of hardness which says hard problems remain hard regardless of the complexity measure you consider.
Of course my feeling originates from the problem of factoring integers. I’m almost sure that, if quantum computers were to be proved scalable someday, they would stimulate the finding of classical, feasible polynomial algorithms for many problems currently known to lie in BQP. For now, I incline to believe that factoring might be in P but only in a galactic (and/or) nonconstructive way.
Comment #103 August 1st, 2015 at 10:22 am
What could happen if there is a O(n) algorithm for SAT (take a reasonable 1000000n)? Is it really the end of humanity?
Comment #104 August 1st, 2015 at 8:45 pm
a #103: It would be the end of non-SAT-solving humanity.
Comment #105 August 1st, 2015 at 9:41 pm
@Scott Thank you. I cannot tell your comment is sarcastic or serious. What is ‘non-SAT-solving humanity’? Note that this question of mine was not intended as a joke. But with Elon Musk, Stephen Hawking, Bill Gates, Steve Wozniak talking about end of humanity from AI, may be this question is at least worth $\$3$ Billion + a brilliant mind.
Comment #106 August 2nd, 2015 at 9:36 am
Scott’s comment #92 is (as it seems to me) clearly stated, scrupulously respectful, and inarguably correct:
Reason for hope It is natural to consider whether the case for Gil Kalai’s skeptical postulates can be made with comparable clarity, good humor, and inarguable correctness.
To begin, Scott’s assertion has the same inarguable logical form as
Thermodynamical struggles Here the point is that, at present, we simply don’t know whether fundamental thermodynamic principles obstruct scalable BosonSampling experiments. History shows us that a good way to identify thermodynamic obstructions is to struggle to design, simulate, and build practical devices … the good news is, BosonSamplers certainly are doing that.
Entropy costs So let’s consider the entropy cost of simulating BosonSampling processes by strictly classical means. A quick experiment shows that my laptop’s Mathematica program computes (by Glynn’s algorithm) a \(20\times 20\) complex permanent in about \(90\,\mathsf{\text{ms}}\). The entropy cost of this calculation is about \(6\,\mathsf{\text{mJ/K}}\), and it follows that one dollar’s worth of electricity (at present Seattle utility rates) would suffice to compute the permanent of a \(42\times 42\) complex matrix.
We see that classical permanent calculations presently range far ahead of any BosonSampling technology whose design we can presently specify.
Hopeful futures What about the future? It’s perfectly consistent to imagine a future that strikingly affirms both Aaronson-style optimism and Kalai-style skepticism:
• Feasible BosonSampling experiments do scale to arbitrarily large photon-numbers … perhaps at exponential entropy-cost.
• Classical BosonSampling simulations do scale to arbitrarily large photon-numbers, … also perhaps at exponential entropy-cost.
This leads naturally to
Conclusion Young quantum researchers would benefit greatly from a 21st century in which classical-vs-quantum / simulated-vs-experimental BosonSampling communities both make sustained progress toward ever-larger photon-numbers, while both exhibit same-order entropy costs.
In this hopeful world, the Permanent Entropy challenge remains open to the end of the 21st century and beyond.
Comment #107 August 2nd, 2015 at 12:36 pm
a, there’s a book that imagines what would happen if P=NP: http://www.amazon.com/The-Golden-Ticket-Search-Impossible/dp/0691156492
Comment #108 August 2nd, 2015 at 12:53 pm
John Sidles #37, #79: Those are open-minded thoughts, respectful summaries, worthy appreciations and interesting references. But your contributions partly illustrate my point
You don’t behave slightly off, and as a consequence you get nearly no feedback (or at least not as much feedback as some more extrovert characters). I don’t want to imply that you are a passionate amateur scientist, I know that you are a professional medical researcher and quantum systems engineer. I watched a video of a talk you gave at the Freiburg Institute for Advanced Studies.
Gil Kalai #59: That discussion with Boaz Barak raises good points. I especially appreciated the following
Comment #109 August 2nd, 2015 at 6:22 pm
Scott’s list #84 is truly exciting and I spent some time thinking about those and related problems. Except (4) which I dont understand that well. I would be happy to learn about a precise reference to (4) and also Q: what “BS output probabilities given thermal initial states” means.
Regarding #96/#98 I wrote with Guy Kindler a paper about noisy BosonSampling which can be found on the arxive (and there is a HUJI CS colloquium videotaped lecture about it on you tube called BosonSampling and noise sensitivity or something like that.) The Hermite-Fourier expansion we use may be relevant to the problems in the list in #84. On the question “how many photons can be randomly lost in a BosonSampling experiment, before sampling the resulting distribution becomes easy for a classical computer.” I think Scott and I have the same guess (o(n)) but (I suppose) a completely opposing interpretation of such a result. I think that in spite of such a result, losing only (say) n^{0.9} will not allow demonstrating anything that classical computers cannot demonstrate. (This is related to Dorit Aharonov’s question at the end of my videotaped BosonSampling lecture). This is a sufficiently narrow issue that it is not impossible that one of us will convince the other.
There are few interesting (utterly non-quantum) questions that are motivated by the discussion above. For example: does supreme computational power for problems on small input size (say n/2) give you real advantage for solving problems (that can be “just” NP-complete, or even in P) on a larger input size (n)?
Comment #110 August 3rd, 2015 at 7:28 am
@Vadim I am aware of the book. I am curious what Scott thinks since he is a non-believer and I am curious if he ever spent time thinking of what if the believers are absolutely right in a very strong manner?
Comment #111 August 3rd, 2015 at 7:31 am
particularly if he sees it as end of humanity like I see it? It is sometimes good to know if we think same way as experts:)
Comment #112 August 3rd, 2015 at 8:09 am
Regarding the last paragraph of my previous comment. Let me ask it in more details (but still not in fully formal way.)
The question is: to what extent, computational ability for hard tasks really helps you in solving easy tasks.
Question 1:
Consider a circuit for solving SAT for a formula with n variables. (Or for finding Hamiltonian cycle for a graph with $n$ edges.)
Suppose that every gate allows the computation of an arbitrary Boolean function on $m$ variables. For concreteness let’s take $m=0.6 n$.
The Strong exponential time hypothesis (SETH) asserts that even with such strong gates we need superpolynomial circuit size. In fact, we need size at least $\Omega (2^{0.4-\epsilon n})$ for every $\epsilon.$ In a sense, gates on fraction of the variables that represent very complicated Boolean functions (much beyond NP-completeness) do not give you much advantage.
We can further ask:
(i) Can we have such a circuit of size $2^{0.9 n}$? $2^{(1-\epsilon)n}$?
A “no” answer will be a vast strengthening of the SETH . Of course, maybe there is an easy “Yes” answer.
(ii) If the answer to (i) is YES. do gates that computes arbitrary Boolean functions give some advantages compared to gates which “just” compute SAT (or arbitrary NP functions.)?
Quetion 2:
As before let $m< n$ and for concreteness put $m=0.6n$. (Other values of $m$ such as $m=n^\alpha$ are also of interest.) Consider the following types of circuits:
a) In one step you can compute an arbitrary Boolean function on $m$ variables.
b) In one step you can solve a SAT problems with $m$ variables. Or perhaps an arbitrary nondeterministic circuit of polynomial size in $m$.
c) In one step you can perform an arbitrary circuit on $m$ variables of size $m^d$.
d) In one step you can perform ordinary Boolean gates.
Let us consider the question of finding a perfect matching for a graph with $n$ edges. Matching has a polynomial size circuit. The question is if the exponent in such a matching algorithm can be improved when you move from circuits of type d) to circuits of type c), and from circuits of size c) to circuits of size b), and from circuits of size b) to circuits of size a).
(This may be related to well-trodden issues about parallel computation and about oracles.)
Comment #113 August 3rd, 2015 at 9:49 am
John Sidles #106:
Is this really true? I thought at a fairly low n, like 25 or 30, Boson Sampling would be able to access results that would take any classical computer much longer to compute.
Comment #114 August 3rd, 2015 at 12:09 pm
AS #89. the ideas are hard to follow but the idea of a connection between (analysis of) TMs computational tableaus and random walks seems very deep & have been pursing that analogy for some year esp wrt number theoretic problems eg Collatz, & think it also strongly applies to the Riemann hypothesis, think there might be some general principle at play, which maybe might be exploitable wrt auto thm proving somehow, but (not surprisingly) extremely difficult to attack/ analyze. it also shows up in the erdos discrepancy problem. intending to write up/ flesh out some more ideas/ collected links on it sometime.
Comment #115 August 3rd, 2015 at 8:36 pm
Scott #83:
One way to interpret this is as some form of Skolemization. Because I believe in some form of the “law of conservation of difficulty”, I doubt that this can really turn a PSPACE problem into an NP problem. Otherwise, games like chess or go would also be NP problems, just formulate them as “there is a proof shorter than n in this specific formal system that white (black) has a winning (non-losing) strategy for the given position”.
The question which interests me is the practical complexity of automated theorem proving in the real world where P!=NP. For me, the practical complexity also includes the possibility to give relevant and useful partial and approximative answers. Knowing that no sufficiently small (or simple) counterexample exists (like we know for RH and knew for FLT even before it was proved) can be such useful information.
regarding gentzen #46:
When I wrote that objection, I didn’t notice that you had cited Gödel’s 1956 letter to von Neumann before. Note that in the German original, Gödel doesn’t mention ZF set theory, but talks of “engeren Funktionenkalkül”, which means a Hilbert style system for first order predicate logic. The original letter also contains the relativizing footnote “abgesehen von der Aufstellung der Axiome”, which means “apart from the postulation of axioms”. But to be honest, I only noticed when I checked the German original, so those details are probably not too important.
I looked up some further references regarding the length of proofs for different formal systems. The oldest is probably
“Kurt Gödel. Über die Länge von Beweisen. (1936)”
but it is not really detailed enough. More useful are
Samuel R. Buss. “On Gödel’s theorems on lengths of proofs I: Number of lines and speedups for arithmetic.” Journal of Symbolic Logic 39 (1994) 737-756.
Samuel R. Buss. “On Gödel’s theorems on lengths of proofs II: Lower bounds for recognizing k symbol provability” In Feasible Mathematics II, P. Clote and J. Remmel (eds), Birkhauser, 1995, pp. 57-90.
Comment #116 August 4th, 2015 at 8:36 am
It only took 2000 years to figure out straight edge compass construction of some previously difficult objects and just about 400 years to prove Fermat’s Last Theorem. It seems entirely within possibility that a 1000 bit proof may not take more much more than 1000 time units. It also agrees with the philosophy that we are not at center of anything. Not even our own knowledge production and culture.
Comment #117 August 4th, 2015 at 10:19 am
Rahul, your insight is correct, but with present-day algorithms for computing the permanent, the practical upper bound for classical simulations of scattershot BosonSampling experiments is more like 50–60 photons than 25–30.
Even my laptop, running the not-too-fast program Mathematica, at the not-too-fast rate of 6.5 GFLOP/s, computes a 25×25 permanent in less than four seconds.
For details and working code, see the Mathematica StackExchange question “Q: Can (compiled) matrix permanent evaluation be further sped-up?” (2013).
Question What is the relative likelihood that coming decades will witness sustained advances in algorithms for simulating scattershot BosonSampling, versus advances in experimental methods for observing it?
Answer (at present) Opinions are abundant, optimism plentiful, evidence sparse, rigorous proofs nonexistent.
\[\begin{array}[b]{r} \mathsf{\text{SIMULATION}}\\[-3ex] \ \end{array} \begin{array}[b]{r} \mathsf{\text{EXPERIMENT}}\mspace{20mu}\\ \begin{array}[b]{rcc} &\mathsf{\text{feasible}}&\mathsf{\text{infeasible}} \\ \mathsf{\text{feasible}}&\mathsf{\text{?}}&\mathsf{\text{?}} \\ \mathsf{\text{infeasible}}&\mathsf{\text{?}}&\mathsf{\text{?}} \end{array} \end{array}\]
Conclusion As with any STEAM enterprise blending simulations and experiments, it is reasonable to pursue a broad spectrum of research objectives and strategies.
————
Code (with apologies for formatting)
Clear[nPhoton,GFlop,zeroFunction];zeroFunction := nPhoton^2 * 2^nPhoton - flopIterate[[2]];
Do[ FindRoot[zeroFunction,{nPhoton,40},
WorkingPrecision->2*$MachinePrecision
]//ReplaceAll[nPhoton,#]&//Floor//
Print["One ",flopIterate[[1]]," computes a ",
#,"x",#," matrix permanent"
]&;,{flopIterate,{{MFLOP,10^6},{GFLOP,10^9},
{TFLOP,10^12},{PFLOP,10^15},{XFLOP,10^18}}}];
Result
One MFLOP computes a 12x12 matrix permanentOne GFLOP computes a 21x21 matrix permanent
One TFLOP computes a 30x30 matrix permanent
One PFLOP computes a 39x39 matrix permanent
One XFLOP computes a 48x48 matrix permanent
Comment #118 August 4th, 2015 at 12:54 pm
Hi.
many of you talk about exact definitions as a cause to “unsolvability” of the question P?NP ,
I never seen *exact* definition of “time complexity” , it seems like hand waving to call it “time” when we don’t have such thing as “time” in computer science, if we wan’t to talk about physical “real time” then “real time” can be reduced by the laws of physics with same “CS” laws ( with the usage of energy ).
In CS we count something else that is not well defined -the basic action of our “computation device” .
what is the definition of a basic action of a computation device? I think writing State table is not a solution to this.
I think that this “basic action” real definition is beyond the “math” world, but the physical world.
It’s like saying in math that doing any calculations is not a computation it’s a definition.
but actually computers and people do calculations to see what the expression actual value is.
Comment #119 August 4th, 2015 at 3:37 pm
Itai #118,
The standard way of making “time” make sense in a complexity context is to define the time as the number of steps a Turing machine takes.
Comment #120 August 5th, 2015 at 3:50 am
Regarding (4) of #84 (again, some reference would be very helpful) a sort of easier problem would be to consider the random case. Namely, the product of a random Gaussian matrix and its transpose. An efficient approximating algorithm would follow e.g. if most of the L_2 norm is concentrate on bounded levels for the Fourier-Hermite expansion.
Comment #121 August 5th, 2015 at 9:38 am
Scott #84
(2) … What is a paper about convergence to lognormal variable you are talking about?
(5) … In paper about Gurvits algorithm mentioned there you are (re)raising questions about sampling vs estimation. But if there are some classical algorithms for estimation of Per, how to guarantee that an experiment under consideration may not calculate Per in some “classical” way. Let me explain with a simple example. In a Troyansky and Tishby 1996 paper permanent is initially defined as an expectation of operator, but it is not difficult to define classical variable with mathematical expectation is equivalent to Per of n x n matrix. It is enough to generate a random permutation and calculate product of elements of matrix with respect to the permutation multiplied on n! Certainly, such method is not effective, because such variable converges to Per for N ~ n!, but how rule out such method of classical computation, if we are talking about expectation value of an operator. Later in the same paper Per is re-expressed via probability amplitude, and the similar method is used in your later paper. Intuitively it is clear, such reformulation rules out classical “trick” as a reasonable analogue of such method, but how to formalize the difference?
Comment #122 August 5th, 2015 at 5:47 pm
Over at the Institute for Quantum Information and Matter @ Caltech’s weblog Quantum Frontiers, the indomitable Nicole Yunger Halpern has posted an essay “Bits, bears, and beyond in Banff” that draws attention to Philippe Faist’s wonderful (as it seems to me) new poster Welcome to the Entropy Zoo.
Two Zoo News Shtetl Optimized readers may wonder “What (if anything) does the Entropy Zoo have to do with the Complexity Zoo?” One natural connexion is supplied by Section 7.2.2.2 of Donald Knuth’s new fascicle “Satisfiability (c.f. comment #7), specifically Knuth’s account of phase transitions in 3SAT, as given on fascicle pages 50-52 and 149-150.
Provably hard vs practically easy It is striking that a decision problem like 3SAT, which is (provably) NP-complete in general, is assuredly (yet not provably) decidable trivially in the random-instance case.
In regard to Conjectures (1–4) (of Scott’s comment #84), these considerations lead us to consider a prequel “Conjecture (0)”, that is associated not to the formally hard / practically easy problem of random 3SAT, but to the formally hard (?) / practically easy (?) problem of scattershot BosonSampling.
(0) The Permanent-of-Gaussians Scattershot Conjecture. Is there a fast algorithm to sample \(k\times k\) submatrices of an ensemble of random complex gaussian \(n\times n\) matrices, with \(k \ll n\), such that for \(n\gg 1\) the associated sampling of complex permanents is indistinguishable by Kolmogorov-Smirnov test from a distribution weighted by \(|\mathsf{\text{perm}}|^2\,\)?
Realism Note that “Conjecture (0)” captures certain aspects of experimental vs simulated scattershot BosonSampling experiments more fully than Conjectures (1-4)” (of Scott’s comment #84), in the crucial sense that the experimental data of a scattershot BosonSampling experiment does not provide case-by-case estimates of \(|\mathsf{\text{perm}}|^2\), thus freeing simulation algorithms from the awkward necessity of doing so.
Question for Complexity Theory Experts If Conjecture (0) is true (either provably or empirically) — and bearing in mind that “indistinguishable by Kolmogorov-Smirnov test” does not imply the stronger claim “indistinguishable” — then does the Polynomial Hierarchy collapse?
Simulationists wonder!
Comment #123 August 5th, 2015 at 6:42 pm
@Itai , comment #128
I’m not a computer scientist but I think we do have an explicit example of time complexity in cryptography with the Alternating Step Generator(pseudorandom generator) invented by Christoph Gunther in 1987. The cryptographic strength of the generator comes from the fact that the clocking(timing) of the output shift registers in the circuit is controlled by a non linear shift register (a de Bruijin sequence). Because sequential bits of the output registers are sometimes (read randomly) sampled more than once for output via the XOR gate, each output register can be modeled as a “sticky channel”. So you effectively have one sticky channel causing a one way permutation of another sticky channel via the XOR function. All this happens of course thanks to the random clock timing.
Comment #124 August 5th, 2015 at 7:32 pm
Itai,
It doesn’t really matter how fine-grained the step is, because all of the reasonable definitions will be off from each other by only a constant factor, and analysis of time complexity smooths out constant factors by looking at asymptotic growth. E.g., an algorithm that takes up to n steps or up to 10n steps will be O(n) either way.
Comment #125 August 13th, 2015 at 4:55 pm
For those of you interested in a Boson Sampling update: the Bristol group published an N=6 version in Science today (
http://www.sciencemag.org/content/349/6249/711.full.pdf ).
Comment #126 August 15th, 2015 at 10:13 am
FYI: NSA announces plans for transitioning to quantum resistant algorithms (nsa.gov)
https://www.nsa.gov/ia/programs/suiteb_cryptography/index.shtml
Wow 🙂
Comment #127 August 16th, 2015 at 4:41 pm
asdf #126: I don’t know that this is as big a deal as one might think. Let me quote from an email I sent someone who asked me about this:
Lots of people are thinking about “quantum resistance” these days; there have been whole workshops, etc. on it. Not that surprising that NSA would have a white paper on it. If you need an encrypted message to be secure for the next ~30 years, then even if you only assign (let’s say) a 10% probability to scalable QC by then, it’s not a bad idea. But if you were serious about it, you wouldn’t just be using RSA, DH, or ECC with somewhat-larger key sizes! You’d be using
symmetric ciphers like AES, or if you needed public-key, probably one of the lattice-based systems.
Comment #128 August 16th, 2015 at 4:42 pm
joe #125: Wow, that IS exciting, and somehow your comment is the first anyone told me about it! I’ll put up a short post about it after I land in Singapore.
Comment #129 August 16th, 2015 at 4:54 pm
Alexander #121: My original paper with Arkhipov cites results in the literature (from Costello and Vu, maybe?) about the convergence of Gaussian determinants to lognormals. We have more results in this paper.
Regarding how we know there’s not a classical “trick”: that’s like, the entire point of our main theorem! Recall, we prove that any polytime classical algorithm to sample the same distribution as the optical experiment would imply a collapse of the polynomial hierarchy (and even an approximate sampler would let you approximate Gaussian permanents in BPPNP.
Comment #130 August 16th, 2015 at 10:28 pm
Scott, my “Question for Complexity Theory Experts ” (#122) is motivated by …
————
The Story of Sinful Alice
Alice (claims sinfully) “With PTIME(n) resources, I can sample n-bit integers weighted by their Kolmogorov complexity.”
Bob (responds doubtfully) “With an NP oracle, I could falsify your sampling claim”
Alice (replies triumphantly) “But you haven’t got an NP oracle, have you?”
————
The point is that Alice’s state-of-sin — she is using a random-number generator — has extraordinary practical utility. So much so, that vast industries (like public key cryptography) are predicated upon the proposition that sinful claims like Alice’s cannot feasibly be disproven.
In other words, for all practical purposes Alice’s algorithm does have the “impossible” (yet extraordinarily useful) algorithmic property that she sinfully claims.
The Sinful Postulate Sinful algorithms are presently known for a vast class of problems, that practically are feasible to solve, even though formally they belong to hard complexity classes; it is therefore reasonable to postulate (or at least hope) that a great many quantum simulation problems — including perhaps even BosonSampling — are susceptible to sinful algorithms.
Comment #131 August 17th, 2015 at 11:15 am
@joe
Very interesting indeed this update about Boson Sampling!
Comment #132 August 17th, 2015 at 2:50 pm
Joe #125: that’s paywalled, arxiv preprint (May 2015) is here: http://arxiv.org/abs/1505.01182
Scott #126: yeah, but this didn’t seem to be a white paper, it sounds like they actually want to deploy QC resistant crypto, which surprised me some.
Meanwhile, here’s an Alabama license plate, though the person later came around to the other side: http://s3.neyer.me/pnp.jpg
Comment #133 August 17th, 2015 at 8:59 pm
Both the BosonSampling preprint [ arXiv:1505.01182] and the Science article contain the following marvelous passage:
Our intuitions upon contemplating this passage call to mind the 19th century couplet:
Our “blessed hearts” of quantum optimism hope that large LO circuits will prove to be a scalable path leading experimental refutation of the extended Church-Turing Thesis (ECT).
Conversely, our “dark hearts” of quantum skepticism wonder whether, in universes governed by QED at least, “large LO circuit” inescapably means “large lossy LO circuit”.
And it is natural to wonder too, whether the implications of a “mathematical proof (using plausible conjectures)” are strictly stronger than the implications of an unadorned “plausible conjecture”.
With these conflicting visions in mind, a third synthetic path is suggested by (mathematician) Michael Harris’ Mathematics Without Apologies (2015), specifically by a quotation from Goethe’s character Mephistopheles (on page 82):
(here Harris’ translation closely approximates the Faust translation of physicist Tom Mellett)
Mephistopheles’ quantum prediction Fuller appreciation of the “evil” effects of noise in large-scale quantum simulation, and of “sinful” loopholes in the no-go postulates of complexity theory, will inescapably create the “good” of performative engineering methods for simulating practical quantum technologies, in a QED universe that strictly upholds the ECT … accompanied (we can hope) by a “heavenly” mathematical and scientific appreciation as to why the Creation is so helpful (helpful to Faustian engineers at least).
Here the word “performative” has the sense that Harris specifies (on page 85), namely, that performative theories “do not simply describe a pre-existing world, but help to create a world of which the theory is a truer reflection.”
Conclusion An appreciation that Kalai-style quantum skepticism, and Harrow-style quantum optimism, alike are performative frames-of-mind — and even are compatibly performative — helps to deepen our appreciation of the tremendous fundamental worth of BosonSampling research.
And for this new research discipline, which so delights all of our scientific instincts, Scott Aaronson and Alex Arkhipov deserve immense credit.
Comment #134 August 18th, 2015 at 1:24 pm
As a follow-on to “Mephistopheles’ quantum prediction” (of comment #133 above)
Shtetl Optimized readers will appreciate that this IAD recommendation faithfully and even artfully reflects Mephistophelian quantum duality (of #133).
For if the optimistic quantum light teaches that quantum computers can break the Suite B cryptographic algorithms, and the skeptical quantum dark teaches that quantum computers are innately lossy — hence noisy, hence simulable in PTIME — then it follows that only quantum-resistant algorithms can resist PTIME classical attacks.
As for the move to a quantum resistant algorithm suite occurring “in the not distant future” … well, who *knows* what secrets remain to be mined from the Snowden disclosures?
Opinion The implications of Mephistophelian quantum duality for the engineering and medical arts so greatly surpass in long-term strategic, economic, and humanitarian significance the implications (if any) for the cryptographic arts, that a reasoned appreciation of this enduring asymmetric significance is the only durable “secret” that can rationally be associated to quantum information theory.
Conclusion Not the least of the virtues of BosonSampling research, for young researchers especially, is that it is unencumbered by secrecy and cryptolects.
Comment #135 August 19th, 2015 at 5:47 am
[…] experiments done by groups around the world). Humorously, I only learned the big news from a commenter on this blog, after the paper was already published (protip: if you’ve pushed forward the BosonSampling […]
Comment #136 August 19th, 2015 at 11:11 am
Scott 129, Thanks, but I still may not guess from the proof, why it is O’K to sample permanent of positive matrix (or maybe even negative one), but not absolute value of complex matrix
Comment #137 August 20th, 2015 at 1:26 pm
If I think I have a procedure to reduce factoring to P/poly, do you think that is reasonable? There is really no way to test this on large integers.
Comment #138 August 26th, 2015 at 10:00 am
[…] question is partly motivated by discussion on Aaronsons blog/ comments “introducing some British people to P vs NP” where there is questions about using supercomputers for theorem proving in the comments […]