用于检索增强生成的形式语言知识语料库
Formal Language Knowledge Corpus for Retrieval Augmented Generation
- The Hebrew University of Jerusalem（耶路撒冷希伯来大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本研究探索使用Lean语言填充RAG系统的知识语料库，以改善LLMs在生成与评估数学证明等高级逻辑推理任务中的表现。
AI中文摘要：
检索增强技术与LLMs的整合在提升各领域性能方面展现出潜力。然而，它们在需要高级推理的任务（如生成和评估数学陈述与证明）中的效用仍有待探索。本研究探索使用Lean（一种用于编写数学证明的编程语言）来填充RAG系统使用的知识语料库。我们希望这能为探索使用RAG提升LLMs在高级逻辑推理任务中性能的不同方法奠定基础。
英文摘要：
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.
