TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

使用像Lean这样的计算机可验证形式语言来证明数学定理，显著影响了数学推理。一种形式化定理证明的方法涉及使用基于自然语言证明的大型语言模型（LLMs）生成完整证明。类似的方法在代码生成方面已经显示出有希望的结果。然而，大多数现代LLMs由于缺乏对齐的自然语言和形式语言定理证明数据而表现出次优性能。这种稀缺性导致缺乏训练LLMs的方法和技术，以充分利用它们在组合形式证明方面的能力。为了解决这些挑战，本文提出了TheoremLlama，一个端到端框架，用于训练通用的LLM成为Lean4专家。该框架包括NL-FL对齐数据集生成方法、LLM形式定理证明的训练方法以及LLM Lean4证明编写技术。使用数据集生成方法，我们提供了Open Bootstrapped Theorems（OBT），一个NL-FL对齐和引导式的数据集。该框架的一个关键创新是NL-FL引导方法，其中将NL证明集成到Lean4代码中以训练数据集，利用LLMs的NL推理能力进行形式推理。TheoremLlama框架在MiniF2F-Valid和Test数据集上分别实现了36.48%和33.61%的累积准确率，超过了22.95%和25.41%的GPT-4基线。我们还公开了模型检查点和生成的数据集，并将很快公开所有代码。

训练一个通用的大型语言模型（LLM）成为Lean4专家，解决由于缺乏自然语言和形式语言定理证明数据而导致的性能不佳的问题。

提出了一个端到端的框架TheoremLlama，包括生成NL-FL对齐数据集的方法、LLM形式定理证明的训练方法和LLM Lean4证明撰写技巧。其中，NL-FL引导方法是一个关键创新，将NL证明集成到Lean4代码中进行训练数据集，充分利用LLM的NL推理能力进行形式推理。

使用提出的数据集生成方法，提供了一个NL-FL对齐和引导的数据集Open Bootstrapped Theorems（OBT）。框架在MiniF2F-Valid和Test数据集上分别实现了36.48%和33.61%的累积准确率，超过了GPT-4基线。研究还开源了模型检查点和生成的数据集，将很快公开所有代码。

最近的相关研究包括使用LLM进行代码生成的方法，以及使用机器学习进行定理证明的方法。