LeanComb

LeanComb是一个基于Lean的组合恒等式定理证明基准数据集，由华东师范大学、河南大学和中国科学院的研究人员构建。该数据集从经典组合数学文献中选取组合恒等式，手工转化为Lean中的形式化定义和定理，包括它们的陈述和证明。数据集分为训练集和测试集，涵盖了一系列组合技巧和数学领域，旨在为自动化定理证明工具的性能评估提供严格的验证和形式化集合。LeanComb is a Lean-based benchmark dataset for combinatorial identity theorem proving, constructed by researchers from East China Normal University, Henan University, and the Chinese Academy of Sciences. This dataset selects combinatorial identities from classic combinatorial mathematics literature, and manually formalizes them into definitions and theorems in Lean, including their statements and proofs. The dataset is divided into training and test sets, covering a range of combinatorial techniques and mathematical domains. It aims to provide a rigorous verification and formalized collection for performance evaluation of automated theorem proving tools.

搜集汇总

数据集介绍

构建方式

为了解决组合数学中自动定理证明（ATP）面临的挑战，研究团队构建了LeanComb数据集。该数据集基于Lean证明辅助工具，包含418个组合恒等式和209个引理作为训练集，以及100个组合恒等式作为测试集。数据集的构建过程涉及手动将非正式的数学陈述转换为形式化的定义和定理，并包括它们的陈述和证明。为了增强数据集，研究团队开发了自动化定理生成器ATG4CI，该生成器结合了自改进的大型语言模型和基于蒙特卡洛树搜索的强化学习策略，以预测和生成新的组合恒等式和它们的证明。

特点

LeanComb数据集的特点在于其专注于组合恒等式，为评估ATP工具的性能提供了严格验证和形式化的集合。数据集涵盖了广泛的组合数学主题，包括经典和现代恒等式，并分类为8个类别，如组合数学、微积分、概率等。此外，ATG4CI生成的增强数据集LeanComb-Enhanced包含了260,466个组合恒等式定理，每个定理都带有完整的Lean形式化证明。数据集的另一个特点是其复杂性和多样性，证明了不同长度的证明步骤和使用的战术类型。

使用方法

使用LeanComb数据集的方法包括将其作为基准来评估自动定理证明工具的性能，以及作为训练数据来增强大型语言模型在自动定理证明方面的能力。通过在LeanComb和LeanComb-Enhanced数据集上进行微调，研究团队发现模型在自动证明组合恒等式方面的成功率显著提高。实验结果表明，与仅在Mathlib上训练的模型相比，使用LeanComb和LeanComb-Enhanced数据集进行微调的模型，其成功率提高了5%到17%。此外，评估还显示，在miniF2F数据集上，使用这些数据集进行微调的模型也取得了更好的性能。

背景与挑战

背景概述

LeanComb数据集的创建旨在解决大语言模型在复杂数学领域，尤其是组合数学中，自动定理证明能力受限的问题。由华东师范大学、河南大学和中国科学院的研究人员于2025年构建，LeanComb是首个针对组合恒等式的形式化定理证明基准。该数据集的构建基于Lean 4证明助手，包含了418个恒等式和209个引理的训练集以及100个恒等式的测试集。LeanComb的创建填补了数学领域中高质量训练数据的稀缺，为自动定理证明提供了宝贵的资源。该数据集的发布对组合数学和相关领域的研究产生了深远的影响，为后续的研究和模型训练提供了基础。

当前挑战

LeanComb数据集面临的挑战主要来自于组合数学的复杂性以及自动定理证明技术的局限性。首先，组合数学的复杂性使得自动定理证明成为一项艰巨的任务，尤其是在构建过程中，需要将非正式的数学陈述转换为形式化的定义和定理。其次，现有的自动定理生成方法大多依赖于从完整的定理中提取子定理或合成新的定理，这可能导致数据集的覆盖范围有限，且在不同数学领域中的分布不均。此外，自动定理证明的成功率仍然较低，尤其是在处理复杂的组合恒等式时。因此，提高自动定理证明的成功率和效率，以及生成更多高质量的定理，仍然是该领域面临的挑战。

常用场景

经典使用场景

LeanComb 数据集主要应用于自动化定理证明（ATP）领域，特别是组合恒等式的证明。该数据集包含大量的组合恒等式及其形式化证明，为训练和评估 ATP 工具提供了宝贵的数据资源。通过 LeanComb，研究人员可以测试 ATP 工具在处理组合恒等式问题时的性能和效率，从而推动 ATP 技术的发展。

衍生相关工作

LeanComb 数据集的构建和发布，为自动化定理证明（ATP）领域的研究提供了重要的基础。基于 LeanComb 数据集，研究人员可以进行更深入的研究，例如探索更有效的 ATP 算法、开发更强大的 ATP 工具等。此外，LeanComb 数据集还可以促进与其他相关领域的研究合作，例如人工智能、计算机科学等，从而推动整个数学和计算机科学领域的发展。

数据集最近研究

最新研究方向

近年来，随着人工智能的快速发展，大型语言模型（LLMs）在形式化定理证明方面取得了显著进展。然而，由于高质量训练数据的稀缺，它们在处理复杂数学领域的能力仍然受限。组合数学作为数学的基础，为分析和解决优化问题提供了重要的工具。然而，其固有的复杂性使得自动定理证明（ATP）在组合恒等式方面面临巨大挑战。为了解决这个问题，我们手动构建了LeanComb，一个基于Lean的组合恒等式基准，这是我们所知的第一个为组合恒等式构建的形式化定理证明基准。我们还开发了一个自动定理生成器，ATG4CI，它结合了自改进大型语言模型建议的候选策略和强化学习树搜索方法进行策略预测。通过利用ATG4CI，我们生成了一个包含26万个组合恒等式定理的LeanComb-Enhanced数据集，每个定理都有完整的Lean形式证明。实验评估表明，在这个数据集上训练的模型可以生成更有效的策略，从而提高组合恒等式自动定理证明的成功率。

相关研究论文

• A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation

  华东师范大学, 河南大学, 中国科学院 · 2025年