Alchemy: Amplifying Theorem-Proving Capability Through Symbolic Mutation

We want to express our sincere gratitude for your time and effort in evaluating our work. We have carefully considered your concerns and questions and attempted to give our answers.

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.

We have discussed the data diversity issue and provided a metric to verify the diversity of our data in the general response. We concur with the idea of generating a broader range of theorems through multi-round mutation (deep proof tree construction), a process that may encounter numerous non-trivial challenges.

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.

We have addressed the reasons for the non-100% conversion ratio in the general response. If you have any questions, please let us know.

We want to express our sincere gratitude for your time and effort in evaluating our work. We have carefully understood your concerns and questions. Some of them are shared concerns between reviewers. So, we answer them in the general response respectively:

• Marginal Gains in Benchmark Performance: Poor Improvement Section of general response.
• Computational Cost and question-3: High-Synthesis Cost Section of general response
• Lack of Quality Metrics for Synthetic Theorems and question-1: Data Diversity Issue Section of general response
• question-4: Data Contamination Section of general response

We really hope our response could resolve your concerns and questions.

For the individual concerns:

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.

We have discussed this possible limitation in diversity in Appendix B of original paper. We also provide a metric to verify the diversity of synthesized theorems in the general response.

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.

We have discussed the importance of advanced tactics for competition-level theorem-proving in Section 4.3.4 and Appendix E.2.1. We also discuss the possibility to combine our methods with RAG in Appendix B to further enhance the effectiveness of our method.

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.

We analyze the subjects of newly proved theorems by the models after fine-tuning with Alchemy data. As in the Table below,

Algebra, number theory, and induction are represented by the abbreviations "alg," "nt," and "ind," respectively. Test theorems sourced from MATH and custom curation are distinguished by the labels "m" or "c."

Comparing the discrepancy of distribution of solved problems for different data-compositions, we assume that rw state-tactic pairs play an important role in proving algebra problems and apply data can help for proving challenging theorems (e.g., aime, amc or custom theorems in miniF2F).

We would like to express our sincere gratitude to you for your time and effort in evaluating our work.

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.

We have deliberated on the factors contributing to the relatively modest improvements and discussed potential refinements aimed at enhancing the performance of our method in the general response.

Narrow application possibility: the approach highly replies on a library of existing equivalence (or implying) theorems and their usage in proofs of other theorems.

Our symbolic mutation technique indeed relies on a formal library that comprises equality or implication rules and constructs new proofs by leveraging these theorems in conjunction with original proofs. While this method necessitates certain prerequisites, we view its development as a valuable step towards exploring free-form theorem-synthesis methods within the symbolic space.

How do you explain a Conversion Ratio of only 37% while the idea seems to work with a theoretical guarantee (i.e. 100%)?

We have explained the reason behind the non-100% conversion ratio in the general response.

Do you think a framework like Alchemy is the correct way to significantly improve NTP to face challenging problems such as IMO problems?

As an exploration on data-synthesis in symbolic space, Alchemy has shown promising results on enhancing NTP. We assume Alchemy-like methods may indeed offer valuable assistance in tackling challenging problem sets like IMO problems.

1. Such methods, following the general spirit of AlphaGeometry [1], engage in random wandering within the symbolic space and synthesize new knowledge upon a well-designed symbolic framework. They may lay the groundwork for an AlphaGeo-style victory in Lean.
2. In practice, Alchemy-like method can be combined with existing NTP techniques.
   1. It may serve as a statement-augmenter for autoformalized statements or theorem-augmenter before retraining for each round of expert iteration.
   2. It can be used to augmenting existing knowledge base (available useful premises), which may be beneficial for Retrieval Augment Generation (RAG).
3. Transitioning from single-round mutations to multi-round mutations could potentially lead to the synthesis of exceedingly intricate and challenging theorems.

[1] Trinh, Trieu H., et al. "Solving olympiad geometry without human demonstrations." Nature 625.7995 (2024): 476-482.

We are sincerely grateful to you for your comprehensive assessment. We have carefully thought about your questions and made attempts to provide answers.

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)?

We conjecture the Mathlib corpus is included in the baseline models’ pretraining corpus, so we didn’t continual pretrain them in our paper. According to your advice, we retrain the baseline using two finetuning methodologies. Specifically, we conduct the continual pretraining on the Mathlib (theorems in the trainset of Leandojo) and then finetuning on Mathlib-train. The experimental results are listed in table below:

The minor improvement brought by CPT on Mathlib (without augmentation) may be attributed to Mathlib's inclusion in the pretraining data of LLMs [1, 2]. The improvements achieved on the novel_premises split is still promising (3.7% for Llama-3-8b; 3.9% for deepseek-prover-7B-v1.5).

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?

We conduct additional experiments on the finetuning hyperparameters. We retrain the Llama-3-8b with the same number of steps as the model finetuned on the augmented dataset. The experimental results are listed in table below:

The finetuning process with equal steps has not yielded the anticipated improvements for the baseline model. This outcome could be linked to unbalanced learning, as the additional 400 steps do not align with the number of steps in a single epoch.

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.

We have provided more details about this question in the general response.

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).

We have discussed the reasons for the high cost and possible optimization methods in the general response.

We want to thank you again for your time and patience in evaluating our work. Considering that the review time is soon coming to a close, we would greatly appreciate it if you have any further questions so that we can provide timely answers.

5. Data Diversity Issue

Reviewer BkaD and Reviewer NSyk show their concern about the lack of metrics for evaluating the diversity of synthesized theorems.

Reviewer BkaD 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.

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?

Reviewer NSyk

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.

In our methodology, mutations are applied to the statements of each theorem, capturing the essence of the theorems. Synthesized statements that successfully pass the Lean can be considered meaningful theorems to a certain degree. Additionally, our approach involves merging two existing proof trees from the Lean Mathematical Library, ensuring the significance of the generated theorems. As illustrated in Figure 1, a statement can undergo mutation to produce meaningful variants with mathematical meanings distinct from the original theorem.

To give deeper information about the diversity of our generated statements, we compute the Rouge score [1], a metric used in automatic summary generation tasks to evaluate the text similarity between the reference summary and generated summary. Specifically, with a reference sentence ref and a generated sentence gen, it computes the similarity between them.

We define below metrics to evaluate the diversity of generated theorems:

1. intra-diversity: A metric that evaluates how different the mutated theorems are compared to their original theorems and shows the effectiveness of our mutations. We select the original theorem as ref and its variants as gen. For each original theorem, we compute an average Rouge score. The returning score is the average of scores of all original theorems.
2. inter-diversity: A metric that evaluates the diversity of all synthesized variants. We adopt a bootstrap-like method. For each variant, we randomly sample twenty variants from the dataset as refs and compute the average score. The returning score is the average of scores of all variants.

For all these metrics, the lower, the better. The scores are listed in the table below: (Rouge-L)

The intra-diversity score of 0.52 indicates that our synthesized statements differ from the original theorems, demonstrating the effectiveness of our mutation process. Furthermore, we have noticed that the "apply" method outperforms the "rw" method in terms of mutation.

With an inter-diversity score of 0.167, we note a high level of diversity among the synthesized theorems. This score is nearly matching the original inter-diversity score, which means our method does not lower the diversity of original data.

In summary, our mutation methodology proves effective in generating a range of mutated theorems. Besides, as Reviewer NSyk said, synthesizing theorems in multi-round and generating deeper proof trees may further improve the diversity of generated theorems.

[1] Lin, Chin-Yew. ROUGE: a Package for Automatic Evaluation of Summaries. In Proceedings of the Workshop on Text Summarization Branches Out (WAS 2004), Barcelona, Spain, July 25 - 26, 2004.

Retraining Experiments

We remove the overlap data in our dataset and retrain the Llama-3-8b. The cleaned CPT data is now referred to as cpt-clean, while the cleaned SFT data is labeled as sft-clean. Their respective original training datasets, "Mathlib-train + rw + apply," are denoted as cpt-old and sft-old in our framework.

• CPT-ablation (all experiments with mathlib-tain sft)

• SFT-ablation (all experiments without cpt)

• CPT + SFT-ablation

The experimental results show that the overlap contributes a little to our improvement.

[1] Yang, Kaiyu, et al. "Leandojo: Theorem proving with retrieval-augmented language models." Advances in Neural Information Processing Systems 36 (2024).

4. Data Contamination

Reviewer FuWS and Reviewer BkaD express similar concerns about the data-contamination problems.

Reviewer FuWS

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?

Reviewer BkaD How do you avoid the data contamination problem in the evaluation/generation phase?

We take the data contamination problem seriously. We will show as many details about our work on this topic as possible.

The format of our synthesized data

We synthesize data with the whole mathlib dataset and do deduplication as in the following sections. The synthesized data are stored in jsonl format. Each line is as follows.

{
	"file_name": the name of the lean file in mathlib, 
	"original_text": the content of the file before writing variants back,
	"text": the content of the file with variants
	# we store the line number of each mutated 
	# variant with its original theorem name as key, [line_start, line_end]
	"loc": {   
			“theorem_name_1": [[20, 24], [25, 29]....], 
			“theorem_name_2": [[122, 127], [128, 133]....],
			“theorem_name_3": [[222, 227], [228, 233]....]
			...
	},
	# valid_loc has the same format as loc. But it only stores the variants
	# that passes the check of theorem prover (after Stage Two)
	"valid loc": {...},
	"meta": meta information (url, commit)
}

With the location and original name of each variant recorded, we are capable of conducting thorough data de-contamination.

Details of Continual Pre-Training

We conduct continual pre-training at the theorem level. An example of our training data is shown in Fig 10. Besides, as shown in Fig 6, the number of variants of different target theorems varies a lot. To mitigate the risk of biased learning due to this imbalance, we reduce the number of variants for each original theorem to adhere to a predefined maximum threshold.

De-contamination

Our training data for CPT and SFT are composed of two parts:

• Mathlib-train: Theorems (State-Tactics) in the training set of respective splits (random, novel_premises)
• Synthetic Data: Mutated Theorems (Additional Synthesized State-Tactics)

We try our best to avoid the train-test overlap:

1. Each model evaluated on different splits (random, novel_premises) is trained on distinct data. That’s to say, for a single line in Table 3, we need to train two models.
   1. Mathlib-train is the corresponding training set of the specific split
   2. Synthetic Data comprises unique subsets of our synthesized data achieved by excluding variants of theorems and their associated state-tactics pairs present in the test split.
2. Our training datasets strictly exclude theorems and variants from the test split.
   1. CPT Dataset: We eliminate all theorems and their synthesized variants present in the test split from the CPT dataset by matching theorem names.
   2. SFT Dataset: State-tactic pairs traced from the theorems in the test split and their corresponding synthesized variants are removed from the SFT dataset.
3. As for the novel_premises split, according to the explanation in Leandojo [1], it indicates that the proof of a test theorem includes at least one premise usage that is not present in the training set. In response to Reviewer FuWS's concerns regarding the effectiveness of the novel_premises benchmark and potential train-test overlaps with the data construction, we conduct a post-analysis. The whole procedure is as follows:
   1. We identify the novel premises by comparing the used premises in the training set and test set of the Leandojo Benchmark leveraging annotations provided by Leandojo [1].
   2. We parse the introduced “have” lemma in the CPT dataset and parse the additional state-tactic pairs in the SFT dataset that contain the novel premises (via simple regex matchings).
   3. We undertake additional training to rectify any issues with the experimental setup by removing such overlaps and retraining the model.

Novel-Premise overlap

We show the overlap ratios (num_containing_premise/total_num) in the table below:

We observed that the overlap ratio is relatively low, suggesting that its impact on improvement might be marginal.

3. Non-100% Conversion Ratio

Reviewer EDxu and Reviewer NSyk have questions about the non-100% conversion ratio from stage one to stage two.

Reviewer EDxu

How do you explain a Conversion Ratio of only 37% while the idea seems to work with a theoretical guarantee (i.e. 100%)?

Reviewer NSyk

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.

We will recap the exact behavior of each stage and explain the reason why the conversion ratio is not equal to 100%.

As discussed in Appendix C, our implementation consists of two stages.

• Stage One Find invocable theorems for each target theorem by running tactics. Each invocable theorem is stored as a triplet (initial proof state, next proof state, tactic) as in Fig 5.
• Stage Two We construct the mutated hypothesis or conclusion by parsing the next proof state and do symbolic replacement with the help of AST. Then, we build the new proof by integrating a “have” lemma with the original proof.

Indeed, synthesizing theorems in symbolic space works with a theoretical guarantee when the symbolic system is robust and well-designed. However, implementing the symbolic replacement is a non-trivial problem, which transforms codes in a pretty-printed proof state into raw lean code.

Our implementation of symbolic replacement involves conducting various string manipulations and parsing the ASTs for localization. Although conceptually straightforward, this method grapples with intricate scenarios like meta-variables, coercions, and other complexities.

For example, when replacing the old hypothesis of the target theorem with subgoals introduced by the invocable theorem for “apply”, navigating the relationship between metavariables [1] (e.g.,?a,?u.1338287) in the next proof state may be complex. Analyzing these relationships and assigning valid values to fill the gaps accurately poses a significant challenge, especially when conflicts arise in variable naming. Our conflict-detection and renaming mechanism [2] may falter in handling such intricate scenarios.

The complex metavariables cases account for a large ratio of the unpassed theorems, which is hard to tackle using several rules. We speculate that leveraging Large Language Models (LLMs) to fill these holes could offer a potential solution.

Despite these hurdles, our current implementation has successfully synthesized over three million theorems, augmenting the theorem-proving capacity of LLMs. Improving our implementation will further increase the conversion ratio, which requires a meticulous examination of the Lean parser and elaborator.

[1] MetaM - Metaprogramming in Lean 4

[2] Mathlib naming conventions

2. High Synthesis Cost

Reviewer FuWS

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).

Reviewer BkaD 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.

Given the computational demands, are there potential optimizations in the synthesis process to reduce the time and resources required for theorem mutation?

Reviewer FuWS and Reviewer BkaD show their concerns about the huge cost of our synthesizing algorithm and expect some possible optimizations.

Reason for the huge cost

As detailed in Section 4.1 and Appendix C.2, the primary computational bottleneck stems from Lean interaction time.

We choose Leandojo [1] as the tool to interact with Lean (run_tac API). The dojo version we used during the development of Alchemy is memory-intensive (requiring substantial memory usage and intensive IO), which hinders the implementation of multiprocessing. Besides, the initialization of the dojo is very slow (Several minutes for a dojo env).

Due to the drawbacks of the dojo, we just split the target theorems into groups and send them to hundreds of CPU nodes. Nested for loops run on each node (for each target theorem t in this group, for each possible tactic instruction i, run_tac(t, i)). This is a relatively slow but steady implementation on our existing hardware, compared to the multi-thread version (multi-dojo env for each node).

Possible speedup methods

The possible speedup methods are listed below:

1. Leverage updated Leandojo features Several updates about Leandojo may help decrease the cost. It significantly improves initialization speed when interacting with Lean4 after the 2.0.0 version and adds support for local and Remote Repositories after the 2.1.0 version [2].
2. Develop a fast and light interface.
   • The Lean repl [3] has its advantages over Dojo. It is lighter than Leandojo and friendly for multi-processing. Some Python wrappers [4, 5] for it are available, which may serve as bases for further development.
   • However, the Lean repl also has its limitations. It requires a higher latency to extract the information.
   • Based on the above discussion, we assume that it is promising to develop a fast interface for Lean based on Lean repl, which will not only speed up our algorithm a lot but also contribute to the research of Tree Search and Reinforcement Learning in NTP [6, 7, 8].
3. Narrow search space We can implement some heuristics or learn a model to narrow the search beam of possibly invocable theorems and help to avoid unnecessary operations.
4. Scale the computing units (Trivial one) It is much cheaper to extend the CPU than the GPU. Getting more CPU is the easiest way to lower the time cost.

[1] Yang, Kaiyu, et al. "Leandojo: Theorem proving with retrieval-augmented language models." Advances in Neural Information Processing Systems 36 (2024).

[2] https://github.com/lean-dojo/LeanDojo/releases?page=1

[3] leanprover-community/repl: A simple REPL for Lean 4, returning information about errors and sorries.

[4] zhangir-azerbayev/repl: A simple REPL for Lean 4, returning information about errors and sorries.

[5] cmu-l3/minictx-eval: Neural theorem proving evaluation via the Lean REPL

[6] Lample, Guillaume, et al. "Hypertree proof search for neural theorem proving." Advances in neural information processing systems 35 (2022): 26337-26349.

[7] 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).

[8] ABEL: Sample Efficient Online Reinforcement Learning for Neural Theorem Proving