用检索增强生成提升大模型数学证明能力
LemmaHead: RAG Assisted Proof Generation Using Large Language Models
- 构建知识库LemmaHead，通过检索教材上下文增强模型推理
- 在Lean语言下证明任务中表现优于纯提示方法
- 适合需要严谨数学推理的AI研究者与形式化验证开发者
大语言模型在解决数学问题或撰写数学证明方面仍具挑战。现有主流方法多通过对学术文献和教科书进行微调，使模型模仿数学写作风格。本文探索使用检索增强生成（RAG）弥补大模型在数学推理上的不足。我们提出LemmaHead，一个基于教科书内容的RAG知识库，为模型查询提供相关数学上下文。通过在Lean形式语言下生成给定数学命题的证明任务评估模型性能，测试表明该方法显著提升了推理能力。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。