Baptisés AlphaProof et AlphaGeometry 2, ces systèmes d'IA spécialisés ont résolu quatre des six problèmes présentés cette année dans le cadre de l'Olympiade Internationale de Mathématiques. Une compétition mondiale de mathématiques à destination des élèves du secondaire (lycées et collèges).
Google DeepMind rapporte que les solutions ont été notées par d'éminents mathématiciens, en respectant les règles d'attribution de points de la compétition. L'IA aurait ainsi obtenu la médaille d'argent en résolvant les problèmes.
Initialement, les problèmes ont été traduits manuellement en langage mathématique formel afin que les systèmes d'IA soient en mesure de les comprendre. La résolution d'un problème a été obtenue en quelques minutes et jusqu'à trois jours pour les autres.
AlphaGeometry 2 a buté sur deux problèmes
AlphaProof a résolu deux problèmes d'algèbre et un problème de théorie des nombres considéré le plus difficile du concours, avec seulement cinq participants (humains) victorieux cette année. AlphaGeometry 2 a résolu un problème de géométrie, mais a échoué pour deux problèmes de combinatoire.
AlphaProof est présenté comme un nouveau système basé sur l'apprentissage par renforcement pour le raisonnement mathématique formel. Il est entraîné dans le langage Lean. AlphaGeometry 2 est décrit comme une version améliorée d'un précédent modèle d'IA de résolution de géométrie. Il s'appuie sur un modèle de langage basé sur Gemini et entraîné sur davantage de données.
Un accomplissement à pondérer
" Nous sommes enthousiastes à l'idée d'un avenir dans lequel les mathématiciens travailleront avec des outils d'IA pour explorer des hypothèses, essayer de nouvelles approches audacieuses pour résoudre des problèmes de longue date et compléter rapidement des éléments de preuve qui prennent du temps ", écrivent les équipes d'AlphaProof et AlphaGeometry.
Pour le moment, le mathématicien anglais (Sir) Timothy Gowers (médaille Fields en 1998) se dit très impressionné, mais apporte cependant quelques réserves.
Hormis l'assistance humaine préalable pour la traduction, il souligne que pour certains problèmes, il a fallu beaucoup de temps à l'IA pour les résoudre (plus de 60 heures). " Si les concurrents humains du concours avaient eu droit à ce genre de temps par problème, ils auraient sans aucun doute obtenu de meilleurs résultats. "
N.B. : Source images : Google DeepMind.
