用数学证明语言Lean构建知识库，提升大模型逻辑推理能力
Formal Language Knowledge Corpus for Retrieval Augmented Generation
- 用Lean语言构建数学证明知识库，增强RAG系统
- 在数学命题生成与证明任务中验证了效果
- 适合研究大模型逻辑推理与知识增强的学者
将检索增强技术与大语言模型结合，在多个领域展现出提升性能的潜力。然而，其在需要高级推理的任务（如生成和评估数学命题与证明）中的应用仍缺乏探索。本研究利用Lean——一种用于编写数学证明的编程语言——来填充RAG系统所用的知识库。旨在为探索不同RAG方法在提升大模型在复杂逻辑推理任务中表现方面奠定基础。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。