Title (Tentative): Large Language Models for Formal Theorem Proving
Supervisor: Dr. Kong, Lingpeng
Student: Tao, Xijia
Overview:
In recent years, there have been significant advancements in deep learning, specifically in the development of large language models (LLM) like OpenAI’s GPT-3. These models have demonstrated impressive abilities in understanding, generating, and reasoning with natural language. They have been successfully applied to tasks such as language translation, text summarization, and question answering.
However, the application of these language models in formal theorem proving, which involves using rigorous reasoning to establish the correctness of mathematical statements, is relatively unexplored. Formal theorem proving has traditionally been a complex and time-consuming process, requiring expertise in mathematical logic and manual effort. This project aims to explore how AI techniques, combined with natural language understanding and reasoning capabilities, can create an intuitive and user-friendly environment for theorem proving.
By employing the power of LLM, the project seeks to address the challenges associated with formal theorem proving. The proposed system will allow users to interact with the language model using natural language queries, enabling them to express mathematical statements, explore proof strategies, and receive real-time suggestions and feedback. This interactive formal theorem proving system holds several advantages, including reducing the time and effort required for theorem proving tasks, enhancing the discovery and exploration of new theorems, and pushing the boundaries of what is currently achievable in formal mathematics.
Existing approaches in this field have shown limited performance on benchmarks, indicating room for improvement. By augmenting LLM to improve reasoning over longer distances, substantial advancements can be made in theorem proving.