Voir la source de Théorème PCP

{{confusion | Problème de correspondance de Post}}

En [[théorie de la complexité (informatique théorique)|théorie de la complexité]], un domaine de l'[[informatique théorique]], le '''théorème PCP''' ([[acronyme]] de l'anglais ''probabilistically checkable proof'', qui peut se traduire en français par « [[Preuve vérifiable de manière probabiliste|preuve vérifiable en probabilité]] »<ref>{{Ouvrage|prénom1=Bernard H.|nom1=Korte|prénom2=Jens|nom2=Vygens|traducteur=Jean Fonlupt et Alexandre Skoda|titre=Optimisation combinatoire|sous-titre=Théorie et algorithmes|éditeur=[[Springer Science+Business Media|Springer-Verlag]]|année=2010|passage=443|isbn=|lire en ligne=https://books.google.fr/books?id=KkZ5liP7CFAC&pg=PA443}}</ref>) est une caractérisation de la classe '''[[NP (complexité)|NP]]''' dans le contexte d'un [[système de preuve interactive]]. Plus précisément, '''NP''' est la classe des [[Problème de décision|problèmes de décision]] qui ont des preuves pouvant être vérifiées de façon probabiliste en ayant accès à un nombre constant de bits de la preuve et en utilisant un nombre logarithmique de bits aléatoires.

Le théorème PCP est très important en informatique théorique : il apporte notamment de nombreux résultats sur la difficulté d'[[algorithme d'approximation|approximer]] les [[problème algorithmique|problèmes algorithmiques]]. 

== Présentation informelle ==

Le théorème PCP affirme que, si l'on tolère une marge d'erreur, il est inutile de lire une [[Démonstration (logique et mathématique)|démonstration]] en entier pour être convaincu de sa correction. On peut reformuler cette affirmation aussi comme suit : il existe une constante ''K'' telle que toute preuve mathématique ''P'' de longueur ''n'' peut être réécrite en une preuve ''P’'' de longueur polynomiale en ''n'', de sorte qu'il suffise d'examiner seulement ''K'' symboles de ''P’'' (à l'aide d'un [[algorithme randomisé]]) pour être convaincu de l'exactitude de la preuve à 99 %. 

=== « Le coup de la confiture » ===
[[Fichier:אירית.jpg|vignette|Irit Dinur]]
[[Fichier:Illustration du théorème PCP.png|vignette|Considérons une tranche de pain avec une goutte de confiture dessus. Il y a peu de chance de trouver la confiture en inspectant un échantillon du morceau de pain. Par contre, en étalant la confiture, on est quasiment sûr d'en trouver en inspectant un échantillon.]]


Lors de sa conférence plénière au [[congrès international des mathématiciens]] de 2010, [[Irit Dinur]] a utilisé<ref>La conférence plénière d'Init Dinur est accessible sur sa page personnelle, à l'adresse [http://www.wisdom.weizmann.ac.il/~dinuri/pubs.html Probabilistically Checkable Proofs (survey and talk)].</ref> une analogie pour faire comprendre ce théorème. Elle est rapportée en ces termes par [[Étienne Ghys]]<ref>Dans les termes du compte-rendu paru dans {{harv|Ghys|2010}}.</ref> : {{citation bloc|C’est un peu comme si vous avez une tranche de pain qui a peut-être quelque part, une petite goutte de confiture, mais vous ne savez pas où. Vous prélevez un bout de la tartine, au hasard, et vous ne trouvez pas de confiture ; pouvez-vous en déduire qu’il n’y a pas de confiture du tout ? Certainement pas, sauf si vous faites beaucoup d’échantillonnages. Mais si vous commencez par étaler la confiture sur la tranche de pain avec un couteau, elle se retrouvera un peu partout et il suffit d’en prendre un échantillon pour savoir s’il y avait ou pas une goutte de confiture. Ici, c’est la même chose. On part d’une preuve ''P'' qui possède quelque part, peut-être, une erreur. Il existe une manière d’« étaler » la preuve pour en construire une autre  ''P’'' dans laquelle les erreurs, s’il y en a, se sont « propagées » un peu partout et elles sont maintenant faciles à détecter en prenant un tout petit nombre d’échantillons.}}

=== Système PCP ===
Considérons le problème de vérifier une preuve pour un théorème mathématique. Puisque les preuves peuvent être longues et difficiles à vérifier dans leur intégralité, on peut chercher une façon de présenter une preuve de telle sorte qu'il suffise d'en vérifier une petite partie seulement pour juger la validité du théorème avec un niveau de confiance raisonnablement élevé. Cette question est abordée par des systèmes de [[preuve vérifiable de manière probabiliste]].

De manière informelle, un système de preuve vérifiable en probabilité (PCP) pour un langage est un ''vérificateur''  probabiliste en temps polynomial qui a un accès direct aux bits individuels d'un mot binaire. Ce mot, appelé ''oracle'', représente une preuve et ne sera examiné qu'en partie seulement par le vérificateur. Les questions posées à l'oracle sont des positions dans le mot binaire et des tirages à pile ou face qui peuvent éventuellement dépendre des réponses aux requêtes précédentes. C'est le vérificateur qui décide si une entrée donnée appartient au langage. Si l'entrée est dans le langage, on demande que le vérificateur accepte toujours le mot, pourvu qu'on lui fournisse un oracle adéquat. En d'autres termes, le vérificateur ne rejette jamais un mot qui est dans le langage. Sinon, si le mot n'est pas dans le langage, le vérificateur le rejette avec une probabilité supérieure à un demi, peu importe l'oracle utilisé.

On peut voir les systèmes PCP en termes de [[système de preuve interactive|systèmes de preuve interactifs]]. On considère alors l'oracle comme un ''prouveur'' (qui veut prouver l'énoncé), et les questions comme autant de messages qui lui sont envoyés par le vérificateur. Dans le cadre de la PCP, le prouveur est vu comme étant sans mémoire des questions précédentes, et ne tient donc pas compte, dans ses réponses, des questions posées précédemment.

Une interprétation plus intéressante est de voir les systèmes PCP comme une généralisation des vérificateurs pour la classe NP. Au lieu d'effectuer un calcul en temps polynomial à la réception de la preuve complète (comme dans le cas d'un vérificateur pour un problème de NP), on permet au vérificateur d'effectuer des tirages à pile ou face et d'examiner la preuve seulement aux emplacements de son choix. Ceci lui permet d'inspecter de longues preuves, en ne regardant pas plus qu'un certain nombre polynomial d'emplacements, ou de manière équivalente de ne regarder que très peu de bits d'une preuve.

Il est remarquable que les systèmes PCP permettent de caractériser entièrement les langages dans '''[[NP (complexité)|NP]]'''. Cette caractérisation s'est révélée utile par la connexion établie entre la difficulté d'approximation de quelques problèmes NP-difficiles et la question de l'égalité entre P et NP. Autrement dit, des résultats de non approximabilité pour divers problèmes d'optimisation classiques ont été établis en utilisant des systèmes PCP pour des langages de la classe NP<ref>{{lien web|auteur=Christian Scheideler|titre=Computational Models |url=http://www.cs.uni-paderborn.de/fachgebiete/fg-ti/lehre0/ss2013/rm0.html|consulté=16 juillet 2013}}.</ref>.

=== Énoncé ===

Les preuves vérifiables en probabilité donnent naissance à des classes de complexité selon le nombre de questions exigées et la quantité d'aléatoire utilisé. La classe '''PCP'''[''r(n),q(n)''] réfère à l'ensemble des problèmes de décision qui ont des preuves vérifiables en probabilité qui peuvent être vérifiées en temps polynomial avec au plus ''r(n)'' bits aléatoires et en lisant au plus ''q(n)''  bits de la preuve. Comme déjà dit plus haut, les preuves correctes doivent toujours être acceptées et des preuves incorrectes doivent être rejetées avec une probabilité d'au moins 1/2. Le théorème PCP énonce que 
:'''PCP'''[O(log ''n''), O (1)] = '''NP'''.

== Démonstration ==
Une démonstration d'un résultat plus faible, '''NP''' = '''PCP'''[n<sup>3</sup>, 1], est donnée dans un des cours de Dexter Kozen<ref>{{Ouvrage|langue=en|prénom1=Dexter C.|nom1=Kozen|titre=Theory of Computation|lieu=Londres|éditeur=[[Springer Science+Business Media|Springer-Verlag]]|collection=Texts in Computer Science|année=2006|pages totales=119–127|isbn=978-1-84628-297-3|lire en ligne=https://www.springer.com/gp/book/9781846282973}}</ref>.

== Application aux algorithmes d'approximation ==
Le théorème PCP a des conséquences importantes dans le domaine des [[algorithmes d'approximation]]. En particulier, il sert à montrer que les problèmes MAX-3SAT et Maximum Independent Set entre autres, ne peuvent pas être approximés efficacement, sauf si [[problème P=NP|P=NP]].

=== Exemple de MAX-3SAT ===

Le problème MAX-3SAT est le suivant : étant donné une formule 3CNF, c'est-à-dire en [[forme normale conjonctive]], dont chaque [[clause]] contient au plus 3 littéraux (comme dans le [[problème 3-SAT]]), quel est le nombre maximum de clauses pouvant être satisfaites par la même affectation des variables ?

Le résultat de difficulté d'approximation est le suivant<ref>{{Computational Complexity (Arora et Barak)|numéro chapitre=11.2.2|titre chapitre=PCP and hardness of approximation}}</ref> :
:Il existe une constante <math>\rho < 1</math> telle que l'existence d'un algorithme d'approximation pour MAX-3SAT de rapport d'approximation <math>\rho</math>, implique que P = NP.

Ceci est en fait un corollaire du théorème suivant :
:Il existe une constante <math>\rho < 1</math> telle que pour tout langage  <math>L \in NP</math>, il existe une fonction <math>f</math> allant des [[Chaîne de caractères|chaînes de caractères]] vers les formules 3CNF telle que <math>x \in L</math> implique que toutes les clauses de <math>f(x)</math> peuvent être satisfaites, et  <math>x \notin L</math> implique que la fraction de clauses satisfiables de <math>f(x)</math> est inférieure à <math>\rho</math>.

== Historique et importance ==
L'histoire du théorème commence dans les années 1980, avec des travaux sur les [[preuves à divulgation nulle de connaissance]] (''zero knowledge proof'') par Goldwasser, Micali, et Rackoff<ref name=tale>
{{article
 |auteur    = Dana Moshkovitz
 |titre     = The tale of the PCP theorem
 |périodique   = ACM Crossroads
 |volume    = 18 |numéro    = 3| passage     = 23-26
 |année   = 2012
 |lire en ligne=http://xrds.acm.org/article.cfm?aid=2090286}}</ref>. Ces résultats n'ont a priori rien à voir avec l'approximation, mais introduisent l'idée de prouveur et de vérificateur. Le lien entre la vérification de preuve et l'approximation est fait au début des années 1990, par Feige, Goldwasser, Lovász, Safra et Szegedy<ref name=tale/>.

En 2001, [[Sanjeev Arora]], [[Uriel Feige]], [[Shafi Goldwasser]], [[Carsten Lund]], [[László Lovász]], [[Rajeev Motwani]], [[Shmuel Safra]], [[Madhu Sudan]] et [[Mario Szegedy]] ont reçu le prestigieux [[prix Gödel]] pour leurs articles sur le théorème PCP {{Référence Harvard|Feige|Goldwasser|Lovász|Safra|1996}} {{Référence Harvard|Arora|Safra|1998}} {{Référence Harvard|Arora|Lund|Motwani|Sudan|1998}}<ref>[http://www.eatcs.org/index.php/component/content/article/507 Page officielle du prix Gödel 2001]</ref>.

En 2006, [[Irit Dinur]] a publié une preuve complètement nouvelle du théorème<ref>[http://www.sigact.org/Prizes/Godel/2009.html Page du prix Gödel 2009, pour le produit zig-zag de graphes, dont le dernier paragraphe porte sur la preuve de Dinur]</ref>, [[combinatoire]], utilisant notamment les [[graphe expanseur|graphes expanseurs]] {{Référence Harvard|Dinur|2007}}. Cette preuve lui a valu le [[prix Gödel]] 2019<ref>{{lien web |titre=2019 Gödel Prize |url=http://eatcs.org/index.php/component/content/article/1-news/2807-2019-03-12-20-31-09 |site=EATCS |consulté le=09-08-2020}}.</ref>. 

[[Ingo Wegener]]<ref name="Wegener2005">« ''The most important result in complexity theory since Cook's Theorem'' » dans : {{Ouvrage|langue=en|nom1=Wegener|prénom1=Ingo|lien auteur1=Ingo Wegener|titre=Complexity Theory|sous-titre=Exploring the Limits of Efficient Algorithms|éditeur=Springer|année=2005|pages totales=308|passage=161|isbn=978-3-540-21045-0|lire en ligne=https://books.google.com/books?id=1fo7_KoFUPsC&pg=PA161}}.</ref> a dit à propos de ce théorème qu'il était « le résultat le plus important en théorie de la complexité depuis le [[théorème de Cook]] ».
Pour [[Oded Goldreich]]<ref name="Goldreich2008">« ''A culmination of a sequence of impressive works [...] rich in innovative ideas'' » dans : {{Ouvrage|langue=en|auteur1=Oded Goldreich|titre=Computational Complexity|sous-titre=A Conceptual Perspective|lieu=Cambridge|éditeur=[[Cambridge University Press]]|année=2008|pages totales=606|passage=405|isbn=978-0-521-88473-0|lire en ligne=https://books.google.com/books?id=EuguvA-w5OEC&pg=PA405}}.</ref>, c'est « l'aboutissement d'une série de travaux impressionnants, riches en innovations ».

== Bibliographie ==
=== Articles ===
*{{article | nom1=Feige | prénom1=Uriel | nom2=Goldwasser | prénom2=Shafi | nom3=Lovász | prénom3=Laszlo | nom4=Safra | prénom4=Shmuel | nom5=Szegedy | prénom5=Mario | titre=Interactive proofs and the hardness of approximating cliques | url=http://groups.csail.mit.edu/cis/pubs/shafi/1996-jacm.pdf  | année=1996 | journal=Journal of the ACM  | volume=43 | numéro=2 | pages=268–292 | doi=10.1145/226643.226652}}

*{{article | nom1=Arora | prénom1=Sanjeev | nom2=Safra | prénom2=Shmuel | titre=Probabilistic checking of proofs: a new characterization of NP | url=http://www.cs.umd.edu/~gasarch/pcp/AS.pdf | année=1998 | journal=Journal of the ACM | volume=45 | numéro=1 | pages=70–122 | doi=10.1145/273865.273901 | archiveurl=https://web.archive.org/web/20110610101051/http://www.cs.umd.edu/~gasarch/pcp/AS.pdf | archivedate=10 juin 2011 }}

*{{article | nom1=Arora | prénom1=Sanjeev | nom2=Lund | prénom2=Carsten | nom3=Motwani | prénom3=Rajeev | nom4=Sudan | prénom4=Madhu | nom5=Szegedy | prénom5=Mario | titre=Proof verification and the hardness of approximation problems | url=https://www.cs.umd.edu/~gasarch/pcp/ALMSS.pdf  | année=1998 | journal=Journal of the ACM  | volume=45 | numéro=3 | pages=501–555 | doi=10.1145/278298.278306}}

*{{Article| prénom1= Irit| nom1= Dinur
 | lien auteur1 = Irit Dinur| titre= The PCP theorem by gap amplification
 | périodique= Journal of the ACM| volume= 54| numéro= 3| année= 2007| pages= 12
 | doi = 10.1145/1236457.1236459}}

=== Vulgarisation ===
*{{Article| prénom1 = Étienne| nom1= Ghys 
 | titre = Vérifier une preuve : la conférence de Irit Dinur
 | périodique = Images des Mathématiques| année = 2010
 | url=http://images.math.cnrs.fr/Verifier-une-preuve-la-conference,755.html}}

*{{Computational Complexity (Arora et Barak)|numéro chapitre=11|titre chapitre=PCP Theorem and Hardness of Approximation: An introduction}}

* {{article
 |auteur    = Dana Moshkovitz
 |titre     = The tale of the PCP theorem
 |périodique   = ACM Crossroads
 |volume    = 18 |numéro    = 3| passage     = 23-26
 |année   = 2012
 |lire en ligne=http://xrds.acm.org/article.cfm?aid=2090286}}

== Liens externes ==
{{Complexity Zoo|fin=P#pcp|nom=PCP}}

== Notes et références ==
<references />

{{Palette|Théorie de la complexité}}

{{Portail|Informatique théorique}}

{{DEFAULTSORT:Theoreme PCP}}
[[Catégorie:Théorème de la théorie de la complexité|PCP]]