22 Aug 2024 | Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si
This paper provides a comprehensive survey of deep learning approaches in theorem proving, covering various tasks such as autoformalization, premise selection, proofstep generation, and proof search. It reviews existing datasets and strategies for synthetic data generation, analyzes evaluation metrics, and discusses the performance of state-of-the-art methods. The paper also highlights persistent challenges and future research directions, emphasizing the need for more unified evaluation protocols and better human-AI interaction. The authors aim to serve as a foundational reference for researchers in this rapidly growing field.This paper provides a comprehensive survey of deep learning approaches in theorem proving, covering various tasks such as autoformalization, premise selection, proofstep generation, and proof search. It reviews existing datasets and strategies for synthetic data generation, analyzes evaluation metrics, and discusses the performance of state-of-the-art methods. The paper also highlights persistent challenges and future research directions, emphasizing the need for more unified evaluation protocols and better human-AI interaction. The authors aim to serve as a foundational reference for researchers in this rapidly growing field.