💬 NLP

Fixing FOLIO and MALLS: Verified Annotations and an LLM-assisted Framework to Focus Human Relabeling

Cet article révèle des erreurs d'annotation significatives dans les benchmarks NL-vers-FOL FOLIO et MALLS, publie des vérités de terrain corrigées qui améliorent substantiellement les métriques d'évaluation des LLM, et propose un cadre assisté par LLM qui permet un réétiquetage humain efficace pour atteindre une haute précision de l'ensemble de données avec un effort de révision minimal.

Auteurs originaux : Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, Nicola Saccomanno

Publié 2026-06-03

📖 4 min de lecture☕ Lecture pause café

CC BY 4.0

Auteurs originaux : Andrea Brunello, Cristian Curaba, Luca Geatti, Michele Mignani, Angelo Montanari, Nicola Saccomanno

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

Imaginez que vous essayez d'apprendre à un robot à comprendre la logique humaine. Pour ce faire, vous lui donnez un manuel rempli d'histoires écrites en anglais courant, accompagnées de leurs « traductions mathématiques » dans un langage strict appelé la Logique du Premier Ordre (LPO). Le robot étudie ces paires pour apprendre à traduire de nouvelles histoires de lui-même.

Ce document traite de la découverte que le manuel était truffé de fautes de frappe et d'erreurs, et de la création d'une méthode plus intelligente pour le corriger sans avoir à relire chaque page à la main.

Voici la décomposition de ce que les chercheurs ont découvert et accompli :

1. Le Problème : Le « Manuel » était défectueux

Les chercheurs ont examiné deux ensembles de données populaires (FOLIO et MALLS) que tout le monde utilise pour tester ces robots d'IA. Ils ont agi comme une équipe d'éditeurs rigoureux passant en revue les corrigés.

La Découverte : Ils ont découvert qu'environ 39 % des réponses dans FOLIO et 36 % dans MALLS étaient en réalité fausses.
- Certaines traductions n'étaient que du charabia (erreurs de syntaxe).
- Certaines étaient des absurdités logiques (erreurs sémantiques).
- Certaines phrases en anglais original étaient si vagues qu'elles pouvaient être interprétées de plusieurs manières, mais le manuel ne donnait qu'une seule réponse.
La Conséquence : Parce que la « clé de correction » était brisée, les robots étaient notés injustement. Un robot pouvait avoir donné une traduction parfaitement correcte, mais parce qu'elle ne correspondait pas à la mauvaise réponse du livre, il était sanctionné.
La Correction : L'équipe a corrigé manuellement ces erreurs. Lorsqu'ils ont retesté les meilleurs modèles d'IA en utilisant les nouveaux corrigés corrects, les scores des robots ont bondi de manière spectaculaire, de 9 à 22 points de pourcentage. Il s'est avéré que les robots étaient plus intelligents que nous le pensions ; c'était le test qui était défectueux.

2. Le Défi : On ne peut pas lire chaque page

Maintenant que l'équipe savait que les livres étaient désordonnés, elle a été confrontée à un nouveau problème : Comment corriger une immense bibliothèque de livres sans passer 100 ans à lire chaque page ?

Si vous embauchez un humain pour vérifier chaque traduction, cela coûte trop de temps et d'argent. Si vous laissez un ordinateur les vérifier, les ordinateurs ne sont pas encore parfaits pour comprendre la nuance humaine.

3. La Solution : La stratégie du « Contrôle par échantillonnage »

Les chercheurs ont inventé un système d'assistant intelligent (un cadre assisté par LLM) qui agit comme un détecteur de métaux pour les erreurs.

Au lieu de demander à un humain de vérifier chaque page, le système fonctionne comme suit :

L'éclaireur IA : Une IA puissante lit la traduction et demande : « Est-ce que cela me semble correct ? »
Le Filtre :
- Si l'IA dit : « Cela semble parfait », l'humain passe à la suite. (Les chercheurs ont constaté que l'IA est très douée pour repérer les réponses correctes ; elle signale rarement une bonne réponse comme étant mauvaise).
- Si l'IA dit : « Cela semble suspect », ou « Je ne suis pas sûr », elle place un drapeau rouge sur cette page.
L'Expert Humain : Le réviseur humain ne regarde que les pages portant des drapeaux rouges.

4. Le Résultat : Faire moins, obtenir plus

Cette méthode de « contrôle par échantillonnage » a été incroyablement efficace.

Ancienne Méthode (Vérification aléatoire) : Pour obtenir un ensemble de données précis à 90 %, un humain devrait lire entre 70 % et 74 % de toute la bibliothèque.
Nouvelle Méthode (Échantillonnage intelligent) : En ne regardant que les pages signalées comme suspectes par l'IA, l'humain a atteint 90 % de précision après n'avoir lu que 13 % à 24 % de la bibliothèque.

Ce qu'il faut retenir

Voyez cela comme la recherche d'une aiguille dans une botte de foin.

Avant : On vous disait de sortir chaque morceau de foin un par un pour trouver les aiguilles.
Maintenant : Vous avez un aimant (l'IA) qui attire le métal (les erreurs). Vous n'avez qu'à inspecter le métal que l'aimant a trouvé.

L'article conclut qu'en utilisant l'IA pour guider l'attention humaine vers les erreurs les plus probables, nous pouvons nettoyer des ensembles de données massifs beaucoup plus rapidement et à moindre coût, garantissant que les futurs systèmes d'IA soient entraînés sur des informations de haute qualité et précises. Ils ont publié les ensembles de données corrigés ainsi que le code de ce système de « contrôle par échantillonnage » afin que d'autres puissent l'utiliser.

Résumé technique : Correction de FOLIO et MALLS

Énoncé du problème

La traduction du langage naturel (NL) vers la logique du premier ordre (FOL) est une composante critique de l'IA neurosymbolique et de l'inférence de langage naturel (NLI). Cependant, la qualité des benchmarks existants utilisés pour entraîner et évaluer ces systèmes n'a pas été rigoureusement auditée. Cet article identifie que les jeux de données largement utilisés, spécifiquement FOLIO et MALLS, contiennent des erreurs d'annotation significatives et des ambiguïtés dans leurs étiquettes de vérité de terrain (ground truth). Ces erreurs faussent l'évaluation des grands modèles de langage (LLM) de pointe, conduisant à des mesures de performance inexactes. De plus, l'examen manuel exhaustif de grands jeux de données est trop coûteux et ne peut passer à l'échelle, nécessissant une méthode plus efficace de curation de données.

Méthodologie

1. Audit humain systématique et correction

Les auteurs ont mené une inspection humaine systématique de la division de validation de FOLIO (275 instances) et d'un sous-ensemble du ensemble de test de MALLS (100 instances). Deux réviseurs expérimentés (étudiant en doctorat et chercheur associé) ont annoté les données de manière indépendante, recoupé les résultats et résolu les conflits par consensus.

Gestion de l'ontologie : Étant donné que les jeux de données manquent d'ontologies explicites, les auteurs ont extrait les signatures (prédicats, arités, constantes) des formules FOL et ont utilisé un LLM pour assigner des significations en langage naturel, suivies d'une vérification manuelle. Ils ont distingué les incohérences (conflits d'arité/sens), qui ont été corrigées, de la lâcheté ontologique (conventions non conventionnelles mais cohérentes), qui a été préservée pour éviter de réécrire l'intégralité du jeu de données.
Classification des erreurs : L'audit a catégorisé les erreurs en :
- Erreurs syntaxiques : Discordances de parenthèses, fautes de frappe, mauvais usage de l'ontologie (10,5 % dans FOLIO, 3 % dans MALLS).
- Erreurs sémantiques : Formules valides qui représentent mal le sens du NL, incluant des erreurs de portée de quantificateur et des informations manquantes (28,3 % dans FOLIO, 33 % dans MALLS).
- Ambiguïtés : Phrases en NL admettant plusieurs formalisations non équivalentes mais défendables (16,4 % dans FOLIO, 48 % dans MALLS).
- Incohérences d'étiquetage NLI : Étiquettes (Vrai/Faux/Inconnu) incohérentes avec les formalisations fournies (8,4 % dans FOLIO).
Groupe de contrôle : Les auteurs ont également examiné 213 instances du jeu de données GGC (Barker-Plummer et al., 2011b), un corpus de haute qualité validé par des instructeurs, pour vérifier que leur cadre de curation n'introduit pas de bruit dans des données déjà correctes.

2. Cadre de supervision assisté par LLM

Pour répondre au problème de passage à l'échelle de la revue manuelle, les auteurs proposent un cadre utilisant les LLM pour prioriser l'effort humain.

Tâche de Verdict et de Raffinement (V&R) : Un LLM est chargé d'évaluer un triplet $(p, \Omega, \phi)$ $(p, Ω, ϕ)$ — où $p$ $p$ est une phrase en NL, $\Omega$ $Ω$ est une ontologie, et $\phi$ $ϕ$ est une formule FOL candidate. Le LLM produit :
1. Un verdict $v \in \{yes, no, ?\}$ (correct, incorrect, ou ambigu/incertain).
2. Un raffinement $\psi$ (une formule corrigée si $v \neq yes$ ).
Pipelines : Deux conceptions de pipelines ont été testées :
- Pipeline 1 (V&R Direct) : Le LLM juge directement la formule originale $\phi$ .
- Pipeline 2 (Régénération) : Le LLM génère d'abord un nouveau candidat $\hat{\phi}$ à partir de $p$ et $\Omega$ , puis juge ce nouveau candidat.
Stratégie de Priorisation : Le cadre tire parti du constat empirique selon lequel les LLM signalent rarement des formalisations correctes comme étant incorrectes (taux de faux positifs $\approx 3 \%$ dans FOLIO). En dirigeant les réviseurs humains vers les instances marquées comme "no" (incorrect) ou "?" (ambigu) en priorité, le cadre vise à maximiser les gains de précision par unité d'effort humain.

Contributions Clés

Jeux de données corrigés : Les auteurs ont publié les vérités de terrain révisées pour la division de validation de FOLIO et un sous-ensemble du test de MALLS, corrigeant respectivement 39 % et 36 % des entrées, ainsi que les étiquettes NLI corrigées le cas échéant.
Analyse de l'impact sur l'évaluation : L'article démontre que les erreurs d'annotation pénalisent significativement l'évaluation des modèles. La réévaluation de trois LLM de pointe (Gemma 4 31B-it, Qwen3-30B-A3B, GPT-4o-mini) par rapport aux vérités de terrain corrigées a entraîné des gains de précision allant de +9 à +22 points de pourcentage.
Cadre de supervision assisté par LLM : Une stratégie novatrice qui réduit le coût de la curation de jeux de données. En concentrant la revue humaine sur le sous-ensemble d'instances signalées comme sujettes à erreur par le LLM, le cadre atteint 90 % de précision de jeu de données après avoir examiné seulement 24 % des instances de FOLIO et 13 % de celles de MALLS. Cela représente une réduction substantielle par rapport à une revue aléatoire non guidée, qui nécessite plus de 70 % des instances pour atteindre la même précision.

Résultats

Taux d'erreur : L'audit humain a confirmé qu'environ 39 % des instances de FOLIO et 36 % de MALLS contiennent des formalisations FOL incorrectes. De plus, 16,4 % de FOLIO et 48 % de MALLS contiennent des phrases en NL ambiguës.
Évolutions de performance : Testés sur les jeux de données curés, tous les modèles évalués ont montré une amélioration de la précision de traduction. Par exemple, Gemma 4 31B-it a connu une augmentation de +21,8 % sur FOLIO (toutes les instances) et de +18,0 % sur MALLS.
Efficacité de la supervision :
- Le Pipeline 1 a surpassé le Pipeline 2 et les méthodes de base (revue aléatoire des données originales ou régénérées) sur tous les indicateurs (Aire sous la courbe, $T_{90}$ , $T_{95}$ ).
- En utilisant l'ordre de priorité (sorties malformées $\to$ ? $\to$ no $\to$ yes), le cadre a atteint 90 % de précision avec un effort humain minimal (24 % pour FOLIO, 13 % pour MALLS).
- Sur le jeu de données de haute qualité GGC, le cadre a introduit un bruit négligeable (dégradation $\le 5 \%$ ), confirmant sa fiabilité lorsqu'il est appliqué à des données déjà largement correctes.

Signification et Revendications

L'article affirme que la qualité des benchmarks NL-vers-FOL a été une "boîte noire" qui a faussé l'évaluation des systèmes d'IA neurosymbolique. En fournissant des vérités de terrain corrigées, les auteurs montrent que les estimations de performance précédentes étaient artificiellement supprimées par le bruit d'annotation.

Le cadre de supervision assisté par LLM proposé offre une solution pratique au problème de "passage à l'échelle" de la curation de données. Il démontre qu'il est possible d'obtenir des jeux de données de haute qualité sans le coût prohibitif d'une revue humaine exhaustive. Les auteurs positionnent ce cadre comme un outil pour :

La Curation de Données : Permettre aux curateurs de se concentrer exclusivement sur les instances suspectes.
Les Méthodes Formelles : Agir comme une couche d'avertissement pour les experts révisant les spécifications en langage naturel.
La Vérification au Runtime : Fournir un retour immédiat sur la capacité des formules générées à capturer les exigences prévues dans des scénarios où la revue manuelle est impossible.

Les auteurs publient les jeux de données corrigés et le code du cadre pour soutenir la reproductibilité, tout en notant que les conclusions sont spécifiques aux jeux de données et aux LLM testés et peuvent nécessiter une adaptation pour d'autres formalismes logiques ou domaines.