Posts by Collection

Portfolio item number 1

Short description of portfolio item number 1

Portfolio item number 2

Short description of portfolio item number 2

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

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

Introduction to Databases

Undergraduate course, University of Toronto, Department of Computer Science, 2023

Introduction to database management systems. The relational data model. Relational algebra. Querying and updating databases: the query language SQL. Application programming with SQL. Integrity constraints, normal forms, and database design. Elements of database system technology: query processing, transaction management.

Introduction to Artificial Intelligence

Undergraduate Courses, University of Toronto, Department of Computer Science, 2024

Theories and algorithms that capture (or approximate) some of the core elements of computational intelligence. Topics include: search; logical representations and reasoning, classical automated planning, representing and reasoning with uncertainty, learning, decision making (planning) under uncertainty. Assignments provide practical experience, in both theory and programming, of the core topics.