Google DeepMind a développé AlphaProof, un système d'IA qui a égalé la performance d'une médaille d'argent à l'Olympiade internationale de mathématiques de 2024, obtenant 28 points sur 42. Le système n'a manqué que d'un point l'or dans la compétition de mathématiques pour étudiants les plus prestigieuse au monde. Cette avancée démontre des progrès dans la capacité de l'IA à gérer des preuves mathématiques complexes.
Les ordinateurs excellent depuis longtemps dans les calculs mais peinent avec le raisonnement logique requis pour les mathématiques avancées. La nouvelle IA de Google DeepMind, AlphaProof, y remédie en atteignant une performance de médaillé d'argent à l'Olympiade internationale de mathématiques de 2024 (IMO), la principale compétition de mathématiques au niveau lycée. L'IMO comportait six problèmes valant sept points chacun, pour un total de 42 points. Les médailles d'or nécessitaient 29 points ou plus, obtenus par 58 des 609 participants, tandis que l'argent était attribué à ceux ayant entre 22 et 28 points, avec 123 lauréats. AlphaProof a obtenu 28 points, résolvant quatre problèmes de manière indépendante pour 21 points et s'appuyant sur l'AlphaGeometry 2 spécialisée pour le problème de géométrie afin d'atteindre le niveau argent.
Le développement d'AlphaProof a commencé par surmonter la pénurie de données d'entraînement pour les preuves mathématiques formelles. L'équipe a utilisé le logiciel Lean, un outil pour des définitions et vérifications mathématiques précises. Pour élargir l'ensemble de données, ils ont entraîné un modèle de langage large Gemini pour traduire des énoncés mathématiques en langage naturel en Lean, générant environ 80 millions d'énoncés formalisés. Comme l'a expliqué Thomas Hubert, chercheur chez DeepMind et auteur principal, « La principale difficulté du travail avec les langages formels est qu'il y a très peu de données. » Malgré les imperfections, « Il y a de nombreuses façons de tirer parti de traductions approximatives », a-t-il ajouté.
L'architecture du système s'inspire d'AlphaZero de DeepMind, combinant un réseau neuronal entraîné par essais et erreurs avec un algorithme de recherche arborescente pour explorer les voies de preuve. Il récompense les preuves correctes et pénalise les étapes inefficaces, favorisant des solutions élégantes. Une nouveauté, l'apprentissage par renforcement en temps de test (TTRL), permet à AlphaProof de générer des variations de problèmes difficiles pour un entraînement en temps réel, imitant la résolution de problèmes humains. « Nous essayions d'apprendre ce jeu par essais et erreurs », a déclaré Hubert.
Cependant, AlphaProof a requis une assistance humaine pour formaliser les problèmes en Lean et a pris plusieurs jours par problème difficile, consommant des centaines de jours-TPU – bien au-delà des limites de temps humaines de 4,5 heures par session. Seulement six humains ont résolu le problème le plus difficile ; AlphaProof était le septième. DeepMind reconnaît les coûts computationnels élevés mais vise à optimiser pour une utilisation plus large. « Nous ne voulons pas nous arrêter aux compétitions de mathématiques. Nous voulons construire un système d'IA qui pourrait vraiment contribuer aux mathématiques au niveau de la recherche », a déclaré Hubert. L'équipe prévoit un programme de testeurs de confiance pour partager un outil AlphaProof avec des mathématiciens.
Le travail est détaillé dans un article de Nature de 2025 (DOI : 10.1038/s41586-025-09833-y).