Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

Each language version is independently generated for its own context, not a direct translation.

🧠 Elenchus : Quand l'IA joue au "Diable" pour aider un expert à construire sa pensée

Imaginez que vous êtes un architecte expert (un humain) et que vous devez construire les plans d'une nouvelle ville (une base de connaissances). Traditionnellement, on vous demande de sortir vos plans déjà finis de votre tête et de les écrire. Le problème ? Vos idées sont souvent floues, contradictoires ou cachées dans votre esprit, et il est très difficile de les mettre par écrit sans se tromper.

Elenchus propose une méthode totalement différente. Au lieu de vous demander de "sortir" vos idées, il vous propose de les construire ensemble à travers un débat.

1. Le Jeu du "Proveur" et du "Sceptique"

Dans ce système, vous jouez le rôle du Proveur (celui qui avance des idées). L'Intelligence Artificielle (IA) joue le rôle du Sceptique (celui qui pose des questions pièges).

Le Sceptique (l'IA) ne cherche pas à vous battre ni à vous humilier. Il joue le rôle d'un détective de la logique. Il écoute ce que vous dites et cherche les failles.
- Exemple : Si vous dites "Tous les oiseaux volent" et "Le pingouin est un oiseau", le Sceptique va dire : "Attends, si ton pingouin est un oiseau, et que tous les oiseaux volent, alors ton pingouin devrait voler. Mais on sait qu'il ne vole pas. Il y a une contradiction ici !"
Le Proveur (vous) doit alors réagir. Vous avez trois options :
1. Retirer votre affirmation (admettre que vous aviez tort).
2. Affiner votre idée (préciser : "Tous les oiseaux sauf les pingouins volent").
3. Contester le Sceptique (lui expliquer pourquoi il a tort).

2. L'IA n'est pas un Oracle, c'est un "Miroir Défectueux"

C'est le point le plus important du papier. L'IA n'est pas infaillible. Elle peut se tromper et inventer des contradictions qui n'existent pas (ce qu'on appelle des "hallucinations").

Mais dans Elenchus, ce n'est pas grave.

Si l'IA invente un faux problème, vous (l'expert humain) direz : "Non, ce n'est pas une contradiction, tu as mal compris."
L'IA est donc un oracle défaillable : elle propose des pistes, mais c'est vous qui décidez de ce qui est vrai ou faux. Elle sert de catalyseur pour révéler ce qui était caché dans votre propre esprit.

3. De la conversation à la "Carte de la Vérité" (La Base Matérielle)

À la fin de la discussion, on ne garde pas juste le texte de la conversation. Le système transforme tout ce débat en une structure logique rigoureuse appelée "Base Matérielle".

Imaginez que chaque fois que vous acceptez une contradiction ou que vous affinez une règle, vous posez une brique dans un mur.

Ce mur n'est pas une simple liste de faits. C'est une carte qui montre comment vos idées sont liées.
Si vous changez une idée, la carte montre immédiatement quelles autres idées sont affectées.

Le papier montre que cette carte possède des propriétés mathématiques très précises (comme le fait que certaines règles ne s'appliquent pas toujours, ou que certaines idées sont indépendantes). C'est comme si la conversation avait créé une géométrie de la pensée.

4. L'Exemple Concret : Le Projet PROV-O

Pour tester leur système, les auteurs ont pris un document complexe de l'organisation mondiale du web (W3C) sur la "provenance" (comment on sait d'où vient une information).

Ils ont donné un petit paragraphe de texte à l'expert humain.
L'IA a joué au Sceptique pendant une seule session de dialogue.
Résultat : Ils ont réussi à extraire et structurer les règles de décision qui avaient pris des années à être définies par des centaines d'experts dans des milliers d'e-mails.

C'est comme si, en une heure de discussion avec un robot, on avait pu reconstruire l'histoire complète d'un projet qui a duré des années.

🌟 En résumé : Pourquoi c'est génial ?

On ne "mine" pas le savoir, on l'éclaire. Au lieu de chercher des pépites d'or dans votre cerveau (ce qui est difficile), on allume une lumière (le débat) pour voir ce qui est déjà là.
L'erreur est utile. Si l'IA se trompe, ce n'est pas un bug, c'est une occasion pour vous de préciser votre pensée.
La traçabilité totale. On sait exactement quelle phrase de la conversation a conduit à quelle règle finale. Plus de "boîte noire".
La logique vivante. Le résultat n'est pas une liste morte de règles, mais un système dynamique qui respecte les nuances de la pensée humaine (parfois, une règle s'applique, parfois non, selon le contexte).

En une phrase : Elenchus transforme un débat humain avec une IA en une carte logique précise, où chaque règle est solidement défendue et où chaque erreur de l'IA devient une opportunité de clarification pour l'humain.

Each language version is independently generated for its own context, not a direct translation.

Voici un résumé technique détaillé de l'article « Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues » de Bradley P. Allen, rédigé en français.

1. Problématique : La crise de l'acquisition des connaissances

L'article aborde le problème persistant de l'ingénierie des connaissances, défini comme la difficulté de formaliser les connaissances d'experts exprimées en langage naturel.

Limites des approches traditionnelles : Les méthodes actuelles (systèmes experts, ontologies, graphes de connaissances) reposent sur une conception « représentationaliste » erronée. Elles supposent que l'expert possède une structure formelle préexistante dans son esprit qu'il suffit d'extraire ou de transcrire.
Le constat de l'auteur : La connaissance n'est pas déterminée avant son articulation ; elle est constituée par des pratiques d'expression et de négociation. Le goulot d'étranglement réside dans l'incapacité des méthodes actuelles à capturer les relations inférentielles implicites plutôt que de simples déclarations de contenu.

2. Méthodologie : Elenchus et l'Explicitation Inférentialiste

L'auteur propose une alternative fondée sur la sémantique inférentialiste (Brandom, Hlobil), où la signification d'une phrase est définie par son rôle inférentiel (ce qui en découle, ce qui en est incompatible).

Le Protocole Elenchus

Elenchus est un protocole dialectique bilatéral (Prover-Skeptic) impliquant un expert humain et un adversaire basé sur un Grand Modèle de Langage (LLM).

Rôle de l'Expert (Répondant) : Développe une position bilatérale (un ensemble d'engagements $C$ et de dénis $D$ ) sur un sujet donné.
Rôle du LLM (Opposant) : Agit comme un oracle de dérivabilité défaisable. Il ne fournit pas de connaissances, mais propose des tensions (claims d'incohérence) entre les engagements et les dénis de l'expert.
Résolution : L'expert résout les tensions par :
1. Retrait (retraction) d'un engagement ou d'un déni.
2. Raffinement (refinement) d'une proposition pour dissoudre le conflit.
3. Contestation (contestation) de la tension proposée par le LLM (si l'incohérence n'est pas réelle).
Gestion de l'incertitude du LLM : Le LLM peut halluciner des tensions (faux positifs), mais l'autorité épistémique reste chez l'expert. Une tension n'entre dans la base de connaissances que si elle est acceptée par l'expert. Les faux négatifs (tensions manquées) sont un risque, mais l'architecture permet de structurer la connaissance même avec un seul session.

De l'État Dialectique à la Base Matérielle

Le système mappe les états du dialogue vers une Base Matérielle ( $B$ ) dans la logique NMMS (NonMonotonic MultiSuccedent) de Hlobil et Brandom.

Structure de la base : $B = \langle L_B, \vdash_B \rangle$ , où $L_B$ est un langage atomique et $\vdash_B$ est une relation de conséquence de base.
Relation de conséquence : $\Gamma \vdash_B \Delta$ signifie que la position consistant à affirmer $\Gamma$ tout en niant $\Delta$ est incohérente.
Propriété de Containment : La base satisfait la contrainte minimale de cohérence : affirmer et nier la même proposition est incohérent.
Composition de la relation : La relation $\vdash_B$ $⊢_{B}$ est l'union de deux ensembles :
1. $I$ (Implications Matérielles) : Découvertes dialectiquement (tensions acceptées).
2. $Cont$ (Contenue) : Norme pragmatique de cohérence bilatérale (affirmer et nier la même chose), présupposée par tout dialogue rationnel.

3. Contributions Clés

Le Protocole Elenchus : Une méthode opérationnelle pour transformer le dialogue expert-LLM en une structure formelle de connaissances, redéfinissant l'ingénierie des connaissances comme une « explicitation » plutôt qu'une extraction.
Mapping Formel : Une définition rigoureuse reliant les états dialectiques aux bases matérielles de la logique NMMS. Ce mapping satisfait la propriété de Containment et permet l'élaboration d'un vocabulaire logique explicite (connecteurs $\to, \land, \lor, \neg$ ) qui rend explicites les relations inférentielles négociées.
Implémentation et Étude de Cas : Une implémentation fonctionnelle utilisant Claude Code et GitHub pour le stockage persistant de l'état dialectique, appliquée à l'ontologie PROV-O (W3C).

4. Résultats : Étude de Cas PROV-O

L'approche a été testée sur la section 3.1 de la recommandation PROV-O (350 mots de spécification en prose).

Processus : Un expert (co-auteur de la spécification PROV) a interagi avec le LLM. Le dialogue a généré 19 engagements, 0 déni, et 9 implications matérielles acceptées après résolution de 7 défis.
Correspondance avec l'historique : Les tensions découvertes correspondent directement à des décisions de conception documentées dans une analyse rétrospective de 8820 e-mails et 152 téléconférences (Moreau et al., 2015).
Vérification par pyNMMS : Un raisonneur automatique (pyNMMS) a vérifié les propriétés structurelles de la base générée :
- Non-transitivité : La chaîne de déduction ne s'effondre pas (ex: l'entité n'implique pas automatiquement les termes étendus), reflétant la frontière entre le noyau et les extensions de PROV.
- Non-monotonie : L'ajout de contexte (ex: détails de la chaîne) peut invalider une inférence précédente, modélisant le passage d'une preuve « scruffy » à une preuve « proper ».
- Indépendance : Les résolutions de design pour différents défis sont inférentiellement indépendantes (pas de fuite d'inférence entre les vues : Données, Processus, Responsabilité).
- Conservatisme et Supraclassicité : L'ajout de vocabulaire logique via NMMS n'ajoute pas de nouvelles conséquences au niveau de la base, mais permet d'exprimer les relations existantes.

5. Signification et Impact

Révolution Épistémologique : Elenchus déplace le paradigme de l'ingénierie des connaissances. La base de connaissances n'est pas une description statique du monde, mais un enregistrement dynamique de ce qui a été articulé et défendu à travers le dialogue.
Gestion des LLM : L'article propose une nouvelle façon d'utiliser les LLM non pas comme générateurs de contenu (source de vérité), mais comme partenaires dialectiques dont les erreurs sont filtrées structurellement par l'autorité humaine. Cela transforme le problème des hallucinations en un mécanisme de filtrage naturel.
Traçabilité Complète : Contrairement aux bases extraites de corpus où la provenance est opaque, chaque implication dans la base Elenchus est traçable jusqu'à un mouvement spécifique du dialogue (une tension proposée et acceptée).
Fondation Logique Solide : En s'appuyant sur la logique NMMS, le système garantit que les connaissances générées possèdent des propriétés formelles vérifiables (non-monotonie, non-transitivité) qui correspondent aux besoins réels de modélisation des domaines complexes (comme la provenance des données), là où la logique classique échouerait.

En conclusion, Elenchus démontre qu'il est possible de construire des bases de connaissances formelles, structurées et vérifiables directement à partir du dialogue naturel, en utilisant la tension dialectique comme moteur de l'explicitation des relations inférentielles.