Modèles et conséquence logique

L’essentiel de ce site estime des quantités incertaines. Ce parcours pose une autre question : étant donné ce qu’un système sait déjà, qu’est-ce qui doit être vrai ? Cette question a une réponse définie, et la machinerie qui la calcule est la logique.

Trois définitions

Une base de connaissances (BC) est un ensemble de phrases affirmées vraies. Un modèle est une assignation complète de valeurs de vérité à chaque symbole - un monde possible entièrement spécifié. En notant $M(\alpha)$ l’ensemble des modèles où $\alpha$ est vraie, la relation centrale est la conséquence logique :

$$\text{KB} \models \alpha \quad\text{iff}\quad M(\text{KB}) \subseteq M(\alpha).$$

Autrement dit : $\alpha$ tient dans tout modèle où la BC tient. L’image de Russell & Norvig mérite d’être retenue. Voyez les conséquences de la BC comme une meule de foin et $\alpha$ comme une aiguille : la conséquence logique, c’est que l’aiguille est dans la meule ; l’inférence, c’est la procédure qui l’y trouve. La première est un fait de signification, la seconde un algorithme, et on peut en parler séparément.

La décider par énumération

Trois cases peuvent chacune contenir un puits : il y a donc $2^3 = 8$ mondes possibles. La BC dit deux choses : il n’y a pas de vent en $[1,1]$, donc sa voisine $[1,2]$ est saine ; et il y a du vent en $[2,1]$, donc au moins l’une de $[2,2]$, $[3,1]$ contient un puits.

Trois modèles survivent. Lisez-y maintenant les conclusions :

• « pas de puits en $[1,2]$ » est vraie dans les trois, donc elle est entraînée ;
• « pas de puits en $[2,2]$ » est fausse dans deux d’entre eux, donc elle n’est pas entraînée ;
• et sa négation ne l’est pas non plus, puisqu’elle est vraie dans le troisième.

Ne pas entraîner $\alpha$ n’est pas entraîner $\lnot\alpha$. Deux des trois modèles mettent un puits en $[2,2]$ et un n’en met pas : les indices ne tranchent tout simplement pas cette case. Annoncer « pas de puits » ou « puits » serait dans les deux cas une affirmation que la BC ne soutient pas - la réponse honnête est que c’est indéterminé.

Essayez-le en direct. Énumérez les huit mondes et laissez la définition de la conséquence répondre aux trois questions à votre place :

Cette procédure - énumérer tous les modèles, vérifier que $\alpha$ tient partout où la BC tient - est la vérification de modèles, transcription directe de la définition.

Les huit mondes sont dans la figure ci-dessous, les trois qui survivent à la base de connaissances étant marqués. Choisissez une conclusion et le tableau marque quelque chose de plus utile encore : chaque monde survivant où cette conclusion est fausse. Pour « pas de fosse en [2,2] » il y en a deux, et chacun est un monde parfaitement compatible avec tout ce qui est su - c’est cela que signifie « non impliquée », et c’est pourquoi affirmer le contraire serait tout aussi peu fondé. Désactivez une phrase de la base et regardez l’ensemble survivant grandir.

Correcte, complète et coûteuse

Dès lors que l’inférence est une procédure et non une définition, deux propriétés comptent. Une procédure est correcte (Russell & Norvig disent aussi préservant la vérité) si tout ce qu’elle dérive est réellement entraîné : elle n’annonce jamais la découverte d’une aiguille qui n’existe pas. Elle est complète si elle dérive tout ce qui est entraîné : elle n’en manque jamais.

La vérification de modèles est les deux - correcte parce qu’elle implémente la définition, complète parce qu’elle examine tous les modèles. Le problème est le coût : $n$ symboles donnent $2^n$ modèles, et Russell & Norvig consignent que la conséquence propositionnelle est co-NP-complète : le comportement exponentiel dans le pire cas est intrinsèque, non une faiblesse de cet algorithme. Nos trois symboles ont donné huit lignes ; trente en donneraient plus d’un milliard.

C’est la motivation de la leçon suivante. Un démonstrateur par résolution n’énumère pas de mondes du tout - il manipule les phrases syntaxiquement, dérivant des conclusions avec une seule règle d’inférence. Ce qu’aucun raisonneur pratique ne fait, c’est construire la table entière : les solveurs SAT de type DPLL explorent bien des affectations de vérité, mais une affectation partielle à la fois.

Avant le quiz

Sachez énoncer la conséquence comme une inclusion entre ensembles de modèles, mener une petite énumération et lire ce qu’elle tranche ou non, définir séparément correction et complétude, et dire pourquoi la vérification de modèles est exacte et pourtant impraticable. L’article La logique et la représentation des connaissances couvre le même terrain plus longuement.