LemmaHead: RAG Assisted Proof Generation Using Large Language Models

TL;DR

LemmatHead leverages retrieval augmented generation to enhance large language models' ability to generate mathematical proofs, focusing on theorem proving in the Lean language by supplementing models with relevant textbook context.

Contribution

This work introduces LemmaHead, a RAG-based knowledge base that improves mathematical reasoning in LLMs by integrating relevant textbook information for proof generation.

Findings

Improved proof generation accuracy in Lean theorem proving

Effective integration of textbook context enhances reasoning

Demonstrated benefits of RAG in mathematical tasks

Abstract

Developing the logic necessary to solve mathematical problems or write mathematical proofs is one of the more difficult objectives for large language models (LLMS). Currently, the most popular methods in literature consists of fine-tuning the model on written mathematical content such as academic publications and textbooks, so that the model can learn to emulate the style of mathematical writing. In this project, we explore the effectiveness of using retrieval augmented generation (RAG) to address gaps in the mathematical reasoning of LLMs. We develop LemmaHead, a RAG knowledge base that supplements queries to the model with relevant mathematical context, with particular focus on context from published textbooks. To measure our model's performance in mathematical reasoning, our testing paradigm focuses on the task of automated theorem proving via generating proofs to a given mathematical claim in the Lean formal language.