TheoremLlama: 汎用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のようなコンピュータ検証可能な形式言語を用いて数学定理を証明することは、数学的推論に大きな影響を与えます。形式定理証明の一つのアプローチとして、自然言語（NL）証明に基づいて大規模言語モデル（LLMs）を使用して完全な証明を生成する方法があります。同様の手法は、コード生成において有望な結果を示しています。しかし、現代のほとんどのLLMsは、NLと形式言語（FL）の定理証明データの整合性が不足しているため、最適な性能を発揮していません。この不足は、LLMsを訓練する方法論や、形式証明を構成するためにそれらの能力を十分に活用する技術の欠如を引き起こしています。これらの課題に対処するため、本論文では、汎用LLMをLean4の専門家に訓練するためのエンドツーエンドのフレームワークである**TheoremLlama**を提案します。このフレームワークは、NL-FL整合データセット生成方法、LLM形式定理証明器の訓練アプローチ、およびLLM Lean4証明作成技術を含んでいます。データセット生成方法を使用して、NL-FL整合およびブートストラップされたデータセットである*Open Bootstrapped Theorems*（OBT）を提供します。このフレームワークの重要な革新点は、NL証明をLean4コードに統合して訓練データセットを作成するNL-FLブートストラップ方法であり、LLMsのNL推論能力を形式推論に活用します。**TheoremLlama**フレームワークは、MiniF2F-ValidおよびTestデータセットにおいて、それぞれ36.48%および33.61%の累積精度を達成し、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.