tag:blogger.com,1999:blog-3722233.post2456039078989668567..comments2024-06-22T00:23:11.174-05:00Comments on Computational Complexity: Our Obsession with ProofsLance Fortnowhttp://www.blogger.com/profile/06752030912874378610noreply@blogger.comBlogger33125tag:blogger.com,1999:blog-3722233.post-16642447723563222452024-05-08T14:14:39.941-05:002024-05-08T14:14:39.941-05:00We not only need proofs, but UNDERSTANDABLE proo...We not only need proofs, but UNDERSTANDABLE proofs. In that sense the community’s “obsession” for proofs is warranted – it can take a lot of work to get to the heart of the matter. The new MOR proof needs to be judged not only on correctness but on crispness and simplicity.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-90189687566172267562024-05-07T23:17:59.476-05:002024-05-07T23:17:59.476-05:00I think this is a good question, but an answerable...I think this is a good question, but an answerable one! And the answer is that, as long as there's no proof of a mathematical statement, there's apparently something crucial still to be understood about it (since otherwise why ISN'T there a proof?). Furthermore, this is just as true in physics as it is in CS! The difference is that, in physics, in principle the ultimate arbiter of truth is "can you predict what's going to happen in this experiment?" -- and if the prediction comes out right, you usually feel vindicated enough to move forward even without the full understanding that would've come from clear mathematical definitions of all your concepts and proofs of all the statements you make about them. Now, we of course also have experiments in CS, and those ARE relied on in all the non-theoretical branches of the field! But the difference is, in CS we're typically concerned with the WORST that an adversary could possibly do to break our cryptosystem, or invalidate our protocol, or make our program or algorithm fail. And here experiment is inherently less useful as a guide to truth. And that forces us to fall back more on actually understanding what's going on, i.e. proof. And when that slows us down too much, we also have our own workaround for it, which is to agree socially on a relatively small set of conjectures, and then prove theorems modulo those conjectures. :-)Scotthttps://www.blogger.com/profile/13456161078489400740noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-25727920553312349402024-05-06T22:43:31.302-05:002024-05-06T22:43:31.302-05:00Thanks for the clarification.
It is a reasonable...Thanks for the clarification. <br /><br />It is a reasonable position to say the field was young and the norms were different. But we should be clear what is the expected behavior these days, and be careful to avoid creating an impression of favoritism and bias. <br /><br />I agree with you that algorithms can be useful even without formal correctness proof and without proven complexity upper bounds. We should explore what criteria we should apply to these when reviewing them.<br /><br />Simplex is a good example of algorithm that essentially everyone used in practice where the worst case was clearly exponential, and for a very long time we didn't have much theory about why it is performing much better in practice.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-23739893427136422052024-05-06T14:43:43.026-05:002024-05-06T14:43:43.026-05:00Yes, there could have been a formal retraction or ...Yes, there could have been a formal retraction or at least note for the Combinatorica article. But I strongly disagree that "the goal is mainly to prove things." Our goal is understanding. Proofs are just a small part of that. Lance Fortnowhttps://www.blogger.com/profile/06752030912874378610noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-20197721966499812202024-05-05T22:50:01.882-05:002024-05-05T22:50:01.882-05:00Is the algorithm actually valuable? It would be if...Is the algorithm actually valuable? It would be if it was known to perform well in practice (when compared to other competing algorithms) and always output a correct solution even if it did not have the claimed worst-case guarantee on its running time. Our community does a poor job of implementing and testing algorithms even for fundamental problems. The goal is mainly to prove things. Nothing wrong with it and we make fantastic progress but then the proof of correctness is important.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-4043952343997271302024-05-05T14:39:03.620-05:002024-05-05T14:39:03.620-05:00The new paper discusses errors in the Combinatoric...The new paper discusses errors in the Combinatorica paper in great detail. If the 1994 paper is not a poster child for retraction, what sorts of papers should be retracted? And what message does the absence of retraction send?<br />Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-9458375357500330342024-05-05T09:28:31.210-05:002024-05-05T09:28:31.210-05:00Do you think the 1994 Combinatorica paper should h...Do you think the 1994 Combinatorica paper should have been retracted by the authors and/or journal? The paper asserts a proof of correctness of MV, but the proof is fundamentally flawed. Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-51476273959387952542024-05-05T05:09:27.756-05:002024-05-05T05:09:27.756-05:00The original paper had value as the algorithm is m...The original paper had value as the algorithm is more important than the proof. But instead of a separate publication for the proof, it could have been the journal version of the original paper. It would be different if the proof was done by someone who wasn't an author on the first paper.<br /><br />Should there have been some kind of errata for an incomplete proof? Maybe but those were tricky especially back in 1980 and Vazirani hardly kept the lack of a proof a secret.Lance Fortnowhttps://www.blogger.com/profile/06752030912874378610noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-64166270505246885972024-05-04T22:39:23.848-05:002024-05-04T22:39:23.848-05:00Your post reads like a criticism of people who are...Your post reads like a criticism of people who are criticizing the fact that Vijay essentially got away without officially retracting a paper for an issue where a retraction would be expected.<br /><br />You might want to clarify your poison on that, if that is not your intention.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-11815570691836309132024-05-03T19:44:53.935-05:002024-05-03T19:44:53.935-05:00if you don't know who was the author of that p...if you don't know who was the author of that paper, and the algorithm was submitted but without proof of correctness or its complexity, would you accept the paper? or are you implying that the lower bar should apply only to well-known people like him?<br /><br />we can have a separate experimental algorithms track or conference where people submit heuristic algorithms and benchmarks on canonical datasets like SAT competitors, and so on, it is not gonna replace the algorithms with correctness proofs and performance analysis. They serve different purposes.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-21964485492179519862024-05-03T08:56:03.745-05:002024-05-03T08:56:03.745-05:00One of my math teachers (Glenn Stevens) liked sayi...One of my math teachers (Glenn Stevens) liked saying, "We don't prove things to establish truth."<br /><br />Implicitly, he was saying that one of the most important things proofs provide is *understanding*. When we prove, we understand better, and that helps us make progress.<br /><br />It is not the *only* way to make progress, and demanding proof to the exclusion of all other ways of understanding would be folly -- but proof is a very effective catalyst for progress.Chris Peikerthttps://web.eecs.umich.edu/~cpeikert/noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-10239939873159601042024-05-03T08:48:20.989-05:002024-05-03T08:48:20.989-05:00Not sure whether Lance is just trolling, but as a ...Not sure whether Lance is just trolling, but as a computer scientist who also publishes in economics, I strongly disagree with the claim that "theoretical economists [...] don't put such an emphasis on proofs". Quite to the contrary, there is more rigor in theoretical economics than in TCS. Most results in STOC/FOCS are not thoroughly checked for correctness before they are published. Some don’t even have complete proofs and the authors don't bother making a journal version. Vijay's 1980 paper is not an exception. <br />There is a reason why the community resisted double-blind reviewing for so long. It's easier to check the authors' names than the correctness of proofs ;-)<br /><br />I agree with Lance's observation that TCS papers are often judged based on the complexity of a proof rather than the statement of the theorem itself, which is crazy.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-32059686823998939922024-05-03T04:46:21.522-05:002024-05-03T04:46:21.522-05:00In CS, the cases where proofs were available used ...In CS, the cases where proofs were available used to outnumber the cases where proofs were missing. Before the current "phase of machine learning and optimization" including huge LLMs flipped the scales, the abscence or difficulty of proof was the mystery that caught my attention (not sure whether it caught your attention too). In this current phase, the abscence or difficulty of proof is not so mysterious.<br /><br />The obsession with proofs had good reasons, because either proof was attainable, or else the mere fact that proof was apperently too difficult in a specific case was an intriguing result too.Jakitohttps://www.blogger.com/profile/08235089048981338795noreply@blogger.comtag:blogger.com,1999:blog-3722233.post-29799820844065847902024-05-03T03:03:14.932-05:002024-05-03T03:03:14.932-05:00Your are drinking too much LLM hype. These huge LL...Your are drinking too much LLM hype. These huge LLMs, none of them can multiply 20 digit numbers.<br /><br />They are useful for some talks. They are far from what the hype makes people believe. <br /><br />AGI is no where near, yet people are raising huge sums of money (think billions) as of it is just around the corner. <br /><br />There seems to be some level of envy in your post regarding what ML researchers do.<br /><br />And economists and physicists do prove theorems. That is often the most prestigious work. Just take a look at Nobel prize winners in those fields. They might not be at the same level of right as we are in math, but they still do prove things. Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-79078463034568422182024-05-02T19:27:44.975-05:002024-05-02T19:27:44.975-05:00P is NP could be 100% correct.P is NP could be 100% correct.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-28730387590029929512024-05-02T14:15:34.862-05:002024-05-02T14:15:34.862-05:00Quite a number of people believe in QAnon conspira...Quite a number of people believe in QAnon conspiracies, too... Of course, we might even have both possibilities - the question might be independent. <br /><br />Here's one if you don't like that one: NP doesn't have linear size circuits.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-52116941777912306852024-05-02T13:34:56.614-05:002024-05-02T13:34:56.614-05:00Is it perhaps that without the proofs there is not...Is it perhaps that without the proofs there is nothing of value being generated by the field? Even with the proofs what actual societal impact can be attributed to complexity theory other than material for tenure boards?Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-51271274810848996452024-05-02T11:13:09.627-05:002024-05-02T11:13:09.627-05:00> confirm what we already believe.
Suspect, ye...> confirm what we already believe.<br /><br />Suspect, yes. But not believe. Most people wouldn't bet their life on P!=NP. And quite a number of people consider P=NP more likely.John Tromphttp://tromp.github.ionoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-318207005003144742024-05-02T10:18:52.194-05:002024-05-02T10:18:52.194-05:00proof is what makes you know that an algorithm act...proof is what makes you know that an algorithm actually works and behaves the way you say in the worst case. <br /><br />ML folks didn't care about worst case or even average case. They are just heuristics they fail all the time. If that is the level of reliability that you need from your system, fine, you don't Even need an algorithm. Just tell an LLM your wish and with probability less than .5 you will get what you want. <br /><br />Try running a plane on LLM or performing a surgery, or loan application decision without human in the loop, see what will happen. <br /><br />Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-11316927928979461202024-05-02T09:25:30.541-05:002024-05-02T09:25:30.541-05:00On the Bullinger's blog post, the discussions/...On the Bullinger's blog post, the discussions/comments raise many interesting aspects pertaining to diversity, bias, cliques, and non-public information that is available to only a select few. I am disappointed that instead of discussing those aspects and raising awareness about them, this blog post chose to focus on an aspect that no comment was interested in.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-51824048086392551592024-05-02T05:57:59.394-05:002024-05-02T05:57:59.394-05:00"Theoretical economists and physicists don...<i>"Theoretical economists and physicists don't put such an emphasis on proofs"</i><br /><br />LMAO...<br />Of course not, that would be the end of their trade!<br />Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-32475831281676296162024-05-02T02:34:09.132-05:002024-05-02T02:34:09.132-05:00The two words "theorem" and "theore...The two words "theorem" and "theoretical" have the same the two words have the same etymology. But "A theorem without a proof is a mere hypothesis" [cit. me] ... so, you get "hypothesis computer science" which doesn't sound very good.Marzio De Biasihttps://www.nearly42.orgnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-87149756678402720482024-05-02T01:21:57.427-05:002024-05-02T01:21:57.427-05:00Leaving a comment, because I got a bit of whiplash...Leaving a comment, because I got a bit of whiplash from that last paragraph.<br /><br />It's true that NeurIPS et al are big on empirical benchmarks, and aren't necessarily huge sticklers for proofs.<br /><br />But! When I think of "proofs" and "modern ML" intersected, I think of how LLMs are helping mathematicians prove new things. The more things we can prove are true, the better our stochastic parrots will be at priming us to prove the next true thing.<br /><br />I read between the lines of this letter, and presume: "A conversation with $CHATBOT about math, will go much smoother when $CHATBOT can tool-use Lean, and over a broader set of proven results": https://unlocked.microsoft.com/ai-anthology/terence-tao/<br /><br />Proofs in STOC and FOCS and all are the raw ingredients that make these seems-to-work-in-practice ML systems, actually work in practice.Brian Gawalthttps://brian.gawalt.comnoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-6723234009449103782024-05-01T22:23:02.566-05:002024-05-01T22:23:02.566-05:00"A proof does not make a theorem true; it was..."A proof does not make a theorem true; it was always true."<br />But how did you know it was true?Clément Canonnenoreply@blogger.comtag:blogger.com,1999:blog-3722233.post-14188016591704351282024-05-01T21:18:07.848-05:002024-05-01T21:18:07.848-05:00(Bill) There needs to be a place for speculative w...(Bill) There needs to be a place for speculative work: ideas for theorems that there is evidence for but haven't been proven, but labelled as such. Perhaps ITCS already does this. My SIGACT news open problems column might qualify. But then the question arises, how much credit should speculation get? More then they do? Credit in what form? Anonymousnoreply@blogger.com