LeanDojo est une plateforme open source permettant de prouver des théorèmes mathématiques à l’aide de modèles de langage.

La démonstration automatisée de théorèmes (ATP) est une tâche qui génère des preuves pour les théorèmes formulés en logique formelle. Elle est utile pour les mathématiques formelles et soutient la vérification formelle, qui garantit l’exactitude et la sécurité des applications à haut risque.

Cependant, l’ATP est un défi en raison de son vaste espace de recherche. C’est pourquoi la preuve interactive de théorèmes (Interactive Theorem Proof – ITP) est apparue comme une alternative. Dans la PTI, les preuves sont générées par des mathématiciens qui interagissent avec des outils logiciels appelés assistants de preuve.

L’apprentissage automatique pourrait automatiser ce processus, ouvrant ainsi une nouvelle voie à la démonstration de théorèmes.

Les grands modèles de langage peuvent automatiser la preuve des théorèmes

Les grands modèles de langage combinés à des assistants de preuve, tels que Lean, sont des candidats pour ce processus.

Cependant, les méthodes existantes sont difficiles à reproduire ou à faire évoluer en raison de la propriété du code, des données et des exigences informatiques élevées, selon une équipe de chercheurs de Caltech, Nvidia, MIT, UC Santa Barbara et UT Austin.

Pour remédier à cette situation, ils ont créé LeanDojo, une plateforme open source permettant de prouver des théorèmes mathématiques à l’aide de modèles de langage.

LeanDojo et ReProver ouvrent la voie à d’autres recherches

LeanDojo offre deux fonctionnalités principales pour la démonstration de théorèmes basée sur l’apprentissage : l’extraction de données et l’interaction programmatique du modèle avec Lean, un assistant de preuve largement utilisé. Selon les chercheurs, LeanDojo est le premier outil capable d’interagir de manière fiable avec Lean, ce qui devrait réduire considérablement les erreurs de preuve.

LeanDojo s’attaque également à un goulot d’étranglement important dans la démonstration de théorèmes : la sélection des prémisses. L’équipe en fait la démonstration avec ReProver (Retrieval-Augmented Prover), un prouveur basé sur un modèle de langage qui génère une stratégie de preuve basée sur certaines prémisses extraites de la bibliothèque mathématique de Lean.

Selon l’équipe, ReProver surpasse d’autres méthodes, prouvant un pourcentage significatif de théorèmes sur le benchmark LeanDojo ainsi que sur deux ensembles de données existants, MiniF2F et ProofNet. ReProver peut également prouver des théorèmes pour lesquels il n’existe pas encore de preuve dans Lean, ce qui en fait un outil utile pour étendre les bibliothèques mathématiques existantes dans Lean.

Des modèles de langage comme coauteurs des mathématiques d’ici 2026 ?
L’équipe publie également un benchmark construit avec LeanDojo, qui inclut près de 97 000 théorèmes de Mathlib, ainsi qu’un plugin pour ChatGPT.

Le mathématicien Terence Tao a récemment prédit que les modèles de langage utilisant des outils externes pourraient devenir des coauteurs de confiance en mathématiques et dans d’autres sciences d’ici 2026. LeanDojo et ReProver montrent à quoi ces outils pourraient ressembler et offrent désormais aux autres chercheurs une base d’amélioration.

De plus amples informations sont disponibles sur le site web de LeanDojo.