PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Zijian Wu, Jiayu Wang, Dahua Lin, Kai Chen

arXiv:2407.17227v1cs.AIcs.CL

TL;DR

Formal theorem proving with language models is limited by scarce formal data. LEAN-GitHub extracts data from open Lean repositories and is used to train InternLM2-StepProver, which reports strong results across Lean 4 benchmarks, including 54.5% on miniF2F-Test.

  • Problem

    Formal theorem-proving data is scarce, limiting language-model performance on formal mathematical reasoning.

    Source: §1 · p. 1

  • Method

    The paper extracts formal data from open Lean 4 repositories as LEAN-GitHub and trains InternLM2-StepProver using the dataset.

    Source: §1 · pp. 1–2, §4 · p. 5, §4.1.1 · p. 5

  • Results

    54.5% accuracy on miniF2F-Test versus DeepSeek-Prover’s 52.0%, with reported state-of-the-art results across Lean 4 benchmarks including ProofNet and Putnam.

    Source: §1 · p. 2, §4.2 · p. 6

  • Takeaways & Limitations

    Models trained with LEAN-GitHub show improved formal reasoning across mathematical fields and difficulty levels.

    Source: §5 · p. 9

Abstract

from arXiv · show

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

1 Introduction

Formal theorem proving is promising but constrained by scarce, difficult-to-extract training data. LEAN-GitHub uses open Lean repositories to expand that data and supports strong results across Lean 4 benchmarks.

1 Introduction

  • Formal proof creation demands substantial human effort, while formal-language data is scarce and raw code omits intermediate proof states.The authors also note that auto-formalized data has constrained quality and diversity and cannot substitute for human-crafted data.Source: §1 · p. 1
  • LEAN-GitHub contributes large-scale data extracted from open Lean 4 repositories, complementing Mathlib with 28,597 theorems and 218,866 tactics.The authors train InternLM2-StepProver using the dataset and report improved formal reasoning across varied benchmarks.Source: §1 · pp. 1–2
  • A scalable extraction pipeline recovers previously uncompiled Lean corpus data and addresses state duplication in tree proof search.The introduction presents these as contributions supporting formal reasoning on versatile mathematical topics.Source: §1 · p. 2
  • 48.8% single-pass and 54.5% with 64 passes on Lean 4 miniF2F-Test; the model also reports results on ProofNet and Putnam.The paper reports 18.1% Pass@1 on ProofNet and solving 5 of 640 Putnam problems.Source: §1 · p. 2

2 Related works

Prior automated theorem-proving work includes traditional search and learning-based methods. For Lean 4, existing extraction tools face overhead when applied across multiple projects.

Automatic Theorem Proving

  • Many learning-based provers train language models on proof-state and next-tactic pairs, then search over tactics, following GPT-f [21] and related systems.Other approaches generate whole proofs or incorporate informal proofs into formal ones.Source: §2 · p. 3
  • Earlier automated theorem provers also used KNN, GNN [32], and reinforcement learning [13] [28].Some methods generate tactics as abstract syntax trees rather than plain text.Source: §2 · p. 3

Data Extraction for Lean Corpus

  • The passage states that prior Lean 4 extraction tools incur significant extraction overhead because they are designed for a single project, making them unsuitable for massive extraction across multiple projects.Source: §2 · p. 3

3 The GitHub-Lean dataset

LEAN-GitHub compiles and extracts formal proof data from open Lean 4 repositories. Its scale and topic variety complement existing datasets focused on narrower topics or smaller collections.

3 The GitHub-Lean dataset

  • LEAN-GitHub draws on 147 repositories and contains 28,597 theorems, 218,866 tactics from 2,133 files, and 0.138B tokens.The authors describe it as one of the largest Lean 4 formal mathematics theorem-proving datasets.Source: §3 · p. 3

3.1 Dataset Construction

  • Of 237 candidate repositories, 90 deprecated-version repositories were discarded; only 61 of the remaining 147 compiled unchanged as valid Lean 4 projects.Keyword filtering estimated approximately 48,091 theorems, but a keyword did not guarantee a tactic proof.Source: §3.1 · p. 3
  • The compilation approach uses the underlying leanc compiler rather than relying on Lake to build whole projects.The authors describe handling isolated files and dependencies through a global import graph and a custom script with increased parallelism.Source: §3.1 · pp. 3–4
  • LeanDojo-based extraction was adapted for isolated files and parallelism, yielding valid tactic information from 2,133 files and 28K theorems.Across 8,639 source files, 6,352 files and 42K theorems were successfully extracted.Source: §3.1 · p. 4

3.2 Dataset Statistics

  • The theorem-name and repository distributions indicate topic variety, including logic, matroids, cutting-edge fields, data structures, and Olympiad problems.Logic, FirstOrder, Matroid, and Arith(mezation) are among the most prominent theorem-name keywords.Source: §3.2 · p. 4
  • Compared with existing datasets, LEAN-GitHub spans diverse fields, levels, and styles, while synthetic datasets have narrower topics and MiniF2F-curriculum has only 327 examples.LeanDojo-Mathlib mainly describes specific mathematical theories rather than problem-solving.Source: §3.2 · pp. 4–5, Table 1 · p. 4

4 Experiments

Experiments evaluate InternLM2-StepProver across Lean 4 benchmarks and report leading performance on miniF2F, ProofNet, and Putnam. They also examine training data, inference budgets, and proof-search efficiency.

4.1.1 Model and Training

  • InternLM2-StepProver builds on InternLM-math-plus-7B and uses a proofstep objective to predict a Lean tactic from the goal and theorem declaration.Training combines LEAN-GitHub, Mathlib, and synthetic theorem data.Source: §4 · p. 5, §4.1.1 · p. 5

4.1.2 Evaluation settings

  • Evaluation uses best-first search, generating 32 tactic candidates per state with at most 100 expansions per iteration.Source: §4.1.2 · p. 5
  • More than 50% of intermediate states were duplicates; Lean’s runtime metadata and hypothesis renaming by storage order let search identify equivalent states.The approach targets states with the same hypotheses and goals despite differing names.Source: §4.1.2 · pp. 5–6, Figure 6 · p. 6

4.2 Main Results

  • 18.1% Pass@1 on ProofNet exceeds ReProver’s 13.8%; the model also finds 24 proofs without existing Lean proofs.Source: §4.2 · p. 6, Table 3 · p. 7
  • On Lean 4 PutnamBench, InternLM2-StepProver solves 5 problems in one pass, compared with one each for GPT-4 and COPRA and none for ReProver.The paper also reports a solution to Putnam 1988 B2, not previously reported solved by an ITP.Source: §4.2 · pp. 6–7, Table 3 · p. 7
  • 63.9% on miniF2F-Valid and 54.5% on miniF2F-Test surpass DeepSeek-Prover’s 60.2% and 52.0%, respectively.Source: §4.2 · p. 6, Table 2 · p. 7

4.3 Ablation Studies

  • Models trained with GitHub-extracted data significantly outperform models trained only with Mathlib and/or synthetic data.Source: §4.3 · pp. 7–8, Table 4 · p. 8, Table 5 · p. 8
  • With 32 inferences at each of temperatures 0.7 and 1.0, pass rates reach 54.5% on miniF2F-test and 63.9% on miniF2F-valid, above no-LEAN-GitHub baselines.The baselines are 53.2% and 62.3%, respectively; figures also compare pass@64 results across data sources.Source: §4.3 · p. 8, Figure 7 · p. 8, Figure 8 · p. 8

5 Conclusion

The paper introduces LEAN-GitHub, a large-scale dataset extracted from open Lean 4 repositories, and trains InternLM2-StepProver with it. The authors report performance improvements across fields and difficulty levels in Lean 4 formal reasoning.

5 Conclusion

  • LEAN-GitHub contains 28,597 theorems and 218,866 tactics extracted from open Lean 4 repositories.The paper presents the dataset as a resource for exploiting underused information in raw corpora.Source: §5 · p. 9
  • InternLM2-StepProver trained with LEAN-GitHub achieves state-of-the-art performance on Lean 4 formal reasoning.The paper also evaluates other models trained with the dataset.Source: §5 · p. 9
  • Models trained on LEAN-GitHub show performance improvements across formal reasoning tasks spanning different fields and difficulty levels.The authors conclude that a well-extracted, diverse dataset can enhance model performance across a range of reasoning tasks.Source: §5 · p. 9

A Case study

The case studies illustrate InternLM2-StepProver on problems spanning induction, algebra, modular reasoning, and undergraduate group theory. They highlight both proof tactics and reasoning over mathematical premises.

Case 1: Binomial Coefficients

  • The binomial-coefficient case uses simple induction to prove the recurrence for Nat.choose.The displayed theorem states Nat.choose n k = Nat.choose (n - 1) k + Nat.choose (n - 1) (k - 1).Source: A Case study · p. 12

Case 2: Putnam 1988 B2

  • In the Putnam 1988 B2 case, automated tactics close the remaining subgoal after the proof splits into two implications.The account identifies a hint, sq_nonneg, as key to the ring_nf and nlinarith tactics closing the other subgoal.Source: A Case study · p. 12

Case 3: IMO 1964 P1(2)

  • For IMO 1964 P1(2), the prover uses the three-residue cycle of 2^n mod 7 to guide a case analysis.The formalized problem omits the first part's lemma, increasing its difficulty relative to the composite original problem.Source: A Case study · pp. 12–13

Case 4: Pough 3.2.8

  • The Pough 3.2.8 case demonstrates solving an undergraduate group-theory problem using group and coprimality premises.The goal is to show that finite subgroups with relatively prime orders have trivial intersection.Source: A Case study · p. 13

Related papers

Loading 2407.17227v1…