LeanDojo: Доказательство теорем с использованием языковых моделей, дополненных поиском

Аннотация

Крупные языковые модели (LLM) продемонстрировали потенциал в доказательстве формальных теорем с использованием систем автоматизированного доказательства, таких как Lean. Однако существующие методы сложно воспроизвести или развить из-за закрытого кода, данных и высоких требований к вычислительным ресурсам. Это создало значительные барьеры для исследований в области машинного обучения для автоматического доказательства теорем. Данная работа устраняет эти барьеры, представляя LeanDojo: открытую платформу для работы с Lean, включающую набор инструментов, данные, модели и бенчмарки. LeanDojo извлекает данные из Lean и позволяет программно взаимодействовать со средой доказательств. Она содержит детализированные аннотации предпосылок в доказательствах, предоставляя ценные данные для задачи выбора предпосылок — ключевого узкого места в доказательстве теорем. Используя эти данные, мы разработали ReProver (Retrieval-Augmented Prover): первую LLM-модель для доказательства теорем, дополненную механизмом поиска для выбора предпосылок из обширной математической библиотеки. Она экономична и требует всего одной недели обучения на одном GPU. Наш механизм поиска использует возможности программного анализа LeanDojo для идентификации доступных предпосылок и сложных отрицательных примеров, что значительно повышает эффективность поиска. Кроме того, мы создали новый бенчмарк, состоящий из 96 962 теорем и доказательств, извлеченных из математической библиотеки Lean. Он включает сложные разделы данных, требующие от модели обобщения на теоремы, основанные на новых предпосылках, которые никогда не использовались при обучении. Мы используем этот бенчмарк для обучения и оценки, и экспериментальные результаты демонстрируют превосходство ReProver над базовыми моделями без механизма поиска и GPT-4. Таким образом, мы предоставляем первый набор открытых LLM-моделей для доказательства теорем, не использующих проприетарные данные, и выпускаем их под разрешительной лицензией MIT для содействия дальнейшим исследованиям.

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.

LeanDojo: Доказательство теорем с использованием языковых моделей, дополненных поиском

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

Аннотация

Support