2024 | Zhao Yu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si
This paper presents a comprehensive survey of deep learning approaches for theorem proving, covering key tasks such as autoformalization, premise selection, proofstep generation, proof search, and other related tasks. The survey reviews existing methods, datasets, and evaluation metrics, while highlighting challenges and future directions in this rapidly evolving field. The paper discusses the transition from informal to formal theorem proving, the role of deep learning in enhancing traditional theorem proving techniques, and the impact of large language models on this domain. It also explores the use of deep learning for generating and verifying mathematical proofs, including the development of datasets and the evaluation of state-of-the-art methods. The survey emphasizes the importance of structured approaches, the need for standardized evaluation frameworks, and the potential of deep learning to improve the efficiency and accuracy of theorem proving. Challenges such as data scarcity, evaluation inconsistencies, and the need for better human-AI interaction are discussed, along with promising future directions in conjecturing, verified code generation, and math education. The paper concludes with a call for further research and collaboration between deep learning researchers and mathematicians to advance the field of theorem proving.This paper presents a comprehensive survey of deep learning approaches for theorem proving, covering key tasks such as autoformalization, premise selection, proofstep generation, proof search, and other related tasks. The survey reviews existing methods, datasets, and evaluation metrics, while highlighting challenges and future directions in this rapidly evolving field. The paper discusses the transition from informal to formal theorem proving, the role of deep learning in enhancing traditional theorem proving techniques, and the impact of large language models on this domain. It also explores the use of deep learning for generating and verifying mathematical proofs, including the development of datasets and the evaluation of state-of-the-art methods. The survey emphasizes the importance of structured approaches, the need for standardized evaluation frameworks, and the potential of deep learning to improve the efficiency and accuracy of theorem proving. Challenges such as data scarcity, evaluation inconsistencies, and the need for better human-AI interaction are discussed, along with promising future directions in conjecturing, verified code generation, and math education. The paper concludes with a call for further research and collaboration between deep learning researchers and mathematicians to advance the field of theorem proving.