💬 NLP

Sound and Complete Neurosymbolic Reasoning with LLM-Grounded Interpretations

Cet article présente un cadre de raisonnement neurosymbolique qui intègre les grands modèles de langage dans la fonction d'interprétation d'une logique paraconsistante, permettant un raisonnement formel sain et complet qui exploite les connaissances des LLM tout en localisant efficacement les contradictions pour prévenir l'explosion logique et améliorer les critères de référence de facticité.

Auteurs originaux : Bradley P. Allen, Prateek Chhikara, Thomas Macaulay Ferguson, Filip Ilievski, Paul Groth

Publié 2026-06-09

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Bradley P. Allen, Prateek Chhikara, Thomas Macaulay Ferguson, Filip Ilievski, Paul Groth

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Le gros problème : Intelligent mais peu fiable

Imaginez que vous avez un assistant brillant et encyclopédique (un grand modèle de langage, ou LLM) qui sait presque tout. Vous lui posez une question, et il vous donne une réponse convaincante. Mais parfois, il se trompe. Parfois, il vous donne deux réponses qui se contredisent (par exemple : « Ce médicament est sûr » et « Ce médicament est dangereux »).

Dans le monde de la logique traditionnelle, si vous avez une contradiction, tout le système s'effondre. C'est comme un programme informatique qui dirait : « Si A est vrai et A est faux, alors le ciel est vert et la lune est faite de fromage. » C'est ce qu'on appelle l'explosion logique, et cela rend le système inutile.

Les auteurs de cet article se sont posé la question suivante : Comment pouvons-nous utiliser cet assistant super intelligent mais parfois contradictoire pour nous aider à raisonner sur des faits sans que tout le système ne s'effondre ?

La solution : Un « ordinateur de Belnap » avec une touche d'originalité

Les auteurs ont construit un nouveau type de machine de raisonnement qu'ils appellent un ordinateur de Belnap. Voyez cela comme un juge très strict qui ne se contente pas de demander « Est-ce vrai ou faux ? », mais qui pose deux questions distinctes :

Peux-tu prouver que c'est vrai ?
Peux-tu prouver que c'est faux ?

Au lieu de forcer un « Oui » ou un « Non » unique, le système accepte quatre états possibles pour chaque information :

Vrai : Vous pouvez le prouver, mais vous ne pouvez pas prouver que c'est faux.
Faux : Vous pouvez prouver que c'est faux, mais vous ne pouvez pas prouver que c'est vrai.
Glut (Contradiction) : Vous pouvez prouver que c'est vrai ET vous pouvez prouver que c'est faux. (L'assistant est confus ou les faits sont en conflit).
Gap (Ignorance) : Vous ne pouvez pas prouver que c'est vrai ET vous ne pouvez pas prouver que c'est faux. (L'assistant ne sait pas).

Comment ça marche : Le duo de « Fact-Checkers »

L'article introduit une méthode appelée Évaluation de la factualité bilatérale. Imaginez que vous avez une équipe de deux vérificateurs de faits travaillant sur une seule affirmation :

Le Vérificateur A essaie de trouver des preuves pour vérifier l'affirmation.
Le Vérificateur B essaie de trouver des preuves pour réfuter (infirmer) l'affirmation.

Ils ne disent pas seulement « Vrai » ou « Faux ». Ils rendent compte avec un score :

Si A dit « Vérifié » et que B dit « Impossible de réfuter », l'affirmation est Vraie.
Si A dit « Impossible de vérifier » et que B dit « Réfuté », l'affirmation est Fausse.
Si les deux disent « Vérifié » et « Réfuté », nous avons un Glut (une contradiction).
Si les deux disent « Impossible de vérifier » et « Impossible de réfuter », nous avons un Gap (nous ne savons pas).

L'article montre qu'en utilisant cette approche « à deux côtés », le système devient bien meilleur pour repérer quand l'IA est confuse ou quand les faits sont désordonnés, plutôt que de simplement deviner.

Le tour de magie : Garder la logique en sécurité

La partie la plus impressionnante de l'article est la façon dont ils connectent cette IA désordonnée à une mathématique stricte. Habituellement, si vous branchez une IA « bruyante » dans un système de logique strict, les mathématiques se brisent.

Les auteurs ont prouvé mathématiquement qu'ils peuvent brancher l'IA directement dans la « définition de la vérité » de leur système logique sans en briser les règles.

L'analogie : Imaginez un système de feux de signalisation strict (la logique). Habituellement, le feu doit être soit Rouge, soit Vert. Les auteurs ont montré qu'ils peuvent installer une « caméra intelligente » (l'IA) qui dit parfois « C'est Rouge ET Vert » ou « Je ne sais pas ».
Le résultat : Même si la caméra est confuse, le système de feux de signalisation ne s'effondre pas. Il reconnaît simplement la confusion, maintient les feux fonctionnels pour les voitures qui ont des signaux clairs, et signale l'intersection confuse pour qu'un humain puisse l'examiner plus tard. Le système reste satisfaisable (il continue de fonctionner) même en présence de contradictions.

Test en conditions réelles : Le laboratoire de sécurité des médicaments

Pour prouver que cela fonctionne, les auteurs ont construit un prototype de système pour vérifier une base de données de règles médicamenteuses.

Ils ont injecté dans le système des règles comme « Tous les benzodiazépines sont non addictifs » (ce qui est médicalement faux).
Le système utilise l'IA pour vérifier ces règles par rapport à ses connaissances internes.
Le résultat : L'IA a signalé les fausses règles. Elle a trouvé 92 contradictions (gluts). Par exemple, elle savait que l'affirmation « Les opioïdes sont non addictifs » était un mensonge parce qu'elle pouvait à la fois vérifier la règle (depuis la base de données) et la réfuter (depuis ses connaissances médicales).
Crucialement : Le système ne s'est pas effondré. Il n'a pas dit « Tout est vrai maintenant ». Au lieu de cela, il a dit : « J'ai trouvé 92 erreurs spécifiques, mais le reste du système fonctionne toujours correctement. »

Le compromis : Qualité vs Quantité

L'article a identé un compromis. Lorsque le système utilise ce contrôle « à deux côtés » :

Il devient meilleur pour être juste (précision plus élevée).
Il répond à moins de questions (couverture moindre).

Pourquoi ? Parce que si l'IA est confuse ou ne sait pas, le système dit poliment : « Je ne suis pas sûr, je passe mon tour », plutôt que de deviner. C'est comme un médecin qui refuse de diagnostiquer un patient lorsque les symptômes sont peu clairs, plutôt que de deviner et de potentiellement nuire au patient.

Résumé

Cet article présente un moyen d'utiliser de puissants assistants d'IA pour des tâches de raisonnement sérieuses sans laisser leurs erreurs briser tout le système. En demandant à l'IA de vérifier à la fois la preuve et la réfutation, et en utilisant un type spécial de logique qui tolère les contradictions, ils ont construit un système capable de :

Repérer quand l'IA est confuse.
Identifier des erreurs spécifiques dans les bases de connaissances (comme de mauvaises règles médicales).
Continuer à fonctionner en toute sécurité même lorsque des contradictions existent, plutôt que de s'effondrer.

C'est un pont entre les connaissances désordonnées et humaines de l'IA et le monde strict et fiable de la logique formelle.

Résumé Technique : Raisonnement Neuro-Symbolique Sonore et Complet avec des Interprétations Fondées sur les LLM

Énoncé du Problème

Les grands modèles de langage (LLM) possèdent de vastes connaissances paramétriques mais souffrent d'incohérences et d'incomplétudes inhérentes, ce qui les rend peu fiables en tant que bases de connaissances autonomes pour le raisonnement formel. Les approches traditionnelles du raisonnement neuro-symbolique — telles que le prompting des LLM pour effectuer un raisonnement logique, l'utilisation de ces derniers pour générer des entrées symboliques pour des solveurs externes, ou leur ajustement fin (fine-tuning) sur des preuves — ne parviennent pas à fournir de garanties formelles concernant la correction (soundness) et la complétude (completeness) du processus de raisonnement lorsque les connaissances du LLM sont contradictoires. De plus, les méthodes d'évaluation de la facticité standard produisent généralement une valeur de vérité unique, occultant l'état épistémique du LLM (par exemple, s'il est incertain ou véritablement en conflit). Le défi central est de savoir comment intégrer les connaissances étendues d'un LLM dans un système de raisonnement formel tout en préservant les propriétés théoriques de la logique (correction et complétude) et en gérant efficacement les incohérences produites par le LLM.

Méthodologie

Les auteurs proposent un cadre qui intègre directement un LLM dans la fonction d'interprétation d'une logique paraconsistante, spécifiquement l'Analytic Containment (AC), une logique bilatérale capable de gérer les informations incohérentes sans explosion logique.

1. Évaluation de la Facticité Bilatérale

Au lieu de demander à un LLM d'assigner une valeur de vérité unique (Vrai/Faux), le système emploie une approche d'évaluation bilatérale. Un juge LLM est incité à évaluer indépendamment deux conditions pour une formule atomique $\phi$ :

Vérification ( $P^+$ ) : Le LLage peut-il vérifier $\phi$ ?
Réfutation ( $P^-$ ) : Le LLM peut-il réfuter $\phi$ ?

Les sorties sont mappées vers des valeurs de vérité de Kleene faible ( $t$ =vrai, $f$ =faux, $e$ =indéfini/inconnu). Celles-ci sont appariées pour former une valeur de vérité généralisée $\langle u, v \rangle \in V_3 \times V_3$ . Cela donne lieu à quatre états principaux :

$\langle t, f \rangle$ : Vérifié (Vrai).
$\langle f, t \rangle$ : Réfuté (Faux).
$\langle t, t \rangle$ : Glut (À la fois vérifié et réfuté ; incohérence).
$\langle f, f \rangle$ : Gap (Ni vérifié ni réfuté ; incertitude/ignorance).

Pour assurer la stabilité requise pour le raisonnement formel, un mécanisme de mise en cache ( $\zeta_c$ ) est utilisé, stockant la valuation des formules atomiques de manière immuable une fois calculée.

2. Interprétations Fondées sur les LLM

Le papier définit une interprétation fondée sur un LLM ( $I$ ) où l'interprétation des formules atomiques est déterminée par la fonction d'évaluation bilatérale mise en cache $\zeta_c$ .

Intégration Théorique : Les auteurs prouvent que pour chaque interprétation fondée sur un LLM, il existe une interprétation standard équivalente, et vice versa.
Préservation des Propriétés : Ils démontrent que la correction et la complétude du système de tableau analytique pour AC (spécifiquement $AC^{rQ}$ ) sont préservées même lorsque l'interprétation est fondée sur un LLM. Cela signifie que le raisonneur peut dériver des conclusions avec les mêmes garanties qu'une logique standard, malgré l'incohérence potentielle du LLM.

3. Implémentation : Un Ordinateur de Belnap

Les auteurs ont implémenté une preuve de concept d'un ordinateur de Belnap (un raisonneur conçu pour gérer les informations incohérentes) en Python.

Architecture : Il combine le raisonnement par chaîne avant (dérivation de nouveaux faits à partir de règles) avec la vérification de satisfaisabilité par tableaux.
Règle d'Évaluation LLM : Lors de la construction du tableau, une règle llm-eval interroge le juge LLM pour la valeur de vérité bilatérale des formules atomiques.
Gestion des Gluts : Lorsqu'un glut est détecté (par exemple, le système infère $P(a)$ mais le LLM le réfute), le tableau ne se ferme pas (ne produit pas d'explosion). Au lieu de cela, il maintient à la fois l'assertion et sa réfutation, localisant ainsi la contradiction.

Contributions Clés

Évaluation de la Facticité Bilatérale : Une méthode novatrice qui fait émerger l'état épistémique du LLM (cohérent, incohérent ou incertain) plutôt que de forcer une décision binaire, offrant des diagnostics plus exploitables que l'évaluation unilatérale.
Interprétations Fondées sur les LLM : Un cadre théorique qui intègre les LLM directement dans la sémantique formelle d'une logique paraconsistante, préservant la correction et la complétude du système de raisonnement sous-jacent.
Validation Empirique : Démonstration que l'évaluation bilatérale améliore les scores macro-F1 par rapport aux bases de référence unilatérales (d'environ 6 points de pourcentage) sur les benchmarks de facticité (GPQA et SimpleQA), bien qu'avec une couverture réduite en raison de l'abstention sur les cas incertains.
Système Pratique : Une implémentation fonctionnelle d'un ordinateur de Belnap qui détecte avec succès des erreurs médicalement significatives (gluts) dans une base de connaissances tout en maintenant la satisfaisabilité globale.

Résultats Expérimentaux

Les auteurs ont évalué l'approche en utilisant des jeux de données dérivés des benchmarks GPQA et SimpleQA avec divers LLM (modèles de pointe et modèles distillés).

Précision vs Couverture : L'évaluation bilatérale a obtenu un score macro-F1 plus élevé (environ 0,699 pour les modèles de pointe sur GPQA) par rapport aux bases de référence unilatérales (0,633), mais avec une couverture plus faible (0,589 contre 1,000). Le système s'abstient dans les cas incohérents ( $\langle t, t \rangle$ ) ou incertains ( $\langle f, f \rangle$ ), ce qui augmente la fiabilité sur les cas où il fournit une réponse.
États Épistémiques : Les expériences ont révélé que les LLM produisent fréquemment des gluts (incohérences) plutôt que des gaps. Par exemple, sur le jeu de données SimpleQA, les modèles GPT ont montré une forte tendance à la contradiction (taux de glut ~59 %), tandis que les modèles Claude étaient plus prudents (taux de gap plus élevés).
Cas d'Usage de la Sécurité Médicamenteuse : Le système a été appliqué à une base de connaissances de 228 affirmations et 712 déductions concernant la sécurité des médicaments.
- Il a détecté 92 gluts correspondant à des erreurs médicalement significatives (ex: inférer que les opioïdes ne sont pas addictifs ou que les bêta-bloquants sont sûrs pour les patients asthmatiques).
- Malgré ces 92 contradictions, le système est resté satisfaisable, localisant avec succès les erreurs sans provoquer d'explosion logique.
- L'analyse computationnelle a montré que la latence du LLM est le goulot d'étranglement dominant, mais que l'approche est scalable à des bases de connaissances de taille moyenne (100k+ énoncés) grâce aux optimisations standards comme la parallélisation et la mise en cache.

Signification et Revendications

Le papier affirme offrir un cadre théorique avec une implémentation pratique pour le raisonnement neuro-symbolique qui exploite les connaissances d'un LLM tout en préservant la correction et la complétude de la logique sous-jacente.

Changement de Paradigme : Contrairement aux travaux antérieurs qui tentent de faire raisonner les LLM en utilisant la logique, cette approche fait raisonner la logique en utilisant le LLM comme un oracle d'interprétation.
Robustesse : Le système est conçu pour des scénarios réels où les sources de connaissances sont intrinsèquement incohérentes. Il traite les contradictions non pas comme des erreurs fatales nécessitant une réparation, mais comme des états épistémiques localisés (gluts) pouvant être identifiés et gérés.
Diagnostics Actionnables : En distinguant les états de "conflit" (glut) et d'"ignorance" (gap), le système fournit aux applications en aval des informations spécifiques sur la raison pour laquelle une conclusion est incertaine, permettant une prise de décision plus conservatrice et sûre (ex: dans les contextes médicaux).
Scalabilité : Les auteurs soutiennent que si la latence de l'API LLM est actuellement le coût principal, la charge logique est minimale, et que le système est traitable pour des bases de connaissances à échelle de production en utilisant les techniques d'optimisation existantes des raisonneurs de logique de description.