Résumé Technique : Mêmes Formules, Sémantiques Différentes

Énoncé du Problème

L'article traite d'une lacune critique dans l'évaluation des capacités de raisonnement des grands modèles de langage (LLM) concernant la logique modale. Alors que les benchmarks existants (par exemple, ProofWriter, FOLIO, LogicNLI) évaluent la déduction sous une logique de fond fixe et implicite, ils ne parviennent pas à tester si les modèles peuvent adapter leur raisonnement à des spécifications sémantiques explicitement énoncées. En logique modale, la validité d'une inférence dépend souvent de propriétés de cadre spécifiques (par exemple, réflexivité, transitivité, symétrie) ou de conditions de domaine (par exemple, domaines constants vs variables). Un modèle peut bien performer en apprenant un régime d'inférence dominant (une logique « familière » comme S5) plutôt qu'en adhérant aux contraintes spécifiques fournies dans le prompt. Le problème central est de déterminer si les LLM peuvent supprimer leurs intuitions logiques par défaut pour suivre des conditions sémantiques stipulées, potentiellement non standard.

Méthodologie

Les auteurs construisent un benchmark diagnostique conçu pour isoler le contrôle sémantique de la reconnaissance de formes formulaires.

1. Construction du Benchmark :

• Problèmes Appariés : Le jeu de données central consiste en des paires de problèmes où les prémisses ($P$) et la conjecture ($C$) sont identiques, mais la spécification sémantique ($S$) diffère exactement d'une condition (par exemple, remplacer un cadre réflexif par un cadre transitif, ou un domaine cumulatif par un domaine décroissant).
• Vérification par Oracle : Un oracle de raisonnement automatisé (utilisant Vampire et Leo-III via la chaîne d'outils d'intégration LET) vérifie que les deux spécifications produisent des valeurs de vérité opposées ($y_a \neq y_b$) pour la même formule.
• Noyau Équilibré : Pour empêcher les modèles d'exploiter un raccourci de type « condition uniquement » (où la réponse est déterminée uniquement par l'étiquette sémantique sans lire la formule), les auteurs ont créé un « noyau non imbriqué équilibré » de 160 paires. Dans ce sous-ensemble, chaque condition sémantique apparaît aussi souvent avec les étiquettes True et False. Le succès ici nécessite strictement de lire la formule pour déterminer quelle condition la valide.
• Portée : Le jeu de données couvre cinq contrastes de propriétés de cadre (K–D, K–T, T–B, T–S4, B–S5) et trois contrastes de domaine (variable–cumulatif, variable–décroissant, cumulatif–constant), totalisant 800 paires de systèmes imbriqués et 160 paires de noyaux équilibrés.
• Prompting : Les prompts utilisent un anglais contrôlé pour énoncer explicitement les règles (par exemple, « La relation d'accessibilité est réflexive et symétrique ») sans utiliser de noms de systèmes conventionnels (comme « S4 »), forçant le modèle à se fier aux règles fournies.

2. Protocole Expérimental :

• Modèles : L'étude évalue cinq modèles récents : DeepSeek V4 (Flash et Pro), GPT-5.6 (Luna et Terra), et Claude Sonnet 5.
• Conditions :
  • Prompt Direct : Inférence standard sans mode de raisonnement.
  • Mode de Raisonnement : Activé pour des modèles spécifiques (par exemple, DeepSeek Flash « high effort ») pour tester si l'augmentation du calcul au moment de l'inférence aide l'adhérence sémantique.
  • Sensibilité à la Représentation : Un sous-ensemble teste les performances à travers des conditions nommées en anglais, des définitions relationnelles et la syntaxe formelle TPTP.
  • Affinité Sémantique : Des expériences omettent les spécifications de cadre pour identifier quelle logique « par défaut » les modèles favorisent lorsqu'ils sont non contraints.

Résultats Clés

1. Échec du Contrôle Sémantique sous Prompt Direct :
Sur le noyau équilibré, quatre des cinq modèles ont performé de manière significative en dessous de la ligne de base de 50 % du « condition-only » (qui suppose que le modèle ignore la formule et devine en fonction de l'étiquette de la condition).

• DeepSeek V4 Flash : 4,4 % de précision stricte par paire.
• DeepSeek V4 Pro : 2,5 %.
• GPT-5.6 Luna : 21,2 %.
• GPT-5.6 Terra : 25,0 %.
• Claude Sonnet 5 : 65,0 % (le seul modèle dépassant la ligne de base).
  Cela indique que la plupart des modèles échouent à suivre les sémantiques énoncées, appliquant plutôt une logique fixe et familière, indépendamment des contraintes du prompt.

2. Le Mode de Raisonnement comme Mécanisme Restaurateur :
L'activation du mode de raisonnement a considérablement amélioré les performances de DeepSeek V4 Flash, faisant passer sa précision sur le noyau équilibré de 4,4 % à 88,1 %. Des gains similaires ont été observés pour GPT-5.6 Luna sur les problèmes de cadre. Cela suggère que l'échec n'est pas nécessairement un manque de connaissances logiques, mais un échec de l'activation du mode d'inférence correct pour traiter les contraintes spécifiques.

3. Affinité Sémantique et Défauts :
Lorsque les spécifications étaient omises, les modèles présentaient des affinités cohérentes avec des logiques familières (par exemple, DeepSeek Flash favorisait K, tandis que Sonnet favorisait K, et d'autres favorisaient T). Cependant, ces défauts n'ont pas prédit de manière fiable les erreurs lorsque des contraintes explicites étaient présentes ; les modèles étaient souvent d'accord sur des problèmes sous-spécifiés mais échouaient à s'ajuster lorsque les contraintes étaient ajoutées.

4. Sensibilité à la Représentation :
Le changement de format d'entrée (passant de conditions nommées à des définitions relationnelles ou TPTP) a modifié le classement des performances mais n'a pas restauré de manière cohérente le contrôle sémantique. Par exemple, la précision de GPT-5.6 Terra est passée de 38 % (nommé) à 6 % (définitions relationnelles), indiquant que le formatage de surface n'est pas une solution simple au problème sous-jacent d'adhérence sémantique.

Contributions Clés

• Benchmark Diagnostique : Introduction d'un cadre d'évaluation contrôlé qui maintient fixe le problème de l'objet tout en variant la spécification sémantique, spécifiquement conçu pour tester la « sensibilité à la spécification ».
• Noyau Équilibré : Conception d'un jeu de données novatrice qui élimine la possibilité de résoudre les problèmes en mappant les conditions sémantiques aux réponses sans lire la formule logique.
• Preuve Empirique de la Dépendance au Mode : Démonstration que la capacité à suivre les sémantiques modales est fortement dépendante du mode d'inférence (direct vs raisonnement), remettant en question la notion de capacités de raisonnement logique statiques chez les LLM.
• Libération de Ressources : Publication des formules, des artefacts de l'oracle, des contre-modèles et des réponses des modèles.

Signification et Revendications

L'article soutient que les benchmarks à sémantique fixe peuvent surestimer la robustesse du raisonnement des LLM. La conclusion principale est que la connaissance modale (connaître la logique) est distincte du contrôle sémantique (appliquer la logique spécifique donnée). Un modèle peut posséder les règles logiques nécessaires mais échouer à laisser une spécification locale gouverner sa réponse, revenant par défaut à un régime d'inférence familier.

Les auteurs revendiquent modestement que leur travail sépare ces deux capacités. Ils notent que si le mode de raisonnement peut restaurer la sensibilité aux interventions sémantiques, il ne garantit pas la correction des étapes de dérivation intermédiaires (par exemple, un modèle peut changer de logique correctement mais toujours dériver une conclusion fausse en raison d'une erreur de raisonnement). L'étude conclut que les évaluations futures doivent explicitement tester si les modèles peuvent s'adapter aux contraintes énoncées plutôt que de s'appuyer sur des hypothèses de fond fixes. L'article ne propose pas de nouvelles applications ou de changements architecturaux futurs, se concentrant strictement sur l'évaluation diagnostique des modèles actuels.