Using large language model for formal proof generation

The Hong Kong University of Science and Technology
Department of Computer Science and Engineering

Final Year Thesis Oral Defense

Title: "Using large language model for formal proof generation"

by

SEN Yigit

Abstract:

Formal proofs are applications of theorems and other logic operations on a 
problem definition to prove that propositions derived from it are logically 
sound. With improvements in technology, these proofs are increasingly 
completed using computers and proof assistants. To write proofs, one needs a 
strong understanding of the lemmas and functions of the proof assistants 
chosen. With recent advancements in artificial intelligence, and in 
particular large language models (LLMs), this requirement is relaxed and 
developers can use LLMs to assist in or even generate proofs. This final year 
thesis investigates the performance of current models in generating proofs 
for Rocq (formerly Coq) Proof Assistant, and proposes an LLM-based model that 
is capable of generating complete proofs assisted by the state of the proof, 
allowing the LLM to make more informed predictions.


Date            : 2 May 2025 (Friday)

Time            : 16:00 - 16:40

Venue           : Room 2129A (near lift 19), HKUST

Advisor         : Dr. WANG Shuai

2nd Reader      : Dr. WU Daoyuan