wu :: forums (http://www.ocf.berkeley.edu/~wwu/cgi-bin/yabb/YaBB.cgi)
riddles >> general problem-solving / chatting / whatever >> The most amazing result in theoretical CS
(Message started by: amichail on Apr 24th, 2007, 6:04pm)

Title: The most amazing result in theoretical CS
Post by amichail on Apr 24th, 2007, 6:04pm
See:

http://www.cs.princeton.edu/~chazelle/pubs/nature06.pdf

Title: Re: The most amazing result in theoretical CS
Post by tiber13 on Apr 24th, 2007, 7:01pm
isnt working 4 me

Title: Re: The most amazing result in theoretical CS
Post by Icarus on Apr 24th, 2007, 8:02pm
Yes, tiber13, but you would have to understand what it was talking about first, wouldn't you?

While interesting, I am always leery of anything reported in such a fashion. I've seen too many results I know well "slaughtered" to be reported in a non-technical article, with significant issues simply overlooked in order to make the result seem greater than it is.

I am not qualified to address the usefulness of this result, but it strikes me that converting, for example, a 500 page proof of the Reimann Hypothesis into a checkable form might be as much a Herculean task as coming up with the proof in the first place.

And of course, the result is only probabilistic, so that even if the probabilities are high, there is always a slim chance the result is still false.

Still, if the conversion process can be algorized(?), it looks like a very useful verification technique.

Title: Re: The most amazing result in theoretical CS
Post by amichail on Apr 24th, 2007, 8:05pm
I think the Reimann Hypothesis proof example is misleading as this result is for propositional logic.

http://en.wikipedia.org/wiki/PCP_theorem

It's still an amazing and highly counter-intuitive result though.

BTW, the proof conversion is automated and runs in polynomial time.

Title: Re: The most amazing result in theoretical CS
Post by Icarus on Apr 24th, 2007, 8:13pm
Although I've never been clear on CS terminology, mathematics is generally reducible to propositional logic.

Title: Re: The most amazing result in theoretical CS
Post by amichail on Apr 24th, 2007, 8:14pm
"In its full splendour, PCP asserts that
any statement S whose validity can be ascertained
by a proof P written over n bits also
admits an alternative proof, Q. This proof Q
has two appealing features: it can be derived
from P in a number of steps proportional to
n^c, where c is some constant; and P can be verified
by examining only three bits of Q picked
at random. If S is true, a correct P will satisfy
the verifier with a probability of 99%. If it is not
true, any alleged proof P will trigger a rejection
from Q with a probability higher than 50%
(ref. 4). Not impressed with this error rate?
Then all you have to do is pick, instead of three
bits of Q, as many bits as are contained in this
line of text. The error probability will drop to
one in a billion."

Title: Re: The most amazing result in theoretical CS
Post by amichail on Apr 24th, 2007, 8:19pm

on 04/24/07 at 20:13:11, Icarus wrote:
Although I've never been clear on CS terminology, mathematics is generally reducible to propositional logic.

How would you translate a mathematical proof into propositional logic (without approximations)?

Note for example that first-order logic is only semidecidable.

Title: Re: The most amazing result in theoretical CS
Post by Aryabhatta on Apr 24th, 2007, 10:19pm
Bernard Chazelle (the author of that article) is a well known professor in CS (Princeton).

About the PCP theorem which is being talked about, it is a really important result in Computer Science.

It has been used to give pretty good results about Inapproximability of algorithms (i.e proving things like it is hard to even come up with reasonable approximations of certain NP complete problems etc)

Title: Re: The most amazing result in theoretical CS
Post by towr on Apr 25th, 2007, 1:05am

on 04/24/07 at 20:05:34, amichail wrote:
I think the Reimann Hypothesis proof example is misleading as this result is for propositional logic.

http://en.wikipedia.org/wiki/PCP_theorem
The wiki page at least says
"The PCP theorem, proven in the early 1990's, states that every NP problem has a very efficient probabilistically checkable proof system."
It doesn't seem to limit the statement to only propositional logic.

There are decidable fractions of first order logic that are rich enough to account for many mathematical statements; so those would certainly fall under this theorem (assuming the wikipage is accurate about it applying to all NP problems)

Title: Re: The most amazing result in theoretical CS
Post by amichail on Apr 25th, 2007, 6:36am

on 04/25/07 at 01:05:03, towr wrote:
The wiki page at least says
"The PCP theorem, proven in the early 1990's, states that every NP problem has a very efficient probabilistically checkable proof system."
It doesn't seem to limit the statement to only propositional logic.

There are decidable fractions of first order logic that are rich enough to account for many mathematical statements; so those would certainly fall under this theorem (assuming the wikipage is accurate about it applying to all NP problems)


Here's a book chapter on the topic:

http://www.cs.princeton.edu/theory/complexity/pcpchap.pdf

Note in particular:

"Suppose somebody wants to convince you that a Boolean formula is satisfiable. He could present
the usual certificate, namely, a satisfying assignment, which you could then check by substituting
back into the formula. However, doing this requires reading the entire certificate. The PCP
Theorem shows an interesting alternative: this person can easily rewrite his certificate so you
can verify it by probabilistically selecting a constant number of locations—as low as 3 bits— to
examine in it. Furthermore, this probabilistic verification has the following properties: (1) A
correct certificate will never fail to convince you (that is, no choice of your random coins will make
you reject it) and (2) If the formula is unsatisfiable, then you are guaranteed to reject every claimed
certificate with high probability.
Of course, since Boolean satisfiability is NP-complete, every other NP language can be deterministically
and efficiently reduced to it. Thus the PCP Theorem applies to every NP language.
We mention one counterintuitive consequence. Let A be any one of the usual axiomatic systems of
mathematics for which proofs can be verified by a deterministic TM in time that is polynomial in
the length of the proof. Recall the following language is in NP:
L = {<phi,1^n> : phi has a proof in A of length phi <= n} .
The PCP Theorem asserts that L has probabilistically checkable certificates. Such certificate
can be viewed as an alternative notion of “proof” for mathematical statements that is just as valid
as the usual notion. However, unlike standard mathematical proofs, where every line of the proof
has to be checked to verify its validity, this new notion guarantees that proofs are probabilistically
checkable by examining only a constant number of bits in them1.
"

Title: Re: The most amazing result in theoretical CS
Post by Grimbal on Apr 25th, 2007, 7:04am
Where can I see a practical example?  How to convince me that a map is 3-colourable with "3 bits" only?

Title: Re: The most amazing result in theoretical CS
Post by amichail on Apr 25th, 2007, 12:36pm
You can learn more about this result and its proof here:

http://www.cs.washington.edu/education/courses/533/05au/

Title: Re: The most amazing result in theoretical CS
Post by Aryabhatta on Apr 25th, 2007, 1:08pm
Note that this is not a new result.. I has been known for about 10 years now.

It has come into buzz again following a different proof of the result found in 2006.

Title: Re: The most amazing result in theoretical CS
Post by Icarus on Apr 25th, 2007, 6:14pm

on 04/24/07 at 20:19:46, amichail wrote:
How would you translate a mathematical proof into propositional logic (without approximations)?

Note for example that first-order logic is only semidecidable.


http://quod.lib.umich.edu/cgi/t/text/text-idx?c=umhistmath;idno=AAT3201.0001.001



Powered by YaBB 1 Gold - SP 1.4!
Forum software copyright © 2000-2004 Yet another Bulletin Board