Résumé Technique : Géométrie de la Raison : Signatures Spectrales du Raisonnement Mathématique Valide

1. Énoncé du Problème

Vérifier si les grands modèles de langage (LLM) s'engagent dans un véritable raisonnement logique ou s'ils ne font que réaliser une correspondance de motifs sophistiquée demeure un défi critique. Les méthodes de vérification actuelles se divisent en deux catégories, toutes deux présentant des limites significatives :

• Vérification basée sur la sortie : Repose sur des assistants de preuve formels (ex. Lean, Coq) pour vérifier si les preuves compilent. Cela confond la validité logique avec l'acceptabilité syntaxique ; des preuves valides peuvent être rejetées en raison de problèmes techniques (délais d'attente, imports manquants), tandis que des preuves erronées peuvent passer si elles exploitent des lacunes dans le typage.
• Vérification apprise : Entraîne des classifieurs sur les internes du modèle ou les caractéristiques de sortie. Ces méthodes nécessitent un étiquetage substantiel, risquent d'apprendre des corrélations spécieuses et échouent souvent à se généraliser à travers différentes architectures de modèles.

L'article pose l'hypothèse qu'un raisonnement mathématique valide induit une « signature spectrale » mesurable et sans entraînement au sein des mécanismes d'attention du transformer, distincte des artefacts d'acceptation par un compilateur ou de l'entraînement spécifique du modèle.

2. Méthodologie

Le cadre proposé traite le mécanisme d'auto-attention d'un transformer comme un graphe pondéré dynamique sur des jetons (tokens). En appliquant la théorie spectrale des graphes, les auteurs extraient les propriétés géométriques du flux d'information sans entraîner de paramètres.

2.1. L'Attention comme Graphes Dynamiques

Pour un transformer avec $L$ couches et $H$ têtes traitant une séquence de $N$ jetons :

1. Construction du Graphe : À chaque couche $\ell$ et tête $h$, la matrice d'attention post-softmax $A^{(\ell,h)}$ est interprétée comme un graphe dirigé pondéré. Pour permettre l'analyse spectrale, elle est symétrisée : $W^{(\ell,h)} = \frac{1}{2}(A^{(\ell,h)} + (A^{(\ell,h)})^\top)$.
2. Agrégation : Les matrices d'attention à travers les têtes sont agrégées en un seul graphe par couche en utilisant la pondération par masse d'attention : $\bar{W}^{(\ell)} = \sum_{h=1}^H \alpha_h^{(\ell)} W^{(\ell,h)}$.
3. Laplacien : Le Laplacien de graphe combinatoire est calculé comme $L^{(\ell)} = \bar{D}^{(\ell)} - \bar{W}^{(\ell)}$, où $\bar{D}$ est la matrice de degré.

2.2. Diagnostics Spectraux

La matrice d'état caché $X^{(\ell)}$ est traitée comme un signal de graphe. La Transformée de Fourier sur Graphe (GFT) projette ces états sur la base propre du Laplacien. Quatre diagnostics sont extraits de chaque couche :

• Ratio d'Énergie Haute Fréquence (HFER) : Mesure la proportion d'énergie du signal dans les composantes spectrales à haute fréquence. Un HFER plus bas indique une concentration d'énergie dans des modes lisses à basse fréquence.
• Valeur de Fiedler ($\lambda_2$) : La deuxième plus petite valeur propre du Laplacien, mesurant la connectivité algébrique. Des valeurs plus élevées indiquent un graphe bien connecté avec un flux d'information efficace.
• Entropie Spectrale : Quantifie la distribution de l'énergie à travers les modes spectraux.
• Lissage (Smoothness) : Une mesure normalisée de l'énergie de Dirichlet, où les valeurs proches de 1 indiquent des signaux lisses et les valeurs proches de 0 (ou négatives) indiquent des signaux rugueux.

2.3. Classification

Un classifieur à seuil unique est appliqué à une métrique sélectionnée à une couche spécifique (ex. HFER à la couche 30). Le seuil est calibré sur un petit ensemble de validation. La méthode ne nécessite aucun paramètre appris et opère directement sur la structure de l'attention.

3. Contributions Clés

1. Cadre Sans Entraînement : Introduction d'un cadre d'analyse spectrale pour la détection de la validité du raisonnement qui atteint une précision de 82,8–85,9 % sous validation croisée imbriquée et jusqu'à 95,6 % avec des seuils calibrés.
2. Universalité Trans-Architecture : Démonstration que la signature spectrale est universelle à travers sept modèles de quatre familles architecturales (Meta Llama, Alibaba Qwen, Microsoft Phi, Mistral AI), avec des tailles d'effet (Cohen's $d$) allant de 2,09 à 3,30 ($p < 10^{-47}$).
3. Validité Platonicienne : Découverte que la méthode spectrale détecte la cohérence logique (« validité platonicienne ») plutôt que l'acceptation par un compilateur. La méthode classifie correctement les preuves mathématiquement saines que les systèmes formels rejettent en raison de défaillances techniques (ex. délais d'attente), une distinction confirmée par un audit manuel ($\kappa = 0,82$).
4. Déterminisme Architectural : Identification du fait que la caractéristique spectrale spécifique encodant la qualité du raisonnement dépend du mécanisme d'attention. Pour l'attention globale standard, le HFER est dominant ; pour l'attention par fenêtre glissante (Mistral-7B), la caractéristique discriminante bascule vers le Lissage.
5. Utilité Aval : Application du HFER en tant que ré-classeur (reranker) zero-shot dans une recherche de preuve de type Best-of-16, améliorant le Pass@1 de 4,4–6,6 % et égalant 98 % de l'AUC de sondes entièrement supervisées avec zéro étiquette.

4. Résultats Expérimentaux

Les expériences ont été menées sur le benchmark MiniF2F (preuves Lean formalisées) sur 488 problèmes.

• Signification Statistique : Les sept modèles ont montré une signification statistique extrême ($p_{MW} < 10^{-47}$).
• Tailles d'Effet : La séparation entre les preuves valides et invalides était exceptionnellement grande. Par exemple, Phi-3.5-mini a atteint $d = 3,30$, et Llama-3.2-1B a atteint $d = 3,02$.
• Précision : Les classifieurs à seuil unique ont atteint une précision de 85,9–94,9 % sans entraînement. La validation croisée imbriquée a produit 82,8–85,9 %.
• Robustesse :
  • Difficulté : Le signal persiste à travers tous les niveaux de difficulté, avec $d \ge 1,31$ même pour les preuves complexes.
  • Longueur : La précision reste stable à travers les longueurs de preuve (87–100 %), indiquant que la méthode ne repose pas sur la longueur comme proxy.
  • Généralisation : La méthode se généralise au raisonnement informel de type Chaîne de Pensée (dataset MATH), bien que la taille d'effet s'atténue ($d = 0,78$).
• Ablation :
  • Contrôle 1 : Le signal distingue les preuves générées par le modèle valides des invalides, et non simplement humain vs modèle.
  • Contrôle 2 : Les perturbations humaines qui corrompent la logique tout en maintenant le style dégradent significativement le signal spectral, confirmant qu'il suit la cohérence logique.
  • Architecture : Mistral-7B (Attention par Fenêtre Glissante) repose sur le Lissage plutôt que sur le HFER, confirmant que la conception de l'attention gouverne le canal spectral.

5. Signification et Revendications

L'article affirme établir un « principe géométrique » où un raisonnement mathématique valide nécessite un graphe d'attention connecté et à basse fréquence, tandis que les anomalies logiques se manifestent par des discontinuités spectrales mesurables.

• Vérification Fondée sur des Principes : Ce travail démontre que les cadres mathématiques classiques (théorie spectrale des graphes) peuvent produire des outils pratiques et sensibles à l'architecture pour vérifier le raisonnement des réseaux de neurones sans données étiquetées.
• Validité Platonicienne : La capacité de distinguer la cohérence logique de l'acceptation par le compilateur offre une nouvelle perspective sur la vérification, permettant potentiellement d'identifier des preuves « récupérées » qui sont mathématiquement correctes mais techniquement rejetées.
• Efficacité : La méthode offre une alternative efficace par rapport aux vérificateurs appris, ne nécessant que la décomposition en valeurs propres du graphe d'attention (complexité $O(N^3)$ ou $O(kN^2)$ avec Lanczos), ce qui ajoute un surcoût négligeable pour les longueurs de preuve typiques.

Les auteurs concluent que cette signature spectrale reflète l'état épistémique du modèle, permettant potentiellement de distinguer un raisonnement « faussement confiant » (basse énergie spectrale) d'un effort cognitif réel (haute énergie spectrale), ouvrant des voies pour l'estimation de la difficulté et la détection de la surconfiance.