LeanDojo : Preuve de théorèmes avec des modèles de langage augmentés par la récupération

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

June 27, 2023

Auteurs: Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, Anima Anandkumar

cs.AI

Résumé

Les grands modèles de langage (LLM) ont montré des résultats prometteurs dans la démonstration de théorèmes formels en utilisant des assistants de preuve tels que Lean. Cependant, les méthodes existantes sont difficiles à reproduire ou à développer, en raison de code privé, de données et de besoins importants en calcul. Cela a créé des obstacles substantiels à la recherche sur les méthodes d'apprentissage automatique pour la démonstration de théorèmes. Cet article élimine ces obstacles en introduisant LeanDojo : un environnement de jeu open-source pour Lean comprenant des boîtes à outils, des données, des modèles et des benchmarks. LeanDojo extrait des données de Lean et permet d'interagir programmatiquement avec l'environnement de preuve. Il contient des annotations granulaires des prémisses dans les preuves, fournissant des données précieuses pour la sélection de prémisses : un goulot d'étranglement clé dans la démonstration de théorèmes. En utilisant ces données, nous développons ReProver (Retrieval-Augmented Prover) : le premier démonstrateur basé sur LLM qui est augmenté par un système de récupération pour sélectionner des prémisses dans une vaste bibliothèque mathématique. Il est peu coûteux et nécessite seulement une semaine d'entraînement sur un GPU. Notre système de récupération tire parti de la capacité d'analyse de programme de LeanDojo pour identifier les prémisses accessibles et des exemples négatifs difficiles, ce qui rend la récupération beaucoup plus efficace. De plus, nous construisons un nouveau benchmark composé de 96 962 théorèmes et preuves extraits de la bibliothèque mathématique de Lean. Il présente une division des données exigeante, nécessitant que le démonstrateur généralise à des théorèmes reposant sur des prémisses nouvelles qui ne sont jamais utilisées lors de l'entraînement. Nous utilisons ce benchmark pour l'entraînement et l'évaluation, et les résultats expérimentaux démontrent l'efficacité de ReProver par rapport aux baselines sans récupération et à GPT-4. Nous fournissons ainsi le premier ensemble de démonstrateurs de théorèmes basés sur LLM open-source sans aucun ensemble de données propriétaire, et le publions sous une licence MIT permissive pour faciliter la recherche future.

English

Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has created substantial barriers to research on machine learning methods for theorem proving. This paper removes these barriers by introducing LeanDojo: an open-source Lean playground consisting of toolkits, data, models, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs, providing valuable data for premise selection: a key bottleneck in theorem proving. Using this data, we develop ReProver (Retrieval-Augmented Prover): the first LLM-based prover that is augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo's program analysis capability to identify accessible premises and hard negative examples, which makes retrieval much more effective. Furthermore, we construct a new benchmark consisting of 96,962 theorems and proofs extracted from Lean's math library. It features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research.