🤖 machine learning

Evaluating the Architectural Reasoning Capabilities of LLM Provers via the Obfuscated Natural Number Game

Ce papier présente le Jeu des Nombres Naturels Obscurci comme une référence pour évaluer le « Raisonnement Architectural » — la capacité à synthétiser des preuves en utilisant uniquement des axiomes locaux sans indices sémantiques — et démontre que, tandis que les grands modèles de langage généraux subissent une dégradation des performances sous l'effet de l'obscurcissement, les modèles de raisonnement spécialisés maintiennent leur précision, distinguant ainsi le raisonnement logique authentique de l'appariement de motifs.

Auteurs originaux : Lixing Li

Publié 2026-05-04

📖 4 min de lecture☕ Lecture pause café

CC0 1.0

Auteurs originaux : Lixing Li

Article original placé dans le domaine public sous CC0 1.0 (http://creativecommons.org/publicdomain/zero/1.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous enseignez à un élève comment résoudre une énigme mathématique. Habituellement, l'énigme est accompagnée d'étiquettes utiles comme « Addition », « Multiplication » ou « Successeur ». Un élève intelligent pourrait ne pas réellement comprendre les règles du jeu ; il pourrait simplement reconnaître le mot « Addition » et se souvenir d'un astuce mémorisée qu'il a déjà vue.

Cet article pose une question difficile : Ces modèles d'IA font-ils réellement des mathématiques, ou sont-ils simplement doués pour reconnaître des mots ?

Pour le découvrir, les chercheurs ont créé une version « bandée » d'un célèbre jeu mathématique appelé le Natural Number Game. Voici comment ils l'ont fait et ce qu'ils ont découvert, expliqué simplement :

L'Expérience : Le Jeu « Alien »

Les chercheurs ont pris un jeu mathématique standard où chaque règle et chaque nombre possède un nom clair (comme add ou zero). Ensuite, ils ont appliqué un « brouilleur » dessus. Ils ont remplacé chaque nom significatif par des chaînes aléatoires et absurdes comme x9z, q22 et b7a.

Le Jeu Original : Vous voyez add et vous savez que cela signifie addition.
Le Jeu Brouillé (NNG Obfusqué) : Vous voyez x9z et vous ne savez pas du tout ce que cela signifie. Vous ne pouvez pas deviner ; vous devez examiner la logique de la manière dont les pièces s'assemblent pour comprendre ce que fait x9z.

Cela teste ce que les auteurs appellent le « Raisonnement Architectural ». C'est la capacité de construire une solution en utilisant uniquement les plans structurels (la logique), en ignorant les panneaux utiles sur les portes (les noms).

Les Résultats : La « Taxe de Latence »

Les chercheurs ont testé plusieurs modèles d'IA de premier plan sur le jeu original et sur le jeu brouillé. Ils ont découvert deux choses principales :

1. La « Taxe de Latence Universelle » (Tout le monde ralentit)
Lorsque les noms ont été brouillés, chaque modèle d'IA a pris plus de temps pour résoudre les problèmes.

Analogie : Imaginez que vous conduisez vers un café familier. Vous connaissez les panneaux, les noms de rues et les repères. Maintenant, imaginez que quelqu'un a peint par-dessus tous les panneaux et renommé les rues avec des lettres aléatoires. Vous savez toujours conduire, mais vous devez vous arrêter, regarder la carte et réfléchir davantage à chaque tournant. Vous arrivez éventuellement, mais cela prend beaucoup plus de temps.
La Découverte : Les modèles d'IA ont dû effectuer cette « reconstruction de carte mentale » pour chaque problème. Ils ne pouvaient pas simplement s'appuyer sur la mémoire ; ils devaient traiter la logique brute, ce qui leur a coûté du temps.

2. La Séparation « Raisonnement vs Par Cœur »
Bien que tout le monde ait ralenti, la précision des modèles s'est divisée en deux groupes distincts :

Les Modèles « Généraux » (par exemple GPT-4o, Claude) : Ces modèles sont comme des élèves excellents pour mémoriser des flashcards. Lorsque les noms ont été brouillés, ils se sont perdus. Leur taux de réussite a considérablement diminué.
- Ce que cela signifie : Ils s'appuyaient sur les « panneaux » (les noms) pour résoudre l'énigme. Lorsque les panneaux ont disparu, ils ne pouvaient plus trouver leur chemin.
Les Modèles « de Raisonnement » (par exemple DeepSeek-R1, GPT-5, DeepSeek-Prover-V2) : Ces modèles sont comme des élèves qui comprennent réellement les règles du jeu. Même lorsque les noms ont été brouillés, leur taux de réussite est resté exactement le même.
- Ce que cela signifie : Ils n'avaient pas besoin des étiquettes. Ils ont examiné la structure logique (l'« architecture ») et ont trouvé la solution aussi bien qu'avant.

La Conclusion

L'article conclut qu'il existe une réelle différence entre une IA qui correspond simplement à des motifs (comme reconnaître le mot « add ») et une IA capable de véritablement raisonner à travers des structures logiques.

Les modèles généraux sont comme des touristes qui ont besoin d'un guide avec des noms. Si vous enlevez le guide, ils se perdent.
Les modèles de raisonnement sont comme des architectes capables de lire les plans. Même si le bâtiment n'a aucun panneau, ils peuvent toujours comprendre comment les murs et les poutres s'assemblent.

L'étude prouve que si tous les modèles d'IA deviennent « plus lents » lorsqu'ils sont forcés de réfléchir sans étiquettes, seuls les vrais modèles de « raisonnement » peuvent maintenir leur précision élevée dans cet environnement « alien ». Cela suggère que pour que l'IA découvre de nouvelles mathématiques à l'avenir (où aucun nom ni aucune étiquette n'existent encore), nous avons besoin de ces modèles axés sur le raisonnement, et non pas seulement de ceux qui sont bons pour la correspondance de motifs.

1. Énoncé du Problème

Malgré le succès des Modèles de Langage à Grande Échelle (LLM) sur des benchmarks de mathématiques formelles comme MiniF2F et PutnamBench, une ambiguïté critique subsiste : ces modèles possèdent-ils de véritables capacités de raisonnement logique, ou se contentent-ils d'effectuer une correspondance de motifs sémantiques par rapport à leurs données d'entraînement préliminaire ?

Le Vide : Les benchmarks actuels reposent souvent sur la récupération de bibliothèques (par exemple, Mathlib), où le succès dépend de la reconnaissance de lemmes de haut niveau et d'identifiants sémantiques (par exemple, add, succ). Cela échoue à tester la capacité d'un modèle à synthétiser des preuves dans des domaines mathématiques « étrangers » où aucune bibliothèque externe ni aucun indice sémantique familier n'existe.
Le Besoin : Pour réaliser la découverte automatisée de théorèmes, l'IA doit démontrer un Raisonnement Architectural : la capacité à synthétiser des preuves formelles en utilisant uniquement des axiomes locaux, des définitions et une logique structurelle, indépendamment du sens sémantique ou des dépôts externes.

2. Méthodologie

Les auteurs introduisent le Jeu des Nombres Naturels Obscurci (O-NNG), un benchmark à connaissance nulle conçu pour isoler le raisonnement structurel de la récupération lexicale.

A. L'Algorithme d'Obscurcissement

L'innovation centrale est la suppression systématique des indices sémantiques du Jeu des Nombres Naturels (NNG) dans Lean 4 :

Niveau de Bruit ( $\lambda$ ) : Défini dans l'intervalle $[0, 1]$ $[0, 1]$ .
- $\lambda = 0$ : NNG original (identifiants sémantiques intacts).
- $\lambda = 1.0$ : Randomisation complète des identifiants.
Mécanisme de Perturbation : Une relation exponentielle $P = \lambda^{2.5}$ $P = λ^{2.5}$ détermine la probabilité de perturbations au niveau des caractères.
- Substitution : Remplace les caractères par des candidats valides Unicode/ASCII.
- Insertion : Injecte de nouveaux caractères (probabilité $0.4P$ ).
- Suppression : Retire des caractères (probabilité $0.3P$ ), en veillant à ce que les identifiants restent non vides.
Objectif : Ce processus transforme le jeu de données en un « environnement fermé » où les identifiants (par exemple, axiomes, théorèmes, tactiques) sont des chaînes aléatoires, forçant le modèle à se fier exclusivement à la structure logique des axiomes de Peano.

B. Configuration Expérimentale

Jeu de Données : 68 problèmes formels issus du NNG, organisés en 8 modules (Addition, Multiplication, etc.).
Modèles Évalués : Cinq modèles de pointe via API :
- Modèles de Raisonnement : DeepSeek-R1, GPT-5, DeepSeek-Prover-V2.
- Modèles Généraux : GPT-4o, Claude-Sonnet-4.5.
Chaîne de Traitement :
1. Analyse : Extraction du NNG avec un ordre de dépendance strict.
2. Obscurcissement : Application de perturbations au niveau des caractères basées sur $\lambda$ .
3. Génération de Requêtes : Construction de prompts contenant des axiomes « étrangers », des théorèmes cibles et des tactiques disponibles.
4. Inférence : Les modèles produisent un JSON contenant un plan en langage naturel (« Ébauche ») et du code Lean 4 (« Code »).
5. Vérification : Validation automatisée utilisant le compilateur Lean 4 (v4.27.0) pour vérifier les erreurs de syntaxe et de logique.
Métriques :
- Taux de Correction (%) : Ratio de théorèmes prouvés avec succès.
- Temps Moyen (s) : Latence d'inférence.

3. Contributions Clés

Définition du Raisonnement Architectural : Formalisé comme la capacité à synthétiser des preuves en utilisant exclusivement des définitions et des axiomes locaux au sein d'une théorie fermée, excluant les bibliothèques externes et les tactiques automatisées de haut niveau (comme linarith).
Le Benchmark O-NNG : Un cadre d'évaluation novateur à connaissance nulle qui quantifie le « Vide Sémantique-Raisonnement » en mesurant la dégradation des performances lorsque les identifiants sémantiques sont supprimés.
Quantification de la « Taxe de Latence » : Établissement du fait que la navigation dans des domaines étrangers impose un coût computationnel universel (augmentation du temps d'inférence) à tous les modèles, indépendamment de leur architecture.

4. Résultats et Analyse

L'étude révèle une divergence nette dans le comportement des modèles lorsque les indices sémantiques sont supprimés :

Taxe de Latence Universelle :
- Tous les modèles ont présenté une augmentation statistiquement significative du temps d'inférence à mesure que $\lambda$ augmentait.
- Implication : La suppression des identifiants sémantiques force les modèles à effectuer des recherches internes plus intensives ou une reconstruction logique, indépendamment de leur capacité de base.
Divergence de Robustesse (Précision) :
- Modèles de Raisonnement (DeepSeek-R1, GPT-5, DeepSeek-Prover-V2) : Ont maintenu une précision stable sur tous les niveaux de bruit ( $\lambda \in [0, 1]$ $λ \in [0, 1]$ ). La baisse de performance n'était pas statistiquement significative.
  - Conclusion : Ces modèles reposent sur la logique structurelle et peuvent naviguer dans les axiomes de Peano sans ancres sémantiques.
- Modèles Généraux (GPT-4o, Claude-Sonnet-4.5) : Ont subi une baisse statistiquement significative des taux de réussite à mesure que $\lambda$ $λ$ augmentait.
  - Conclusion : Leur performance sur les tâches formelles standard repose lourdement sur la correspondance de motifs sémantiques et la familiarité avec les conventions de nommage plutôt que sur une synthèse logique pure.
Significativité Statistique : L'ANOVA à un facteur a confirmé que la baisse de performance pour les modèles généraux et l'augmentation de latence pour tous les modèles étaient statistiquement significatives ( $p < 0.05$ ).

5. Signification et Implications

Évaluation du Vrai Raisonnement : O-NNG fournit une métrique rigoureuse pour distinguer les modèles qui « connaissent » les mathématiques via la correspondance de motifs de ceux qui peuvent « raisonner » via la logique structurelle.
Orientation Architecturale : Les résultats suggèrent que pour l'avenir de la découverte automatisée de théorèmes (AI4Math), les architectures axées sur le raisonnement (comme DeepSeek-R1 et GPT-5) sont supérieures aux modèles à usage général, car elles sont robustes à l'absence de priors sémantiques.
La « Vallée Étrange du Raisonnement » : Les données suggèrent une relation non linéaire où un bruit partiel pourrait être plus préjudiciable qu'une obscurcissement total, indiquant que des indices sémantiques résiduels peuvent agir comme des heuristiques distractrices.
Agents IA Futurs : Les conclusions plaident pour le développement d'« Agents Sémantiques Ancrés dans la Connaissance » capables d'opérer dans des domaines aux ontologies incomplètes ou obscurcies, une condition préalable à la découverte de nouveaux théorèmes mathématiques.

En résumé, le papier démontre que si les LLM actuels peuvent résoudre des problèmes connus via la correspondance de motifs, seules des architectures spécifiques de « raisonnement » possèdent le Raisonnement Architectural nécessaire pour résoudre des problèmes dans des environnements logiques entièrement inconnus et obscurcis.