Résumé technique : ForEx – Un cadre de vérification formelle pour le raisonnement explicable dans la détection des sophismes logiques

1. Énoncé du problème

Les évaluations actuelles des grands modèles de langage (LLM) sur la détection des sophismes logiques reposent principalement sur la précision de la prédiction (exactitude de l'étiquette). Cependant, cette approche ne permet pas de vérifier si le raisonnement fourni par le modèle soutient réellement l'étiquette prédite. Des prédictions correctes peuvent découler de corrélations superficielles plutôt que d'une véritable dérivation logique, tandis que des prédictions incorrectes peuvent être accompagnées d'un raisonnement qui est formellement sain selon une interprétation spécifique, mais qui diverge des annotations humaines.

De plus, les approches symboliques existantes (par exemple, NL2FOL) formalisent généralement l'argument d'entrée pour vérifier la satisfaisabilité, plutôt que de formaliser la chaîne de raisonnement générée par le modèle. De plus, les pratiques d'annotation standard compressent souvent les variations interprétatives en une étiquette « gold » unique, ce qui peut occulter des lectures alternatives plausibles d'un argument. Il manque un cadre capable d'analyser conjointement les étiquettes prédites, les explications générées et la dérivabilité formelle de ces explications.

2. Méthodologie : Le cadre ForEx

Les auteurs proposent ForEx (Formal Verification for Explainable Reasoning), un cadre qui traduit les explications en langage naturel générées par les LLM en Lean4 (un assistant de preuve formelle) afin de vérifier si le raisonnement traduit est dérivable sous des prémisses encodées. Le flux de travail comprend trois étapes :

A. Génération de candidats de raisonnement

Un modèle « Raisonneur » reçoit un énoncé et génère jusqu'à $k$ candidats. Chaque candidat est un tuple $(f_i, a_i, s_i)$ contenant :

• $f_i$ : Le type de sophisme logique prédit.
• $a_i$ : L'explication en langage naturel (le rationnel).
• $s_i$ : La structure Lean4 formalisant l'explication.

Un « Modificateur » convertit $s_i$ en un code Lean4 initial.

B. Retour de l'exécution et vérification Lean4

Cette étape utilise une boucle de réparation itérative pour garantir que le code Lean4 généré compile :

1. Tentative de compilation : L'« Exécuteur » tente de compiler le code Lean4.
2. Boucle de rétroaction : Si la compilation échoue (état F), l'Exécuteur reçoit le message d'erreur et l'explication originale $a_i$ pour réviser le code.
3. Contraintes : Les révisions sont strictement limitées à l'explication originale et au code initial pour éviter la dérive sémantique ; l'Exécuteur ne peut pas introduire de nouveau contenu logique.
4. Terminaison : La boucle continue jusqu'à ce que le code compile avec succès (état T) ou que le nombre maximal d'itérations de réparation ($iter_{max}$) soit épuisé.

C. Évaluation de la cohérence de l'étiquette

Le cadre introduit la Matrice de vérification d'argument LLM pour découpler la correction de l'étiquette de l'état de vérification formelle. La matrice classe les sorties en quatre quadrants basés sur deux axes :

1. Vérification Lean4 : Succès (compile) vs Échec (ne compile pas).
2. Cohérence de l'étiquette : Correspondance (la prédiction est égale à l'annotation humaine) vs Discordance.

Les quatre catégories résultantes sont :

• Compilable-Correct (CC) : Succès & Correspondance.
• Compilable-Alternatif (CA) : Succès & Discordance (indique une chaîne de raisonnement formellement valide qui soutient une étiquette différente de l'annotation humaine).
• Incompilable-Correct (UC) : Échec & Correspondance.
• Incompilable-Incorrect (UI) : Échec & Discordance.

D. Pipeline d'annotation guidé par le consensus

Pour traiter l'ambiguïté de l'annotation, les auteurs proposent un pipeline qui :

1. Représente les modèles et les annotations humaines sous forme de vecteurs multi-chauds sur les catégories de sophismes.
2. Utilise l'analyse en composantes principales (PCA) et la distance de Mahalanobis pour identifier et filtrer les modèles aberrants.
3. Calcule les distances de Jaccard par paires pour identifier les énoncés à « haut consensus » (faible désaccord).
4. Augmente les annotations pour les énoncés à haut consensus si au moins 50 % des modèles conservés assignent une étiquette spécifique sous vérification formelle.

3. Contributions clés

1. Cadre ForEx : Un système novateur qui traduit les explications en langage naturel des LLM en Lean4, permettant une analyse vérifiable par machine des chaînes de raisonnement formalisées plutôt que de simples arguments d'entrée.
2. Matrice de vérification d'argument LLM : Une métrique qui sépare la cohérence de l'étiquette de l'état de vérification formelle, exposant les cas où les modèles fournissent un raisonnement formellement dérivable qui contredit les étiquettes humaines existantes (la catégorie « Compilable-Alternatif »).
3. Pipeline d'annotation guidé par le consensus : Une méthode combinant les normes humaines, l'accord multi-LLM et la vérification formelle pour soutenir l'analyse des annotations et l'augmentation conservatrice des étiquettes, traitant le désaccord d'annotation comme un signal de variation interprétative plutôt que comme du bruit.

4. Résultats expérimentaux

Le cadre a été évalué sur le jeu de données LOGIC-Climate (1 074 instances, 13 catégories de sophismes), en utilisant un sous-ensemble échantillonné de 10 % et 15 modèles de Raisonneur différents (incluant des variantes avec et sans « pensée »/thinking).

• Succès de compilation : Le taux de réussite moyen de la compilation Lean4 est passé de 36,70 % (initial) à 98,65 % après quatre itérations de réparation. La plupart des gains sont survenus après la première itération.
• Vérification vs Accord de l'étiquette :
  • Le taux combiné Compilable-Correct (CC) + Compable-Alternatif (CA) était systématiquement élevé, dépassant 90 % pour la plupart des modèles (atteignant un pic de 97,59 %). Cela indique que la vaste majorité des sorties de LLM peuvent être traduites en chaînes de raisonnement formelles qui passent la vérification.
  • Cependant, le taux CC (accord avec les étiquettes humaines) était nettement plus faible, se situant environ entre 17 % et 23 % pour les meilleurs modèles.
  • Le taux CA était dominant, suggérant que de nombreuses chaînes de raisonnement formellement vérifiées soutiennent des étiquettes différentes des annotations humaines.
• Analyse d'erreurs :
  • Les taux de Incompilable-Correct (UC) étaient très faibles (<2 %), indiquant que les étiquettes correctes sont rarement dépourvues de chaîne de raisonnement vérifiable dans ce contexte.
  • Les échecs Incompilable-Incorrect (UI) étaient souvent dus à des prédictions de « Pas de sophisme » (NF), potentiellement causées par le manque de contexte dans les entrées isolées d'une seule phrase.
• Augmentation d'annotation : Le pipeline guidé par le consensus a identifié un sous-ensemble d'énoncés à haut consensus. Les annotations augmentées ont atteint un rappel de 0,77 par rapport aux annotations humaines originales, préservant la plupart des étiquettes originales tout en ajoutant des alternatives soutenues par la vérification formelle.

5. Signification et affirmations

L'article affirme que ForEx déplace l'évaluation des LLM au-delà de la simple correction de l'étiquette vers une analyse de la chaîne de raisonnement formalisée vérifiable par machine.

• Écart systématique : Les résultats exposent un écart systématique entre la dérivabilité formelle et l'accord de l'étiquette. La prévalence élevée des sorties « Compilable-Alternatif » suggère que les annotations humaines existantes pourraient ne pas capturer pleinement les interprétations plausibles des arguments d'entrée, ou que les modèles raisonnent correctement sous des hypothèses différentes.
• Au-delà de la prédiction : Le cadre démontre qu'un modèle peut fournir une chaîne de raisonnement qui est formellement valide (dérivable sous les prémisses encodées) même s'il est en désaccord avec l'étiquette « gold ». Cette distinction est invisible pour les métriques standard basées uniquement sur la prédiction.
• Utilité de l'annotation : ForEx est présenté non seulement comme un outil de vérification, mais aussi comme un mécanisme pour l'analyse descendante des annotations. Il peut identifier les cas où les étiquettes « gold » pourraient être insuffisantes ou là où plusieurs interprétations valides existent, soutenant l'augmentation des jeux de données avec des étiquettes alternatives basées sur le consensus.

Les auteurs restent modestes quant aux implications, notant que la vérification formelle dans Lean4 certifie la dérivabilité sous des prémisses encodées mais ne garantit pas l'alignement sémantique avec l'énoncé en langage naturel original. Ils reconnaissent que le langage naturel manque d'une base sémantique entièrement spécifiée, et que les résultats formels peuvent donc surestimer la capacité du modèle si la formalisation elle-même est imparfaite. Des travaux futurs sont proposés pour améliorer l'alignement entre les résultats de vérification et la correction sémantique en incorporant des structures d'argumentation plus riches et des informations contextuelles.