Large Language Models (LLMs) and the Formalization of Mathematics

Mentored by Bjoern Andres, Markus Krötzsch
at TU Dresden, Chair of Machine Learning for Computer Vision

Recent advances of Large Language Models (LLMs) in applications such as ChatGPT have sparked interest in learning and applying such models also for formal languages, notably mathematics [1]. The goal of this blue-skies, curiosity-driven research project is to study LLMs in connection with corpora of formal mathematics, e.g. [2], and in combination with proof checkers, toward the goal of synthesizing meaningful mathematical theorems and correct mathematical proofs. Specific topics include, but are not limited to: Automated theorem proving, computer-assisted theorem proving and computer-assisted formalization of mathematics.

[1] https://arxiv.org/abs/2310.10631
[2] https://us.metamath.org/

Work Environment

This SECAI position is shared between the Machine Learning for Computer Vision group and the Knowledge-Based Systems group within in the Institute of Artificial Intelligence at the Faculty of Computer Science of TU Dresden. The admitted student will be a member of SECAI, with complete access to the support structure and plenty of opportunity to enjoy the graduate school culture.

Prerequisites

• Master’s Degree (or equivalent) in computer science, mathematics, or related fields
• Very good, comprehensive education in mathematics, especially discrete mathematics
• Very good programming skills in C, C++, Rust or Java
• Strong interest in the formalization of mathematics
• Willingness to work with corpora of formal mathematics
• Ability to collaborate well in an interdisciplinary environment

Further details on the requirements and application process can be found in SECAI's announcement for open PhD positions in 2024.