Advancements and Challenges in Automated Theorem Proving: A Survey

PhD Qualifying Examination


Title: "Advancements and Challenges in Automated Theorem Proving: A Survey"

by

Mr. Jae Boum KIM


Abstract:

Advancements in artificial intelligence, particularly in large language models 
(LLMs), have revolutionized multiple domains, surpassing human capabilities. 
However, automated theorem proving (ATP), which verifies software and hardware 
systems and facilitates mathematical research and discovery, remains an 
important and challenging area of AI. Historically, ATP has faced data 
shortages that have prevented it from training efficient machine learning 
models: fragmented formal languages and a lack of machines-interpretable and 
formalized data. The introduction of the transformer model to ATP in 2020 
revolutionized ATP technology, and since then, the utilization of LMs has been 
a pivotal component of research in the field of ATP. However, despite many 
technological advances since then, ATP technology has been limited by the 
inherent limitations of the transformer architecture and an ongoing lack of 
data, with over 50% of the problems in the miniF2F benchmark dataset from 2021 
still unresolved. In this paper, we provide a brief introduction to formal 
mathematics, survey the challenges currently facing ATP, review recent advances 
in ATP research and benchmark dataset, and discusses future research directions 
based on these insights.


Date:                   Tuesday, 21 May 2024

Time:                   9:00am - 11:00am

Venue:                  Room 3494
                        Lifts 25/26

Committee Members:      Dr. Sunghun Kim (Supervisor)
                        Prof. Raymond Wong (Chairperson)
                        Dr. Jiasi Shen
                        Dr. Shuai Wang