Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Système de preuve interactive
Résumé
vignette|504x504px|Un système de preuve interactive est composé de deux machines abstraites : un prouveur et un vérificateur qui s'échangent des messages.
En théorie de la complexité des algorithmes, un système de preuve interactive est un protocole formel de démonstration de théorèmes qui fait intervenir deux participants qui échangent des messages. Cela permet de définir des classes de complexité intéressantes, notamment la classe IP qui est le modèle utilisé dans le théorème PCP qui caractérise la classe NP.
Formellement, un système de preuve interactive est une machine abstraite qui modélise un échange de messages entre deux protagonistes : un prouveur et un vérificateur ; ceux-ci communiquent afin que le prouveur convainque le vérificateur de la véracité d'une proposition qui porte sur l'appartenance ou la non-appartenance d'une chaîne de caractères à un langage formel donné. Le prouveur a des ressources de calcul illimitées tandis que le vérificateur a des ressources limitées. Les deux protagonistes interagissent aussi longtemps qu'il est nécessaire au vérificateur pour trouver une réponse au problème et être convaincu qu'elle est la bonne.
Deux propriétés doivent être satisfaites :
complétude : si le fournisseur de preuve et le vérificateur suivent le protocole alors le vérificateur doit toujours tôt ou tard accepter la preuve ;
consistance : si la proposition est fausse, la probabilité qu'un fournisseur de preuve malveillant puisse convaincre un vérificateur que la proposition est vraie est infime.
vignette|Un graphe colorié avec trois couleurs
La classe NP peut être redéfinie à l'aide de systèmes de preuve interactive. Un problème de décision (par exemple le problème de coloration avec trois couleurs) est dans NP s'il existe un système de preuve interactive tel que :
le prouveur est une machine déterministe sans limite de ressources qui construit, à partir de l'instance (par exemple un graphe à colorier) un certificat (une coloration des sommets) ;
le vérificateur est une machine déterministe en temps polynomial qui vérifie que le certificat est valide (que la coloration attribue des couleurs différentes aux sommets voisins).
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.