用于检索增强生成的形式语言知识库

本研究解决了检索增强技术与大型语言模型结合在高级推理任务中的应用不足问题，尤其是在生成和评估数学语句及证明方面。通过使用Lean语言构建知识库，为检索增强系统提供支持，期望为提升大型语言模型在高级逻辑推理任务中的性能打下基础。