Zhaoyu Li (李照宇)



Photo credit: Weizhe Chen.

I am a Ph.D. student in Computer Science at the University of Toronto, working with Prof. Xujie Si. Before coming to U of T, I spent one and a half years at McGill University and Mila - Quebec AI Institute as a Ph.D. student. Prior to that, I obtained my bachelor's degree with honors from the ACM class at Shanghai Jiao Tong University (SJTU).

During my undergraduate studies, I was fortunate to work with Prof. Junchi Yan as a research assistant at SJTU Think Lab in 2019, and with Prof. Le Song as a research intern at the Georgia Tech Machine Learning Group in 2020.

My research interests mainly lie in neuro-symbolic AI, with a special focus on using deep neural networks to perform logical reasoning and mathematical reasoning. Recently, I have been working on using large language models to generate mathematical proofs like human beings, tackling the automated theorem proving problem in both formal and informal settings.

With a strong theoretical understanding and specific domain knowledge, I am also interested in developing machine learning algorithms for combinatorial optimization problems, particularly those around satisfiability problems such as SAT, SMT, and #SAT (model counting) problems, and applying them as reasoning engines in various downstream applications.

If you find any research interests that we might share, feel free to drop me an email. I am always open to potential collaborations.


  1. Autoformalization with Symbolic Equivalence and Semantic Consistency
    Zenan Li, Yifan Wu, Zhaoyu Li, Xinming Wei, Xian Zhang, Fan Yang, Xiaoxing Ma
  2. APPL: A Prompt Programming Language for Harmonious Integration of Programs and Large Language Model Prompts [paper] [code]
    Honghua Dong, Qidong Su, Yubo Gao, Zhaoyu Li, Yangjun Ruan, Gennady Pekhimenko, Chris J. Maddison, Xujie Si
  3. A Survey on Deep Learning for Theorem Proving [paper] [code]
    COLM 2024
    Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, Xujie Si
  4. Autoformalizing Euclidean Geometry [paper] [code]
    ICML 2024
    Logan Murphy*, Kaiyu Yang*, Jialiang Sun, Zhaoyu Li, Anima Anandkumar, Xujie Si
  5. G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks [paper] [code]
    TMLR 2024
    Zhaoyu Li, Jinpei Guo, Xujie Si
  6. Learning Reliable Logical Rules with SATNet [paper] [code]
    NeurIPS 2023
    Zhaoyu Li, Jinpei Guo, Yuhe Jiang, Xujie Si
  7. Neuro-symbolic Learning Yielding Logical Constraints [paper] [code]
    NeurIPS 2023
    Zenan Li, Yunpeng Huang, Zhaoyu Li, Yuan Yao, Jingwei Xu, Taolue Chen, Xiaoxing Ma, Jian Lu
  8. NSNet: A General Neural Probabilistic Framework for Satisfiability Problems [paper] [code]
    NeurIPS 2022
    Zhaoyu Li, Xujie Si
  9. Graph Contrastive Pre-training for Effective Theorem Reasoning [paper]
    ICML Workshop on Self-Supervised Learning for Reasoning and Perception 2021 (Contributed talk)
    Zhaoyu Li, Binghong Chen, Xujie Si

Selected Awards

  • GREAT Awards, McGill University, 2022
  • Max Stern Recruitment Fellowship, McGill University, 2021
  • Graduate Excellence Fellowship, McGill University, 2021 - 2022
  • Chinese National Scholarship, (Top 1% in SJTU), 2020
  • Excellent School-level Scholarship, (Top 3% in SJTU), 2017 - 2019
  • Zhiyuan Honorary Scholarship, (Top 5% in SJTU), 2017 - 2020

Teaching Experience

  • Teaching Assistant of CSC2547: Automated Reasoning with Machine Learning, 2024, U of T
  • Teaching Assistant of CSC2547: Automated Reasoning with Machine Learning, 2023, U of T
  • Guest Lecturer of MS326: Deep Learning and Its Applications, 2022, SJTU
  • Teaching Assistant of MS110: Computer System (2), 2020, SJTU
  • Teaching Assistant of MS108: Computer System (1), 2019, SJTU


  • zhaoyu [at] cs [dot] toronto [dot] edu