When Verification Fails: How Compositionally Infeasible Claims Escape Rejection

1. Problématique : L'illusion de la vérification rigoureuse

Le papier aborde un problème fondamental dans la vérification des affirmations scientifiques par les grands modèles de langage (LLM). La tâche consiste à déterminer si une affirmation est étayée par des preuves (evidence). La norme épistémique requise est l'Hypothèse du Monde Clos (Closed-World Assumption - CWA) : une affirmation doit être acceptée si et seulement si toutes les contraintes qu'elle énonce sont positivement soutenues par les preuves. À l'inverse, l'absence de soutien pour n'importe quelle contrainte doit entraîner un rejet.

Cependant, les auteurs démontrent que les benchmarks existants (tels que NLI4CT, SCITAB, SciVer) sont incapables de distinguer deux comportements de modélisation :

1. Vérification CWA complète : Le modèle vérifie exhaustivement toutes les contraintes, y compris celles déduites de manière compositionnelle.
2. Vérification par contrainte saillante (Salient-Constraint Checking) : Le modèle applique une "raccourci" (shortcut) où il ne vérifie que la contrainte la plus saillante (la plus évidente ou accessible) et accepte l'affirmation si celle-ci est soutenue, ignorant les autres contraintes non saillantes.

Les benchmarks actuels construisent des affirmations infeasibles (fausses) en perturbant un seul élément saillant (ex: inversion d'un nombre). Dans ce cas, les deux méthodes (CWA et le raccourci) aboutissent au même résultat (rejet), rendant les modèles performants sur ces benchmarks mais potentiellement défaillants dans des scénarios réels plus complexes.

2. Méthodologie

Pour révéler cette faille, les auteurs proposent une nouvelle approche méthodologique basée sur la construction de revendications compositionnellement infeasibles.

A. Construction de Données Adverses (Graph-Based Adversarial Construction)

Au lieu de perturber un seul élément saillant, les auteurs utilisent une méthode basée sur un graphe de raisonnement à trois couches pour générer des affirmations trompeuses :

1. Couche d'Observation (Observation Layer) : Contient des faits directement récupérables (ex: valeurs numériques, étiquettes).
2. Couche de Contexte (Context Layer) : Combine les observations pour former des relations intermédiaires.
3. Couche d'Interprétation (Interpretation Layer) : Tire des conclusions de haut niveau à partir des relations de contexte.

Le processus de corruption :

• On part d'une affirmation faisable (vraie) et de ses preuves.
• On corrompt un seul nœud non saillant (dans la couche de contexte ou d'interprétation) par des opérations comme le changement de portée (scope swapping) ou la sur-généralisation.
• Résultat : La contrainte saillante reste soutenue par les preuves (le modèle la voit et l'accepte), mais une contrainte non saillante (compositionnelle) est contredite.
• Ces affirmations sont appelées "adversarial negatives".

B. Évaluation Expérimentale

Les auteurs évaluent plusieurs familles de modèles (GPT-5, Gemini, Claude, Qwen3) sur trois domaines :

• NLI4CT : Textes d'essais cliniques.
• SCITAB : Tableaux scientifiques.
• SciVer : Graphiques et diagrammes.

Ils comparent la performance sur :

• Les affirmations infeasibles standards (perturbation saillante).
• Les affirmations infeasibles compositionnelles (perturbation non saillante).

C. Interventions et Analyse des Traces

• Interventions de Prompting : Utilisation d'instructions pour forcer le modèle à adopter l'hypothèse du monde clos (CWA) ou l'hypothèse du monde ouvert (OWA), ainsi que des techniques de décomposition (DCP) pour énumérer explicitement les sous-affirmations.
• Analyse de traces (Rubric-based Judge) : Un juge LLM évalue le processus de raisonnement du modèle pour voir s'il vérifie toutes les contraintes (CWA) ou s'il s'arrête prématurément à la contrainte saillante.

3. Contributions Clés

1. Identification d'une limitation structurelle des benchmarks : Les auteurs prouvent que les benchmarks actuels, basés sur des violations de contraintes uniques, rendent le "raccourci" de vérification saillante indistinguable d'une vérification rigoureuse CWA.
2. Création d'un nouveau défi (Compositionally Infeasible Claims) : Ils introduisent un ensemble de données adverses où la violation est cachée dans une relation compositionnelle, forçant les modèles à effectuer une inférence multi-étapes pour rejeter l'affirmation.
3. Diagnostic du goulot d'étranglement de raisonnement : Ils démontrent que l'échec des modèles n'est pas dû à un manque de capacité de récupération d'information, mais à une incapacité structurelle à effectuer l'inférence compositionnelle nécessaire pour détecter les contradictions non saillantes.

4. Résultats Principaux

• Écart de performance systématique : Tous les modèles, quelle que soit leur taille ou leur famille, obtiennent une précision élevée sur les affirmations infeasibles standards (rejet correct) mais chutent significativement sur les affirmations compositionnellement infeasibles (acceptation incorrecte).
  • Exemple : Sur SciVer, Gemini-3.0-Flash voit sa précision chuter de 26,7 points sur les affirmations adverses par rapport aux standards.
• Le raccourci est la norme : Les modèles adoptent par défaut la stratégie de "Salient-Constraint Checking". Ils acceptent les affirmations dès que la partie la plus visible est soutenue, ignorant les contradictions cachées dans la structure globale.
• Limites du Scaling : L'augmentation de la taille du modèle améliore la récupération des faits, mais ne résout pas le problème de l'inférence compositionnelle. L'écart de performance persiste même pour les modèles les plus grands (ex: 32B).
• Interventions et Courbe ROC : Les interventions de prompt (CWA, décomposition) déplacent les modèles le long d'une courbe ROC commune (compromis entre acceptation et rejet).
  • Les instructions CWA augmentent le taux de rejet (réduisant les faux positifs sur les affirmations adverses) mais augmentent également le taux de rejet des affirmations faisables (faux négatifs).
  • Cela indique que le problème n'est pas un choix de stratégie, mais un goulot d'étranglement de raisonnement : les modèles ne peuvent pas distinguer de manière fiable les affirmations faisables des infeasibles compositionnelles, quel que soit le seuil de décision.
• Analyse des traces : Les scores de traces révèlent que les modèles qui réussissent à rejeter les affirmations adverses sont ceux qui énumèrent et vérifient explicitement les contraintes non saillantes. Les échecs correspondent à une terminaison précoce après la vérification de la contrainte saillante.

5. Signification et Implications

• Surévaluation des capacités actuelles : Les benchmarks existants surestiment la capacité des LLM à vérifier rigoureusement les affirmations scientifiques. Ils ne testent que la détection d'erreurs locales, pas la cohérence globale.
• Nature du problème : Le problème n'est pas un manque de connaissances, mais une tendance structurelle à privilégier les heuristiques de surface (contraintes saillantes) plutôt que le raisonnement logique exhaustif (∀-type reasoning).
• Limites des interventions actuelles : Le simple prompting (guidage stratégique) ne suffit pas à surmonter ce goulot d'étranglement. Il déplace le point de fonctionnement du modèle mais n'améliore pas sa capacité intrinsèque à effectuer des inférences compositionnelles complexes.
• Perspectives futures : Pour progresser, il faudra probablement des méthodes d'entraînement (SFT, RL) spécifiquement conçues pour renforcer le raisonnement de type "pour tout" (∀) et la vérification exhaustive, plutôt que de se fier uniquement aux données pré-entraînées qui favorisent le raisonnement de type "il existe" (∃).

En conclusion, cet article met en lumière une faille critique dans la vérification scientifique par IA : les modèles semblent vérifier, mais en réalité, ils ne vérifient souvent que la partie la plus visible de l'affirmation, laissant passer des désinformations subtiles et structurellement complexes.