LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

要約

大規模言語モデル (LLM) は、Lean などの証明アシスタントを使用した形式定理の証明に有望であることが示されています。
ただし、プライベート コード、データ、大規模なコンピューティング要件があるため、既存のメソッドを再現したり構築したりするのは困難です。
このことは、定理証明のための機械学習手法の研究に大きな障壁を生み出しています。
このペーパーでは、ツールキット、データ、モデル、ベンチマークで構成されるオープンソースのリーン プレイグラウンドである LeanDojo を紹介することで、これらの障壁を取り除きます。
LeanDojo は、Lean からデータを抽出し、プログラムによる証明環境との対話を可能にします。
これには証明における前提のきめ細かい注釈が含まれており、定理証明の主要なボトルネックである前提の選択に貴重なデータを提供します。
このデータを使用して、ReProver (検索拡張証明者) を開発します。これは、膨大な数学ライブラリから前提を選択するための検索で拡張された LLM ベースの証明者です。
安価で、GPU のトレーニングに必要なのは 1 週間だけです。
当社の検索機能は、LeanDojo のプログラム分析機能を活用して、アクセス可能な前提と明確な否定的な例を特定することで、検索をより効率的にします。
さらに、Lean の数学ライブラリから抽出された 98,734 の定理と証明で構成される新しいベンチマークを構築します。
これは、証明者がトレーニングでは決して使用されない新しい前提に依存して定理に一般化する必要がある、困難なデータ分割を特徴としています。
私たちはこのベンチマークをトレーニングと評価に使用しており、実験結果は非検索ベースラインや GPT-4 に対する ReProver の有効性を示しています。
したがって、私たちは独自のデータセットを使用せずにオープンソースの LLM ベースの定理証明器の最初のセットを提供し、さらなる研究を促進するために寛容な MIT ライセンスの下でリリースします。

要約(オリジナル)

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): an LLM-based prover 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 98,734 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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google