Terence Tao aime ! ChatGPT s'avère automatiquement une percée majeure, et l'IA dominera le monde des mathématiques dans 10 ans

**Source :**Xinzhiyuan

**Guide :**Bien que beaucoup de gens ne veuillent pas l'admettre, il est très probable que l'IA dépassera les mathématiciens humains d'ici dix ans.

Il y a quelques jours, un article rédigé par des chercheurs de Caltech et du MIT utilisant ChatGPT pour prouver des théorèmes mathématiques a explosé et attiré une grande attention dans le cercle des mathématiques.

Jim Fan, le scientifique en chef de Nvidia, l'a transmis avec enthousiasme, affirmant que le copilote des mathématiques de l'IA est arrivé et que la prochaine personne qui découvrira de nouveaux théorèmes sera un mathématicien de l'IA entièrement automatique !

Le New York Times a également publié un article récemment, affirmant que les mathématiciens sont prêts et que l'IA rattrapera ou même dépassera les meilleurs mathématiciens humains d'ici dix ans.

Et Tao Zhexuan lui-même a republié cet article.

Siobhan Roberts a participé à l'atelier IPAM de cette année organisé par Machine Assisted Proofs, puis elle a écrit cet article sur l'IA et les mathématiques basé sur sa propre expérience et des entretiens

**L'IA vient aussi subvertir le monde des mathématiques ! **

Aujourd'hui, les mathématiciens doivent faire face à la dernière force révolutionnaire : l'IA.

En 2019, l'informaticien Christian Szegedy, un ancien employé de Google qui travaille maintenant dans une startup de Bay Area, a prédit que les systèmes informatiques égaleraient ou dépasseraient les capacités de résolution de problèmes des meilleurs mathématiciens humains d'ici une décennie. L'année dernière, il a révisé la date cible à 2026.

Jeremy Avigad, logicien de l'Université Carnegie Mellon (en bleu) avec des étudiants de l'école d'été de mathématiques formelles

Akshay Venkatesh, lauréat de la médaille Fields 2018 et mathématicien à l'Institute for Advanced Study de Princeton, n'est actuellement pas intéressé par l'utilisation de l'IA, mais il est très désireux de discuter de sujets liés à l'IA.

Dans une interview l'année dernière, Venkatesh a déclaré : "Je veux que mes étudiants réalisent que ce domaine va beaucoup changer."

Et récemment, son attitude est la suivante : "Je n'ai aucune objection à l'utilisation délibérée, même délibérée, de l'IA pour aider la compréhension humaine. Mais je crois fermement que nous devons être attentifs et prudents quant à la façon dont nous l'utilisons."

En février de cette année, l'Institut de mathématiques théoriques et appliquées de l'UCLA a organisé un atelier sur les "preuves assistées par machine".

Le principal organisateur du séminaire est Tao Terence, un mathématicien qui a remporté la médaille Fields en 2006 et travaille à l'UCLA.

Il a souligné que l'utilisation de l'IA pour assister les preuves mathématiques est en fait un phénomène digne d'attention.

Ce n'est que ces dernières années que les mathématiciens ont commencé à s'inquiéter de la menace potentielle de l'IA, qu'il s'agisse de la destruction de l'esthétique mathématique par l'IA ou de la menace pour les mathématiciens eux-mêmes.

Et des membres exceptionnels de la communauté mettent ces questions sur la table et commencent à explorer comment « briser le tabou ».

Les organisateurs de l'école d'été, de gauche à droite : Avigad, Patrick Massot et Heather Macbeth

Des primitives géométriques euclidiennes au code informatique

Depuis des millénaires, les mathématiciens se sont adaptés aux dernières avancées de la logique et du raisonnement. Mais sont-ils prêts pour l'IA ?

Portrait du mathématicien grec du XVIIe siècle Euclide au Getty Museum de Los Angeles : il est vêtu de haillons et tient son traité de géométrie, Elements

Depuis plus de 2 000 ans, le texte d'Euclide est le paradigme de l'argumentation et du raisonnement mathématiques.

Jeremy Avigad, logicien de l'Université Carnegie Mellon, dit qu'Euclide a commencé par une "définition" presque poétique sur laquelle construire les mathématiques de son temps - en utilisant des concepts de base, des définitions et des théorèmes précédents, chacun successif. Les étapes "suivent clairement" les étapes précédentes, en manière à prouver les choses.

Certains se sont plaints que certaines des étapes "évidentes" d'Euclide n'étaient pas si évidentes, mais le Dr Avigad a déclaré que le système fonctionnait.

Mais après le XXe siècle, les mathématiciens n'étaient plus disposés à fonder les mathématiques sur cette base géométrique intuitive.

Au lieu de cela, ils ont développé des systèmes formels avec des représentations symboliques précises et des règles mécaniques.

Finalement, dans un tel système, les mathématiques pourraient être traduites en code informatique.

En 1976, le théorème des quatre couleurs est devenu le premier théorème majeur à être prouvé à l'aide de calculs de force brute.

Le théorème des quatre couleurs : quatre couleurs suffisent pour remplir une carte de sorte qu'aucune région adjacente n'ait la même couleur

AI qui se plaint : Désolé, je ne comprends pas votre théorème

Il existe un tel gadget mathématique appelé Proof Assistant, ou Interactive Theorem Prover.

Étape par étape, les mathématiciens convertissent les preuves en code, puis utilisent des logiciels pour vérifier que le raisonnement est correct.

Le processus de vérification est accumulé dans une bibliothèque de référence de spécification dynamique, qui est disponible pour les autres.

Le Dr Avigad, directeur du Hoskinson Center for Formal Mathematics, a déclaré que ce type de formalisation a jeté les bases des mathématiques d'aujourd'hui, tout comme Euclide a tenté de transcoder les mathématiques de cette époque, leur fournissant ainsi une base.

Récemment, Lean, un système d'assistant de preuve open-source, a de nouveau attiré beaucoup d'attention.

Lean a été développé par l'actuel informaticien d'Amazon Leonardo de Moura alors qu'il était chez Microsoft.

Lean utilise un raisonnement automatisé, propulsé par l'IA GOFAI à l'ancienne, une IA symbolique inspirée de la logique.

Jusqu'à présent, Lean a vérifié un théorème intéressant qui transforme une sphère de l'intérieur vers l'extérieur, ainsi qu'un théorème clé qui unifie les schémas à travers la sphère mathématique.

Cependant, l'assistant de preuve a aussi des lacunes : il se plaindra souvent de ne pas comprendre les définitions, les axiomes ou les étapes de raisonnement saisis par le mathématicien, il est donc aussi nommé "preuve plaignant".

Ces plaintes compliqueraient la recherche, mais le type de fonctionnalité qui fournit une rétroaction ligne par ligne rendrait également le système utile pour l'enseignement, explique Heather Macbeth, mathématicienne à l'Université Fordham.

Ce printemps, la Dre Macbeth a conçu un cours « bilingue ». Elle a traduit chaque problème au tableau noir en code Lean dans les notes de cours, et les étudiants doivent soumettre des solutions en langage Lean et naturel.

"Cela leur a donné confiance", a déclaré le Dr Macbeth, car ils recevaient un retour instantané sur le moment où la preuve était terminée et si chaque étape était bonne ou mauvaise.

Et après avoir assisté à un atelier, la mathématicienne Emily Riehl de l'Université Johns Hopkins s'est lancée.

Emily Riehl, mathématicienne à l'Université Johns Hopkins, utilise un assistant de preuve expérimentale

Elle a utilisé une applet d'assistant de preuve pour prouver les théorèmes dans ses articles publiés précédemment.

Après l'avoir utilisé, elle a été choquée. "Je comprends maintenant le processus de preuve beaucoup plus profondément que je ne l'ai jamais fait. Ma pensée est si claire que je peux l'expliquer à l'ordinateur le plus stupide."

Un projet de groupe auquel les élèves ont participé lors de l'École d'été de formalisation mathématique

** Raisonnement violent - ce n'est pas "mathématique" **

Un autre outil que les informaticiens utilisent souvent pour résoudre certains problèmes mathématiques est appelé "raisonnement violent", mais la communauté des mathématiques se moque souvent de cette méthode.

Cependant, les scientifiques de l'IA ne semblent pas se soucier beaucoup des idées des mathématiciens et continuent d'utiliser leurs propres méthodes familières pour capturer les "hautes terres" des mathématiques.

Heule, informaticien à l'Université Carnegie Mellon, a utilisé un fichier "SAT solver" de 200T pour résoudre le "triple problème booléen de Pythagore" en 2016.

Le magazine « Nature » a déclaré dans l'article : La preuve de 200 T est le plus grand processus de preuve de l'histoire. Est-ce vraiment mathématique d'utiliser ces outils pour résoudre des problèmes ?

Mais de l'avis de l'informaticien Heule, l'auteur de l'article sur la résolution du problème lui-même, "cette approche est nécessaire pour résoudre des problèmes au-delà de la portée des capacités humaines".

De même, après avoir vaincu des humains dans une partie d'échecs (AlphaZero), DeepMind a conçu des algorithmes d'apprentissage automatique pour résoudre le repliement des protéines (AlphaFold).

DeepMind a publié un article affirmant que la façon dont ils ont obtenu ces résultats était d'utiliser l'IA pour guider l'intuition humaine afin de faire progresser les mathématiques.

Yuhuai Wu, un ancien informaticien de Google qui démarre maintenant une entreprise dans la Bay Area, a également déclaré que la direction de son entreprise était d'utiliser l'apprentissage automatique pour résoudre des problèmes mathématiques.

Son projet actuel, Minerva, est un grand modèle de langage affiné pour résoudre des modèles mathématiques.

À l'avenir, il espère que le projet se transformera en un "mathématicien automatisé" qui pourra "résoudre des problèmes mathématiques de manière indépendante" en tant qu'assistant de recherche général.

Les mathématiques sont un test décisif

D'autre part, de nombreux mathématiciens qui ont été en contact approfondi avec la technologie de l'IA ont également exprimé leur inquiétude quant au fait que l'IA n'est pas prise au sérieux dans la recherche mathématique.

Ils croient que la technologie de l'intelligence artificielle peut souvent "directement" aider les mathématiciens à "trouver" les réponses qu'ils veulent.

Bien que les mathématiciens ou les experts en IA n'aient aucune idée de la façon dont l'IA a trouvé cette réponse.

Geordie Williamson, un mathématicien qui a travaillé avec DeepMind, a partagé une fois une expérience de travail avec DeepMind.

Au cours de sa coopération avec DeepMind, un réseau de neurones découvert par DeepMind peut prédire la valeur des données qu'il juge très importante, et elle est extrêmement précise.

Il essaie vraiment de comprendre comment l'IA le fait, car cela pourrait être la base d'un théorème.

Mais il ne pouvait toujours pas comprendre la logique de l'IA à la fin, et les gens de DeepMind ne pouvaient pas le faire non plus.

Comme Euclide, les réseaux de neurones trouvent d'une manière ou d'une autre la vérité, mais les raisons logiques sont difficiles à comprendre.

L'inférence, en revanche, du point de vue du mathématicien, est l'essence des mathématiques mais une pièce manquante du puzzle de l'apprentissage automatique.

Dans le monde de la technologie, le monde de la technologie serait parfaitement satisfait s'il existait une boîte noire qui fournirait une solution à un problème la plupart du temps.

L'IA est une telle boîte noire.

Mais les mathématiciens ne sont pas satisfaits de cette situation.

Selon le mathématicien, essayer de comprendre le fonctionnement des réseaux de neurones soulève des questions mathématiques fascinantes.

Et la résolution de ces problèmes permettra aux mathématiciens "d'apporter des contributions significatives au monde".

Si l'IA peut prouver des théorèmes mathématiques

Que ferions-nous si le monde était inondé d'hypothèses générées par l'IA ?

Les internautes ont envoyé la torture de l'âme à cela, et j'ai des doutes sur le fait que le système d'IA proposant de nouvelles hypothèses/formules est la première étape, car DeepMind l'a déjà fait dans la théorie des nœuds.

Je me demande comment la communauté réagira au flot de nouvelles hypothèses émises par l'IA. C'est une chose de vérifier un argument logique créé par une IA ; c'en est une autre d'être submergé par des millions de suggestions "oh, cela pourrait être vrai". Je ne pense pas que nos systèmes d'examen et de publication existants soient prêts pour cela.

Comment cela affecte-t-il la confiance des gens dans les mathématiques ?

On a fait valoir que les machines ne seraient pas capables de faire des mathématiques de sitôt, mais on pourrait voir qu'elles changeaient la façon dont la recherche est effectuée de la même manière que les modèles d'apprentissage automatique et la puissance de calcul ont changé le domaine de la biologie.

Certains internautes ont dit que depuis AlphaDev, je réfléchissais à ce problème, mais le même programme peut construire des algorithmes de tri et peut également utiliser des vérificateurs de preuves automatiques pour prouver des théorèmes mathématiques. La vraie question est de savoir si cela peut être utilisé pour prouver quelque chose d'important, pas seulement une découverte insignifiante.

Cependant, certains internautes sont encore sceptiques quant à savoir si les outils de type GPT peuvent vraiment découvrir des vérités précieuses.

Certains internautes ont également souligné qu'il peut y avoir une différence entre les humains et l'IA dans la compréhension et l'attention aux mathématiques. L'IA prouve ce qui est vrai, tandis que les humains se concentrent toujours sur pourquoi c'est vrai.

Les références: