Le système d’intelligence artificielle, développé sous la direction du mathématicien Dong Bin de l’Université de Pékin, a résolu le problème d’algèbre posé par le professeur Dan Anderson de l’Université de l’Iowa en 2014. Anderson est décédé en 2022.
Selon les chercheurs, l’intelligence artificielle a résolu le problème en analysant des décennies de littérature mathématique et a confirmé le résultat à elle seule. L’étude n’a pas encore été évaluée par des pairs et a été publiée sur la plateforme arXiv.
RÉALISÉ SANS INTERVENTION HUMAINE
Selon les informations de Mynet, l’équipe a déclaré que le système qu’elle a développé résolvait un problème ouvert d’algèbre commutative « avec presque aucune intervention humaine » et formalisait automatiquement la preuve.
Le système utilisé dans la recherche se compose de plusieurs composants. Le moteur de raisonnement appelé « Rethlas » développe des stratégies de solutions en utilisant le moteur de recherche de théorèmes appelé « Matlas ». Ensuite, le deuxième système appelé « Archon » transforme cette solution en preuve formelle grâce au « LeanSearch ».
Les preuves obtenues sont vérifiées sur Lean 4, qui est également un langage de programmation et un prouveur de théorèmes interactif. Ce système repose sur une vaste bibliothèque contenant des centaines de milliers de définitions et de théorèmes mathématiques.
IL POURRAIT LE RÉSOUDRE EN 80 HEURES
Les chercheurs ont déclaré que l’intelligence artificielle a résolu le problème en environ 80 heures de travail.
Les scientifiques ont souligné que les preuves mathématiques nécessitent une grande précision et que les systèmes d’intelligence artificielle actuels courent toujours le risque de commettre des erreurs ou de produire des « hallucinations ». Malgré cela, il est affirmé que cette approche développée fournit un exemple concret montrant que la recherche mathématique peut être considérablement automatisée.
Selon la recherche, il est indiqué que le processus peut être encore plus accéléré si l’on y ajoute le guidage humain ; Il a été noté que la nouvelle approche est prometteuse dans la mesure où elle produit des résultats vérifiables en combinant des systèmes de raisonnement formels et informels.
