Lors de l’Olympiade internationale de mathématiques (OMI) de 2024, un concurrent a si bien réussi qu’il aurait reçu le prix d’argent, à une exception près : il s’agissait d’un système d’IA. C'était la première fois qu'IA obtenait une performance de niveau médaille dans l'histoire de la compétition. Dans un article publié dans la revue Natureles chercheurs détaillent la technologie derrière cette réalisation remarquable.
L'IA est AlphaProof, un programme sophistiqué développé par Google DeepMind qui apprend à résoudre des problèmes mathématiques complexes. La réussite de l'OMI était assez impressionnante, mais ce qui rend AlphaProof vraiment spécial, c'est sa capacité à trouver et à corriger les erreurs. Même si les grands modèles de langage (LLM) peuvent résoudre des problèmes mathématiques, ils ne peuvent souvent pas garantir l'exactitude de leurs solutions. Il se peut qu’il y ait des failles cachées dans leur raisonnement.
AlphaProof est différent car ses réponses sont toujours correctes à 100 %. En effet, il utilise un environnement logiciel spécialisé appelé Lean (développé à l'origine par Microsoft Research) qui agit comme un enseignant strict vérifiant chaque étape logique. Cela signifie que l’ordinateur vérifie lui-même les réponses et que ses conclusions sont donc fiables.
Processus de formation en trois étapes
Entraîner ce puissant système à raisonner à un niveau d’élite impliquait trois étapes de formation différentes. Premièrement, les chercheurs ont exposé AlphaProof à environ 300 milliards de jetons de code général et de texte mathématique pour lui donner une large compréhension de concepts tels que la logique, le langage mathématique et la structure de programmation. Ensuite, il a reçu 300 000 épreuves de mathématiques rédigées par des experts qui étaient déjà dans l'environnement Lean.
La dernière étape était celle où le système apprenait à résoudre les problèmes par lui-même. Il lui a été confié un devoir massif de 80 millions de problèmes mathématiques formels à résoudre. Grâce à l'apprentissage par renforcement (RL), basé sur des essais et des erreurs, AlphaProof a été récompensé pour chaque preuve réussie. En s’attaquant à des problèmes mathématiques à une telle échelle, le système a appris lui-même des stratégies de raisonnement nouvelles et complexes qui allaient au-delà de la copie d’exemples humains.
Pour les problèmes les plus difficiles, AlphaProof a utilisé une technique développée par les chercheurs appelée Test-Time RL (TTRL), qui crée et résout des millions de versions simplifiées du problème cible jusqu'à ce qu'il trouve une solution.
« Notre travail démontre que l'apprentissage à grande échelle à partir d'une expérience concrète produit des agents dotés de stratégies de raisonnement mathématique complexes, ouvrant la voie à un outil d'IA fiable pour la résolution de problèmes mathématiques complexes », ont écrit les chercheurs dans leur article.
En plus de résoudre des problèmes mathématiques apparemment insolubles, AlphaProof pourrait également être utilisé par des mathématiciens pour corriger leur travail et les aider à développer de nouvelles théories.
Écrit pour vous par notre auteur Paul Arnold, édité par Gaby Clark, et vérifié et révisé par Robert Egan, cet article est le résultat d'un travail humain minutieux. Nous comptons sur des lecteurs comme vous pour maintenir en vie le journalisme scientifique indépendant. Si ce reporting vous intéresse, pensez à faire un don (surtout mensuel). Vous obtiendrez un sans publicité compte en guise de remerciement.
