Dans une nouvelle sensationnelle du monde des mathématiques, un groupe d'anciens élèves de Tsinghua, aidés par l'IA, a réussi à prouver 162 théorèmes mathématiques auparavant insolubles. Plus impressionnant encore, cet agent intelligent, nommé LeanAgent, a même résolu le problème de formalisation de la conjecture de Freiman-Ruzsa sur les polynômes posée par Terence Tao ! Cela nous force à constater que les méthodes de recherche en sciences fondamentales ont été radicalement transformées par l'IA.
Comme chacun le sait, les modèles linguistiques actuels (LLM), bien que performants, sont pour la plupart statiques et incapables d'apprendre de nouvelles connaissances en ligne, et prouver des théorèmes de mathématiques supérieures est une tâche extrêmement difficile. Cependant, LeanAgent, développé conjointement par les équipes de recherche du California Institute of Technology, de l'Université Stanford et de l'Université de Washington, est un assistant IA doté d'une capacité d'apprentissage continu, capable d'apprendre et de prouver des théorèmes sans cesse.
LeanAgent utilise un chemin d'apprentissage soigneusement conçu pour gérer les différentes difficultés mathématiques, gérant un flux constant de connaissances mathématiques grâce à une base de données dynamique, garantissant qu'il ne perd pas les compétences déjà acquises lorsqu'il apprend de nouvelles connaissances. Les expériences ont montré qu'il a réussi à prouver 162 théorèmes mathématiques auparavant insolubles à partir de 23 bibliothèques de code Lean différentes, des performances 11 fois supérieures à celles des grands modèles traditionnels, ce qui est tout simplement étonnant !
Ces théorèmes couvrent de nombreux domaines des mathématiques supérieures, y compris des problèmes complexes d'algèbre abstraite et de topologie algébrique. LeanAgent est non seulement capable de commencer par des concepts simples pour progressivement maîtriser des sujets complexes, mais il fait également preuve d'une excellente performance en termes de stabilité et de transfert inverse.
Cependant, le défi de Terence Tao reste un obstacle pour l'IA. Bien que les prouveurs de théorèmes interactifs (ITP) comme Lean jouent un rôle important dans la formalisation et la vérification des preuves mathématiques, la construction de telles preuves est souvent complexe et longue, nécessitant des étapes très précises et un grand nombre de bibliothèques de code mathématiques. Des grands modèles avancés comme o1 et Claude peuvent faire des erreurs lorsqu'ils sont confrontés à des preuves non formalisées, ce qui souligne les lacunes des LLM en termes de précision et de fiabilité des preuves mathématiques.
Les recherches passées ont tenté d'utiliser les LLM pour générer des étapes de preuve complètes. LeanDojo, par exemple, est un prouveur de théorèmes créé en entraînant un grand modèle sur un ensemble de données spécifique. Cependant, les données de preuves de théorèmes formalisées sont extrêmement rares, ce qui limite l'applicabilité de cette méthode. Un autre projet, ReProver, est un modèle optimisé pour la bibliothèque de code de preuve de théorèmes Lean mathlib4. Bien qu'il couvre plus de 100 000 théorèmes et définitions mathématiques formalisés, il se limite aux mathématiques de niveau licence et, par conséquent, ses performances sont médiocres face à des problèmes plus complexes.
Il est important de noter que la nature dynamique de la recherche mathématique pose un défi supplémentaire à l'IA. Les mathématiciens travaillent souvent sur plusieurs projets simultanément ou alternativement. Terence Tao, par exemple, travaille simultanément sur plusieurs domaines de recherche, notamment la conjecture PFR et la moyenne symétrique des nombres réels. Ces exemples montrent une lacune essentielle des méthodes actuelles de preuve de théorèmes par l'IA : l'absence d'un système IA capable d'apprendre et de s'améliorer de manière adaptative dans différents domaines mathématiques, notamment lorsque les données Lean sont limitées.
C'est pourquoi l'équipe de LeanDojo a créé LeanAgent, un nouveau framework d'apprentissage continu visant à résoudre les problèmes susmentionnés. Le processus de LeanAgent comprend la dérivation de la complexité des théorèmes pour élaborer un programme d'apprentissage, l'entraînement progressif pour équilibrer la stabilité et la flexibilité pendant l'apprentissage, et l'utilisation de la recherche par arbre de priorité optimale pour trouver les théorèmes non encore prouvés.
LeanAgent est utilisé avec n'importe quel grand modèle, utilisant la « récupération » pour améliorer ses capacités de généralisation. Son innovation réside dans l'utilisation d'une base de données dynamique personnalisée pour gérer les connaissances mathématiques en constante expansion, ainsi qu'une stratégie d'apprentissage par le biais de cours basés sur la structure des preuves Lean, facilitant l'apprentissage de contenus mathématiques plus complexes.
Pour faire face au problème de l'oubli catastrophique de l'IA, les chercheurs ont utilisé une méthode d'entraînement progressif, permettant à LeanAgent de s'adapter continuellement aux nouvelles connaissances mathématiques sans oublier les connaissances acquises précédemment. Ce processus implique un entraînement incrémental sur chaque nouvel ensemble de données, garantissant un équilibre optimal entre stabilité et flexibilité.
Grâce à cet entraînement progressif, LeanAgent a démontré des performances exceptionnelles dans la preuve de théorèmes, réussissant à prouver 162 problèmes non résolus par l'homme, en particulier dans les théorèmes stimulants de l'algèbre abstraite et de la topologie algébrique. Ses capacités à prouver de nouveaux théorèmes sont 11 fois supérieures à celles de ReProver statique, tout en conservant sa capacité à prouver les théorèmes connus.
LeanAgent a montré des caractéristiques d'apprentissage progressif dans le processus de preuve de théorèmes, passant de théorèmes simples à des théorèmes plus complexes, démontrant la profondeur de sa maîtrise des connaissances mathématiques. Par exemple, il a prouvé des théorèmes de structures algébriques fondamentales liées à la théorie des groupes et à la théorie des anneaux, démontrant une compréhension approfondie des mathématiques. Dans l'ensemble, LeanAgent, avec ses puissantes capacités d'apprentissage et d'amélioration continus, offre des perspectives passionnantes pour le monde des mathématiques !
Adresse de l'article : https://arxiv.org/pdf/2410.06209
