Neural approaches to theorem search & proof repair

This interdisciplinary formal methods/machine learning thesis builds neural automation for two proof-centric tasks that catalyze the reuse of existing proofs: (1) natural language theorem search, in which theorems and their corresponding proofs are retrieved from a database using natural language descriptions and (2) proof repair, in which proofs broken by external changes are mended. The theorem search model is also used as a component of the proof repair tool, allowing it to better interact with the environment. Each task is tackled holistically: we contribute datasets, fine-tuned large language models, and the end-user tools needed to make use of those models.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2024

Author dc:creator

• Reichel, Thomas

Contributors dc:contributor

• Ringer, Talia

• Machine Learning
• Formal Methods
• Large Language Models
• Proof Repair
• Theorem Search
• Natural Language Search
• Coq

Statement dc:rights

• Copyright 2024 Thomas Reichel

Language dc:language

en, eng

Handle dc:identifier

https://hdl.handle.net/2142/125634

OAI record oai:identifier

https://www.ideals.illinois.edu/oai-pmh?verb=GetRecord&metadataPrefix=etdms&identifier=oai%3Awww.ideals.illinois.edu%3A2142%2F125634