Formal Language Knowledge Corpus for Retrieval Augmented Generation
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.
Code (0)
등록된 구현이 없습니다.
Tasks
Logical ReasoningMathematical ProofsRAGRetrievalRetrieval-augmented GenerationMethods 이 논문이 사용한 방법론
Similar Papers 제목 키워드 기반
Retrieved But Not Reliable: A Survey on Attacks, and Defenses in Retrieval-Augmented Generation
Retrieval-Augmented Generation (RAG) enhances large language models by grounding outputs in external knowledge, improving factuality and reducing hallucinations. At the same time, the retrieval-augmented pipeline introdu…
Embedding-Informed Adaptive Retrieval-Augmented Generation of Large Language Models
Retrieval-augmented large language models (LLMs) have been remarkably competent in various NLP tasks. However, it was observed by previous works that retrieval is not always helpful, especially when the LLM is already kn…
Continual LearningRetrievalRetrieval-augmented GenerationZero-RAG: Towards Retrieval-Augmented Generation with Zero Redundant Knowledge
Retrieval-Augmented Generation has shown remarkable results to address Large Language Models' hallucinations, which usually uses a large external corpus to supplement knowledge to LLMs. However, with the development of L…
Improving Retrieval-Augmented Large Language Models via Data Importance Learning
Retrieval augmentation enables large language models to take advantage of external knowledge, for example on tasks like question answering and data imputation. However, the performance of such retrieval-augmented models …
ImputationQuestion AnsweringRetrievalAutomated Formalization via Conceptual Retrieval-Augmented LLMs
Interactive theorem provers (ITPs) require manual formalization, which is labor-intensive and demands expert knowledge. While automated formalization offers a potential solution, it faces two major challenges: model hall…
Code Generation