L’intelligence artificielle surpasse déjà l’humain dans de nombreux domaines techniques, dont la résolution de certains problèmes mathématiques. Récemment, une IA a réfuté cinq conjectures mathématiques alors qu’elle ne disposait au préalable d’aucune information sur ces dernières. Un exploit qui en réjouit certains, et qui en effraie d’autres.
Les conjectures mathématiques sont des théorèmes non validés ou non réfutés. De nombreuses conjectures dans différentes branches des mathématiques ont ainsi été établies au fil des siècles. Elles représentent donc le type de challenge idéal pour tester les compétences de nouveaux algorithmes et réseaux de neurones développés ces dernières années.
Une équipe de recherche de l’université de Tel-Aviv en Israël, dirigée par Adam Zsolt Wagner, a utilisé un système d’intelligence artificielle pour rechercher des exemples qui réfuteraient une série de conjectures de longue date en théorie des graphes, un domaine des mathématiques qui implique l’étude d’objets composés de nœuds et de liens. Les mathématiciens à leur origine pensaient que ces conjectures étaient vraies, mais n’avaient pas été en mesure de les prouver.
Réseaux de neurones et apprentissage automatique
Pour chaque conjecture, Wagner et son équipe ont créé une mesure de la distance entre un exemple et sa réfutation. Par exemple, si une conjecture proposait qu’un certain problème ne pouvait être résolu en moins de cinq étapes, un exemple comportant six étapes serait plus proche de la réfutation qu’un autre comportant sept étapes, et une solution comportant quatre étapes servirait de contre-exemple à la conjecture, permettant sa réfutation.
Ils ont alors programmé un réseau neuronal pour créer des exemples aléatoires et utiliser ces mesures pour évaluer leur pertinence en tant que contre-exemple, par apprentissage automatique. L’IA éliminait les exemples les plus mauvais, puis les remplaçait par d’autres exemples aléatoires avant de recommencer. Dans des dizaines de cas, l’IA n’a pas réussi à trouver un exemple qui réfute la théorie, mais dans cinq cas, elle a trouvé une solution qui montre que la conjecture est fausse.
« Nous éliminons simplement les mauvais exemples et apprenons des meilleurs à chaque itération », explique Wagner. « C’est fondamentalement la chose la plus simple possible, l’architecture. Il n’y a rien d’extraordinaire ».
Wagner a fait tourner l’IA sur son ordinateur portable datant d’il y a 5 ans, qui a impliqué entre quelques heures et quelques jours pour réfuter chacune des cinq conjectures. Selon lui, les résultats étaient souvent contre-intuitifs. « Je n’aurais jamais trouvé ces constructions tout seul, même si vous me donniez des centaines d’années ». Les détails ont été publiés sur le serveur de préimpression arXiv.
« Un énorme avantage de l’intelligence artificielle »
« C’est vraiment impressionnant », déclare Leslie Hogben, de l’université d’État de l’Iowa, dont l’une des conjectures a été réfutée par l’IA. « Ce que nous voyons ici est un énorme avantage de l’intelligence artificielle sans aucun doute, d’un point de vue mathématique. Elle trouve simplement des choses pour nous, comme le ferait une personne très perspicace. Les contre-exemples sont des aiguilles dans des bottes de foin ».
Si l’IA a réussi à réfuter des conjectures, les prouver est cependant beaucoup plus difficile. Pour réfuter une idée, il faut créer et tester une grande quantité de solutions potentielles pour voir si l’une d’elles contredit la conjecture, une tâche mécanique qui peut être automatisée, mais une preuve est un travail créatif qui nécessite des étapes minutieuses et précises, et implique l’enchaînement de nombreuses réflexions.
Le premier théorème à avoir été prouvé à l’aide d’un ordinateur a été le théorème des quatre couleurs, qui stipule qu’il est possible, en n’utilisant que quatre couleurs différentes, de colorier n’importe quelle carte découpée en régions connexes de sorte que deux régions adjacentes — ayant toute une frontière (et non simplement un point) en commun — reçoivent toujours deux couleurs distinctes. La preuve, trouvée en 1976, impliquait l’utilisation d’un ordinateur pour vérifier une liste exhaustive d’exemples. Elle a été considérée comme inélégante par certains à l’époque, mais l’utilisation de l’informatique pour résoudre des problèmes mathématiques est depuis devenue beaucoup plus répandue.
Néanmoins, Hogben estime qu’il est important que les mathématiciens soient toujours en mesure de suivre une preuve informatique. « Personnellement, je n’aurais jamais de problème avec une réfutation (par ordinateur) qui peut être vérifiée. Cependant, une preuve informatique qui n’est pas vérifiable à la main me poserait personnellement quelques problèmes ».
Timothy Gowers, du Collège de France à Paris, a déclaré sur Twitter que l’approche était une preuve de concept intéressante. « Peut-être peut-on en faire un simple outil de vérification des conjectures qui serait d’une grande utilité pour les chercheurs en mathématiques », a-t-il écrit.