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.
Définitions
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.
NP
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). Il accepte l'instance dans ce cas (le graphe est bien coloriable avec trois couleurs) et la rejette sinon.
Protocoles d'Arthur-Merlin
La classe AM est une classe de complexité définie à l'aide de systèmes de preuve interactive, comme la classe NP, sauf que le vérificateur est une machine probabiliste en temps polynomial.
IP
La classe IP est la classe définie comme AM, c'est-à-dire que le vérificateur est une machine probabiliste en temps polynomial mais il y a un nombre de rounds d'échanges de messages entre le prouveur et le vérificateur.
Classes de complexité associées
Cette section est vide, insuffisamment détaillée ou incomplète. Votre aide est la bienvenue ! Comment faire ?
