Теорема Лама: Преобразование общего назначения LLM в экспертов Lean4.

TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

July 3, 2024

Авторы: Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, Tong Zhang

cs.AI

Аннотация

Доказательство математических теорем с использованием компьютерно-проверяемых формальных языков, таких как Lean, значительно влияет на математическое мышление. Один из подходов к формальному доказательству теорем заключается в создании полных доказательств с использованием больших языковых моделей (LLM) на основе естественного языка (NL). Подобные методы показали многообещающие результаты в генерации кода. Однако большинство современных LLM проявляют неоптимальную производительность из-за недостатка выровненных данных для доказательства теорем на естественном языке (NL) и формальном языке (FL). Этот дефицит приводит к отсутствию методологий для обучения LLM и техник для полного использования их возможностей в составлении формальных доказательств. Для решения этих проблем, в данной статье предлагается **TheoremLlama**, комплексная система для обучения общего LLM стать экспертом Lean4. Эта система включает методы генерации набора данных, выровненных по NL и FL, подходы к обучению формального доказателя теорем на основе LLM и техники написания доказательств Lean4 с помощью LLM. С использованием метода генерации набора данных мы предоставляем *Open Bootstrapped Theorems* (OBT), набор данных, выровненный по NL и FL, а также проинициализированный. Ключевым новшеством в этой системе является метод инициализации NL-FL, где доказательства на естественном языке интегрируются в код Lean4 для обучения наборов данных, используя способности LLM к рассуждению на естественном языке для формального рассуждения. Система **TheoremLlama** достигает накопленной точности 36,48% и 33,61% соответственно на наборах данных MiniF2F-Valid и Test, превосходя базовый уровень GPT-4 в 22,95% и 25,41%. Мы также опубликовали наши контрольные точки модели и созданный набор данных с открытым исходным кодом и вскоре сделаем весь код общедоступным.

English

Proving mathematical theorems using computer-verifiable formal languages like Lean significantly impacts mathematical reasoning. One approach to formal theorem proving involves generating complete proofs using Large Language Models (LLMs) based on Natural Language (NL) proofs. Similar methods have shown promising results in code generation. However, most modern LLMs exhibit suboptimal performance due to the scarcity of aligned NL and Formal Language (FL) theorem-proving data. This scarcity results in a paucity of methodologies for training LLMs and techniques to fully utilize their capabilities in composing formal proofs. To address the challenges, this paper proposes **TheoremLlama**, an end-to-end framework to train a general-purpose LLM to become a Lean4 expert. This framework encompasses NL-FL aligned dataset generation methods, training approaches for the LLM formal theorem prover, and techniques for LLM Lean4 proof writing. Using the dataset generation method, we provide *Open Bootstrapped Theorems* (OBT), an NL-FL aligned and bootstrapped dataset. A key innovation in this framework is the NL-FL bootstrapping method, where NL proofs are integrated into Lean4 code for training datasets, leveraging the NL reasoning ability of LLMs for formal reasoning. The **TheoremLlama** framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets respectively, surpassing the GPT-4 baseline of 22.95% and 25.41%. We have also open-sourced our model checkpoints and generated dataset, and will soon make all the code publicly available.