💬 NLP

Are LLMs Stable Formal Logic Translators in Logical Reasoning Across Linguistically Diversified Texts?

Cet article présente le benchmark SoLT et la méthode MenTaL pour remédier à l'instabilité des traducteurs de logique formelle basés sur les LLM face à la variation linguistique, démontrant qu'un mappage explicite entre concepts et symboles améliore considérablement la cohérence et la précision du raisonnement à travers divers entrées textuelles.

Auteurs originaux : Qingchuan Li, Jiatong Li, Zirui Liu, Mingyue Cheng, Yuting Zeng, Qi Liu, Tongxuan Liu

Publié 2026-02-02

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Qingchuan Li, Jiatong Li, Zirui Liu, Mingyue Cheng, Yuting Zeng, Qi Liu, Tongxuan Liu

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

L'idée principale : Le problème du « Badge Nom »

Imaginez que vous êtes un traducteur essayant de convertir une histoire écrite en anglais en un code strict qu'un robot peut comprendre. Le robot est très doué pour résoudre des énigmes, mais il ne comprend que des symboles spécifiques (comme A, B ou C). Il ne comprend pas les mots comme « chat », « félin » ou « minou ».

Le problème que cet article étudie est le suivant : Si l'histoire utilise différents mots pour la même chose, le traducteur est-il confus ?

Par exemple, si l'histoire dit « Le chat a faim » et plus tard « Le félin est fatigué », un humain sait qu'il s'agit du même animal. Mais l'article a découvert que les modèles de langage étendus (LLM) — les traducteurs IA — se trompent souvent. Ils pourraient traduire « chat » par le symbole A et « félin » par le symbole B.

Pour le solveur robotique, A et B sont deux animaux complètement différents. Le robot pense que l'histoire traite de deux créatures distinctes et échoue à résoudre l'énigme, même si la logique est parfaitement saine. L'article appelle cela la « dérive symbolique » (symbol drift).

L'investigation : Tester avec un texte « Caméléon »

Les chercheurs ont voulu voir si cela se produisait dans la réalité. Ils ont remarqué que la plupart des tests d'IA utilisent des textes très répétitifs (par exemple, en utilisant toujours le mot « chat » à chaque fois). C'est comme tester un traducteur avec un script qui ne change jamais son vocabulaire.

Pour corriger cela, ils ont construit un nouveau test appelé SoLT (Traduction Logique Symbolique).

L'analogie : Imaginez prendre une histoire standard et la passer dans une « Machine Caméléon ». Cette machine réécrit l'histoire de nombreuses façons sans en changer le sens. Elle remplace « chat » par « félin », transforme « Le chat a faim » en « C'est le félin qui a besoin de nourriture », ou passe de la voix active à la voix passive.
Le résultat : Lorsqu'ils ont soumis ces histoires « caméléons » aux traducteurs IA, les performances de l'IA se sont effondrées. Plus le langage variait, plus l'IA se trompait dans la cartographie des symboles, et moins le solveur robotique avait de chances de trouver la bonne réponse.

La solution : Le « Badge Mental » (MenTaL)

Les chercheurs ont réalisé que l'IA échouait parce qu'elle traduisait phrase par phrase sans conserver une liste globale de « qui est qui ».

Pour corriger cela, ils ont créé une nouvelle méthode appelée MenTaL (Table de Représentation Mentale).

L'analogie : Imaginez que le traducteur possède un tableau blanc à côté de lui. Avant de commencer à traduire l'histoire en code, il écrit une liste :
- Chat = Félin = Minou = Symbole A
- Chien = Chiot = Symbole B
Comment ça marche : Chaque fois que l'IA voit un nouveau mot (comme « félin »), elle vérifie d'abord le tableau blanc. Si elle voit que « félin » est déjà lié à « chat », elle utilise le même symbole (A). S'il s'agit d'un nouveau concept, elle ajoute une nouvelle ligne au tableau blanc.
Le résultat : En forçant l'IA à construire d'abord cette liste de « badges nom », les traductions sont devenues beaucoup plus stables. Le solveur robotique a enfin pu faire les liens, et la précision a augmenté de manière significative, même lorsque le texte était très diversifié.

Points clés à retenir

L'IA actuelle est fragile : Lorsque vous changez la formulation d'un problème logique (même légèrement), les traducteurs IA actuels brisent souvent la logique car ils traitent les synonymes comme des choses différentes.
Les anciens tests étaient trop faciles : La plupart des tests existants ne vérifiaient pas cela car ils utilisaient un langage répétitif. Le nouveau benchmark SoLT expose cette faiblesse.
Une solution simple fonctionne : En donnant à l'IA une « Table de Représentation Mentale » (une liste pour garder trace des synonymes), nous pouvons stopper la confusion. Cela fonctionne aussi bien pour les grands modèles d'IA fermés (comme GPT-4) que pour les modèles plus petits et open-source.

En résumé, l'article montre que pour qu'une IA soit un traducteur logique fiable, elle doit cesser de traduire mot par mot et commencer à tenir un « dictionnaire » cohérent de ce que les choses signifient, peu importe la façon dont les mots sont habillés.

Résumé technique : Les LLM sont-ils des traducteurs de logique formelle stables pour le raisonnement logique à travers des textes linguistiquement diversifiés ?

1. Définition du problème

Les systèmes de raisonnement logique utilisant les grands modèles de langage (LLM) emploient souvent un paradigme neuro-symbolique où le LLM traduit le langage naturel (NL) en logique formelle, laquelle est ensuite traitée par un solveur symbolique. Bien qu'efficace, cette approche repose lourdement sur la fidélité et la cohérence de l'étape de traduction. Une vulnérabilité critique, bien que sous-explorée, est la dérive de symbole (symbol drift) : l'incapacité des LLM à mapper des expressions sémantiquement équivalentes vers le même symbole logique lorsque ces expressions apparaissent sous différentes formes linguistiques (par exemple, synonymes, paraphrases ou variations syntaxiques).

Les benchmarks existants pour le raisonnement logique utilisent généralement un langage hautement uniforme, répétant souvent des formes de surface identiques pour les mêmes concepts. Par conséquent, ils ne parviennent pas à évaluer si les LLM peuvent maintenir une cohérence de symbole à travers des variations linguistiques réalistes. Cette lacune entraîne une surestimation de la robustesse des LLM, car le texte du monde réel exprime fréquemment le même concept à travers des formulations diverses, ce qui peut briser la chaîne de raisonnement et provoquer des erreurs de solveur.

2. Méthodologie

2.1 SoLT : Un benchmark pour la diversité linguistique

Pour remédier au manque d'évaluation de la stabilité de la traduction, les auteurs introduisent SoLT (Stability of Logical Translation). SoLT n'est pas un nouveau jeu de données créé de toutes pièces, mais une transformation systématique de jeux de données de raisonnement existants (LogicDeduction, ProntoQA, FOLIO, ProofWriter, ProverQA) utilisant une méthode de Diversification Linguistique Invariante à la Logique.

Le pipeline de diversification opère en trois étapes :

Identification des concepts répétés : Le système identifie les expressions de surface apparaissant plusieurs fois au sein d'un problème ( $freq_q(e) \ge 2$ ).
Construction de la stratégie de diversification : Pour chaque concept répété, le système génère des variantes à trois niveaux :
- Niveau lexical : Substitution par synonymes (via WordNet).
- Niveau phrasal : Paraphrase (via PPDB).
- Niveau de la phrase : Réécritures syntaxiques (ex: alternance actif-passif, reformulation à la troisième personne) utilisant des LLM.
Génération de candidats sous filtrage sémantique : Les candidats générés sont filtrés à l'aide de modèles puissants d'embedding de phrases (ex: BGE-large-en-v1.5) pour s'assurer que la similitude sémantique dépasse un seuil ( $\theta = 0.90$ ). Un LLM assemble ensuite le problème diversifié final, sélectionnant les candidats qui maximisent la diversité de surface tout en minimisant les formes répétées pour des concepts identiques.

La validation via les scores de similitude d'embedding et le scoring d'invariance logique par des humains ou des LLM (échelle de 1 à 5) confirme que SoLT préserve le sens sémantique et la structure logique tout en augmentant significativement la variation linguistique.

2.2 MenTaL : Un cadre guidé par la représentation mentale

Pour atténuer la dérive de symbole, les auteurs proposent MenTaL (Mental Representation Table-guided Translation). Inspiré par les théories cognitives de la représentation mentale, MenTaL guide explicitement le LLM pour construire et maintenir une Table de Représentation Mentale (MRT) durant le processus de traduction.

La MRT mappe les expressions sémantiquement équivalentes vers un symbole logique unifié ( $\sigma$ ). Le cadre définit trois opérations de mise à jour pour la table :

Extension : Assigner un nouveau symbole à un concept précédemment non vu.
Réutilisation : Mapper une nouvelle expression vers un symbole existant si elle est sémantiquement équivalente ( $e^{(i)} \equiv e^{(j)}$ ).
Vérification et Affinement : Ajuster les correspondances pour les chevauchements partiels ou les subsomptions (ex: mapper "émission populaire" vers un symbole atomique raffiné).

MenTaL peut être implémenté via :

Apprentissage en contexte (In-Context Learning) : Fournir des exemples de construction de la MRT dans le prompt pour les modèles fermés.
Apprentissage supervisé par ajustement fin (SFT) : Entraîner de plus petits modèles open-source (ex: LLaMA-3-8B) sur des traces de raisonnement générées par des modèles de haute performance utilisant MenTaL.

3. Contributions clés

Benchmark SoLT : Une méthode générale et un benchmark résultant qui réécrivent les jeux de données de raisonnement en formes diverses et logiquement équivalentes pour évaluer systématiquement la stabilité de la traduction sous la variation linguistique.
Cadre MenTaL : Une approche légère et généralisable qui impose une correspondance de symboles cohérente en organisant explicitement les relations concept-symbole dans une table de représentation mentale.
Analyse empirique : Des expériences approfondies démontrant que les LLM actuels souffrent d'une dérive de symbole omniprésente sous la diversité linguistique et que MenTaL atténue efficacement ce problème.

4. Résultats expérimentaux

4.1 Instabilité des LLM actuels

Les expériences sur SoLT utilisant quatre LLM (GPT-3.5, GPT-4, DeepSeek-V3, DeepSeek-R1) et trois solveurs symboliques révèlent une dégradation significative des performances :

Chute de la précision : Sous prompting direct, la précision chute substantiellement sur les entrées diversifiées (ex: de 0.51 à 0.24 en moyenne sur les tâches).
Score de dispersion de symbole (SDS) : Un nouveau métrique quantifiant la dérive de symbole. Le SDS augmente brusquement sur les entrées SoLT (indiquant une correspondance incohérente) tout en restant proche de zéro sur les jeux de données originaux.
Analyse d'erreurs : Le principal mode de défaillance est l'erreur de logique causée par une assignation de symbole incohérente, plutôt que par des erreurs de parsing ou d'exécution. Même de légères variations linguistiques (ex: substitution de synonymes) provoquent une dégradation claire de la précision.
Limites du réglage de prompt : Les simples ajustements de prompt ou les exemples few-shot encourageant la cohérence n'ont pas réussi à améliorer significativement les performances ou à réduire le SDS sur les tâches diversifiées.

4.2 Efficacité de MenTaL

L'application de MenTaL produit des gains de performance constants et stables :

Apprentissage en contexte : Pour les modèles de haute performance, MenTaL a réduit le SDS à presque zéro sur les tâches SoLT et a amélioré la précision jusqu'à 40,74 % (ex: sur ProntoQA).
Ajustement fin supervisé (SFT) : Pour le modèle plus petit LLaMA-3-8B, le SFT standard a amélioré la précision mais a échoué à réduire la dérive de symbole sur les données diversifiées. En revanche, le SFT basé sur MenTaL a atteint un SDS proche de zéro et une précision nettement plus élevée sur les jeux de données originaux et diversifiés, démontrant une forte généralisation à travers les solveurs et les tâches.
Attribution d'erreurs : Une analyse manuelle a confirmé qu'environ 50 % des erreurs corrigées par MenTaL étaient spécifiquement dues à une meilleure cohérence des symboles, validant l'efficacité ciblée du mécanisme.

4.3 Intensité de la diversification

Les expériences faisant varier l'« intensité de la diversification » (le nombre de phrases modifiées par problème) ont montré une baisse fluide et continue de la précision des LLM à mesure que l'intensité augmentait. Cela indique un effet cumulatif où le traitement de davantage de variantes sémantiques érode progressivement la capacité du modèle à maintenir un alignement de symboles cohérent.

5. Signification et affirmations

L'article affirme que négliger la diversité linguistique dans les benchmarks actuels occulte une faiblesse critique des traducteurs logiques basés sur les LLM : l'incapacité à maintenir une correspondance de symboles cohérente à travers des expressions variées. Cette « dérive de symbole » brise la cohérence logique dans des scénarios réels où les synonymes et les paraphrases sont courants.

La signification de ce travail réside dans :

Diagnostic : Fournir un outil systématique (SoLT) pour identifier et mesurer l'instabilité de la traduction que les benchmarks standards ne détectent pas.
Solution : Offrir une méthode pratique et généralisable (MenTaL) pour améliorer la robustesse des systèmes de raisonnement neuro-symboliques sans nécessiter de changements architecturaux des solveurs.
Fiabilité : Faire progresser le domaine vers un raisonnement logique plus fiable dans les applications réelles en garantissant que la stabilité de la traduction est maintenue malgré la variation linguistique.

Les auteurs concluent que bien que MenTaL améliore significativement la stabilité, le défi d'une correspondance de symboles cohérente reste un domaine de recherche clé, particulièrement à mesure que les LLM sont déployés dans des environnements complexes et linguistiquement diversifiés.