Résumé Technique : Décodable mais non fidèle : Coupler les rationales en langage naturel à des vérificateurs programmatiques

Énoncé du problème

Bien que les grands modèles de langage (LLM) puissent générer des rationales plausibles en langage naturel pour leurs prédictions, ces explications ne parviennent souvent pas à représenter fidèlement le processus de décision interne du modèle. Les modèles peuvent « rationaliser » des décisions a posteriori, omettre la véritable source d'une réponse ou utiliser des raccourcis invisibles dans le texte généré. Des travaux antérieurs indiquent que si le prompting par chaîne de pensée (chain-of-thought) améliore la précision des tâches, les explications générées ne sont pas nécessairement une preuve de raisonnement causal.

Les vérificateurs programmatiques externes (par exemple, les prouveurs de théorèmes, les moteurs de jeu, les exécuteurs de code) offrent un mécanisme pour vérifier les affirmations, mais leur utilisation actuelle est généralement limitée à la supervision au niveau du résultat (vérification de la réponse finale). Cela laisse une lacune : un modèle peut produire une affirmation correcte tout en accompagnant celle-ci d'une explication non étayée, ou encoder l'information du vérificateur en interne sans la verbaliser de manière cohérente. La question centrale abordée est de savoir si le fait de forcer les représentations de la rationale d'un modèle à être décodables par un vérificateur garantit que les explications générées sont fidèles à son raisonnement.

Méthodologie : Raisonnement couplé au vérificateur

Le papier propose un cadre appelé Raisonnement couplé au vérificateur (Verifier-Coupled Reasoning) pour réduire l'écart entre les affirmations vérifiées et les rationales en langage naturel.

Format de séquence et objectif

Le modèle génère une séquence contenant une rationale en langage naturel ($r$) et une affirmation explicite en ligne ($c$) selon le format : [CONTEXTE] x [RAT] r [CLAIM] c [EOS]. Un vérificateur programmatique $V$ fournit une étiquette cible $y = V(x)$ (par exemple, acceptation/rejet de preuve, tranche de taux de victoire, classe de complexité).

Une tête de cohérence auxiliaire (un classificateur linéaire) est entraînée pour prédire la cible du vérificateur $y$ à partir des états cachés moyennés (mean-pooled) de l'étendue de la rationale ($z_{rat}$). L'objectif d'entraînement combine la prédiction du prochain jeton standard ($L_{LLM}$), une supervision optionnelle de l'affirmation ($L_{claim}$), et la perte de cohérence ($L_{cons}$) :
$$L = L_{LLM} + \lambda_{claim}L_{claim} + \lambda_{cons}L_{cons}$$

Contraintes de flux d'information

Pour garantir que la tête d'affirmation ne puisse pas contourner la rationale, les auteurs utilisent un masque d'attention Board-Explanation-Claim (BEC) dans des expériences spécifiques. Cela empêche structurellement les jetons de l'affirmation d'être attentifs aux jetons du contexte d'entrée, les forçant à s'appuyer uniquement sur l'étendue de l'explication.

Échelle de diagnostic

Le papier introduit un cadre de diagnostic à plusieurs niveaux pour distinguer la décodabilité (l'information du vérificateur est présente dans la représentation) de la fidélité (la génération reflète cette information) :

1. Décodabilité : Précision de la tête de cohérence (la label du vérificateur peut-il être linéairement décodé à partir des états de la rationale ?).
2. Suivi contrefactuel : Les étendues permutées (par exemple, échanger une rationale avec une autre étiquette) modifient-elles la prédiction de la tête ?
3. Influence causale : Le patch de l'activation (remplacement des états cachés de la rationale par ceux d'un état latent différent) déplace-t-il les logits de l'affirmation en aval ?
4. Qualité de la génération : Le modèle produit-il des explications cohérentes et fidèles ?

Paramètres expérimentaux

Le cadre est évalué à travers cinq configurations distinctes :

1. Synthétique : Validation contrôlée avec des états latents pour isoler les mécanismes et tester les interventions causales via le patch d'activation.
2. LeanCheck : Preuve de théorèmes formels utilisant Lean 4. Teste le couplage spécifique à l'étendue (rationale vs preuve) sous des conflits contrefactuels.
3. KataGo : Un moteur de jeu de Go fournissant des étiquettes denses et non binaires (tranches de taux de victoire) pour des états de plateau complexes.
4. Couplage de Code : Affirmations algorithmiques (complexité temporelle/spatiale, classe d'algorithme) où le mode de défaillance de la génération infidèle est le plus visible.
5. FEVER : Vérification de preuves en langage naturel, testant le compromis entre l'exactitude brute et la sensibilité aux preuves.

Résultats clés

1. L'écart Décodabilité–Fidélité

La conclusion centrale est que la décodabilité ne garantit pas la fidélité.

• Synthétique & LeanCheck : L'entraînement de cohérence réussit à rendre l'information du vérificateur décodable et causalement influente. Dans LeanCheck, le pooling de la rationale seule et de la preuve seule atteint une séparation directionnelle parfaite sous conflit contrefactuel (100 % de suivi de l'étiquette de l'étendue permutée).
• KataGo : Les étendues de commentaires en langage naturel encodent des tranches de taux de victoire en 10 catégories avec une précision de 81,1 %, démontrant que la méthode s'adapte à des domaines denses et non binaires.
• Code (Le mode de défaillance critique) : Dans le cadre du code, le modèle atteint 98,6 % de couplage de représentation (les états cachés encodent parfaitement les affirmations du vérificateur), pourtant la prose générée reste infidèle. Le modèle émet des explications fluides et grammaticales décrivant un algorithme sans rapport (par exemple, décrivant une « somme de liste » alors que le code implémente un « tri par sélection ») tout en émettant correctement des balises d'affirmation structurées (par exemple, $O(n^2)$).
  • Cet écart est structurel, et non lié à la capacité : des résultats identiques sont observés tant sur GPT-2 préentraîné que sur des modèles entraînés à partir de zéro.
  • Cet écart n'est pas lié aux poids : augmenter le poids de la perte de cohérence ($\lambda_{cons}$) jusqu'à $10^4$ n'améliore pas la qualité de la génération, car la perte de cohérence agit sur les représentations, et non sur les jetons émis.

2. Insights de l'échelle de diagnostic

• Influence causale : Dans les configurations synthétiques, le patch d'activation des états de la rationale à la couche 0 déplace le comportement de l'affirmation dans 73 à 89 % des cas entraînés à la cohérence (contre 31 % pour la base), confirmant que le couplage est causal et non simplement corrélatif.
• Compromis FEVER : Dans les configurations de langage réel, le pooling sur la séquence complète (incluant le texte de l'affirmation) produit une précision quasi parfaite (99 %) mais échoue à isoler la sensibilité aux preuves. Le pooling sur l'évidence seule produit une précision plus faible (44 %) mais isole mieux si le modèle traite réellement les preuves, révélant un compromis entre précision et sensibilité caché par l'évaluation standard.

3. Analyse par affirmation

Dans le cadre du code, la perte de cohérence bénéficie de manière disproportionnée aux affirmations fines (ex: classe d'algorithme, opération clé) par rapport aux affirmations binaires. Les affirmations binaires sont partiellement apprenables à partir de la structure du code, tandis que les affirmations fines dépendent fortement de l'objectif de cohérence pour obtenir une haute précision.

Signification et Revendications

Le papier établit que les pertes de cohérence sont des outils de diagnostic et de façonnage de représentation efficaces, mais elles ne sont pas des conditions suffisantes pour un raisonnement fidèle.

• Représentation vs Génération : Le mécanisme façonne avec succès la représentation interne pour encoder l'information pertinente au vérificateur (décodabilité), mais sans un objectif au niveau de la génération qui récompense le texte pour correspondre au vérificateur, le modèle peut émettre des explications fluides mais infidèles.
• Limites du sondage (Probing) : Une haute précision de sonde (décodabilité) ne doit pas être confondue avec un raisonnement fidèle. Un modèle peut « connaître » la réponse dans ses états cachés tout en « disant » quelque chose de totalement différent dans sa sortie.
• Voie à suivre : Combler l'écart nécessite des objectifs où le gradient atteint les jetons générés et les récompense pour leur cohérence avec le vérificateur. Les auteurs suggèrent l'Apprentissage par Renforcement avec Récompenses Vérifiables (RLVR) comme l'instrument naturel, où le modèle est récompensé sur la base des affirmations structurées qu'il produit réellement, plutôt que par une sonde auxiliaire.

Ce travail fournit une échelle de diagnostic rigoureuse pour évaluer les systèmes de raisonnement, démontant que si nous pouvons forcer les modèles à « connaître » la vérité dans leurs représentations, garantir qu'ils « disent » la vérité nécessite plus que de simples contraintes du côté de la représentation.