Rigueur menant à la perspicacité

41

Sur MathOverflow, Timothy Gowers a posé une question intitulée " Démontrer que la rigueur est importante ". La plupart des discussions ont porté sur des cas montrant l’importance de la preuve, dont les utilisateurs de CSTheory n’ont probablement pas besoin d’être convaincus. Selon mon expérience, les preuves doivent être plus rigoureuses en informatique théorique que dans de nombreuses parties des mathématiques continues, car notre intuition s'avère si souvent fausse pour des structures discrètes et parce que la volonté de créer des implémentations encourage des arguments plus détaillés. Un mathématicien peut se contenter d'une preuve d'existence, mais un informaticien théorique tentera généralement de trouver une preuve constructive. Le lemme local de Lovász est un bel exemple [1].

Je voudrais donc savoir

Existe-t-il des exemples spécifiques en informatique théorique où une preuve rigoureuse d'une affirmation supposée être vraie a permis de mieux comprendre la nature du problème sous-jacent?

Un exemple récent, qui ne provient pas directement des algorithmes et de la théorie de la complexité, est la synthèse probatoire , la dérivation automatique d'algorithmes corrects et efficaces à partir de conditions préalables et postérieures [2].


Modifier:Le genre de réponse que j'avais en tête est semblable à celles de Scott et Matus. Comme Kaveh l'a suggéré, il s'agit d'un triple de ce que les gens voulaient prouver (mais ce n'était pas forcément inattendu par des arguments "physiques", "de la main" ou "intuitifs"), une preuve et des conséquences pour le "problème sous-jacent" suivi de cette preuve qui n’était pas anticipée (peut-être que créer une preuve nécessitait de nouvelles idées inattendues, ou conduisait naturellement à un algorithme, ou changeait la façon dont nous pensons au sujet). Les techniques développées tout en développant des preuves sont les éléments constitutifs de l'informatique théorique. Par conséquent, pour conserver la valeur de cette question quelque peu subjective, il serait intéressant de se concentrer sur l'expérience personnelle, telle que celle fournie par Scott, ou sur un argument étayé par des références, comme Matus l'a fait. De plus, je m essayer d’éviter les disputes sur la question de savoir si quelque chose est admissible ou non; malheureusement, la nature de la question peut être intrinsèquement problématique.

Nous avons déjà une question sur les résultats "surprenants" dans la complexité: Résultats surprenants dans la complexité (pas dans la liste des blogs sur la complexité), donc, idéalement, je cherche des réponses qui se concentrent sur la valeur des preuves rigoureuses , pas nécessairement sur la taille de la percée.

András Salamon
la source
2
Ne voyons-nous pas / ne faisons-nous pas cela tous les jours?
Dave Clarke
Qu'entend-on exactement par "problème sous-jacent?" Voulez-vous dire uniquement les problèmes pour lesquels il existe un problème plus profond qu'un énoncé particulier? Je pensais à tout problème comportant la preuve constructive de l’existence d’un algorithme (par exemple, le test de primalité AKS permettant d’établir que PRIMES est dans P) conduirait à une "nouvelle compréhension" via une preuve rigoureuse, mais si vous ne parlez que à propos de petites déclarations au sein d'un problème, cela n'aurait pas de sens.
Philip White
Pour vous assurer que j'ai bien compris votre question, demandez-vous un triple (déclaration S, preuve P, idée I), où la déclaration S est connue / supposée être vraie, mais nous obtenons une nouvelle idée (I) lorsque quelqu'un vient avec la nouvelle preuve P pour S?
Kaveh
[suite] Par exemple, dans le cas de LLL, nous avions des preuves non constructives pour LLL (S), mais la nouvelle preuve constructive arXive (P) nous donne un nouvel aperçu (I).
Kaveh
Hmm ... Qu'en est-il de commencer avec des algorithmes spécifiques et de les utiliser ensuite comme points de données à généraliser? Tels que, les gens conçoivent quelques algorithmes gloutons, et finalement le champ développe une notion de problème avec une sous-structure optimale.
Aaron Sterling

Réponses:

34

András, comme vous le savez probablement, il y a tellement d'exemples de ce dont vous parlez qu'il est presque impossible de savoir par où commencer! Cependant, je pense que cette question peut réellement être une bonne question si les gens donnent des exemples de leur propre expérience où la preuve d'une conjecture largement répandue dans leur sous-domaine a conduit à de nouvelles perspectives.

Lorsque j'étais étudiant de premier cycle, le premier véritable problème du SDC auquel j'ai été confronté était le suivant: quel est l'algorithme quantique le plus rapide pour évaluer un OU de √n ET de √n variables booléennes chacune? Il était douloureusement évident pour moi et pour tous les autres interlocuteurs à qui j'ai parlé que le mieux que vous puissiez faire était d'appliquer récursivement l'algorithme de Grover, à la fois à l'OR et à l'AND. Cela donnait une limite supérieure O (√n log (n)). (En fait, vous pouvez réduire le facteur logarithmique, mais ignorons-le pour l'instant.)

À mon énorme frustration, cependant, je ne pouvais pas prouver une borne inférieure mieux que le trivial Ω (n 1/4 ). "Aller physicien" et "saluer la réponse" n'ont jamais semblé aussi attrayants! :-RÉ

Cependant, quelques mois plus tard, Andris Ambainis a présenté sa méthode de l'adversaire quantique , dont l'application principale était initialement une limite inférieure Ω (√n) pour les OR-of-AND. Pour prouver ce résultat, Andris a imaginé d’alimenter un algorithme quantique en superposant différentes entrées; Il a ensuite étudié comment l'intrication entre les entrées et l'algorithme augmentait à chaque interrogation de l'algorithme. Il a montré comment cette approche vous permettait de réduire la complexité des requêtes quantiques, même pour les problèmes «désordonnés», non symétriques, en utilisant uniquement les propriétés combinatoires très générales de la fonction f que l'algorithme quantique tentait de calculer.

Loin de simplement confirmer que la complexité des requêtes quantiques d'un problème ennuyeux correspondait à ce à quoi tout le monde s'attendait, ces techniques se sont avérées être l'un des plus grands progrès de la théorie de l'informatique quantique depuis les algorithmes de Shor et Grover. Depuis, ils ont été utilisés pour prouver des dizaines d'autres limites inférieures quantiques, et ont même été réutilisés pour obtenir de nouvelles limites inférieures classiques .

Bien sûr, c’est «juste un autre jour dans le monde merveilleux des mathématiques et du SDC». Même si tout le monde "sait déjà" que X est vrai, prouver que X nécessite très souvent d'inventer de nouvelles techniques qui sont ensuite appliquées bien au-delà de X, et en particulier aux problèmes pour lesquels la bonne réponse était beaucoup moins évidente a priori .

Scott Aaronson
la source
27

La répétition parallèle est un bel exemple de ma région:

Lxq1q2a1a2a1a2q1,q2xLxLs

s1s=1015kq1(1),,q1(k)q2(1),,q2(k)a1(1),,a1(k)a1(1),,a1(k)k

skksΩ(k/log|Σ|)Σ

Σk

Ensuite, il y a les extensions devenues possibles: Anup Rao a été capable d'adapter l'analyse pour montrer que lorsque le système de preuve d'origine est un {\ em projection projection}, c'est-à-dire que la réponse du premier prouveur détermine au plus une réponse acceptable de Dans le second cas, il n’ya aucune dépendance à l’alphabet et la constante dans l’exposant peut être améliorée. Ceci est important car la plupart des résultats d'approximation sont basés sur des jeux de projection, et les jeux uniques constituent un cas particulier des jeux de projection. Il y a aussi des améliorations quantitatives dans les jeux sur expandeurs (de Ricky Rosen et Ran Raz), et plus encore.

Ensuite, il y a des conséquences d'une portée considérable. Quelques exemples: Un lemme de théorie de l'information tiré de l'article de Raz a été utilisé dans de nombreux autres contextes (cryptographie, équivalence d'échantillonnage et de recherche, etc.). La technique "d'échantillonnage corrélé" utilisée par Holenstein a été appliquée dans de nombreux autres travaux (complexité de la communication, PCP, etc.).

Dana Moshkovitz
la source
3
C'est un bel exemple!
Suresh Venkat
20

Un autre bon exemple de rigueur (et de nouvelles techniques) est nécessaire pour prouver des affirmations jugées vraies: l’analyse lissée. Deux cas d'espèce:

  • L'algorithme simplex
  • L'algorithme k-means

kO(nckd)n

Suresh Venkat
la source
13

Je pense que l’exemple suivant a donné lieu à de nombreuses recherches qui ont eu les résultats escomptés, du moins si je suis l’esprit de votre exemple LLL.

Robert E. Schapire. La force de la faible capacité d'apprentissage. Machine Learning, 5 (2): 197-227, 1990.

ϵ>0,δ>01δϵϵδδδγ

Quoi qu'il en soit, les choses sont devenues très intéressantes après le papier de Schapire. Sa solution produisit une majorité de majorité par rapport aux hypothèses de la classe d'origine. Puis vint:

Yoav Freund. Stimuler un algorithme d'apprentissage faible à la majorité. Information and Computation, 121 (2): 256-285, 1995.

Ce document avait un "reproche" du résultat de Schapire, mais maintenant, l'hypothèse construite n'utilisait qu'une seule majorité. Dans cet ordre d'idées, les deux auteurs ont ensuite produit une autre recommandation, appelée AdaBoost:

Yoav Freund et Robert E. Schapire. Une généralisation, basée sur la décision, de l'apprentissage en ligne et une application au boosting. Journal of Computer and System Sciences, 55 (1): 119-139, 1997.

La question de l'apprentissage faible / fort était au départ une préoccupation essentiellement théorique, mais cette séquence de «reproches» a abouti à un bel algorithme, l'un des résultats les plus influents de l'apprentissage automatique. Je pourrais prendre toutes sortes de tangentes ici, mais je vais me retenir. Dans le contexte du TCS, ces résultats respirent beaucoup dans le contexte de (1) algorithmes de pondération multiplicative et (2) de résultats d'ensemble d'ensemble. À propos de (1), je voudrais juste préciser qu'AdaBoost peut être considéré comme un exemple du travail sur les poids multiplicatifs / winnow de Warmuth / Littlestone (Freund était un étudiant de Warmuth), mais il y a beaucoup de nouvelles perspectives dans le renforcement. résultats. À propos de (2), je '

Par souci d'exactitude historique, je devrais également dire que les dates sur mes citations ne correspondent peut-être pas à ce à quoi certaines personnes s'attendent, dans la mesure où certaines versions ont été antérieures à la conférence.

Revenons à la nature de votre question. La valeur clé de la «rigueur» était de fournir la classe d'hypothèses sur laquelle on apprend (majorités pondérées par rapport à la classe d'hypothèses d'origine) et des algorithmes efficaces pour les trouver.

matus
la source
12

Cet exemple va dans le sens des réponses de Dana et Scott.

ndd2n1d2n1/(d1)2n1/(d1)1n1/(d1)d12n1/(d1)2n1/(d1)d2O(n1/(d1))

dAC0

Ryan Williams
la source
11

Le document "Natural Proofs" de Rasborov et Rudich offre une preuve rigoureuse de (formalisation de) la déclaration douloureusement évidente "Il est vraiment difficile de prouver que P ≠ NP."

Jeffε
la source
2
"Il est vraiment difficile de prouver que P ≠ NP" n'est pas équivalent à "des preuves naturelles ne prouveront probablement pas P ≠ NP". Il existe d'autres obstacles, tels que la relativisation et l'algèbre. En réalité, il pourrait y avoir une infinité d’autres obstacles.
Mohammad Al-Turkistany
7
La relativisation est juste "Il est difficile de prouver P ≠ NP." L'algèbre est venue plus tard, mais c'est une formalisation de "C'est vraiment très difficile de prouver P ≠ NP." (Ha ha seulement sérieux.)
Jeffε
6

L'idée que certains problèmes algorithmiques nécessitent un nombre exponentiel d'étapes, ou une recherche exhaustive sur toutes les possibilités, a été évoquée depuis les années 50 et peut-être même avant. (Bien entendu, l'idée naïve en concurrence selon laquelle les ordinateurs peuvent tout faire était également courante.) La principale avancée de Cook et Levin a été de placer cette idée sur des bases rigoureuses. Ceci, bien sûr, a tout changé.

Mise à jour: Je viens de me rendre compte que ma réponse, comme la réponse agréable de Turkistany, porte le titre de la question "Rigueur menant à la perspicacité", mais peut-être pas la formulation spécifique qui parle de "preuve rigoureuse à un théorème".

Gil Kalai
la source
0

Alan Turing a formalisé la notion d'algorithme (calculabilité effective) à l'aide de machines de Turing. Il a utilisé ce nouveau formalisme pour prouver que le problème de Halting est indécidable (c.-à-d. Que le problème de Halting ne peut être résolu par aucun algorithme). Cela a conduit à un long programme de recherche qui a prouvé l'impossibilité du 10ème problème de Hilbert. Matiyasevich en 1970 a prouvé qu’aucun algorithme ne pouvait décider si une équation de Diophantine entière avait une solution entière.

Mohammad Al-Turkistany
la source
1
@Kaveh, qu'est-ce que le MRDP?
Mohammad Al-Turkistany
1
Il existe des ensembles non chiffrables énumératifs (RE) (tels que le problème de l'arrêt). Matiyasevich a prouvé que tout ensemble récursivement dénombrable est Diophantin. Cela implique immédiatement l'impossibilité du dixième problème de Hilbert.
Mohammad Al-Turkistany
1
@ Kaveh, Pourquoi n'avez-vous pas soumis la première réponse à vos tests "rigoureux"? Autant que je sache, la preuve naturelle n'est pas le seul obstacle qui nous empêche de prouver P vs NP.
Mohammad Al-Turkistany
1
PNPPNP
Je pense que c'est une bonne réponse.
Gil Kalai