CombiBench

CombiBench是一个包含100个组合数学问题的综合基准测试集，每个问题都使用Lean 4进行了形式化，并配有相应的非正式描述。问题集涵盖了从初中到IMO和大学水平的各种难度，涵盖了十多个组合数学主题。CombiBench旨在解决自动定理证明领域中组合数学缺乏适当基准和定理库的问题。该数据集包含了自2000年以来所有IMO组合数学问题（除了2004年的第3题，因为其陈述包含图像）。此外，我们提供了一个全面的标准评估框架，称为Fine-Eval，用于形式数学的评估。它不仅适用于基于证明的问题，而且首次支持对填空题的评估。使用Fine-Eval作为评估方法，并以Kimina Lean Server为后端，我们在CombiBench上对几个LLM进行了基准测试，并观察到它们在形式化解决组合数学问题方面的能力仍然有限。在所有测试的模型中（没有一个是为这个特定任务训练的），Kimina-Prover取得了最佳结果，在“有解决方案”和“无解决方案”的情况下都解决了7个问题（共100个）。我们开源了基准数据集以及所提出的评估方法的代码。CombiBench is a comprehensive benchmark dataset consisting of 100 combinatorial mathematics problems. Each problem has been formalized using Lean 4, paired with corresponding informal descriptions. The problem set spans a wide range of difficulty levels, from middle school mathematics, through International Mathematical Olympiad (IMO) and up to university-level content, covering more than ten combinatorial mathematics topics. CombiBench is designed to address the gap in appropriate benchmarks and theorem libraries for combinatorial mathematics within the field of automated theorem proving. This dataset includes all IMO combinatorial problems since 2000, with the exception of Problem 3 from the 2004 IMO, as its problem statement contains an image. Additionally, we present a comprehensive standard evaluation framework named Fine-Eval for formal mathematics. This framework is not only applicable to proof-based problems, but also supports the evaluation of fill-in-the-blank questions for the first time. Using Fine-Eval as the evaluation methodology and Kimina Lean Server as the backend, we benchmarked several large language models (LLMs) on CombiBench, and observed that their capabilities in formally solving combinatorial mathematics problems remain limited. Among all tested models—none of which were trained specifically for this task—Kimina-Prover achieved the best performance, solving 7 out of 100 problems across both the "with solution" and "without solution" evaluation settings. We have open-sourced both the benchmark dataset and the code for the proposed evaluation framework.

搜集汇总

数据集介绍

构建方式

CombiBench数据集的构建过程体现了严谨的学术规范与系统化的设计理念。研究团队基于Brualdi经典组合数学教材的体系框架，采用分层抽样策略从四大来源收集问题：10道基础题源自HackMath平台，42道习题选自教材各章节，36道来自2000年后的IMO试题，以及12道其他数学竞赛题。特别值得注意的是，团队对IMO试题进行了严格筛选，排除了包含图像元素的题目，并通过五名具有Lean语言经验的博士生组成的专业团队，采用Lean 4进行逐题形式化验证，单题平均耗时30分钟至8小时不等。

特点

该数据集展现出三个显著特征：首先，其100道题目全面覆盖组合数学十大核心主题，难度梯度从中学生延伸至IMO金牌水平，形成完整的评估谱系。其次，创新性地采用双模态设计，每道题目均包含自然语言描述与Lean 4形式化语句的精确对应，为神经符号推理研究提供理想实验平台。尤为独特的是，45%的题目采用"填空-验证"双阶段结构，要求模型先构造解决方案再完成形式化证明，这种设计精准模拟了人类解决组合数学问题的认知流程。

使用方法

数据集配套的FINE-EVAL评估框架开创性地支持双模态验证机制。对于填空类题目，系统首先检查模型生成的解决方案能否通过Lean 4编译，随后在第二阶段验证其与标准答案的数学等价性。评估过程严格限制作弊行为，包括禁止注释绕过、禁止新增公理等约束条件。研究团队同时提供简化版单阶段评估流程，通过rfl策略直接验证定义等价性。用户可通过标准化接口连接Lean服务器与LLM，系统将自动生成包含问题陈述、解决方案和验证结果的详细评估报告。

背景与挑战

背景概述

CombiBench是由Moonshot AI等机构的研究人员于2025年提出的一个专注于组合数学问题的形式化基准测试数据集。该数据集旨在填补组合数学领域缺乏高质量基准的空白，包含100个从初中到国际数学奥林匹克（IMO）及大学水平的组合数学问题，涵盖排列组合、鸽巢原理、图论等十余个主题。CombiBench的创建受到神经符号方法在数学定理证明中应用的启发，特别针对组合数学这一当前自动定理证明领域中最具挑战性的分支。数据集所有问题均采用Lean 4语言进行形式化表述，并配套开发了创新的FINE-EVAL评估框架，首次实现了对填空题和证明题的统一评估标准。

当前挑战

CombiBench面临的挑战主要体现在两个方面：领域问题层面，组合数学问题的非结构化特性导致从自然语言到形式化表述的转换存在显著鸿沟，需要频繁定义问题特定的概念和引理；构建过程层面，IMO级别问题的形式化平均耗时超过3小时，最复杂的问题需要67行形式化代码，反映出Mathlib库中组合数学定理的匮乏。评估方法上，传统证明验证框架无法处理填空题的答案生成与验证，促使研究者开发两阶段的FINE-EVAL系统。实验数据显示，即使是72B参数的Kimina-Prover模型也仅能解决7%的问题，凸显出组合数学形式化推理这一核心挑战的难度。

常用场景

经典使用场景

CombiBench数据集专为评估大型语言模型在组合数学竞赛问题中的能力而设计，覆盖了从中学到国际数学奥林匹克（IMO）及大学水平的广泛难度范围。该数据集通过Lean 4语言形式化，为研究者提供了一个标准化的测试平台，用于验证模型在组合数学领域的推理和证明能力。

衍生相关工作

CombiBench的推出促进了相关研究工具和方法的发展，如Fine-Eval评估框架，该框架首次支持对填空问题的评估。此外，该数据集还启发了如Kimina-Prover等新型定理证明器的开发，这些工具在组合数学问题的形式化证明中表现出色，进一步推动了自动定理证明技术的进步。

数据集最近研究

最新研究方向

近年来，组合数学与人工智能的交叉研究逐渐成为热点，特别是在自动化定理证明领域。CombiBench数据集的推出填补了组合数学领域缺乏高质量基准测试的空白，为评估大型语言模型（LLMs）在组合数学问题上的能力提供了标准化工具。该数据集不仅涵盖了从中学到国际数学奥林匹克（IMO）及大学水平的多样化问题，还首次引入了针对填空题的评估框架Fine-Eval，显著提升了模型在形式化数学推理中的全面性。CombiBench的发布不仅推动了组合数学在形式化验证中的研究，还为解决当前模型在组合数学领域表现不佳的问题提供了新的研究方向。

相关研究论文

• CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

  中国科学院数学与系统科学研究院, 中山大学, 剑桥大学, 华东师范大学, 伦敦帝国学院, 斯德哥尔摩大学, Numina, 月之船人工智能公司 · 2025年