Lean Workbook: A large-scale Lean problem set formalized from natural language math problems

大型语言模型已经在各种自然语言处理任务中展现出了令人印象深刻的能力，特别是在解决数学问题方面。然而，大型语言模型在使用像 Lean 这样的形式语言进行数学定理证明方面表现不佳。这个领域面临的一个重要挑战是这些形式语言中可用的训练数据很少。为了解决这个问题，我们提出了一种新颖的流程，通过迭代生成和过滤合成数据来将自然语言数学问题转化为 Lean 4 语句，反之亦然。我们的结果表明，合成数据流程可以提供有用的训练数据，并提高大型语言模型在翻译和理解复杂的数学问题和证明方面的性能。我们最终的数据集包含约57K个正式-非正式问题对，以及从数学竞赛论坛搜索到的证明和21个新的IMO问题。我们在https://github.com/InternLM/InternLM-Math上开源了我们的代码，以及在https://huggingface.co/datasets/InternLM/Lean-Workbook上开源了我们的数据。

如何使用生成的数据来提高大型语言模型在形式语言中的数学定理证明任务的表现？

提出一种迭代生成和过滤合成数据的流程，将自然语言数学问题转化为Lean 4语句，并反之亦然，从而提供有用的训练数据。

论文提供了一个包含57K个正式-非正式问题对的数据集，以及开源代码和数据。实验结果表明，使用合成数据可以提高大型语言模型在理解复杂数学问题和证明方面的表现。

最近的相关研究包括基于自然语言推理的定理证明和形式语言中的数学问题翻译。