💻 computer science

Towards Solving the Gilbert-Pollak Conjecture via Large Language Models

Ce papier présente un système d'intelligence artificielle qui exploite les grands modèles de langage pour générer et affiner des lemmes géométriques exécutables, atteignant une nouvelle borne inférieure certifiée de 0,8559 pour le rapport de Steiner et réalisant des progrès significatifs vers la conjecture de Gilbert-Pollak, qui résiste depuis longtemps.

Auteurs originaux : Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang

Publié 2026-05-22

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Yisi Ke, Tianyu Huang, Yankai Shu, Di He, Jingchu Gai, Liwei Wang

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 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 soyez un urbaniste cherchant à relier un groupe de maisons par des routes. Vous avez deux façons de procéder :

La méthode « Directe » (Arbre couvrant minimal) : Vous reliez les maisons directement entre elles. Vous ne pouvez construire aucune nouvelle intersection ; vous tracez simplement des lignes entre les maisons existantes.
La méthode « Intelligente » (Arbre de Steiner minimal) : Vous avez le droit de construire de nouvelles intersections invisibles (appelées points de Steiner) n'importe où dans la ville. En ajoutant ces hubs supplémentaires, vous pouvez souvent créer un réseau plus court et utilisant moins d'asphalte que la méthode directe.

La Grande Question :
De combien la méthode « Intelligente » peut-elle être plus courte par rapport à la méthode « Directe » ?

En 1968, les mathématiciens Gilbert et Pollak ont émis une hypothèse célèbre (une conjecture). Ils ont déclaré : « Peu importe comment vous arrangez les maisons, la méthode Intelligente ne sera jamais inférieure à 86,6 % (spécifiquement $\sqrt{3}/2$ ) de la longueur de la méthode Directe. »

Pendant des décennies, les mathématiciens ont tenté de prouver cela. Ils sont parvenus à démontrer qu'elle représentait au moins 82,4 % de la longueur, mais ils sont restés bloqués là-bas. Le problème mathématique ressemblait à un nœud géant et emmêlé que les cerveaux humains ne pouvaient pas défaire, car il existait trop de formes et d'angles possibles à vérifier.

La Nouvelle Approche : L'« Usine de Lemmes » de l'IA
Ce papier décrit un nouveau système où une IA (un modèle de langage de grande taille) aide à dénouer ce nœud. Mais l'IA ne tente pas de résoudre le problème entier d'un coup — ce serait comme demander à un robot d'écrire un roman entier en une seconde. Au lieu de cela, les chercheurs ont construit une usine spécialisée pour l'IA.

Voici comment le système fonctionne, en utilisant une analogie simple :

1. La « Preuve » est un immense puzzle

Pour prouver la règle des 86,6 %, vous devez vérifier chaque forme possible que le réseau routier pourrait prendre. C'est impossible à faire un par un.
À la place, les mathématiciens utilisent une stratégie appelée induction. Ils disent : « Si nous pouvons prouver que chaque fois que nous retirons un morceau du réseau, la pièce restante suit toujours les règles, alors l'ensemble suit les règles. »

Pour ce faire, ils ont besoin de règles minuscules et spécifiques appelées lemmes. Considérez un lemme comme une seule pièce de puzzle parfaite qui dit : « Si les routes ressemblent à cela, alors nous savons avec certitude que la longueur est d'au moins cela. »

2. Le travail de l'IA : Fabriquer les pièces du puzzle

Les chercheurs n'ont pas demandé à l'IA de résoudre tout le puzzle. Ils lui ont demandé quelque chose de beaucoup plus petit : Écrire du code qui génère ces pièces de puzzle.

La Contrainte : On dit à l'IA : « Vous ne pouvez écrire que du code décrivant une forme géométrique spécifique (comme un « Point Régulier Piégé » ou un « Arbre à 4 Points »). »
La Sortie : L'IA écrit un petit programme (un « lemme ») qui dit : « Si les longueurs des routes sont $X, Y, Z$ , alors la longueur totale est bornée par $W$ . »
Le Filet de Sécurité : Le code de l'IA n'est pas cru aveuglément. Il est injecté dans une calculatrice mathématique stricte (comme une calculatrice ultra-précise appelée Mathematica). Si la calculatrice indique que le code est erroné, l'IA réessaie. Si elle dit « Correct », la pièce est ajoutée à la collection.

3. La Boucle de « Réflexion » : Trouver les points faibles

C'est la partie ingénieuse. Le système ne devine pas au hasard.

Le système tente de prouver la règle des 86,6 % en utilisant la collection actuelle de pièces de puzzle.
Il échoue. Il trouve un « goulot d'étranglement » spécifique — une forme étrange de routes où les pièces actuelles ne s'adaptent pas.
Le système dit à l'IA : « Hé, vous avez échoué ici. Regardez cette forme spécifique. Allez écrire une nouvelle pièce de puzzle qui s'adapte exactement à cet endroit. »
L'IA génère un nouveau lemme, la calculatrice le vérifie, et si cela fonctionne, le système réessaie.

C'est comme un jeu vidéo où vous continuez à heurter un mur, et le jeu vous indique exactement où construire un pont pour le franchir.

Le Résultat

Après environ 10 tours de cette boucle « essayer, échouer, réfléchir, améliorer », le système a construit une collection de pièces de puzzle si solide qu'elle a finalement pu prouver une nouvelle règle, plus stricte :

La méthode Intelligente représente au moins 85,59 % de la longueur de la méthode Directe.

C'est une amélioration massive par rapport au précédent record de 82,4 %, qui tenait depuis près de 40 ans.

Pourquoi cela compte (selon le papier)

C'est peu coûteux : L'ensemble du projet de recherche n'a coûté que quelques centaines de dollars en temps de calcul.
C'est rapide : L'IA n'a mis que quelques jours de « réflexion » (et quelques milliers d'appels au modèle) pour accomplir ce que les humains n'ont pas pu faire en des décennies.
C'est rigoureux : L'IA n'a pas simplement « deviné ». Elle a généré du code qui a été vérifié mathématiquement comme étant 100 % correct. La preuve finale est une preuve mathématique standard qui se tient seule, indépendante de l'IA.

En résumé : Les chercheurs n'ont pas demandé à une IA d'être un mathématicien génial. Ils lui ont demandé d'être une assistante brillante et infatigable qui construit de minuscules outils vérifiés (des lemmes) pour aider les humains à résoudre un problème qui était auparavant trop vaste à percer. Ils ont transformé une IA « boîte noire » en un moteur de découverte transparent et étape par étape.

Résumé technique : Vers la résolution de la conjecture de Gilbert-Pollak via les grands modèles de langage

1. Énoncé du problème

L'article traite de la conjecture de Gilbert-Pollak (1968), un problème ouvert fondamental en optimisation combinatoire et en géométrie computationnelle. La conjecture postule que, pour tout ensemble fini de points dans le plan euclidien, le rapport entre la longueur de l'Arbre Minimal de Steiner (SMT) et celle de l'Arbre Couvrant Minimum Euclidien (MST) est minoré par $\sqrt{3}/2 \approx 0,866$ . Ce rapport est connu sous le nom de ratio de Steiner.

Bien que la conjecture ait été vérifiée pour un petit nombre de points ( $n \le 6$ ), la borne inférieure générale pour un $n$ arbitraire est restée stagnante depuis 1985. La précédente borne inférieure de l'état de l'art, établie par Chung et Graham (1985), est de 0,824. Les progrès ont stagné en raison de l'explosion combinatoire des structures topologiques requises pour l'analyse et de l'ingérabilité de la vérification géométrique impliquée dans la dérivation manuelle.

Les auteurs examinent si les grands modèles de langage (LLM), qui ont fait preuve de compétence en mathématiques de niveau concours, peuvent être étendus pour aborder de telles conjectures ouvertes de niveau recherche. Ils notent que le fait de demander naïvement aux LLM de résoudre directement la conjecture entraîne souvent des hallucinations et des lacunes logiques en raison de l'immensité de l'espace de recherche non contraint et de la rareté des concepts de niveau recherche dans les données d'entraînement.

2. Méthodologie

Les auteurs proposent un nouveau système d'IA qui évite la génération directe de preuves de bout en bout. Au lieu de cela, le système décompose le problème en un processus de découverte structuré et itératif, piloté par des fonctions de vérification et de réflexion.

2.1. Le cadre de vérification

La stratégie mathématique centrale repose sur un argument de réduction par induction (Du et Hwang, 1983). Pour prouver une borne inférieure $\rho$ , il faut montrer que pour toute configuration géométrique $w$ , il existe une « séparation » de l'arbre telle qu'une fonction de séparation spécifique $F_\tau(w, \rho) \le 0$ .

Fonctions de vérification : Pour rendre le problème continu minimax traitable, le système introduit des fonctions de vérification. Ce sont des bornes supérieures de fonctions de séparation satisfaisant des contraintes structurelles spécifiques (unimodalité le long des axes de coordonnées).
Propriété du maximum aux sommets : Une contribution théorique clé consiste à prouver que, pour ces fonctions de vérification, le maximum global sur un hyperrectangle borné est atteint à l'un de ses sommets. Cela réduit la vérification d'un domaine continu infini à un ensemble fini de vérifications aux sommets.
Branch-and-Bound : Le système utilise un algorithme de Branch-and-Bound pour partitionner récursivement l'espace des paramètres, en vérifiant la condition aux sommets et en contrôlant la monotonie pour les régions non bornées.

2.2. Agent LLM et génération de lemmes

Plutôt que de demander au LLM de prouver la conjecture, le système lui confie la tâche de générer des lemmes géométriques contraints par des règles, implémentés sous forme de code exécutable. L'espace de recherche est restreint à deux types spécifiques de lemmes :

Lemmes de points réguliers piégés : Prouver que, sous certaines contraintes linéaires, un point régulier implicite est confiné dans une région polygonale bornée, permettant d'établir des bornes de distance.
Lemmes d'arbres de Steiner à 4 points valides : Prouver que, sous certaines conditions de convexité orthogonale spécifiques, une topologie d'arbre de Steiner à 4 points donnée est valide, permettant des calculs de longueur exacts.

L'agent LLM opère dans une boucle :

Sélection : Il sélectionne des prédicats géométriques pertinents (Type A : propriétés intrinsèques ; Type B : conditions de piégeage suffisantes) dans un ensemble prédéfini.
Dérivation : Il utilise des outils symboliques (Mathematica) pour dériver les implications de ces prédicats.
Simplification : Il simplifie des régions algébriques complexes en contraintes linéaires ou à convexité orthogonale, adaptées au modèle de récompense.
Codage : Il sort les conditions dérivées sous forme de fonctions C++ (X_cond, AX_upper_bound, etc.) qui servent de fonctions de vérification.

2.3. Mécanisme de réflexion itérative

Le système utilise un mécanisme de réflexion ciblé pour surmonter les goulots d'étranglement :

Évaluation : Le modèle de récompense tente de certifier une borne inférieure candidate $\rho$ .
Identification des goulots d'étranglement : Si la vérification échoue, le système identifie la « région goulot d'étranglement » spécifique (un ensemble d'hyperrectangles non certifiés) où les lemmes actuels sont insuffisants.
Feedback : Cette région est convertie en un prompt structuré, instruisant le LLM à générer de nouveaux lemmes ciblant spécifiquement les contraintes géométriques de ce goulot d'étranglement.
Raffinement : Les nouveaux lemmes sont validés et ajoutés à l'ensemble des fonctions de vérification, et le processus se répète.

3. Contributions clés

Nouveau système d'IA pour la découverte théorique : L'article présente un système qui automatise avec succès la découverte de lemmes géométriques intermédiaires pour un problème ouvert vieux de plusieurs décennies, dépassant la résolution standard de problèmes de niveau concours.
Fonctions de vérification et propriété du sommet : Les auteurs définissent formellement les fonctions de vérification et prouvent la « propriété du maximum aux sommets », ce qui permet une vérification rigoureuse et computationnellement traitable des bornes inférieures sur des domaines continus.
Stratégie de décomposition : En décomposant la conjecture en la génération de lemmes spécifiques et contraints par des règles (points piégés et arbres à 4 points valides) plutôt qu'en preuves complètes, le système gère efficacement l'espace de recherche et minimise les hallucinations.
Réflexion pilotée par les goulots d'étranglement : L'introduction d'un mécanisme de réflexion qui identifie et cible explicitement les régions géométriques empêchant toute amélioration supplémentaire, plutôt que de s'appuyer sur une auto-correction générique.

4. Résultats

Nouvelle borne inférieure : Le système a réussi à améliorer la borne inférieure certifiée du ratio de Steiner, passant de 0,824 (Chung et Graham, 1985) à 0,8559.
Efficacité : L'ensemble de l'effort de recherche n'a requis qu'environ 10 itérations de la boucle de raffinement.
Utilisation des ressources : Le processus a impliqué environ milliers d'appels LLM et a consommé environ 0,5 million de tokens (environ 35K par tour) sur 4,6 heures de temps de raisonnement. Le coût de calcul total s'est élevé à quelques centaines de dollars.
Robustesse : Des expériences utilisant différents modèles de base LLM (GPT-5 et Gemini 3 Pro) ont produit une convergence cohérente vers la même borne inférieure, démontrant la robustesse du cadre face au choix du modèle.
Vérification : Tous les lemmes générés ont été vérifiés manuellement pour leur exactitude, et la borne inférieure finale a été rigoureusement vérifiée sur l'ensemble de l'espace des paramètres à l'aide d'outils symboliques (Décomposition Algébrique Cylindrique).

5. Signification et revendications

L'article prétend démontrer le fort potentiel des systèmes basés sur les LLM pour la recherche mathématique avancée, en particulier dans les domaines nécessitant une intuition géométrique profonde et une recherche combinatoire.

Évolutivité : Les auteurs soutiennent que leur approche offre un paradigme évolutif où les LLM gèrent la recherche créative et la génération de lemmes, tandis que les outils symboliques gèrent la vérification formelle. Cette division du travail exploite les forces des deux.
Accessibilité : Avec un coût total de seulement quelques centaines de dollars, ce travail suggère que la recherche théorique assistée par LLM est accessible aux chercheurs sans budgets de calcul massifs.
Généralisabilité : Les auteurs proposent deux principes de conception qu'ils estiment transférables à d'autres problèmes de découverte mathématique :
1. Construire un espace de raisonnement structuré en décomposant les problèmes en lemmes paramétrés plutôt qu'en preuves de bout en bout.
2. Réfléchir aux échecs localisés du vérificateur en renvoyant des régions de goulot d'étranglement spécifiques au modèle pour guider un raffinement ciblé.

L'article conserve une modestie concernant le résultat final, notant que si la borne inférieure est significativement améliorée, la conjecture elle-même (0,866) reste non prouvée. De plus, les auteurs reconnaissent les limitations actuelles, telles que la dépendance à la vérification humaine pour l'exactitude des lemmes et les problèmes d'évolutivité de la vérification symbolique (CAD) pour des topologies de dimension supérieure ou plus complexes. Ils suggèrent que des travaux futurs pourraient faire intervenir des assistants de preuve formelle (par exemple, Lean) pour parvenir à une découverte entièrement autonome.