View Proposal

Proposer
Kathrin Stark
Title
Autoformalization with LLMs and Proof Assistants
Goal
Description
Are you interested in the intersection of machine learning, mathematics, and verification? Do you want to explore how machine learning models and proof assistants can be combined to automatically translate natural language mathematics into formal specifications? Then this honours thesis project is for you! In this project, you will work on testing how well LLMs perform on autoformalization, i.e. translating natural language mathematics into formal language. You will explore the capabilities and limitations, as well as evaluate its performance in comparison to existing methods for autoformalization. You will also have the opportunity to learn about proof assistants and their role in formal verification. If you are interested in this project, please contact me at [k.stark@hw.ac.uk](mailto:k.stark@hw.ac.uk) or make a short appointment at https://outlook.office365.com/owa/calendar/KathrinsMeetingCalendar@heriotwatt.onmicrosoft.com/bookings/.
Resources
Background
Url
Difficulty Level
Variable
Ethical Approval
None
Number Of Students
1
Supervisor
Kathrin Stark
Keywords
Degrees
Bachelor of Science in Computer Science
Bachelor of Science in Computer Systems
Back to List