Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation

Authors: Shaonan Wu, Shuai Lu, Yeyun Gong, Nan Duan, Ping Wei
Primary area: applications to computer vision, audio, language, and other modalities
Keywords: Synthetic Data, Neural Theorem Proving, Formal Reasoning, Lean Theorem Prover

Abstract:
Formal proofs are challenging to write even for experienced experts.  Recent progress in Neural Theorem Proving (NTP) shows promise in expediting this process. However, the formal corpora available on the Internet are limited compared to the general text, posing a significant data scarcity challenge for NTP.   To address this issue, this work proposes Alchemy, a general framework for data synthesis that constructs formal theorems through symbolic mutation. Specifically, for each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. Subsequently, we mutate the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M. Furthermore, we perform continual pretraining and supervised finetuning on this augmented corpus for large language models. Experimental results demonstrate the effectiveness of our approach, achieving a 4.70% absolute performance improvement on Leandojo benchmark. Additionally, our approach achieves a 2.47% absolute performance gain on the out-of-distribution miniF2F benchmark based on the synthetic data. To provide further insights, we conduct a comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.

Decision: accept (poster)
Reviewer scores: 6, 6, 6, 8

Reviews and discussion:
<thread>
creation date:
1730524355369

thread_type:
official_review

<thread_object>
creator: reviewer_nsyk

<content>
summary:
The paper proposes a new method to synthesize theorem training data for improving LLM's ability in theorem-proving. Given an existing theorem, the proposed method finds theorems that can imply its assumptions and assertions. Then, it replaces the corresponding assumptions/assertions and invokes these theorems to obtain the expanded new theorem. Experiments show the proposed method can generate 5M data and improve 7b models by a 2-4% pass rate.

strengths:
- The paper is well-written and easy to understand. It has a clear motivation and proposes a novel method to generate a lot of new theorem data.

- The experimental results validate the effectiveness of the generated data. It can improve current LLMs by >4% pass rate on the novel_premises split.

weaknesses:
The method seems unable to generate diverse theorem data. It mainly expands existing theorem by combining other theorems. The diversity problem may result in a lower improvement on the harder benchmark miniF2F. I guess the generated theorem can be very different from the original theorem if it has a deep variant proof tree. Authors may show the depth statistics of the generated theorem or other statistics to verify the diversity of the generated theorem.

questions:
Why many generated theorems not pass the Lean prover? Since the generation process is based on symbolic replacement, I suppose most of the theorem should pass the prover.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730573462323

thread_type:
official_review

<thread_object>
creator: reviewer_bkad

<content>
summary:
This paper introduces Alchemy, a framework to generate synthetic theorem data by applying symbolic mutations to existing theorems within Lean’s Mathlib. By mutating known theorems through symbolic operations, Alchemy expands the theorem corpus by an order of magnitude (from 110k to over 6M theorems). The authors evaluate Alchemy’s effectiveness on theorem-proving tasks, reporting a 5% improvement on the Leandojo benchmark and a 2.5% gain on the out-of-distribution miniF2F benchmark (to 36.48% test accuracy).

strengths:
1. The approach is technically robust, with well-documented use of symbolic mutations (specifically rw and apply tactics) to ensure the correctness of new theorems by construction. The improvements seen on Leandojo and miniF2F benchmarks support the framework’s validity.
2. Alchemy significantly increases the number of available theorems in Mathlib, scaling up to 6 million theorems through systematic symbolic mutations. This large corpus helps address the issue of limited formal proof data for theorem-proving models. By providing a synthetic theorem corpus directly in the symbolic space, Alchemy addresses a key limitation in neural theorem proving, especially in formal languages like Lean where data is scarce and difficult to formalize manually.
3. The limitations of the approach, such as data diversity and computational cost, are clearly addressed.

weaknesses:
1. Marginal Gains in Benchmark Performance: Despite generating millions of new theorems, the gains in miniF2F accuracy are limited to 2.5%, notably lower than the >60% accuracy achieved by SOTA models such as DeepSeekProver and InternLM Prover. This modest improvement raises questions regarding the utility and quality of the synthetic theorems for real-world theorem-proving tasks.
2. Computational Cost: The process of generating and verifying theorems is highly resource-intensive. The implementation reports substantial computational overhead, with 14 days on 4,096 CPU cores for rw mutations and 7 days on 2,048 cores for apply mutations, potentially limiting the accessibility and scalability of Alchemy in practice.
3. Lack of Quality Metrics for Synthetic Theorems: Although Alchemy generates a large corpus, there is limited analysis of the quality or mathematical significance of the produced theorems. Without metrics or evaluation methods beyond correctness by construction, it is challenging to assess whether the synthetic theorems provide meaningful, diverse training examples.
4. Limited Innovation Beyond Mutation: The paper relies heavily on mutating existing theorems via basic rw and apply tactics, which may restrict the variety of new insights or concepts that the synthetic data introduces. Advanced tactics (e.g., simp, linarith) and some premise selection approaches are critical in solving more challenging problems, especially in competition-level mathematics. Without these, the generated dataset might lack the depth needed to fully improve theorem-proving performance on complex out-of-distribution tasks.

questions:
1. Given the modest improvement in miniF2F accuracy, are there metrics or quality checks available to assess the mathematical value or diversity of the generated theorems beyond correctness?
2. Which specific theorems in miniF2F were newly proved by the models fine-tuned with Alchemy data? This would provide insights into the areas where synthetic training data are particularly beneficial.
3. Given the computational demands, are there potential optimizations in the synthesis process to reduce the time and resources required for theorem mutation?	
4. How do you avoid the data contamination problem in the evaluation/generation phase?

[1] Xin, Huajian, et al. "DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search." arXiv preprint arXiv:2408.08152 (2024). 
[2] Ying, Huaiyuan, et al. "Lean Workbook: A large-scale Lean problem set formalized from natural language math problems." arXiv preprint arXiv:2406.03847 (2024).
</content>
</thread_object>

</thread>
<thread>
creation date:
1730678737724

thread_type:
official_review

<thread_object>
creator: reviewer_fuws

<content>
summary:
The paper concerns data augmentation for neural theorem proving. The authors propose a method for augmenting theorem statements and the set of (state, tactic) examples given a collection of Lean statements and proofs. Their method augments theorem statements by (1) rewriting expressions in hypotheses or the statement's goal using a rewrite tactic with a suitable premise, (2) replacing a hypothesis with a different set obtained with an apply tactic with a suitable premise. It augments proofs by undoing the rewrite and/or apply and introducing a have statement, which sometimes introduces new (state, tactic) examples.

The authors apply their augmentations to Mathlib, and finetune models with (1) continued pretraining on mathlib plus the augmented statements and proofs, followed by (2) finetuning on (state, tactic) examples from Mathlib plus those from their augmentations. 

The models that have undergone continued pretraining and (state, tactic) finetuning outperform the same models when they have only undergone (state, tactic) finetuning on Mathlib alone. For example, there is a 2.69% improvement on the random LeanDojo test split, and a 4.22% improvement on the novel_premises split with DeepSeek Coder.

strengths:
Originality
- The idea of synthesizing new theorem statements through rewrites and applies is new (as far as I'm aware). 

Quality
- Aside from the concerns discussed below, the experiments were carried out well for several variants while adhering to standard benchmarks and search algorithm protocols.
- Implementing modifications to data extraction in Lean is likely nontrivial.

Clarity
- The data synthesis methodology was explained clearly.

Significance
- Lack of data is widely regarded as a core issue in neural theorem proving. Augmenting data using symbolic techniques is a potential approach to alleviating this issue, and the authors demonstrate a first step in this direction.
- The general direction of augmenting data using symbolic techniques is interesting and under-explored.

weaknesses:
As mentioned in the strengths above, the general direction of augmenting data using symbolic techniques is interesting and under-explored. I have two primary concerns: (1) the experimental evaluation of the proposed techniques; (2) the data augmentation techniques explored in the current paper. 

### Experimental evaluation
1. **Baselines**: the baseline method is a LM finetuned on (state, tactic) pairs from Mathlib. However, the proposed method does (i) continued pretraining and (ii) (state, tactic) finetuning. As a result it is difficult to interpret the main results, since there are two finetuning methodologies used. How does the baseline method perform after continued pretraining on Mathlib (without augmentation), followed by (state, tactic) finetuning on Mathlib (without augmentation)?

2. **Possible train-test overlap**: The LeanDojo benchmark consists of theorems from Mathlib. Therefore, there is potential train-test overlap in at least two places. 
    - (i) First, the continued pretraining dataset, if it includes theorems from the LeanDojo test set (or premises used in the novel_premises split). How was train-test overlap prevented for continued pretraining? I wasn't able to find details on exactly what was done for continued pretraining, so it would be great to clarify this.
    - (ii) Second, the rewrites and applies may use premises that are "novel" in the novel_premises split. How do you ensure that these are not used in the data augmentation process?

As a result of (i) and (ii), it is difficult to interpret the improvement on the novel premises split. Namely, (i) and (ii) may have exposed the model to the premises required in this split, which would negate the purpose of the split. Moreover, (i) may lead to improvements on the random split as well.

3. **Finetuning hyperparameters**. This is perhaps less important than (1) and (2), but the augmented dataset leads to more gradient updates compared to finetuning on the non-augmented dataset, since finetuning is performed for a fixed number of epochs. Do the results change if the baseline is finetuned for the same number of steps as the model finetuned on the augmented dataset?

### Data augmentation techniques
1. The computational cost is very high; it takes 14 days for the rw operation on 512 CPU nodes. To make the authors' method more practical, it would have been nice to see some innovation that makes the extraction faster (either at the algorithmic level or the implementation level).

2. Currently the methods only modify the statement goal using 1 step of rewriting. The overall scientific contribution could be made stronger with more exploration of techniques (e.g., at least > 1 step of rewriting). Could you clarify why only the 1-step rewriting and apply were explored? I realize that it is hard to say how many techniques are needed (and it's always nicer to have more), so this is less of a concern for me than the experimental evaluation of the two techniques described above.

3. From what I understand, proofs are only modified by introducing a have statement that reverses the 1-step augmentation, and then the proof is the same as the original. Again it would be nice to see additional innovation in this direction.

4. It was unclear why each technique helped on unseen_premises split; could you give an intuition or an analysis of why it might help?

questions:
Please see the questions above discussed in the Weaknesses. In particular, if the authors can provide a strong response to the questions regarding the experimental setup I would be willing to raise my score.
</content>
</thread_object>

</thread>
<thread>
creation date:
1730707186938

thread_type:
official_review

<thread_object>
creator: reviewer_edxu

<content>
summary:
This paper introduces a symbolic method called Alchemy to augment formal theorem proving data. Specifically, it mutates "the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent", which increases the number of theorem in mathlib4 from 110k to 6M. After continual pre-training and supervised fine-tuning with the generated data, it improves downstream performances (pass rate) on standard theorem proving benchmarks such as mathlib-test and miniF2F from 2.5% to 5%.

strengths:
Some originality: This is a good and new attempt for augmenting a human-written library (although similar ideas have been applied for "pure symbolic and from scratch" methods for generating theorems such as INT, HTPS-Equations and AlphaGeometry)
Good quality: the paper is well written and all settings are of high relevance
Good clarity: the paper is presented in a clear manner. The experimental setting and results are presented in a standard way and easy to follow
Fair significance: The improvement on pass rate on mathlib-test and miniF2F is consistent, with almost all differences being positive compared with the baseline.

weaknesses:
1. Poor improvement: although the improvement on pass rate is consistent, it's very limited: ranging from 0.62% to 4.7% on mathlib and only 2.47% on miniF2F (34.01% to 36.48%). This is pretty marginal in terms of improvement.
2. Narrow application possibility: the approach highly replies on a library of existing equivalence (or implying) theorems and their usage in proofs of other theorems.

questions:
How do you explain a Conversion Ratio of only 37% while the idea seems to work with a theoretical guarantee (i.e. 100%)?
Do you think a framework like Alchemy is the correct way to significantly improve NTP to face challenging problems such as IMO problems?
</content>
</thread_object>

</thread>
<thread>
creation date:
1732072834784

thread_type:
official_comment

<thread_object>
creator: authors

<content>
title:
General Response to the Shared Concerns or Questions

comment:
We sincerely thank all reviewers for their valuable feedback and constructive comments in the reviewing process. We notice that some reviewers have similar concerns or questions. 

1.  Poor improvement (**Reviewer EDxu, Reviewer BkaD**)
2.  Synthesis Cost (**Reviewer FuWS, Reviewer BkaD**)
3.  Non-100% Conversion Ratio (**Reviewer EDxu, Reviewer NSyk**)
4.  Data-Contamination (**Reviewer FuWS,** **Reviewer BkaD**)
5.  Data-Diversity (**Reviewer BkaD, Reviewer NSyk**)

We have carefully considered them and addressed them comprehensively below.

### 1. Poor Improvement

**Reviewer EDxu** and **Reviewer BkaD** point out that the improvements achieved by our method may be limited. **Reviewer BkaD** also compares the improvement achieved by our method versus the improvement of Deepseek Prover or InternLM Prover. 

> **Reviewer EDxu:**
> 
> 
> Poor improvement: although the improvement on pass rate is consistent, it's very limited, ranging from 0.62% to 4.7% on mathlib and only 2.47% on miniF2F (34.01% to 36.48%). This is pretty marginal in terms of improvement.
> 

> **Reviewer BkaD:**
> 
> 
> Marginal Gains in Benchmark Performance: Despite generating millions of new theorems, the gains in miniF2F accuracy are limited to 2.5%, notably lower than the >60% accuracy achieved by SOTA models such as DeepSeekProver and InternLM Prover. This modest improvement raises questions regarding the utility and quality of the synthetic theorems for real-world theorem-proving tasks.
> 

We will explain the reason behind it and discuss the prevalent synthesis methods in Deepseek Prover or InternlmStepProver.

The limited improvements of Alchemy achieved in competition-level benchmarks might be attributed to the discrepancy between our synthesized data and competition-level theorems.   At the theorem level, our synthesized data is derived from fundamental theorems in Mathlib, which differ substantially from competition-level theorems. At the state-tactic level, as detailed in **Appendix E.2,** synthesized additional tactics of our algorithm are centered on basic tactics (rw and apply), rather than the advanced tactics (linarith, ring, omega, etc.) that are important for proving miniF2F-style theorems. We hypothesize that electing domain-similar seed theorems and focusing on synthesizing advanced tactics could enhance performance on miniF2F-like benchmarks.

The significant performance gains achieved by DeepseekProver [1] and InternLM Stepprover [2] primarily stem from expert iteration on a large set of competition-level statements that align with the downstream task (miniF2F). While these works have provided valuable insights and advanced the research of NTP, these methods face some limitations: 

- They require extensive manual effort for collecting natural language problems and substantial computational resources (GPU-intensive) for formalization and proof generation.
- The distribution of formalized theorems is inherently constrained by the pool of human-collected natural language questions, creating limited new knowledge.

In contrast, constructing theorems in symbolic space offers a more direct pathway for generating new knowledge, eliminating the need for intermediate translation. This approach is also more scalable, leveraging cost-effective CPU resources. Our work explores this challenging yet unexplored direction, demonstrating its potential through improvements in both in-distribution and out-of-distribution benchmarks.

---

[1] Xin, Huajian, et al. "DeepSeek-Prover-V1. 5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search." *arXiv preprint arXiv:2408.08152* (2024).
[2] Wu, Zijian, et al. "InternLM2. 5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN Problems." *arXiv preprint arXiv:2410.15700* (2024).
</content>
</thread_object>

</thread>


Metareview:
metareview:
This paper concerns data augmentation for theorem proving in Lean through symbolic rewriting of hypotheseses and proofs. Evaluations performed on Mathlib datasets show that, with data augumentation, further pretraining and finetuning improves the performance by 2.69% on the random LeanDojo test split and 4.22% on the novel_premises split. Augmenting training data for theorem proving through rewrites and applies is a novel contribution. Given the augmentation only performs one step rewriting, leaving the augumented theorems and proofs nearly identical to the original ones, there is a concern that whether the fine-tuned model will generalize. Other concerns are possible train-test overlap and data contamination. New results shared during the rebuttal partially addresses some of these concerns (e.g., train-test overlap). Overall, this paper makes valuable contributions with relatively marginal improvement by data augmentation for neural theorem proving.