Neural approaches to theorem search & proof repair

Reichel, Thomas

Permalink

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

Description

Title

Neural approaches to theorem search & proof repair

Author(s)

Reichel, Thomas

Issue Date

2024-07-16

Director of Research (if dissertation) or Advisor (if thesis)

Ringer, Talia

Department of Study

Siebel Computing &DataScience

Discipline

Computer Science

Degree Granting Institution

University of Illinois at Urbana-Champaign

Degree Name

M.S.

Degree Level

Thesis

Keyword(s)

• machine learning
• formal methods
• large language models
• proof repair
• theorem search
• natural language search
• Coq

Abstract

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.

Graduation Semester

2024-08

Type of Resource

Thesis

Handle URL

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

Copyright and License Information

Copyright 2024 Thomas Reichel

Owning Collections