L'École impliquée au sein d'un programme de recherche de Meta

27 mai 2022

IA pour les mathématiques avec Meta

Les mathématiques sont l'une des activités les plus difficiles de l'esprit humain. Bien que l'IA ait atteint des performances surhumaines dans des jeux à 2 joueurs comme les échecs ou le go, les modèles les plus avancés sont toujours incapables de prouver même de simples déclarations mathématiques.

Depuis 2020, le CERMICS et une équipe de Meta AI (le laboratoire de Facebook en intelligence artificielle) entraîne une intelligence artificielle capable de prouver des théorèmes et des exercices mathématiques. L'IA reçoit un énoncé mathématique et le résout en donnant la preuve étape par étape. L'approche employée est inspirée d'AlphaZero, l'intelligence artificielle qui apprend à jouer aux échecs contre elle-même et bat tous les humains.

Ce nouvel algorithme, HyperTree Proof Search (HTPS) est inspiré du récent succès d'AlphaZero. Le modèle développé est capable de prouver des théorèmes mathématiques de manière entièrement automatisée et surpasse de manière significative le SOTA machine learning.

Avec HTPS, le modèle atteint les performances SOTA sur plusieurs environnements mathématiques tels que Metamath ou Lean, et a résolu plusieurs problèmes lors des Olympiades mathématiques internationales.

Cette équipe compte 8 personnes : 6 chercheurs de Meta AI, 1 chercheur de Vrije Universiteit Amsterdam et Amaury Hayat chercheur au CERMICS. 

>> Pour en savoir plus