Withdraw
Loading…
Neural approaches to theorem search & proof repair
Reichel, Thomas
Content Files

Loading…
Download Files
Loading…
Download Counts (All Files)
Loading…
Edit File
Loading…
Permalink
https://hdl.handle.net/2142/125634
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
Graduate Dissertations and Theses at Illinois PRIMARY
Graduate Theses and Dissertations at IllinoisManage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…