Strenge führt zu Einsicht

Auf MathOverflow stellte Timothy Gowers eine Frage mit dem Titel " Demonstrieren, dass Genauigkeit wichtig ist ". Die meiste Diskussion gab es über Fälle, die die Wichtigkeit von Beweisen zeigten, von denen die Leute auf CSTheory wahrscheinlich nicht überzeugt werden müssen. Nach meiner Erfahrung müssen Beweise in der theoretischen Informatik strenger sein als in vielen Teilen der kontinuierlichen Mathematik, weil sich unsere Intuition für diskrete Strukturen so oft als falsch herausstellt und weil der Drang, Implementierungen zu erstellen, detailliertere Argumente fordert. Ein Mathematiker mag sich mit einem Existenzbeweis zufrieden geben, aber ein theoretischer Informatiker wird normalerweise versuchen, einen konstruktiven Beweis zu finden. Das Lovász Local Lemma ist ein gutes Beispiel [1].

Ich würde deshalb gerne wissen

Gibt es in der theoretischen Informatik konkrete Beispiele, bei denen ein strenger Beweis einer für wahr gehaltenen Aussage zu neuen Einsichten in die Natur des zugrunde liegenden Problems geführt hat?

Ein aktuelles Beispiel, das nicht direkt aus Algorithmen und der Komplexitätstheorie stammt, ist die beweistheoretische Synthese , die automatische Herleitung korrekter und effizienter Algorithmen aus Vor- und Nachbedingungen [2].

• [1] Robin A. Moser und Gábor Tardos, ein konstruktiver Beweis des General Lovász Local Lemma , JACM 57 , Artikel 11, 2010. http://doi.acm.org/10.1145/1667053.1667060
• [2] Saurabh Srivastava, Sumit Gulwani und Jeffrey S. Foster, Von der Programmüberprüfung zur Programmsynthese , ACM SIGPLAN Notices 45 , 313–326, 2010. http://doi.acm.org/10.1145/1707801.1706337

Bearbeiten:Die Art der Antwort, die ich im Sinn hatte, ist wie die von Scott und Matus. Wie Kaveh angedeutet hat, ist dies ein Dreifach von etwas, was die Leute beweisen wollten (was aber nicht unbedingt durch "Physik", "Handwinken" oder "intuitive" Argumente unerwartet war), ein Beweis und Konsequenzen für das "zugrunde liegende Problem", das Daraus folgten Beweise, die nicht vorweggenommen wurden (vielleicht erforderte die Erstellung eines Beweises unerwartete neue Ideen oder führte natürlich zu einem Algorithmus oder veränderte die Art und Weise, wie wir über das Gebiet denken). Techniken, die bei der Entwicklung von Beweisen entwickelt wurden, sind die Bausteine ​​der theoretischen Informatik. Um den Wert dieser eher subjektiven Frage beizubehalten, lohnt es sich, sich auf persönliche Erfahrungen zu konzentrieren, wie sie von Scott geliefert wurden, oder auf ein Argument, das durch Referenzen gestützt wird. wie Matus. Außerdem habe ich Ich versuche, Streitigkeiten darüber zu vermeiden, ob etwas geeignet ist oder nicht. Leider kann die Art der Frage von sich aus problematisch sein.

Wir haben bereits eine Frage zu "überraschenden" Ergebnissen in Bezug auf Komplexität: Überraschende Ergebnisse in Bezug auf Komplexität (nicht auf der Liste der Komplexitätsblogs). Daher suche ich im Idealfall nach Antworten, die sich auf den Wert strenger Beweise konzentrieren , nicht unbedingt auf die Größe des Durchbruchs.

András, wie Sie wahrscheinlich wissen, gibt es so viele Beispiele für das, wovon Sie sprechen, dass es fast unmöglich ist zu wissen, wo Sie anfangen sollen! Ich denke jedoch, dass diese Frage tatsächlich eine gute sein kann, wenn Menschen Beispiele aus ihrer eigenen Erfahrung nennen, bei denen der Beweis einer weit verbreiteten Vermutung in ihrem Unterbereich zu neuen Einsichten führte.

Als ich ein Student war, war das erste wirkliche TCS-Problem, das ich angesprochen habe, das folgende: Was ist der schnellste Quantenalgorithmus, um ein ODER von √n UND von √n Booleschen Variablen auszuwerten? Mir und allen anderen, mit denen ich gesprochen habe, war es schmerzlich klar, dass das Beste, was Sie tun können, darin besteht, Grovers Algorithmus rekursiv sowohl auf den OP als auch auf die ANDs anzuwenden. Dies ergab eine obere Grenze von O (√n log (n)). (Eigentlich können Sie den Log-Faktor abschalten, aber lassen Sie uns das jetzt ignorieren.)

Zu meiner großen Enttäuschung konnte ich jedoch keine Untergrenze besser als das triviale Ω (n ^1/4 ) nachweisen. "Going Physicist" und "Handwaving the Answer" sahen noch nie so ansprechend aus! :-D

Ein paar Monate später kam Andris Ambainis mit seiner Quanten-Gegner-Methode heraus , deren Hauptanwendung zunächst eine Ω (√n) -Untergrenze für das ODER von UND war. Um dieses Ergebnis zu beweisen, stellte sich Andris vor, einem Quantenalgorithmus eine Überlagerung verschiedener Eingaben zuzuführen. Anschließend untersuchte er, wie die Verflechtung zwischen den Eingaben und dem Algorithmus mit jeder Abfrage des Algorithmus zunahm. Er zeigte, wie Sie mit diesem Ansatz die Komplexität von Quantenabfragen auch bei "chaotischen", nicht symmetrischen Problemen senken können, indem Sie nur sehr allgemeine kombinatorische Eigenschaften der Funktion f verwenden, die der Quantenalgorithmus zu berechnen versucht.

Weit davon entfernt, nur zu bestätigen, dass die Komplexität der Quantenabfragen eines ärgerlichen Problems den Erwartungen entsprach, stellten diese Techniken einen der größten Fortschritte in der Quantencomputertheorie seit den Algorithmen von Shor und Grover dar. Sie wurden seitdem verwendet, um Dutzende anderer unterer Quantengrenzen zu beweisen, und wurden sogar neu verwendet, um neue klassische Untergrenzen zu erhalten .

Natürlich ist dies "nur ein weiterer Tag in der wundervollen Welt von Mathematik und TCS". Selbst wenn alle „bereits kennt“ X wahr ist , X erweist sich als sehr oft neue Techniken erfordert erfinden , die dann weit über X angewendet werden, und insbesondere zu Problemen , für die die richtige Antwort war viel weniger offensichtlich a priori .

Parallele Wiederholung ist ein schönes Beispiel aus meiner Gegend:

Eine kurze Erklärung der parallelen Wiederholung. Angenommen, Sie haben ein Zwei-Prüfer-Beweissystem für eine Sprache : Bei gegebener Eingabe , die jedem bekannt ist, sendet ein Prüfer die Frage an Prüfer 1 und die Frage an Prüfer 2. Die Prüfer antworten mit den Antworten bzw. ohne kommunizieren. Der Prüfer überprüft und (abhängig von ) und entscheidet, ob er akzeptiert oder ablehnt. Wenn , gibt es eine Prüfstrategie, die der Prüfer immer akzeptiert. Wennx q 1 q 2 a 1 a 2 a 1 a 2 q 1 , q 2 x ∈ L x ∉ L $L$$x$$q_1$$q_2$$a_1$$a_2$$a_1$$a_2$$q_1,q_2$$x\in L$$x\not\in L$Für jede Prüfstrategie akzeptiert der Prüfer mit einer Wahrscheinlichkeit von höchstens ("Fehlerwahrscheinlichkeit").$s$

1 s = 10 - $s$$1$$s = 10^{-15}$$k$$q_1^{(1)},\ldots,q_1^{(k)}$$q_2^{(1)},\ldots,q_2^{(k)}$$a_1^{(1)},\ldots,a_1^{(k)}$$a_1^{(1)},\ldots,a_1^{(k)}$$k$

$s^{k}$$k$$s^{\Omega(k/\log|\Sigma|)}$$\Sigma$

$\Sigma$$k$

Dann gibt es die Erweiterungen, die möglich wurden: Anup Rao konnte die Analyse anpassen, um zu zeigen, dass, wenn das ursprüngliche Beweissystem ein {\ em Projektionsspiel} ist, die Antwort des ersten Beweisers höchstens eine akzeptable Antwort von bestimmt Beim zweiten Beweis gibt es überhaupt keine Abhängigkeit vom Alphabet, und die Konstante im Exponenten kann verbessert werden. Dies ist wichtig, da die meisten Näherungsergebnisse auf Projektionsspielen basieren und einzigartige Spiele ein Sonderfall von Projektionsspielen sind. Es gibt auch quantitative Verbesserungen bei Spielen für Expander (von Ricky Rosen und Ran Raz) und mehr.

Dann gibt es die weitreichenden Konsequenzen. Nur ein paar Beispiele: Ein informationstheoretisches Lemma aus Raz 'Arbeit wurde in vielen anderen Zusammenhängen verwendet (in der Kryptographie, bei der Entsprechung von Stichproben und Suchen usw.). Die von Holenstein verwendete "Correlated Sampling" -Technik wurde in vielen anderen Arbeiten angewendet (in Bezug auf Kommunikationskomplexität, in Bezug auf PCP usw.).

Ein weiteres gutes Beispiel für Strenge (und neue Techniken) ist die geglättete Analyse. Zwei Beispiele dafür:

• Der Simplex-Algorithmus
• Der k-Means-Algorithmus

$k$$O(n^{c \cdot kd})$$n$

Ich denke, das folgende Beispiel hat eine Menge Forschung hervorgebracht, die Ergebnisse der Art ergab, nach der Sie suchen, zumindest wenn ich dem Geist Ihres LLL-Beispiels folge.

Robert E. Schapire. Die Stärke der schwachen Lernfähigkeit. Machine Learning, 5 (2): 197 & ndash; 227, 1990.

$\epsilon>0, \delta>0$$1-\delta$$\epsilon$$\epsilon$$\delta$$\delta$$\delta$$\gamma$

Jedenfalls wurden die Dinge nach Schapires Aufsatz sehr interessant. Seine Lösung ergab eine Mehrheit der Mehrheit über Hypothesen in der ursprünglichen Klasse. Dann kam:

Yoav Freund. Mehrheitsförderung eines schwachen Lernalgorithmus. Information and Computation, 121 (2): 256 & ndash; 285, 1995.

Dieses Papier hatte einen "Vorwurf" von Schapires Ergebnis, aber jetzt verwendete die konstruierte Hypothese nur eine einzige Mehrheit. In diesem Sinne machten die beiden dann einen weiteren Vorwurf mit dem Namen AdaBoost:

Yoav Freund und Robert E. Schapire. Eine entscheidungstheoretische Verallgemeinerung des Online-Lernens und eine Anwendung zur Steigerung. Journal of Computer and System Sciences, 55 (1): 119-139, 1997.

Die Frage nach dem schwachen / starken Lernen begann als vorwiegend theoretisches Anliegen, aber diese Abfolge von „Zurechtweisungen“ führte zu einem schönen Algorithmus, einem der einflussreichsten Ergebnisse beim maschinellen Lernen. Ich könnte hier auf alle möglichen Arten von Tangenten losgehen, werde mich aber zurückhalten. Im Kontext von TCS atmen diese Ergebnisse im Kontext von (1) multiplikativen Gewichtsalgorithmen und (2) Hardcore-Mengenergebnissen viel Leben ein. Über (1) möchte ich nur klarstellen, dass AdaBoost als Beispiel für die multiplikativen Gewichte / Winnow-Arbeiten von Warmuth / Littlestone (Freund war ein Warmuth-Student) angesehen werden kann, aber es gibt eine Menge neuer Einsichten in das Boosten Ergebnisse. Über (2), ich '

Aus historischen Gründen sollte ich auch sagen, dass die Daten in meinen Zitaten möglicherweise nicht den Erwartungen entsprechen, die manche Menschen haben, da es für einige von diesen frühere Konferenzversionen gab.

Zurück zur Art Ihrer Frage. Der zentrale Wert von "Rigor" bestand darin, die Hypothesenklasse, über die man lernt (gewichtete Mehrheiten gegenüber der ursprünglichen Hypothesenklasse), und effiziente Algorithmen bereitzustellen, um sie zu finden.

Dieses Beispiel entspricht den Antworten von Dana und Scott.

$n$$d$$d$$2^{n-1}$$d$$2$$n^{1/(d-1)}$$2^{n^{1/(d-1)}}$$1$$n^{1/(d-1)}$$d-1$$2^{n^{1/(d-1)}}$$2^{n^{1/(d-1)}}$$d$$2^{O(n^{1/(d-1)})}$

$d$$AC^0$

Rasborovs und Rudichs Arbeit "Natural Proofs" bietet einen strengen Beweis (eine Formalisierung) der schmerzlich offensichtlichen Aussage "Es ist wirklich schwer, dieses P ≠ NP zu beweisen."

Die Idee, dass einige algorithmische Probleme eine exponentielle Anzahl von Schritten oder eine exaustive Suche über alle Möglichkeiten erfordern, wurde seit den 50er Jahren und vielleicht schon früher aufgeworfen. (Natürlich war die konkurrierende naive Idee, dass Computer alles können, auch weit verbreitet.) Der große Durchbruch von Cook und Levin bestand darin, diese Idee auf rigorose Gründe zu stellen. Das hat natürlich alles verändert.

Update: Ich habe gerade festgestellt, dass meine Antwort wie die schöne Antwort von Turkistany den Titel der Frage "Strenge, die zu Einsicht führt" anspricht, aber vielleicht nicht den spezifischen Wortlaut, der sich mit "strengen Beweisen für ein Theorem" befasst.

Alan Turing formalisierte den Begriff des Algorithmus (effektive Berechenbarkeit) unter Verwendung von Turing-Maschinen. Er benutzte diesen neuen Formalismus, um zu beweisen, dass das Halteproblem unentscheidbar ist (dh, das Halteproblem kann mit keinem Algorithmus gelöst werden). Dies führte zu einem langen Forschungsprogramm, das die Unmöglichkeit des 10. Hilbert-Problems bewies. Matiyasevich hat 1970 bewiesen, dass es keinen Algorithmus gibt, der entscheiden kann, ob eine ganzzahlige Diophantine-Gleichung eine ganzzahlige Lösung hat.