要約
リーンのようなコンピュータで検証可能な形式言語を用いて数学の定理を証明することは、数学的推論に大きな影響を与える。形式的定理証明の1つのアプローチは、自然言語（NL）証明に基づく大規模言語モデル（LLM）を使用して完全な証明を生成することである。同様の手法はコード生成においても有望な結果を示している。しかし、ほとんどの最新のLLMは、整列されたNLと形式言語（FL）の定理証明データが乏しいため、最適とは言えない性能を示している。この乏しさは、LLMを訓練するための方法論や、LLMの能力を形式的証明の構成に十分に活用するためのテクニックが乏しいという結果につながっている。この課題に対処するため、本稿では、汎用LLMをLean4エキスパートに訓練するエンドツーエンドのフレームワークである**TheoremLlama**を提案する。このフレームワークには、NL-FLに整合したデータセット生成手法、LLM形式定理証明器の訓練アプローチ、LLM Lean4証明書作成技術が含まれる。データセット生成法を用いて、NL-FL整列とブートストラップされたデータセットである*Open Bootstrapped Theorems* (OBT)を提供する。このフレームワークの重要な革新点は、NL-FLブートストラップ法であり、LLMのNL推論能力を形式推論のために活用し、NL証明をトレーニングデータセットのLean4コードに統合する。TheoremLlama**フレームワークはMiniF2F-ValidデータセットとTestデータセットでそれぞれ36.48%と33.61%の累積精度を達成し、GPT-4のベースラインの22.95%と25.41%を上回った。我々はまた、モデルのチェックポイントと生成されたデータセットをオープンソース化しており、近々全てのコードを公開する予定です。
要約(オリジナル)
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.
arxiv情報
| 著者 | Ruida Wang,Jipeng Zhang,Yizhen Jia,Rui Pan,Shizhe Diao,Renjie Pi,Tong Zhang |
| 発行日 | 2024-07-03 15:36:18+00:00 |
| arxivサイト | arxiv_id(pdf) |