Résumé Technique : Transformateurs de Déduction sur Treillis

Énoncé du Problème

Les grands modèles de langage (LLM) actuels reposent fortement sur le paradigme de la chaîne de pensée, générant des tokens de raisonnement intermédiaires pour parvenir à une réponse finale. Bien que efficace pour de nombreuses tâches, cette approche manque souvent de la rigueur logique inhérente aux systèmes de raisonnement automatisé. À l'inverse, le raisonnement automatisé traditionnel (par exemple, les solveurs SAT) fonctionne par raffinement itératif d'états d'information partiels, analogue aux modèles de diffusion discrets, mais ces méthodes sont souvent distinctes des architectures neuronales.

Les auteurs postulent un écart : les techniques issues du raisonnement automatisé, spécifiquement l'interprétation abstraite, peuvent-elles être intégrées dans des architectures neuronales pour créer des modèles capables d'effectuer une déduction rigoureuse ? L'objectif est de construire un modèle qui, sur des problèmes logiques difficiles, renvoie soit une réponse correcte, soit s'abstient, sans jamais produire de solution incorrecte, tout en le faisant avec nettement moins de paramètres et de coûts d'entraînement que les raisonneurs récurrents antérieurs ou les LLM de pointe.

Méthodologie

Le Transformateur de Déduction sur Treillis (LDT)

La contribution centrale est le Transformateur de Déduction sur Treillis (LDT), une architecture de transformateur récurrent conçue pour approximer une déduction logiquement rigoureuse.

1. Cadre d'Interprétation Abstraite :
Le modèle traite le raisonnement comme une descente à travers un treillis d'états d'information.

• Domaine Concret ($C$) : L'ensemble des parties de toutes les solutions valides (par exemple, toutes les grilles de Sudoku valides).
• Domaine Abstrait ($A$) : Un « treillis d'ensemble de parties de grille » où chaque cellule contient un ensemble de candidats viables.
  • Haut ($\top$) : Représente l'absence d'information (tous les candidats sont possibles).
  • Bas ($\bot$) : Représente l'incohérence (aucun candidat n'est possible).
• Déduction : Un processus qui se déplace de $\top$ vers des états plus informatifs. Un état s'effondrant vers $\bot$ signale qu'aucune solution valide n'existe pour la branche actuelle.

2. Architecture :

• Transformateur Récurrent : Le modèle utilise une pile de 4 couches d'attention déroulées sur 16 itérations internes par passage avant.
• Encodage du Treillis : L'état abstrait est encodé sous forme de tenseur. Pour les problèmes de grille (comme le Sudoku), il s'agit d'un encodage multi-chaud où chaque cellule possède des sigmoïdes binaires représentant la confiance qu'un candidat spécifique est toujours « actif ».
• Projection : Entre les passages avant, l'état latent est projeté vers et depuis la représentation du treillis. Cela force chaque passage avant à agir comme une étape de déduction rigoureuse.
• Détection de Conflit : Un sigmoïde dédié au token CLS prédit l'incohérence ($\bot$), permettant au modèle de détecter les états insatisfaisables.

3. Procédure d'Entraînement (Boucle de Résolution On-Policy) :
L'entraînement reflète le processus d'inférence, garantissant que le modèle voit la même distribution d'états de treillis qu'il rencontrera au moment du test.

• La Boucle de Résolution : Un processus de recherche stochastique qui alterne entre :
  1. Déduction : Le transformateur affine l'état du treillis (éliminant les candidats).
  2. Branchement : Si l'état n'est ni une solution ni un conflit, le modèle « fixe » stochastiquement une cellule aléatoire à plusieurs candidats sur une seule valeur (échantillonnage selon une softmax sur les candidats actifs).
• Supervision via l'Opérateur $\alpha$ : Au lieu d'être entraîné contre une seule solution de vérité terrain, le modèle est supervisé contre l'abstraction de l'ensemble des solutions valides cohérentes avec l'état actuel.
  • Cible $\hat{y} = x \sqcap \alpha(\{y \in Y \mid y \text{ cohérent avec } x\})$.
  • Cela permet au modèle d'apprendre à partir de multiples solutions valides simultanément (supervision multi-solutions), évitant la pénalité de s'engager sur une vérité terrain arbitraire unique lorsque plusieurs existent.
• Fonction de Perte : Une combinaison de :
  • Entropie Croisée Binaire Asymétrique (BCE) pour l'élimination des candidats (pénalisant lourdement les éliminations fausses pour garantir la rigueur).
  • BCE Symétrique pour la détection de conflits.
  • Entropie Croisée pour les cellules qui se sont effondrées vers un seul candidat.

4. Inférence :
L'inférence exécute un processus de résolution parallèle. Plusieurs chaînes explorent l'espace de recherche simultanément. Si une chaîne rencontre un conflit (détecté par l'état du treillis ou le token CLS), elle revient en arrière ou redémarre. Le système est conçu pour être rigoureux empiriquement : s'il renvoie une réponse, elle est correcte ; s'il ne peut pas trouver de chemin, il s'abstient.

Contributions Clés

1. Architecture : Un transformateur récurrent qui projette les états latents sur un treillis abstrait à chaque itération, transformant les passages avant en étapes de déduction rigoureuse.
2. Entraînement On-Policy : Une procédure d'entraînement où les états de treillis évoluent sous le propre passage avant du modèle, maintenant les états d'entraînement dans la même distribution que les états de recherche d'inférence.
3. L'Opérateur $\alpha$ : Un mécanisme de supervision qui agrège les solutions valides cohérentes avec l'état actuel du treillis. Cela crée un régime « on-policy mais supervisé par une cible dépendante de l'état et agnostique du domaine », gérant naturellement les problèmes à solutions multiples.
4. Caractérisation du Compromis de Calcul : Des preuves empiriques montrant que l'augmentation du calcul d'entraînement réduit considérablement le nombre de passages avant (étapes de recherche) requis lors de l'inférence, déplaçant la charge de la recherche au moment du test vers l'apprentissage au moment de l'entraînement.

Résultats

Les auteurs ont évalué le LDT sur trois benchmarks, le comparant à des LLM de pointe (Claude Opus 4.6, DeepSeek V4-Pro, GPT-5.4) et à des raisonneurs récurrents antérieurs (HRM, TRM, Sotaku).

• Sudoku-Extreme :
  • Un LDT de 800K paramètres a atteint 100 % de précision sur Sudoku-Extreme et Snowflake Sudoku.
  • Il a atteint la rigueur empirique (100 % correct ou abstention) avec 4 000 étapes d'entraînement.
  • Coût : Entraîné en ~15 minutes sur un seul GPU B200, soit une fraction du coût des méthodes antérieures (par exemple, TRM nécessitait 36 heures sur 4 GPU L40S).
  • LLM de pointe : Ont obtenu 0 % sur tous les benchmarks.
• Snowflake Sudoku :
  • Le modèle a généralisé à des grilles hexagonales de topologie variable (ordre $n=4$ à $8$) sans modifications architecturales, en utilisant une grille de couverture fixe et un masquage.
  • Il a atteint 100 % de précision avec 4 minutes d'entraînement.
• Maze-Hard :
  • Une variante de 1,8M paramètres a atteint 99,9 % de précision sur des labyrinthes de 30x30 avec plusieurs chemins les plus courts valides.
  • L'utilisation d'une supervision multi-solutions ($K=512$) a amélioré les performances par rapport à une supervision mono-solution ($K=1$).
  • Les LLM de pointe ont de nouveau obtenu 0 %.

Efficacité : Le LDT démontre un compromis fort : un calcul d'entraînement supplémentaire réduit drastiquement le nombre de passages avant (étapes de recherche) requis lors de l'inférence.

Signification et Revendications

L'article revendique que le LDT comble avec succès le fossé entre les réseaux de neurones et le raisonnement automatisé en traitant le raisonnement comme un calcul de point fixe sur un treillis.

• Rigueur : Contrairement aux LLM standards qui peuvent halluciner, le LDT est conçu pour être rigoureux empiriquement. Il renvoie soit une réponse vérifiée correcte, soit s'abstient, ne renvoyant jamais de faux positifs.
• Efficacité : De petits modèles (moins de 2M de paramètres) entraînés avec cette approche spécifique on-policy basée sur les treillis surpassent des raisonneurs récurrents beaucoup plus grands et des LLM de pointe défaillants sur des benchmarks logiques.
• Généralisation : L'approche est agnostique du domaine concernant la structure du treillis. Bien qu'instanciée sur des puzzles combinatoires, l'architecture peut théoriquement s'appliquer à tout domaine abstrait admettant un opérateur de déduction.
• Limites : Les auteurs notent que le LDT est actuellement mieux adapté aux tâches avec des règles logiques claires et fixes. Il éprouve des difficultés avec des tâches comme ARC-AGI où les règles elles-mêmes doivent être inférées à partir de quelques démonstrations, car la tête de conflit devient peu fiable sans opérateurs de déduction prédéfinis. Combler cet écart pourrait nécessiter des structures récursives plus profondes ou des domaines abstraits sur les programmes générant les solutions.

En résumé, le LDT offre une alternative évolutive, rigoureuse et efficace au raisonnement par chaîne de pensée pour les problèmes logiques structurés, exploitant l'interprétation abstraite pour guider la recherche neuronale.