Lean4trace: Data augmentation for neural theorem proving in Lean

Venue: ICML_cc_2024_Workshop_AI4MATH
Published: 2024-06-01 12:19:27

Abstract: Integrating large language models as proof assistants with theorem provers has shown great promise. However, one of the major challenges in this field is the scarcity of training data. To address this, we release a new open-source tool, *Lean4trace*, for training data extraction from Lean 4 sources. Unlike previous approaches, *Lean4trace* is deeply integrated into the Lean elaborator, allowing us to modify proofs on-the-fly. Leveraging this feature, we propose two methods of data augmentation in Lean: (1) decomposing composite proof steps into multiple simpler steps;  (2) testing existing proof automation tactics at each proof state and collecting the successful ones. Models trained on this augmented data are capable of proving 58.0% of theorems from a hold-out subset of Mathlib and 35.6% of the test subset of the MiniF2F benchmark.

Main paper: 
  
 Appendix:  


Decision: This paper answers a question that is often asked in Lean theorem proving: how do models improve when having data when tactics like simp are split in detailed steps. As the reviewers suggest there are several good points and some limitations, in particular there are important details missing (extracting proof information, canonical datasets, etc.). Surprisingly, the automatic method can sometimes have negative effects. While it would be important to understand why, this is not an obstacle for publication in my opinion, given that the idea explored in this paper is natural and was worth to be explored anyway. I recommend accepting, taking a leap of faith, that the authors will at least elaborate on the missing details pointed by the reviewers in the camera-ready version.

Reviews: review: paper_summary: paper_summary: This paper introduces **Lean4trace**, a novel tool designed for data extraction and augmentation specifically for training neural theorem provers within the Lean theorem proving environment. **Lean4trace** is deeply integrated with the Lean elaborator, enhancing its functionality by enabling on-the-fly interaction with existing proofs and extracting more comprehensive proof states than prior tools.
strength_weakness: strength_weakness: 1.This method is not novel in my opinion. It just applies some tactics' sub-level proofs to the theorem prover to get more detailed proof state and tactic.  
2.This is more like a method[1][2] of breaking down the proof goal and then proving the sub-goals, but this idea is not novel.

**Reference**  
[1] Lample, Guillaume, et al. "Hypertree proof search for neural theorem proving." Advances in neural information processing systems 35 (2022): 26337-26349.  
[2] Zhao X, Li W, Kong L. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving[J]. arXiv preprint arXiv:2305.16366, 2023.
questions: questions: 1. I am skeptical about replacing automatic tactics in any row of tactics, because there are some high-level tactics, such as tidy, which can directly replace several consecutive rows of tactics.  
2. When searching for the sub-level tactic sequence corresponding to Simp, is the language model used for Breadth-First Search?
paper_summary: paper_summary: The paper introduces Lean4trace, an open-source tool for extracting training data from Lean 4 sources, addressing the challenge of limited training data in integrating large language models with theorem provers. By deeply integrating with the Lean elaborator, Lean4trace enables real-time proof modifications and traces proof states, steps, and premises, along with additional meta information. The authors propose two data augmentation methods: decomposing complex proof steps of frequent tactics like simp and rw into simpler steps, and testing automatic tactics at each proof state to collect successful applications.These methods significantly enhance training data, resulting in models that successfully prove 58.0% of theorems from a hold-out Mathlib subset and 35.6% of the MiniF2F benchmark test subset, demonstrating the effectiveness of the approach.
strength_weakness: strength_weakness: **Lack of Detail and Examples**: The section on extracting proof information is inadequately detailed, and the absence of concrete examples makes it challenging to grasp the practical implications and effectiveness of the proposed method.

**Insufficient Analysis of Proof Behavior**: There is a notable lack of in-depth analysis regarding the model's proof behavior post-data augmentation. The paper does not sufficiently explore how the augmentations impact the model's performance, leaving readers with an incomplete understanding of their efficacy.

**Engineering Tricks**: From the current description of the article, the expansion of the premise used by the tactic and the replacement of the advanced automated tactic are more of an engineering trick, and at most provide a rewrite and trivial replacement of the existing proof to make it more understandable, and it is difficult to provide different proofs with essential differences. 

**Limited Improvement in Proof Ability**: The augmentations do not significantly enhance the model's proof capabilities. This is evident from the pass rate control experiments, which show no substantial improvement. In fact, performance on the MiniF2F benchmark declined, suggesting that the model may have become more attuned to specific scenarios in Mathlib without achieving broader proof proficiency.
questions: questions: - Could you provide more detailed descriptions of the process for extracting proof information using the Lean elaborator? Consider adding details with step-by-step examples demonstrating the extraction of proof information and subsequent modifications.
- Could you offer a more detailed analysis of how the augmentations impact the model's performance on different types of proofs? For instance, how do they affect the pattern of tactic application and proof structure?
- What are the possible reasons for the decline in performance on the MiniF2F benchmark? How do you plan to address the issue of the model becoming more attuned to specific scenarios other than Mathlib?
paper_summary: paper_summary: This paper proposes a novel data augmentation method for tracing the Lean Mathlib library. The method consists of two main components:
- Decomposing composite proof steps into multiple simpler steps, including the decomposition of rw and simp tactics.
- Using automatic tactics to prove theorems and obtain new proof state/tactic pairs.

The experimental results show that the newly traced data provides a significant improvement on the Lean Mathlib dataset. Additionally, the new tracing method achieves reduced memory consumption.
strength_weakness: strength_weakness: - The performance gain of the newly proposed augmentation methods is marginal. In the MathLib dataset, the automatic method even has negative effects.
- The majority of the performance gain is achieved with the canonical dataset, which is not discussed in detail in the paper. It would be helpful to provide a more detailed explanation of this canonical dataset.
questions: questions: Please justify the question I raised in the `Reasons To Reject`.
paper_summary: paper_summary: This paper proposes a method of data augmentation for theorem proving data in the formal language Lean 4. Two methods are used: 1. Tactic decomposition: decompose tactics such as simp and rw to get intermediate tactic states and proofs steps; 2. Automatic tactics: apply automatic tactics such as aesop at each proof step. The authors also improve LeanDojo's tracing method to curate a dataset called canonical. The ByT5 model trained using these data achieves +9.4% improvement on pass@1 on Mathlib and +9.1% on miniF2F.
strength_weakness: strength_weakness: 1. The part on canonical is not well explained, while the performance improvements are mainly due to canonical dataset;
2. The contribution on "data augmentation" as claimed in the title of paper seems to harm the performance on many scenarios.
3. The novelty is limited as the proposed techniques focus on rather microscopic aspects and could be specific to Lean 4 language and it's hard to generalize.
questions: questions: 1. Is the data tracing technique used in canonical based on LeanDojo code? The part on canonical part is not well explained in the paper. Please improve the explanations.
2. In line 193, you mentioned "Note that our approach requires considerably less RAM". Why is this? And can you give a concrete quantity for the RAM consumption of both methods?
3. Are you going to open-source your code and dataset?