Jack Sun （孙嘉良）

Jack Sun （孙嘉良）

CS Ph.D. at University of Toronto

Publications

You can also find my articles on my Google Scholar profile.

A Survey on Deep Learning for Theorem Proving

Published in Conference on Language Modeling (COLM), 2024

We presents a pioneering comprehensive survey of deep learning for theorem proving by offering i) a thorough review of existing approaches across various tasks such as autoformalization, premise selection, proofstep generation, and proof search; ii) a meticulous summary of available datasets and strategies for data generation; iii) a detailed analysis of evaluation metrics and the performance of state-of-the-art; and iv) a critical discussion on the persistent challenges and the promising avenues for future exploration.

Recommended citation: Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A Survey on Deep Learning for Theorem Proving. In proceedings of the Conference on Language Modeling, 2024.
Paper

Autoformalizing Euclidean Geometry

Published in International Conference on Machine Learning (ICML), 2024

We release LeanEuclid, a benchmark for testing autoformalization, consisting of Euclid’s Elements (Book I) manually formalized in Lean. It is challenging for state-of-the-art LLMs like GPT-4V. Furthermore, the process of constructing LeanEuclid has uncovered intriguing ambiguities in Euclid’s original works.

Recommended citation: Logan Murphy, Kaiyu Yang, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, and Xujie Si. Autoformalizing Euclidean Geometry. In Proceedings of the International Conference on Machine Learning, 2024.
Paper