Formal Language Knowledge Corpus for Retrieval Augmented Generation

TL;DR

This paper investigates using the Lean proof language to build a knowledge corpus for retrieval-augmented generation systems, aiming to enhance LLMs' performance in complex mathematical reasoning tasks.

Contribution

It introduces a novel approach of leveraging Lean to create a specialized knowledge corpus for RAG systems focused on mathematical reasoning.

Findings

Potential for improved reasoning in LLMs using Lean-based knowledge corpus

Lays groundwork for future research in RAG-enhanced logical reasoning

Highlights the need for specialized corpora in advanced reasoning tasks

Abstract

The integration of retrieval-augmented techniques with LLMs has shown promise in improving performance across various domains. However, their utility in tasks requiring advanced reasoning, such as generating and evaluating mathematical statements and proofs, remains underexplored. This study explores the use of Lean, a programming language for writing mathematical proofs, to populate the knowledge corpus used by RAG systems. We hope for this to lay the foundation to exploring different methods of using RAGs to improve the performance of LLMs in advanced logical reasoning tasks.