🤖 machine learning

Geometric Measurements of the Axiom of Choice in Neural Proof Embeddings

Cet article démontre que l'Axiome du Choix laisse une signature géométrique mesurable dans les plongements de preuves neuronaux — caractérisée par une diminution des scores d'anomalie et des pertes de reconstruction à mesure que les preuves s'éloignent de l'axiome dans le graphe de dépendance — ce qui est corrélé avec et prédit la disparité de performance entre la démonstration de théorèmes constructive et classique dans des systèmes comme Lean 4.

Auteurs originaux : Rodrigo Mendoza-Smith

Publié 2026-06-30✓ Author reviewed ⓘ

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Rodrigo Mendoza-Smith

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.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 par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez une bibliothèque immense et ancienne appelée Mathlib. Cette bibliothèque contient près d'un demi-million de preuves mathématiques, toutes écrites dans un langage strict et lisible par ordinateur appelé Lean. Pendant plus d'un siècle, les mathématiciens se sont disputés sur deux manières différentes de construire ces preuves :

Preuves Constructives : La méthode « Lego ». Si vous affirmez qu'un bâtiment existe, vous devez montrer exactement comment le construire, brique par brique.
Preuves Classiques : La méthode « Magique ». Vous pouvez affirmer qu'un bâtiment existe simplement en disant : « Il est impossible qu'il n'existe pas », sans pour autant montrer comment le construire. Cela repose sur une règle appelée l'Axiome du Choix.

Pendant longtemps, on a pensé qu'il ne s'agissait que de différences philosophiques. Ce document soutient qu'il s'agit en réalité de différences géométriques que l'on peut mesurer, comme la distance entre deux villes sur une carte.

Voici comment les auteurs ont découvert cela, en utilisant des analogies simples :

1. L'« Écho » de la règle magique

Les auteurs ont traité la bibliothèque comme une immense chambre d'écho. Ils ont entraîné un cerveau informatique (une IA) uniquement sur les preuves « Lego » (constructives). L'IA a appris le rythme, le style et la structure de ces preuves. Elle est devenue experte pour reconnaître ce à quoi ressemble une « normale » preuve constructive.

Ensuite, ils lui ont soumis les preuves « Magiques » (classiques).

Le Résultat : L'IA n'a pas seulement dit : « Ceci est différent ». Elle a mesuré à quel point c'était différent.
L'Analogie : Imaginez que vous êtes un professeur de musique qui n'écoute que du piano classique. Si vous entendez un morceau de jazz, vous pourriez dire : « Ça sonne bizarre ». Mais si vous entendez un morceau de jazz écrit il y a 100 ans, il pourrait paraître moins bizarre qu'un morceau de jazz moderne utilisant un instrument très spécifique et inhabituel.

2. La « Loi de la Profondeur »

Les auteurs ont réalisé que toutes les preuves « Magiques » ne sont pas également magiques.

Profondeur Faible (Distance 1-2) : Ces preuves utilisent la « Règle Magique » (l'Axiome du Choix) directement. Elles sont comme un morceau de jazz utilisant cet instrument étrange dès le début. Pour l'IA, elles sonnent très étrangement et sont « hors de propos ».
Profondeur Élevée (Distance 9+) : Ces preuves utilisent la « Règle Magique » bien plus loin dans le passé, enfouie profondément dans une chaîne d'autres lemmes. La preuve elle-même ressemble beaucoup à une preuve « Lego ». Pour l'IA, elles sonnent presque normalement.

La Découverte : Il existe un gradient fluide. À mesure que l'on s'éloigne de l'utilisation directe de la « Règle Magique », la preuve commence à ressembler et à sonner comme une preuve « Lego » standard. L'étrangeté s'estompe. Les auteurs appellent cela la Loi de la Profondeur.

3. Trois façons de mesurer la « Strangeté »

Les auteurs ont utilisé trois « règles » différentes pour mesurer cette distance, et elles étaient toutes d'accord :

Le Score d'Anomalie : À quelle distance cette preuve se trouve-t-elle de la preuve « Lego » la plus proche ? (Comme mesurer la distance entre une note de jazz et une note de piano).
La Perte de Reconstruction : Si l'IA essaie de deviner l'étape suivante d'une preuve « Magique », fait-elle plus d'erreurs que avec une preuve « Lego » ? (Comme un enseignant devinant le mot suivant dans une phrase ; il éprouve plus de difficultés avec les phrases « Magiques »).
Le Contrôle de Densité : Cette preuve vit-elle dans le quartier bondé des « Lego », ou est-elle perdue dans la nature sauvage et vide des « Magiques » ?

Les trois règles ont montré le même schéma : les preuves « Magiques » sont très distinctes lorsqu'elles sont proches de la source, mais elles se fondent dans le décor à mesure que l'on s'en éloigne.

4. Le test du « Robot Solveur »

La partie la plus pratique du document implique un robot nommé Aesop qui tente de résoudre ces problèmes mathématiques automatiquement.

Le Problème : Le robot est excellent pour résoudre les preuves « Lego » (taux de réussite de 20 %) mais très mauvais pour les preuves « Magiques » (seulement 1,5 %). C'est comme un robot qui sait construire avec des blocs mais qui est confus par les sorts magiques.
Le Rebondissement : Les auteurs ont essayé d'aider le robot en lui donnant un « guide neural » (un assistant intelligent qui suggère le premier mouvement).
Le Résultat : Le guide a aidé un peu, mais il n'a pas réglé le problème. Le robot a toujours énormément de mal avec les preuves « Magiques », même lorsqu'elles sont « profondes » et ressemblent à des preuves « Lego ».

La Grande Conclusion : Même si les preuves « Magiques » ressemblent de plus en plus à des preuves « Lego » à mesure que l'on s'éloigne de la source, le robot solveur les considère toujours comme difficiles. Cela suggère que la « Règle Magique » laisse une cicatrice invisible et permanente sur la preuve, ce qui rend la tâche difficile pour les ordinateurs actuels, peu importe l'apparence « normale » de la preuve en surface.

Résumé

Ce document prouve que l'Axième du Choix n'est pas seulement une idée philosophique ; il laisse une empreinte digitale géométrique et mesurable sur les preuves mathématiques.

L'utilisation directe de la règle rend les preuves très « étrangères » pour l'IA.
L'utilisation indirecte les rend plus « normales ».
Cependant, même lorsqu'elles paraissent « normales », les solveurs automatisés éprouvent toujours beaucoup plus de difficultés avec elles qu'avec les preuves purement constructives.

C'est comme découvrir qu'une maison construite avec des « briques magiques » peut ressembler exactement à une maison construite avec des « briques normales » de l'extérieur, mais si vous essayez de la réparer avec un outillage standard, les briques magiques poseront toujours des problèmes.

Résumé Technique : Mesures Géométriques de l'Axiome du Choix dans les Plongements de Preuves Neurales

Énoncé du Problème

L'axiome du choix (AC) a historiquement divisé les fondements mathématiques en camps classiques et constructifs, une distinction qui demeure largement philosophique et méthodologique. Alors que les preuves classiques utilisent des raccourcis non constructifs permis par l'AC, et que les preuves constructives exigent des témoins explicites, il n'était pas clair si ces deux paradigmes diffèrent structurellement de manières détectables au-delà de la simple dépendance aux axiomes. Ce document examine si l'axiome du choix laisse une « signature géométrique » mesurable au sein de l'espace des preuves formelles, spécifiquement dans la bibliothèque Lean 4 Mathlib, et si cette signature a des conséquences opérationnelles pour les prouveurs de théorèmes neuraux.

Méthodologie

Partitionnement des Données et Suivi de Dépendance

Les auteurs utilisent le suivi de la dépendance des axiomes au niveau du noyau de Lean 4 pour partitionner la bibliothèque Mathlib, qui contient 471 260 déclarations certifiées par machine. En effectuant une recherche en largeur sur le graphe de dépendance, ils classent les déclarations en deux ensembles :

Preuves Classiques : Celles qui dépendent transitivement de Classical.choice.
Preuves Constructives : Celles qui n'en dépendent pas.

La « distance » d'une preuve classique est définie comme la longueur de la plus courte chaîne de dépendance reliant cette preuve à Classical.choice. Cela crée un ensemble de données stratifié où les preuves sont groupées par leur profondeur par rapport à l'axiome. L'étude se concentre sur une population filtrée de 42 355 théorèmes (31 144 classiques, 11 211 constructifs) avec des traces de tactiques entre 2 et 200 étapes.

Apprentissage de Représentation Sans Étiquette

Pour mesurer les propriétés géométriques de ces preuves sans biais, les auteurs entraînent un auto-encodeur de débruitage auto-supervisé exclusivement sur des preuves constructives.

Entrée : Les preuves sont représentées comme des séquences de têtes de tactiques (ex: intro, rw, simp), ignorant les arguments spécifiques pour se concentrer sur la composition de la preuve.
Architecture : Un encodeur Transformer à 4 couches couplé à un décodeur à 2 couches. Le modèle est entraîné pour reconstruire les jetons de tactiques masqués (corruption de 20 %) à partir de la séquence d'entrée.
Plongement (Embedding) : Le plongement de la preuve est la moyenne des états cachés de l'encodeur (excluant le padding), normalisée sur la sphère unité.
Contrainte Sans Étiquette : L'encodeur ne voit jamais de preuves classiques lors de l'entraînement, de la construction du vocabulaire ou de la sélection des hyperparamètres. Les preuves classiques servent strictement de population de contrôle.

Mesures Géométriques

Trois métriques complémentaires sont utilisées pour mesurer la divergence des preuves classiques par rapport à la distribution d'entraînement constructive en fonction de leur profondeur de dépendance :

Score d'Anomalie (k-NN) : La distance euclidienne vers les $k$ plus proches voisins constructifs.
Perte de Reconstruction : La perte de cross-entropie subie lorsque le modèle entraîné sur le constructif tente de prédire les jetons masqués dans une preuve classique.
Contenance de Surniveau de Densité : La fraction des preuves classiques tombant en dehors de la région de haute densité (ensemble de surniveau) définie par la distribution d'entraînement constructive.

Évaluation Opérationnelle

L'étude évalue l'impact de ces découvertes géométriques sur la performance de la preuve de théorèmes en utilisant deux systèmes :

aesop : Un prouveur de recherche heuristique symbolique (best-first search).
Hybride (ReProver + aesop) : Une approche guidée par le neural où un générateur de tactiques propose le premier mouvement, suivi de aesop.

Résultats Clés

La Loi de Profondeur

La découverte principale est l'existence d'une « loi de profondeur » : la distinction géométrique entre les preuves classiques et constructives décroît de manière prévisible avec la distance par rapport à Classical.choice.

Séparation Marquée aux Faibles Profondeurs : À la profondeur 2 (preuves invoquant directement des lemmes classiques), la séparation est forte. Le score d'anomalie k-NN atteint une AUC de 0,847, la perte de reconstruction est 34,5 % plus élevée que la ligne de base constructive, et 43 % des preuves classiques tombent en dehors de la région de densité à 90 % du constructif.
Décroissance vers l'Indistinguabilité : À mesure que la profondeur augmente, les métriques convergent vers la ligne de base constructive. À la profondeur 9+, les trois métriques approchent des niveaux de chance (AUC $\approx$ 0,5, perte $\approx$ ligne de base, contenance $\approx$ 90 %), rendant les preuves classiques profondes géométriquement indiscernables des preuves constructives.
Loi de Mélange à Un Seul Paramètre : Les auteurs modélisent ce gradient comme un mélange de deux distributions : une distribution constructive $P$ et une distribution directement classique $R$ . La distribution de profondeur $d$ , notée $Q_d$ , est modélisée comme $Q_d = (1 - \lambda_d)P + \lambda_d R$ , où $\lambda_d$ est un poids de mélange qui diminue avec la profondeur. Les trois mesures distinctes se rejoignent sur une seule courbe lorsqu'elles sont normalisées, soutenant cette loi à un seul paramètre.

Contrôles de Robustesse

La signature est robuste face à plusieurs variables de confusion potentielles :

Mots-clés : La suppression des marqueurs de tactiques classiques explicites (ex: classical, by contra) réduit l'AUC à la profondeur 2 seulement légèrement (de 0,847 à 0,754), indiquant que le signal est structurel et non simplement lexical.
Longueur : La résidualisation des plongements par rapport à la longueur de la preuve n'élimine pas le gradient.
Auteur/Fichier/Sujet : Des modèles à effets mixtes contrôlant l'auteur, le fichier et le sous-domaine mathématique confirment que le signal persiste dans des contextes spécifiques.
Énoncé vs Preuve : Les énoncés de théorèmes montrent un gradient de profondeur beaucoup plus faible (AUC 0,604 agrégé) que les preuves (AUC 0,675 agrégé), confirmant que le signal est principalement compositionnel (structure de la preuve) plutôt que topique (contenu du théorème).
Spécificité de l'Axiome : Bien que propext et Quot.sound présentent également des gradients de profondeur, Classical.choice produit le gradient le plus raide, suggérant un couplage opérationnel unique avec le raisonnement classique.

Conséquences Opérationnelles

La signature géométrique est corrélée avec la performance des prouveurs :

Échec de aesop : aesop résout 20,0 % des théorèmes constructifs mais seulement 1,5 % des classiques (un écart de 13 $\times$ ). Contrairement au signal géométrique, cet écart opérationnel ne s'atténue pas avec la profondeur ; les preuves classiques restent difficiles pour aesop quelle que soit leur distance de l'axiome.
Guidage Neural : L'ajout d'un générateur de tactiques neural (ReProver) réduit l'écart à environ 5 $\times$ (22,0 % vs 4,5 %) mais ne le ferme pas.
Pouvoir Prédictif : Le score d'anomalie géométrique prédit l'échec de aesop de manière nettement plus efficace que la seule longueur de la preuve (l'AUC passe de 0,766 à 0,841 en ajoutant le score d'anomalie).

Signification et Revendications

L'article affirme fournir la première preuve empirique que l'axiome du choix possède un corrélat géométrique mesurable dans l'espace des preuves. Les auteurs soutiennent que :

Distinction Structurelle : La division classique/constructive n'est pas seulement une position philosophique, mais une propriété structurelle de la composition des preuves qui est visible dans les plongements neuraux.
Pertinence Opérationnelle : Cette signature géométrique n'est pas une simple curiosité abstraite ; elle prédit la performance des prouveurs de théorèmes automatisés. La « loi de profondeur » suggère qu'à mesure que les preuves s'éloignent de l'axiome, elles deviennent structurellement plus similaires aux preuves constructives, pourtant la barrière opérationnelle pour les prouveurs symboliques comme aesop reste spécifique à la présence de Classical.choice.
Contribution Méthodologique : Ce travail démontre que l'apprentissage auto-supervisé sans étiquette sur une classe unique (preuves constructives) peut révéler les frontières structurelles d'une classe tenue en réserve (preuves classiques) définie par la dépendance logique, offrant un nouvel outil pour l'analyse méta-mathématique.

Les auteurs restent modestes quant aux mécanismes causaux, notant que bien que la signature géométrique et l'écart opérationnel soient fortement associés, la cause spécifique de la difficulté du prouveur (barrière structurelle vs configuration de l'ensemble de règles) nécessite des investigations plus approfondies. Le travail est présenté comme une invitation à la communauté pour identifier des axes structurels similaires dans les bibliothèques formelles.