💬 NLP

FregeLogic at SemEval 2026 Task 11: A Hybrid Neuro-Symbolic Architecture for Content-Robust Syllogistic Validity Prediction

Ce papier présente FregeLogic, une architecture hybride neuro-symbolique pour la tâche 11 de SemEval 2026 qui combine un ensemble de cinq LLM avec un solveur Z3 pour atténuer les biais de contenu et améliorer la prédiction de validité syllogistique, atteignant un score combiné de 41,88.

Auteurs originaux : Adewale Akinfaderin, Nafi Diallo

Publié 2026-04-21

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Adewale Akinfaderin, Nafi Diallo

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 Problème : Le Piège de la "Crédibilité"

Imaginez que vous demandez à un groupe d'experts (nos intelligences artificielles) de juger si un raisonnement est logique.

Exemple 1 (Logique) : "Tous les chats sont des mammifères. Tous les mammifères ont un cœur. Donc, tous les chats ont un cœur." -> Vrai.
Exemple 2 (Logique mais absurde) : "Tous les chats sont des avions. Tous les avions sont rouges. Donc, tous les chats sont rouges." -> Logiquement Vrai, même si c'est absurde dans la vraie vie.

Le problème, c'est que les IA (comme les humains) ont souvent du mal avec l'exemple 2. Leur cerveau "contaminé" par la réalité leur dit : "Attends, les chats ne sont pas des avions ! Donc le raisonnement est faux." C'est ce qu'on appelle l'effet de contenu. L'IA se laisse distraire par la "vraisemblance" du sujet au lieu de regarder la structure du raisonnement.

🛠️ La Solution : FregeLogic (Le Système Hybride)

Pour résoudre ce problème, les auteurs ont créé FregeLogic, un système qui mélange deux approches, comme un tribunal avec des jurés et un juge expert.

1. Le Jury des IA (L'Ensemble de Modèles)

Imaginez un jury composé de 5 experts (cinq modèles d'intelligence artificielle différents).

Chaque expert a une personnalité différente (certains sont plus littéraux, d'autres plus créatifs).
Ils votent pour dire si le raisonnement est "Vrai" ou "Faux".
Si 4 ou 5 experts sont d'accord, on suit leur avis. C'est simple et rapide.

2. Le Juge Mathématique (Le Solveur Z3)

Mais que se passe-t-il si le jury est divisé ? Par exemple, 3 experts disent "Vrai" et 2 disent "Faux".
C'est là que le système devient intelligent. Les auteurs ont remarqué que quand les experts ne sont pas d'accord, c'est souvent parce qu'ils sont piégés par l'effet de contenu (l'un trouve l'idée absurde, l'autre non).

À ce moment précis, le système fait appel au Juge Mathématique (le solveur Z3).

Ce juge est un robot pur et dur. Il ne connaît pas les chats, ni les avions, ni le monde réel.
Il traduit le texte en équations mathématiques pures (comme traduire une phrase en code binaire).
Il vérifie la logique stricte, sans aucune émotion ni préjugé.

🎯 La Stratégie : "Intervenir seulement quand c'est nécessaire"

Le génie de FregeLogic, c'est qu'il ne demande pas au Juge Mathématique de tout vérifier (ce serait trop lent et coûteux). Il ne l'appelle que quand le jury est en désaccord (le vote 3 contre 2).

Si le jury est d'accord (4-1 ou 5-0) : On suit le jury.
Si le jury est en désaccord (3-2) : On écoute le Juge Mathématique.

📊 Les Résultats : Pourquoi ça marche ?

Grâce à cette méthode, le système a obtenu d'excellents résultats :

Moins d'erreurs dues aux préjugés : En écoutant le Juge Mathématique sur les cas difficiles, le système a réduit son "effet de contenu" de 16 %. Il est devenu plus objectif.
Plus de précision : La précision globale a légèrement augmenté.
La clé du succès : Pour que le Juge Mathématique fonctionne, il faut qu'il comprenne bien la phrase. Les auteurs ont utilisé une astuce pour forcer les IA à extraire la structure logique sous forme de "JSON" (un format très propre), ce qui a réduit les erreurs de compréhension de 22 % à presque 0 %.

🏁 En Résumé

Imaginez que vous essayez de résoudre une énigme logique.

Si vous avez une équipe de 5 amis qui sont tous d'accord, vous les écoutez.
Mais si votre équipe commence à se disputer parce que l'énigme parle de quelque chose d'absurde (comme "des chats qui volent"), vous appelez un mathématicien qui ne regarde que les règles du jeu, pas le sujet.

FregeLogic est cette combinaison parfaite : l'intuition rapide des IA pour la majorité des cas, et la rigueur froide des mathématiques pour corriger les erreurs quand les IA se trompent à cause de leur imagination. C'est un peu comme avoir un assistant qui pense vite, mais qui sait quand appeler un expert pour vérifier les faits !

1. Problématique et Contexte

Le papier aborde le défi de la prédiction de validité des syllogismes (SemEval-2026, Tâche 11, Sous-tâche 1). Le problème central n'est pas seulement la capacité de raisonnement logique, mais la lutte contre les effets de contenu (content effects).

Définition : Les effets de contenu désignent la tendance des modèles de langage (LLM) à laisser leur jugement logique être influencé par la crédibilité ou la plausibilité du monde réel des prémisses, plutôt que par la structure logique pure.
Objectif : Développer un système capable de prédire si un syllogisme est valide ou invalide avec une haute précision tout en minimisant l'impact de la plausibilité sémantique sur la décision.
Métrique : La performance est évaluée via un score combiné qui pénalise logarithmiquement les biais de contenu : $Score = \frac{Précision}{1 + \ln(1 + CE)}$ , où $CE$ est l'effet de contenu.

2. Méthodologie : Architecture Hybride Neuro-Symbolique

L'approche proposée, FregeLogic, est une architecture hybride qui combine la flexibilité des LLM avec la rigueur des solveurs de logique formelle. Elle repose sur trois composants principaux :

A. Un Ensemble de Classificateurs LLM

Composition : Un ensemble de 5 classificateurs utilisant trois modèles open-weight accessibles via Amazon Bedrock : Llama 4 Maverick, Llama 4 Scout et Qwen3-32B.
Diversité : Chaque classificateur est associé à une stratégie de prompt différente (Zero-shot, Few-shot, Few-shot avec Chaîne de Pensée (CoT), et Simple CoT).
Fonctionnement : Pour chaque syllogisme, les 5 modèles votent (0 pour invalide, 1 pour valide). La décision par défaut est le vote majoritaire.

B. Un Solveur Formel (Z3 SMT)

Rôle : Agit comme un vérificateur de logique formelle neutre au contenu.
Pipeline :
1. Extraction de structure : Un LLM extrait la structure logique du syllogisme (termes, prémisses, conclusion) sous forme de JSON structuré. L'utilisation d'une API à sortie structurée a réduit les taux d'échec d'extraction de ~22 % à presque 0 %.
2. Encodage FOL : Les propositions sont encodées en logique du premier ordre (FOL) avec une interprétation aristotélicienne (incluant des axiomes d'existence pour les termes sujets des propositions universelles).
3. Vérification : Le solveur Z3 vérifie la satisfiabilité. Un syllogisme est valide si les prémisses sont satisfaisables et que l'ajout de la négation de la conclusion rend le système insatisfaisable (UNSAT).

C. Module de Décision de « Tiebreaker » (Départage)

Hypothèse centrale : Les désaccords étroits au sein de l'ensemble (vote 3-2) signalent des cas où le biais de contenu interfère avec le jugement logique.
Mécanisme :
- Si le vote de l'ensemble est unanime ou large (4-1 ou 5-0), le vote majoritaire est conservé.
- Si le vote est serré (3-2), le système consulte le verdict du solveur Z3. Si Z3 fournit une réponse valide, elle remplace le vote de l'ensemble.
Stratégie : Cette intervention sélective permet de corriger les erreurs biaisées sans introduire les erreurs d'extraction de Z3 sur les cas où l'ensemble est déjà sûr.

3. Contributions Clés

Intégration Neuro-Symbolique Ciblée : Démonstration que l'application de la vérification formelle uniquement sur les cas de faible consensus (désaccords) améliore les métriques globales, contrairement à une approche purement symbolique ou purement neuronale.
Pipeline d'Extraction Robuste : L'utilisation de l'API de sortie structurée d'Amazon Bedrock pour l'extraction de la structure logique a éliminé pratiquement les échecs de parsing, un goulot d'étranglement majeur dans les approches précédentes.
Validation de l'Interprétation Aristotélicienne : Le papier confirme empiriquement que l'ajout d'axiomes d'existence (import existentiel) est nécessaire pour correspondre aux annotations du jeu de données, en particulier pour les syllogismes de type Felapton.
Analyse des Biais : Identification que les erreurs de Z3 proviennent presque exclusivement de l'étape d'extraction (mauvaise identification des types de propositions ou des limites des termes) et non du solveur lui-même.

4. Résultats Expérimentaux

Les résultats ont été obtenus via une validation croisée imbriquée en 5 plis sur un jeu de données de 960 syllogismes.

Performance Globale :
- Score Combiné : 41,88 (contre 39,12 pour l'ensemble pur).
- Précision : 94,3 % (gain de 0,9 % par rapport à l'ensemble pur).
- Effet de Contenu (CE) : Réduit de 3,39 à 2,85 (une réduction de 16 %).
Analyse par Sous-groupe :
- La stratégie de départage améliore particulièrement la précision sur les cas invalide-plausible (de 90,2 % à 94,5 %), là où le biais de contenu est le plus fort.
- L'approche équilibre mieux les performances entre les groupes valides et invalides que l'ensemble seul ou Z3 seul.
Comparaison des Stratégies :
- L'utilisation de Z3 comme veto systématique ou sur des consensus plus larges (4-1) dégrade les performances car Z3 a un biais vers l'invalide (due aux erreurs d'extraction sur les syllogismes valides).
- La stratégie de départage (3-2 uniquement) est la seule à maximiser le score combiné.

5. Signification et Conclusion

Le papier FregeLogic démontre que les modèles de langage, bien qu'ayant développé des circuits de raisonnement, restent vulnérables aux biais de connaissance du monde. L'approche hybride proposée offre une solution élégante :

Elle utilise les LLM pour la flexibilité et la compréhension du langage naturel.
Elle utilise la logique formelle comme un « arbitre » pour les cas ambigus où le biais sémantique perturbe le consensus.

Limitations et Perspectives :

Le système dépend toujours de l'extraction par LLM, qui reste la source principale d'erreurs résiduelles (11 cas de « faux rejets » de syllogismes valides).
La complexité de mise en œuvre est élevée (sélection de modèles et de prompts par pli, appels API multiples).
L'étude ouvre la voie à l'exploration de seuils de vote adaptatifs et à la généralisation de ce mécanisme de départage à d'autres tâches de raisonnement.

En résumé, FregeLogic prouve qu'une intégration neuro-symbolique sélective et contextuelle est plus efficace qu'une approche monolithique pour atténuer les effets de contenu dans le raisonnement logique.