A Survey on Deep Learning for Theorem Proving

Summary

This paper offers a literature review on theorem proving, with a focus on recent deep learning approaches. The paper begins with introducing the informal and formal formulations of theorem proving, followed by presenting five common tasks in theorem proving and existing methods developed for each task, and then summarizes datasets, evaluation metrics and state-of-the-art model performances. The paper concludes with a discussion of outstanding challenges and promising future directions. In my opinion this paper has a lot of good value. For a novice, it would be a great entry point for them to learn about the research landscape in ML-based theorem proving. For more senior researchers, it can also help organize their knowledge obtained from the large and scattering volume of work.

Rating

8

Confidence

3

Ethics flag

1

Reasons to accept

Overall, I think readers of this paper can gain a comprehensive bird-eye view of the most important recent advances in ML-based theorem proving. As someone who worked in theorem proving, I personally learned a lot from this paper. 1. The paper is well structured and clearly written. 1. This review has very good coverage of notable papers in the field of learning-based theorem proving. For those cited papers that I am familiar with, the summary is generally accurate. 1. It is very refreshing that the paper summarizes theorem proving tasks into five categories: autoformalization, premise selection, proofstep generation, proof search, and others. From the myriad of papers, this structure makes things very clear and easy to understand. Within each task, more fine-grained clustering is made (e.g., formulating the task as classification vs retrieval vs language modeling, early attempts using CNNs/RNNs vs more recent approaches leveraging pretrained LLMs and in-context learning).

Reasons to reject

I wouldn’t say these are reasons to reject, they are more like suggestions to make the paper more clear. Happy to discuss further if there’s any misunderstanding. 1. The presentation of datasets (Figure 3) can be made richer by including additional details, such as dataset size, data source, and annotation type (e.g. theorems, proofs, annotation of premises, fine-grained proof artifacts), so readers who are looking for data can more easily locate the best resource for them. This might be best presented as a table. 1. In section 3.4 “proof search”, I’m not sure if I understand why search methods are discussed separately for ATP and ITP. As mentioned in this section, in both domains, classical search methods like best-first search and MCTS are shown to be applicable. Can you maybe clarify how search is different in APT and in ITP? 1. Nit: In section 5 “theorem proving” paragraph, the Thor method seems to be implied as a “tactic-based model with best-first search” and contrasted with LLM-based methods and search-based methods. However, Thor also employs language models and proof search. It seems to me the takeaway here can be: using powerful LLMs can help, and using advanced search on top can also help. Some nuances could use some adjustment to make the story clearer here.

Summary

This paper presents a comprehensive survey of deep-learning related exploration in the theorem proving. The survey features a summary of related tasks, datasets and evaluation metrics. At the end, the authors also discuss the challenges and the promising avenues for future exploration.

Rating

8

Confidence

4

Ethics flag

1

Reasons to accept

The paper is well structured and comprehensive enough to include all the relevant papers I am aware of in the field.

Reasons to reject

I am not exactly sure about COLM's criteria for a survey paper. The main downside of this paper is the potential overlap of another survey paper published last year (https://arxiv.org/pdf/2212.10535), though I can see some of the latest work have been added.

Questions to authors

I don't have any specific questions. The followings are merely some comments: - page 2, 'saturation-based theorem provers'/'tableau-based', might be worth mentioning SAT/SMT-based approaches, which probably play the most important role in existing ATPs. - page 4, 'premise selection': despite the research in deep-learning-based premise selection, most of the working systems are still based on heuristics. This is especially true for ATPs. In exceptions like LeanCopilot we usually don't do fast proof explorations. The trade-off between efficiency, engineering difficulty, and prediction accuracy could be a topic worth discussion. - page 8, evaluation: Another (general) challenge in this field is the data contamination during the pretraining stage. This is also the reason that the Graph2Tac paper (https://arxiv.org/pdf/2401.02949) chose not to pretrain their LM baseline. More discussion is probably needed here.

Summary

This paper surveys the field of applying deep learning methods to theorem proving. An extensive summary of 170 papers is made on several tasks such as autoformaliztion, premise selection, proofstep generation, proof search and other tasks such as automated conjecturing. A taxonomy on the datasets involved in automated theorem proving is also made in a proper and comprehensive manner. Finally, a review of evaluations is given and a discussion on the future challenges is made, with an emphasis on data scarcity, evaluation and human-ai interaction.

Rating

8

Confidence

4

Ethics flag

1

Reasons to accept

* The summary is very well-structured and well-suited according to the types of tasks and datasets. * The authors have good understanding of the general tendency of the field and its future. The challenges in Section 6 include important directions such as data scarcity. * The writing is clear in general and easy to read In general, automated conjecturing, automated theorem generation and reasoning data synthesis would be a very important direction in the future and it would be good to either have a separate subsection in Section 3 or emphasize it in 3.5 Other tasks.

Reasons to reject

* Several references are missing in some paragraphs: * “DT-Solver” in 3.3 after “Subsequent advancements” * “DT-Solver” in 3.4 after “Moreover, various works” * “MUSTARD” in 3.5 before “explore automated conjecturing” * It would be nice to have some visualizations in the evaluation section for benchmarking and comparison purpose.

Questions to authors

see above

Ethics concerns details

n/a

Summary

This paper provides a comprehensive survey on deep learning approaches for theorem proving. The survey includes a thorough review of existing tasks and methods, meticulous summary of available datasets and strategies for data generation, a detailed analysis of evaluation metrics and the performance of state-of-the-art, and a critical discussion on the challenges and future directions.

Rating

8

Confidence

4

Ethics flag

1

Reasons to accept

The paper provides a very thorough summary and includes most of the related research works. I believe this paper provides a fundamental reference to the community. This paper is well-organized and very easy to follow. The discussions on current challenges and future directions are insightful.

Reasons to reject

Q1. References are missing in Section 2.1. For example, PrOntoQA [3] and EntailmentBank [4] are some demonstrations of informal theorem proving via natural language explanation. Q2. Some search works may be missing. For example, ATG [1] introduces an automated theorem generation task and corresponding evaluation metrics to evaluate if a model can generate new theorems for a given theorem proving to achieve the shortest proof as human mathematicians. They construct the benchmark by synthesizing new theorems based on Metamath language and the “set.mm” library. This paper should be included in Section 4.2. Q3. For proof generation via LLMs with several prompting methods, some of the methods also leverage the theorem prover feedback to prompt the LLMs to self-correct the proofs. For example, MUSTARD [2] uses the error messages from Lean prover to refine the proof generation. Q4. Many references are not the newest version. For example, “Llemma: An Open Language Model for Mathematics”, “Holist: An environment for machine learning of higher-order theorem proving”, “Lego-prover: Neural theorem proving with growing libraries” are all published in conference proceedings. The authors need to carefully check the reference list to make sure the citations are up to date. [1] Xiaohan Lin, Qingxing Cao, Yinya Huang, Zhicheng Yang, Zhengying Liu, Zhenguo Li, Xiaodan Liang (2024). ATG: Benchmarking Automated Theorem Generation for Generative Language Models. 2024 Annual Conference of the North American Chapter of the Association for Computational Linguistics (NAACL 2024 Findings). [2] Yinya Huang, Xiaohan Lin, Zhengying Liu, Qingxing Cao, Huajian Xin, Haiming Wang, Zhenguo Li, Linqi Song, Xiaodan Liang (2024). MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data. The Twelfth International Conference on Learning Representations (ICLR 2024). [3] Abulhair Saparov, He He (2023). Language Models are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought. The Eleventh International Conference on Learning Representations (ICLR 2023). [4] Bhavana Dalvi, Peter Jansen, Oyvind Tafjord, Zhengnan Xie, Hannah Smith, Leighanna Pipatanangkura, Peter Clark (2021). Explaining Answers with Entailment Trees. Proceedings of the 2021 Conference on Empirical Methods in Natural Language Processing (EMNLP 2021).

Questions to authors

Please see the questions above.

Thanks for the response.

Thanks for the response! I will keep my rating.