摘要

本文提出了一种名为TheoremLlama的端到端框架，旨在将通用大型语言模型（LLM）转变为Lean4专家，用于在计算机可验证的正式语言中证明数学定理。该框架通过生成自然语言（NL）与正式语言（FL）对齐的数据集，训练LLM进行正式定理证明，并利用NL引导的证明写作技术，显著提高了LLM在Lean4定理证明任务中的性能。TheoremLlama在MiniF2F-Valid和Test数据集上的准确率分别达到了36.48%和33.61%，超过了GPT-4基线。此外，该研究还开源了模型检查点和生成的数据集，预计将降低学术研究者在相关领域的门槛。

原理

TheoremLlama框架的核心创新在于NL-FL对齐数据集生成方法和NL-FL引导的证明写作技术。首先，通过从Mathlib4库中提取Lean4代码，并使用LLM进行去形式化（deformalization），生成自然语言的定理陈述和证明。然后，通过NL-FL引导的证明写作技术，将自然语言证明嵌入到Lean4代码中，使LLM能够更好地利用其自然语言推理能力进行正式推理。此外，该框架还包括块训练（Block Training）和课程数据排序（Curriculum Data Sorting）技术，以提高LLM在Lean4定理证明任务中的上下文学习能力和训练过程的稳定性。

流程

TheoremLlama的工作流程分为三个主要阶段：(a) NL-FL对齐数据集生成，(b) Lean4证明器训练，(c) 迭代证明写作。在数据集生成阶段，首先从Mathlib4中提取Lean4数据，然后使用T5编码器搜索最佳示例进行去形式化，最后通过Gemini-1.5进行去形式化并生成NL-FL对齐的数据集。在证明器训练阶段，使用块训练和课程数据排序技术对LLM进行微调，使其成为Lean4专家。在迭代证明写作阶段，使用先前生成的正确证明作为上下文示例，进一步提高LLM的证明写作能力。

应用

TheoremLlama框架的应用前景广泛，特别是在数学定理证明和计算机科学领域。该框架不仅能够提高LLM在正式定理证明任务中的性能，还为学术研究者提供了一个有效的工具，以降低在相关领域的研究门槛。此外，该框架的方法和数据集生成技术也可以推广到其他需要NL-FL对齐的任务中，具有很高的实用价值和研究潜力。