Rygor prowadzący do wglądu

Na MathOverflow Timothy Gowers zadał pytanie zatytułowane „ Wykazanie, że rygor jest ważny ”. Większość dyskusji dotyczyła przypadków pokazujących wagę dowodu, o których ludzie w CSTheory prawdopodobnie nie muszą być przekonani. Z mojego doświadczenia wynika, że ​​dowody muszą być bardziej rygorystyczne w informatyce teoretycznej niż w wielu częściach ciągłej matematyki, ponieważ nasza intuicja często okazuje się błędna w przypadku dyskretnych struktur, a ponieważ dążenie do tworzenia implementacji zachęca do bardziej szczegółowych argumentów. Matematyk może być zadowolony z dowodu na istnienie, ale teoretyczny informatyk zwykle próbuje znaleźć konstruktywny dowód. Lovász Local Lemma jest dobrym przykładem [1].

Chciałbym zatem wiedzieć

czy istnieją konkretne przykłady w informatyce teoretycznej, w których rygorystyczny dowód twierdzenia, które uważa się za prawdziwe, doprowadził do nowego wglądu w naturę problemu?

Najnowszym przykładem, który nie pochodzi bezpośrednio od algorytmów i teorii złożoności, jest synteza proof-teoretyczna , automatyczne wyprowadzanie poprawnych i wydajnych algorytmów z warunków wstępnych i końcowych [2].

• [1] Robin A. Moser i Gábor Tardos, Konstruktywny dowód generała Lovásza Local Lemma , JACM 57 , artykuł 11, 2010. http://doi.acm.org/10.1145/1667053.1667060
• [2] Saurabh Srivastava, Sumit Gulwani i Jeffrey S. Foster, Od weryfikacji programu do syntezy programu , ACM SIGPLAN Notices 45 , 313–326, 2010. http://doi.acm.org/10.1145/1707801.1706337

Edytować:Miałem na myśli odpowiedź taką jak Scott i Matus. Jak sugerował Kaveh, jest to potrójne coś, co ludzie chcieli udowodnić (ale niekoniecznie było to nieoczekiwane przez argumenty „fizyki”, „machania ręką” lub „intuicyjne”), dowód i konsekwencje dla „leżącego u podstaw problemu”, że wynikało z nieoczekiwanego dowodu (być może stworzenie dowodu wymagało nieoczekiwanych nowych pomysłów lub naturalnie prowadzi do algorytmu lub zmieniło sposób myślenia o tym obszarze). Techniki opracowane podczas opracowywania dowodów są elementami składowymi teoretycznej informatyki, więc aby zachować wartość tego nieco subiektywnego pytania, warto skoncentrować się na osobistych doświadczeniach, takich jak Scott, lub argumentie popartym referencjami, jak Matus. Ponadto ja staram się unikać dyskusji na temat tego, czy coś się kwalifikuje, czy nie; niestety charakter pytania może być z natury problematyczny.

Mamy już pytanie o „zaskakujące” wyniki w złożoności: zaskakujące wyniki w złożoności (nie na liście blogów o złożoności), więc idealnie szukam odpowiedzi, które koncentrują się na wartości rygorystycznego dowodu , niekoniecznie wielkości przełomu.

András, jak zapewne wiesz, istnieje tak wiele przykładów tego, o czym mówisz, że prawie niemożliwe jest wiedzieć, od czego zacząć! Sądzę jednak, że to pytanie może być dobre, jeśli ludzie podadzą przykłady z własnego doświadczenia, w którym dowód powszechnie uznanej hipotezy na ich podobszarze doprowadził do nowych spostrzeżeń.

Kiedy byłem studentem, pierwszym prawdziwym problemem TCS, z którym się zmierzyłem, było: jaki jest najszybszy algorytm kwantowy do oceny OR dla I AND dla zmiennych boolowskich? Było to dla mnie boleśnie oczywiste i wszyscy inni, z którymi rozmawiałem, że najlepszym, co możesz zrobić, to zastosować rekurencyjnie algorytm Grovera, zarówno do OR, jak i do AND. Dało to górną granicę O (logn log (n)). (Właściwie możesz zmniejszyć współczynnik logarytmiczny, ale na razie zignoruj ​​to.)

Ku mojej ogromnej frustracji nie byłem jednak w stanie udowodnić żadnej dolnej granicy lepiej niż trywialne Ω (n ^1/4 ). „Going physic” i „handwaving the answer” nigdy nie wyglądały tak atrakcyjnie! :-RE

Ale potem, kilka miesięcy później, Andris Ambainis wyszedł ze swoją kwantową metodą przeciwnika , której głównym zastosowaniem na początku była dolna granica Ω (√n) dla OR-of-AND. Aby udowodnić ten wynik, Andris wyobrażał sobie zasilenie algorytmu kwantowego superpozycją różnych danych wejściowych; następnie zbadał, w jaki sposób splątanie między danymi wejściowymi a algorytmem rosło z każdym zapytaniem wykonywanym przez algorytm. Pokazał, w jaki sposób to podejście pozwala na ograniczenie złożoności kwantowych zapytań nawet w przypadku „nieuporządkowanych”, niesymetrycznych problemów, poprzez zastosowanie jedynie bardzo ogólnych właściwości kombinatorycznych funkcji f, którą algorytm kwantowy próbował obliczyć.

Techniki te okazały się być jednym z największych postępów w teorii obliczeń kwantowych od czasów algorytmów Shora i Grovera. Od tego czasu zostały one wykorzystane do udowodnienia dziesiątek innych kwantowych dolnych granic, a nawet zostały przeznaczone do uzyskania nowych klasycznych dolnych granic.

Oczywiście jest to „kolejny dzień we wspaniałym świecie matematyki i TCS”. Nawet jeśli wszyscy „już wiedzą”, że X jest prawdą, udowodnienie, że X bardzo często wymaga wynalezienia nowych technik, które następnie zostaną zastosowane daleko poza X, aw szczególności w przypadku problemów, dla których właściwa odpowiedź była znacznie mniej oczywista a priori .

Równoległe powtarzanie jest dobrym przykładem z mojej okolicy:

Krótkie wyjaśnienie równoległego powtarzania. Załóżmy, że masz system sprawdzania dwóch przysłówków dla języka : Przy danych wejściowych , znanych wszystkim, weryfikator wysyła pytanie do dowcipu 1, a pytanie do dowcipu 2. Dowódca odpowiada odpowiedziami odpowiednio i , bez przyległy. Weryfikator wykonuje pewne sprawdzenie i (w zależności od ) i decyduje, czy przyjąć, czy odrzucić. Jeśli , istnieje strategia sprawdzania, którą weryfikator zawsze akceptuje. Jeśli$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$, dla dowolnej strategii sprawdzania weryfikator przyjmuje z prawdopodobieństwem co najwyżej („prawdopodobieństwo błędu”).$s$

Załóżmy teraz, że chcemy mniejszego prawdopodobieństwa błędu. Może jest bliskie , a my chcemy . Naturalnym podejściem byłoby równoległe powtarzanie : pozwól weryfikatorowi wysłać niezależnych pytań do każdego przysłowia, i , otrzymuj k odpowiedzi od dowódców i i wykonuje sprawdzania odpowiedzi.$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$

Historia. Na początku było „jasne”, że prawdopodobieństwo błędu musi maleć jak , tak jakby weryfikator wykonał kontroli sekwencyjnej. Legenda głosi, że został przekazany uczniowi w celu udowodnienia, zanim zorientowano się, że „oczywiste” stwierdzenie jest po prostu fałszywe. Oto ekspozycja kontrprzykładu: http://www.cs.washington.edu/education/courses/cse533/05au/na-game.pdf . Zajęło to trochę czasu (i kilka słabszych wyników), zanim Ran Raz ostatecznie potwierdził, że prawdopodobieństwo błędu rzeczywiście maleje wykładniczo, ale ma nieco skomplikowane zachowanie: jest to , gdzie alfabet k s Ω ( k / log | Σ | )$s^{k}$$k$$s^{\Omega(k/\log|\Sigma|)}$$\Sigma$to zestaw możliwych odpowiedzi na dowody w oryginalnym systemie. W dowodzie wykorzystano teoretyczne idee informacyjne i podobno zainspirowano go pomysłem Razborowa o złożoności komunikacyjnej. Brudna część oryginalnego dowodu Rana została później pięknie uproszczona przez Thomasa Holensteina, co zaowocowało jednym z moich ulubionych dowodów.

Wgląd w problem i więcej konsekwencji. Najpierw są rzeczy bezpośrednie: lepsze zrozumienie ilościowego zachowania równoległego powtarzania i roli, jaką odgrywa alfabet , lepsze zrozumienie, kiedy dowódcy mogą używać równoległych pytań do oszukiwania, lepsze zrozumienie znaczenia niezależność w równoległym powtórzenia między par pytań (później sformalizowanych przez Feige i Kilian).$\Sigma$$k$

Następnie istnieją rozszerzenia, które stały się możliwe: Anup Rao był w stanie dostosować analizę, aby pokazać, że gdy oryginalny system dowodu jest {gra projekcyjna}, tj. Odpowiedź pierwszego dowcipu określa co najwyżej jedną akceptowalną odpowiedź po drugie, w ogóle nie ma zależności od alfabetu, a stałą wykładnika można poprawić. Jest to ważne, ponieważ większość twardości wyników aproksymacji opiera się na grach projekcyjnych, a wyjątkowe gry są szczególnym przypadkiem gier projekcyjnych. Wprowadzono również ulepszenia ilościowe w grach na ekspanderach (autorstwa Ricky Rosen i Ran Raz) i nie tylko.

Potem są daleko idące konsekwencje. Kilka przykładów: lemat z teorii Razera został wykorzystany w wielu innych kontekstach (w kryptografii, w równoważności próbkowania i wyszukiwania itp.). Technikę „skorelowanego próbkowania”, którą stosował Holenstein, zastosowano w wielu innych pracach (w złożoności komunikacyjnej, w PCP itp.).

Kolejny dobry przykład dyscypliny (i nowych technik) jest potrzebny do udowodnienia twierdzeń, które uważano za prawdziwe: płynna analiza. Dwa przypadki w punkcie:

• Algorytm simpleksowy
• Algorytm k-średnich

W przypadku obu metod „dobrze wiadomo”, że sprawdzają się w praktyce, a po pierwsze wiadomo, że zajęło to dużo czasu wykładniczego. Wygładzoną analizę można postrzegać jako „wyjaśniającą” dobre zachowanie empiryczne w obu przypadkach. W drugim przypadku, gdy było wiadomo, że w najgorszym przypadku złożoność -means to , nie było wiadomo, czy były niższe granice, które były w wykładniczej i obecnie wiadomo to prawda, nawet w samolocie!O ( n c ⋅ k d ) $k$$O(n^{c \cdot kd})$$n$

Myślę, że poniższy przykład zrodził wiele badań, które przyniosły wyniki, których szukasz, przynajmniej jeśli podążam za duchem twojego przykładu LLL.

Robert E. Schapire. Siła słabej zdolności uczenia się. Machine Learning, 5 (2): 197–227, 1990.

Ten artykuł rozwiązał pytanie: czy mocna i słaba nauka PAC jest równoważna? Nie mogę ci powiedzieć z całą pewnością, czy ludzie w tym kręgu (Schapire, Valiant, Kearns, Avrim Blum, ..) czuli się silnie w ten czy inny sposób (tj. Czy jest to już przykład tego, czego szukasz), chociaż mam trochę podejrzenia, a możesz stworzyć własne, przeglądając wówczas gazety. W skrócie (i w przybliżeniu / prawdopodobnie) problemem jest możliwe do nauczenia się PAC (za pomocą klasy hipotez, dla dystrybucji), jeśli dla dowolnego istnieje algorytm („wydajny”), który można wytworzyć za pomocą prawdopodobieństwo co najmniej hipotezy z błędem co najwyżej . Jeśli możesz spełnić ale nie1 - δ ϵ ϵ δ δ δ $\epsilon>0, \delta>0$$1-\delta$$\epsilon$$\epsilon$$\delta$, tak długo, jak nie był trywialny („trywialność” zależy od niektórych szczegółów, ponieważ pomijam znaczenie słowa „efektywny”), powtarzane próby zwiększyłyby pewność siebie . Ale jeśli zamiast tego mógłbyś osiągnąć tylko pewną przewagę nad przypadkowym zgadywaniem (obowiązuje ten sam warunek „trywialności”), czy mógłbyś w jakiś sposób sprytnie zwiększyć ten wynik, aby osiągnąć arbitralnie dobry błąd?$\delta$$\delta$$\gamma$

W każdym razie sprawy stały się bardzo interesujące po pracy Schapire'a. Jego rozwiązanie wytworzyło większość w stosunku do hipotez w klasie oryginalnej. Potem przyszedł:

Yoav Freund. Poprawa słabego algorytmu uczenia się przez większość. Information and Computation, 121 (2): 256--285, 1995.

Ten artykuł miał „napomnienie” wyniku Schapire'a, ale teraz skonstruowana hipoteza wykorzystywała tylko jedną większość. Wzdłuż tych dwóch linii stworzyli kolejny napomnienie, zwane AdaBoost:

Yoav Freund i Robert E. Schapire. Teoretyczna uogólnienie na decyzje dotyczące uczenia się on-line i aplikacja do wzmocnienia. Journal of Computer and System Sciences, 55 (1): 119–139, 1997.

Pytanie słabego / silnego uczenia się początkowo było przede wszystkim kwestią teoretyczną, ale ta sekwencja „napomnień” zaowocowała pięknym algorytmem, jednym z najbardziej wpływowych wyników uczenia maszynowego. Mógłbym tu przejść na wszelkiego rodzaju styczne, ale się powstrzymam. W kontekście TCS wyniki te tchną dużo życia w kontekście (1) multiplikatywnych algorytmów wagi i (2) twardych zestawów wyników. Jeśli chodzi o (1), chciałbym tylko wyjaśnić, że AdaBoost może być postrzegany jako przykład multiplikatywnych wag / znanej pracy Warmuth / Littlestone (Freund był uczniem Warmuth), ale istnieje wiele nowych informacji na temat wzmocnienia wyniki. O (2), I '

Dla dokładności historycznej powinienem również powiedzieć, że daty w moich cytatach mogą nie być takie, jakich niektórzy by się spodziewali, ponieważ dla kilku z nich były wcześniejsze wersje konferencyjne.

Wróć do charakteru twojego pytania. Kluczową wartością „rygoru” było tutaj zapewnienie pierwszej klasy hipotezy, której się uczy (ważona większość w stosunku do oryginalnej klasy hipotezy) oraz wydajnych algorytmów do jej znalezienia.

Ten przykład jest zgodny z odpowiedziami Dany i Scotta.

Jest „oczywiste”, że najlepszym sposobem obliczenia parzystości bitów z nieograniczonym obwodem wachlowania głębokości jest następująca strategia rekurencyjna. Gdy głębokość wynosi 2, nie ma nic lepszego niż napisanie CNF (lub DNF) wszystkich warunków. Gdy jest większe niż , podziel zestaw zmiennych wejściowych na części , zgadnij parzystość każdej z części (weź OR z wachlarza ), i dla tych domysłów, które składają się na parzystośćd d 2 n - 1 d 2 n 1 / ( d - 1 ) 2 n 1 / ( d - 1 $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$

Artykuł Rasborova i Rudicha „Natural Proofs” oferuje rygorystyczny dowód (sformalizowanie) bolesnego oczywistego stwierdzenia „ Naprawdę trudno jest udowodnić, że P ≠ NP”.

Pomysł, że niektóre problemy algorytmiczne wymagają wykładniczej liczby kroków lub wyczerpującego przeszukiwania wszystkich możliwości, pojawił się od lat 50. i być może wcześniej. (Oczywiście konkurencyjny naiwny pomysł, że komputery potrafią robić wszystko, był również powszechny.) Głównym przełomem Cooka i Levina było wprowadzenie tego pomysłu w rygorystyczne podstawy. To oczywiście zmieniło wszystko.

Aktualizacja: Właśnie zdałem sobie sprawę, że moja odpowiedź, podobnie jak miła odpowiedź Turkistany, odnosi się do tytułu pytania „rygor prowadzący do wglądu”, ale być może nie do konkretnego sformułowania, które dotyczyło „rygorystycznego dowodu na twierdzenie”.

Alan Turing sformalizował pojęcie algorytmu (efektywna obliczalność) za pomocą maszyn Turinga. Użył tego nowego formalizmu, aby udowodnić, że problem zatrzymania jest nierozstrzygalny (tj. Problemu zatrzymania nie da się rozwiązać za pomocą żadnego algorytmu). Doprowadziło to do długiego programu badawczego, który wykazał niemożność 10. problemu Hilberta. Matiyasevich w 1970 roku udowodnił, że nie ma algorytmu, który mógłby decydować, czy liczba całkowita Równanie diofantyczne ma rozwiązanie liczby całkowitej.