Rigor que leva ao insight

No MathOverflow, Timothy Gowers fez uma pergunta intitulada " Demonstrando que o rigor é importante ". A maior parte da discussão houve sobre casos mostrando a importância da prova, sobre a qual as pessoas do CSTheory provavelmente não precisam ser convencidas. Na minha experiência, as provas precisam ser mais rigorosas na ciência da computação teórica do que em muitas partes da matemática contínua, porque nossa intuição muitas vezes acaba sendo errada para estruturas discretas e porque o desejo de criar implementações incentiva argumentos mais detalhados. Um matemático pode se contentar com uma prova de existência, mas um cientista da computação teórico geralmente tentará encontrar uma prova construtiva. O lema local de Lovász é um bom exemplo [1].

Gostaria, portanto, de saber

existem exemplos específicos na ciência da computação teórica em que uma prova rigorosa de uma afirmação que se acredita verdadeira levou a uma nova percepção da natureza do problema subjacente?

Um exemplo recente que não é diretamente dos algoritmos e da teoria da complexidade é a síntese teórica da prova , a derivação automática de algoritmos corretos e eficientes das condições pré e pós [2].

• [1] Robin A. Moser e Gábor Tardos, uma prova construtiva do lema local geral de Lovász , JACM 57 , artigo 11, 2010. http://doi.acm.org/10.1145/1667053.1667060
• [2] Saurabh Srivastava, Sumit Gulwani e Jeffrey S. Foster, da verificação do programa à síntese do programa , ACM SIGPLAN Notices 45 , 313–326, 2010. http://doi.acm.org/10.1145/1707801.1706337

Editar:O tipo de resposta que eu tinha em mente é como o de Scott e Matus. Como sugeriu Kaveh, este é um triplo de algo que as pessoas querem provar (mas que não era necessariamente inesperado pelos argumentos "físicos", "ondulados" ou "intuitivos"), uma prova e consequências para o "problema subjacente" que seguidos daquela prova que não era antecipada (talvez a criação de uma prova exigisse novas idéias inesperadas, ou naturalmente conduza a um algoritmo, ou mudou a maneira como pensamos sobre a área). As técnicas desenvolvidas durante o desenvolvimento de provas são os alicerces da ciência da computação teórica; portanto, para manter o valor dessa questão um tanto subjetiva, vale a pena focar na experiência pessoal, como a fornecida por Scott, ou em um argumento apoiado em referências, como matus fez. Além disso, eu estou tentando evitar discussões sobre se algo se qualifica ou não; infelizmente, a natureza da questão pode ser intrinsecamente problemática.

Já temos uma pergunta sobre resultados "surpreendentes" em complexidade: Resultados surpreendentes em complexidade (não na lista de blogs de complexidade). Por isso, idealmente, estou procurando respostas que se concentrem no valor de provas rigorosas , não necessariamente no tamanho da inovação.

András, como você provavelmente sabe, existem tantos exemplos do que você está falando que é quase impossível saber por onde começar! No entanto, acho que essa pergunta pode realmente ser boa, se as pessoas derem exemplos de sua própria experiência, onde a prova de uma conjectura amplamente aceita em sua subárea levou a novas idéias.

Quando eu estava na graduação, o primeiro problema real do TCS que lidei foi o seguinte: qual é o algoritmo quântico mais rápido para avaliar um OR de √n ANDs de √n variáveis ​​booleanas cada? Era dolorosamente óbvio para mim e para todos os outros com quem conversei que o melhor que você poderia fazer seria aplicar o algoritmo de Grover recursivamente, tanto na sala de cirurgia quanto na sala de cirurgia. Isso deu um limite superior O (√n log (n)). (Na verdade, você pode reduzir o fator de log, mas vamos ignorá-lo por enquanto.)

Para minha enorme frustração, porém, não consegui provar um limite inferior melhor do que o trivial Ω (n ^1/4 ). "Ir ao físico" e "acenar com a mão" nunca pareciam mais atraentes! :-D

Porém, alguns meses depois, Andris Ambainis lançou seu método quântico adversário , cuja principal aplicação a princípio era um limite inferior de Ω (√n) para os OR-de-ANDs. Para provar esse resultado, Andris imaginou alimentar um algoritmo quântico sobreposto a diferentes entradas; ele então estudou como o emaranhamento entre as entradas e o algoritmo aumentou a cada consulta que o algoritmo fazia. Ele mostrou como essa abordagem permite reduzir a complexidade da consulta quântica até mesmo para problemas "não confusos" e não simétricos, usando apenas propriedades combinatórias muito gerais da função f que o algoritmo quântico estava tentando calcular.

Longe de apenas confirmar que a complexidade da consulta quântica de um problema irritante era o que todos esperavam, essas técnicas acabaram representando um dos maiores avanços na teoria da computação quântica desde os algoritmos de Shor e Grover. Desde então, eles foram usados ​​para provar dezenas de outros limites inferiores quânticos e foram reaproveitados para obter novos limites inferiores clássicos .

Claro, este é "apenas mais um dia no maravilhoso mundo da matemática e do TCS". Mesmo que todo mundo "já saiba" que X é verdadeiro, provar que X muitas vezes requer a invenção de novas técnicas que são aplicadas muito além de X e, em particular, a problemas para os quais a resposta correta era muito menos óbvia a priori .

A repetição paralela é um bom exemplo da minha área:

Uma breve explicação da repetição paralela. Suponha que você tenha um sistema de prova de dois provadores para um idioma : dada a entrada , conhecida por todos, um verificador envia a pergunta ao provador 1 e a pergunta ao provador 2. Os provedores respondem com as respostas e , respectivamente, sem comunicando. O verificador executa alguma verificação em e (dependendo de ) e decide se aceita ou rejeita. Se , existe uma estratégia de provadores que o verificador sempre aceita. Se$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$, para qualquer estratégia de provadores, o verificador aceita com probabilidade no máximo ("probabilidade de erro").$s$

Agora suponha que queremos uma menor probabilidade de erro. Talvez esteja próximo de , e queremos . Uma abordagem natural seria a repetição paralela : deixe o verificador enviar perguntas independentes para cada provador, e , receba k respostas dos provadores e e executa verificações nas respostas.$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$

A história. A princípio, ficou "claro" que a probabilidade de erro tinha que diminuir como , como se o verificador tivesse feito verificações seqüenciais. A lenda diz que foi dado a um aluno para provar, antes que se percebesse que a afirmação "óbvia" é simplesmente falsa. Aqui está uma exposição de um contra-exemplo: http://www.cs.washington.edu/education/courses/cse533/05au/na-game.pdf . Demorou um pouco (e vários resultados mais fracos), antes Ran Raz finalmente confirmou que a probabilidade de erro de fato diminui exponencialmente, mas tem um comportamento um pouco complicado: é , onde o alfabeto k s Ω ( k / log | Σ | )$s^{k}$$k$$s^{\Omega(k/\log|\Sigma|)}$$\Sigma$é o conjunto de respostas possíveis dos provadores no sistema original. A prova utilizou idéias teóricas da informação e foi inspirada por uma idéia de Razborov na complexidade da comunicação. Uma parte confusa da prova original de Ran foi mais tarde simplificada por Thomas Holenstein, resultando em uma das minhas provas favoritas.

Insights para o problema e mais consequências. Primeiro, existem as coisas imediatas: uma melhor compreensão do comportamento quantitativo da repetição paralela e o papel que o alfabeto desempenha, uma melhor compreensão de quando os provadores podem usar as perguntas paralelas para trapacear, uma melhor compreensão da importância de independência na repetição paralela entre os pares de perguntas (posteriormente formalizados por Feige e Kilian).$\Sigma$$k$

Depois, existem as extensões que se tornaram possíveis: Anup Rao conseguiu adaptar a análise para mostrar que quando o sistema de provas original é um jogo de projeção, ou seja, a resposta do primeiro provador determina no máximo uma resposta aceitável de o segundo provador, não há nenhuma dependência do alfabeto, e a constante no expoente pode ser melhorada. Isso é importante porque a maioria dos resultados de dureza de aproximação se baseia em jogos de projeção, e jogos exclusivos são um caso especial de jogos de projeção. Há também melhorias quantitativas nos jogos de expansores (de Ricky Rosen e Ran Raz) e muito mais.

Depois, há as consequências de longo alcance. Apenas alguns exemplos: Um lema teórico da informação do artigo de Raz foi usado em muitos outros contextos (em criptografia, em equivalência de amostragem e pesquisa, etc.). A técnica de "amostragem correlacionada" usada por Holenstein foi aplicada em muitos outros trabalhos (na complexidade da comunicação, no PCP, etc).

Outro bom exemplo de rigor (e novas técnicas) sendo necessário para provar afirmações que se acredita serem verdadeiras: análise suavizada. Dois casos em questão:

• O algoritmo simplex
• O algoritmo k-means

Para os dois métodos, era "bem sabido" que eles funcionavam bem na prática e, pelo primeiro, sabia-se que levava o tempo exponencial da pior das hipóteses. A análise suavizada pode ser vista como tendo "explicado" o bom comportamento empírico em ambos os casos. No segundo, embora se soubesse que a pior complexidade de médias era , não se sabia se havia limites inferiores que eram exponenciais em , e agora sabemos isso é verdade, mesmo no avião!$k$$O(n^{c \cdot kd})$$n$

Acho que o exemplo a seguir gerou muitas pesquisas que tiveram resultados do tipo que você está procurando, pelo menos se eu seguir o espírito do seu exemplo de LLL.

Robert E. Schapire. A força do aprendizado fraco. Machine Learning, 5 (2): 197-227, 1990.

Este artigo resolveu a questão: o aprendizado forte e fraco do PAC é equivalente? Não posso lhe dizer com certeza se as pessoas naquele círculo (Schapire, Valiant, Kearns, Avrim Blum, ..) se sentiram fortemente de um jeito ou de outro (ou seja, se isso já é uma instância do que você procura), embora eu tenha algumas suspeitas, e você pode se formar olhando os jornais por volta de então. Resumidamente (e aproximadamente / provavelmente), um problema pode ser aprendido pelo PAC (por uma classe de hipótese, para uma distribuição) se, para qualquer , existir um algoritmo ('eficiente') que possa produzir com probabilidade de pelo menos uma hipótese com erro no máximo . Se você pudesse satisfazer o mas não o$\epsilon>0, \delta>0$$1-\delta$$\epsilon$$\epsilon$$\delta$, desde que não seja trivial ('trivialidade' depende de alguns detalhes, já que estou deixando de fora o significado de 'eficiente'), tentativas repetidas aumentariam a confiança . Mas se, em vez disso, você pudesse obter apenas uma vantagem sobre adivinhações aleatórias (a mesma condição de 'trivialidade' se aplica), você poderia de alguma forma aumentar esse resultado de maneira inteligente para obter um erro arbitrariamente bom?$\delta$$\delta$$\gamma$

Enfim, as coisas se tornaram muito interessantes após o trabalho de Schapire. Sua solução produziu uma maioria sobre as hipóteses da classe original. Entao veio:

Yoav Freund. Impulsionar um algoritmo de aprendizado fraco por maioria. Informações e Computação, 121 (2): 256--285, 1995.

Este artigo teve uma 'reprovação' do resultado de Schapire, mas agora a hipótese construída usava apenas uma única maioria. Nesse sentido, os dois produziram outra reprovação, chamada AdaBoost:

Yoav Freund e Robert E. Schapire. Uma generalização teórica da decisão do aprendizado on-line e uma aplicação para impulsionar. Journal of Computer and System Sciences, 55 (1): 119-139, 1997.

A questão do aprendizado fraco / forte começou como uma preocupação principalmente teórica, mas essa sequência de 'reprovações' resultou em um belo algoritmo, um dos resultados mais influentes no aprendizado de máquina. Eu poderia sair por todo tipo de tangente aqui, mas vou me conter. No contexto do TCS, esses resultados dão muita vida no contexto de (1) algoritmos de peso multiplicativo e (2) resultados do conjunto do núcleo duro. Sobre (1), gostaria de esclarecer que o AdaBoost pode ser visto como uma instância do trabalho de pesos multiplicativos / winnow de Warmuth / Littlestone (Freund era um aluno de Warmuth), mas há muitas novas idéias sobre o aumento resultados. Sobre (2), eu '

Para maior precisão histórica, também devo dizer que as datas em minhas citações talvez não sejam o que algumas pessoas esperariam, já que para algumas delas havia versões anteriores da conferência.

Voltar à natureza da sua pergunta. O principal valor de 'rigor' aqui foi o fornecimento da classe de hipótese que se aprende (maiorias ponderadas sobre a classe de hipótese original) e algoritmos eficientes para encontrá-las.

Este exemplo é semelhante ao das respostas de Dana e Scott.

É "óbvio" que a melhor maneira de calcular a PARIDADE de bits com um circuito ilimitado de profundidade é a seguinte estratégia recursiva. Quando a profundidade é 2, nada melhor que você pode fazer do que escrever o CNF (ou DNF) de todos os termos. Quando for maior que , divida o conjunto de variáveis ​​de entrada em partes, adivinhe a paridade de cada uma das partes (faça um OR do fan-in ) e para aquelas suposições que somam a paridade , resolva recursivamente o problema em cada uma das partes (faça um AND de fan-in ) com profundidade$n$$d$$d$$2^{n-1}$$d$$2$$n^{1/(d-1)}$$2^{n^{1/(d-1)}}$$1$$n^{1/(d-1)}$$d-1$o circuito. Se você alternar em cada nível de recursão entre fazer um OR de ANDs e fazer um AND de ORs (tomando o complemento), você termina com um circuito de profundidade e tamanho que calcula PARIDADE.$2^{n^{1/(d-1)}}$$2^{n^{1/(d-1)}}$$d$$2^{O(n^{1/(d-1)})}$

Em 1985, Hastad provou que o "obviamente melhor" circuito de profundidade é ideal até constantes no expoente. Para fazer isso, ele provou o Switching Lemma, que tem sido uma ferramenta muito valiosa para provar limites inferiores para circuitos, algoritmos paralelos e sistemas de prova. Este é um dos poucos casos em que sabemos que um algoritmo natural específico é ideal e levou a um entendimento muito detalhado da potência de .A C $d$$AC^0$

O artigo de Rasborov e Rudich, "Natural Proofs", oferece uma prova rigorosa (formalização) da dolorosamente óbvia afirmação "É realmente difícil provar que P ≠ NP".

A ideia de que alguns problemas algorítmicos requerem um número exponencial de etapas, ou busca exaustiva sobre todas as possibilidades, surgiu desde os anos 50 e talvez antes. (Obviamente, a idéia ingênua e competitiva de que os computadores podem fazer tudo também era comum.) A principal inovação de Cook e Levin foi colocar essa idéia em bases rigorosas. Isso, é claro, mudou tudo.

Atualização: Acabei de perceber que minha resposta, como a boa resposta do Turquistanês, aborda o título da pergunta "rigor levando a insights", mas talvez não o texto específico que tratava de "prova rigorosa de um teorema".

Alan Turing formalizou a noção de algoritmo (computabilidade efetiva) usando máquinas de Turing. Ele usou esse novo formalismo para provar que o problema de Halting é indecidível (ou seja, o problema de Halting não pode ser resolvido por nenhum algoritmo). Isso levou a um longo programa de pesquisa que comprovou a impossibilidade do 10º problema de Hilbert. Matiyasevich, em 1970, provou que não há algoritmo que possa decidir se uma equação diofantina inteira tem uma solução inteira.