LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover

要約

最近、大規模な言語モデルは、形式的な数学的推論を支援する上で有望な結果を示しています。
ただし、形式定理証明データが不足しているため、そのパフォーマンスは制限されており、生の形式言語コーパスから抽出するには追加の労力が必要です。
その一方で、人間が書いた形式言語コーパスのかなりの量が十分に活用されていないままです。
この問題に対処するために、GitHub 上のほぼすべての Lean 4 リポジトリから抽出された大規模な正式データで構成されるデータセットである LEAN-GitHub を提案します。
このデータセットで InternLM-math-plus を微調整した後、私たちのモデルは、Lean 4 miniF2F テストで 1 回のパスで 48.8%、64 回のパスで 54.5% の精度を達成し、最先端の手法の 52% を上回りました。
また、数学のさまざまな分野/レベルを対象とした他の 2 つのリーン 4 ベンチマーク (ProofNet と Putnam) でも最先端を達成しています。
これらの結果は、私たちが提案したデータセットが幅広い数学トピックの形式的推論に有益であることを示しています。
私たちはモデルを https://GitHub でオープンソース化しています。
com/InternLM/InternLM-Math およびデータは https://huggingface.co/datasets/InternLM/Lean-GitHub にあります。

要約(オリジナル)

Recently, large language models have presented promising results in aiding formal mathematical reasoning. However, their performance is restricted due to the scarcity of formal theorem-proving data, which requires additional effort to be extracted from raw formal language corpora. Meanwhile, a significant amount of human-written formal language corpora remains underutilized. To address this issue, we propose LEAN-GitHub, a dataset consisting of large-scale formal data extracted from almost all Lean 4 repositories on GitHub. After fine-tuning InternLM-math-plus on this dataset, our model achieved accuracies of 48.8% with a single pass and 54.5% with 64 passes on the Lean 4 miniF2F test, surpassing state-of-the-art method at 52%. And it also achieves state-of-the-art on two other Lean 4 benchmarks (ProofNet and Putnam) targeting different fields/levels of math. These results demonstrate that our proposed dataset is beneficial for formal reasoning on a wide range of math topics. We open-source our model at https://GitHub. com/InternLM/InternLM-Math and our data at https://huggingface.co/ datasets/InternLM/Lean-GitHub

arxiv情報

提供元, 利用サービス

arxiv.jp, Google