LeanDojo: Demostración de Teoremas con Modelos de Lenguaje Aumentados por Recuperación

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

June 27, 2023

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

cs.AI

Resumen

Los modelos de lenguaje de gran escala (LLMs, por sus siglas en inglés) han mostrado potencial para demostrar teoremas formales utilizando asistentes de pruebas como Lean. Sin embargo, los métodos existentes son difíciles de reproducir o ampliar debido a código privado, datos y grandes requisitos de cómputo. Esto ha creado barreras significativas para la investigación sobre métodos de aprendizaje automático en la demostración de teoremas. Este artículo elimina estas barreras al presentar LeanDojo: un entorno de desarrollo abierto para Lean que incluye herramientas, datos, modelos y puntos de referencia. LeanDojo extrae datos de Lean y permite la interacción programática con el entorno de pruebas. Contiene anotaciones detalladas de las premisas en las demostraciones, proporcionando datos valiosos para la selección de premisas: un cuello de botella clave en la demostración de teoremas. Utilizando estos datos, desarrollamos ReProver (Demostrador Aumentado con Recuperación): el primer demostrador basado en LLM que se complementa con recuperación para seleccionar premisas de una vasta biblioteca matemática. Es económico y requiere solo una semana de entrenamiento en una GPU. Nuestro recuperador aprovecha la capacidad de análisis de programas de LeanDojo para identificar premisas accesibles y ejemplos negativos difíciles, lo que hace que la recuperación sea mucho más efectiva. Además, construimos un nuevo punto de referencia que consta de 96,962 teoremas y demostraciones extraídos de la biblioteca matemática de Lean. Presenta una división de datos desafiante que requiere que el demostrador generalice teoremas que dependen de premisas novedosas que nunca se usan en el entrenamiento. Utilizamos este punto de referencia para entrenamiento y evaluación, y los resultados experimentales demuestran la efectividad de ReProver frente a líneas base sin recuperación y GPT-4. Así, proporcionamos el primer conjunto de demostradores de teoremas basados en LLM de código abierto sin ningún conjunto de datos propietario y lo publicamos bajo una licencia permisiva MIT para facilitar futuras investigaciones.

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.