CombiBench

CombiBench是第一个专注于组合问题的基准测试，基于形式语言LEAN4。它是一个手动生成的基准测试，包含100个不同难度和知识水平的组合数学问题。旨在为评估自动定理证明系统的组合数学能力提供基准，以推动该领域的发展。对于需要先提供解决方案然后证明其正确性的问题，我们参考了PutnamBench的风格。CombiBench represents the first benchmark dedicated to combinatorial problems, based on the formal language LEAN4. It is a manually crafted benchmark encompassing 100 combinatorial mathematics problems of varying difficulty and knowledge levels. The dataset is designed to serve as a benchmark for evaluating the combinatorial capabilities of automated theorem-proving systems, thereby advancing the field. For problems that require the provision of a solution followed by its proof of correctness, we have referenced the style of PutnamBench.

原始信息汇总

CombiBench数据集概述

数据集简介

• 名称：CombiBench
• 类型：组合数学问题基准测试
• 基础语言：LEAN4形式化语言
• 规模：100个组合数学问题
• 特点：手工制作、难度和知识水平多样
• 参考风格：对于需要先提供解再证明正确性的问题，参考PutnamBench风格

数据来源与统计

来源	问题数量
Easy	10
Brualdis book	42
IMO	36
APMO	2
Balticway	1
EGMO	1
IMO-Shortlist	4
IZHO	2
BXMO	1
USAMO	1

应用场景

• 评估自动定理证明系统在组合数学方面的能力
• 推动组合数学领域的发展

使用要求

• Python版本：≥3.10
• Lean版本：≥4.15.0

安装方式

bash pip install -e .

或 bash uv venv .venv --prompt combibench source .venv/bin/activate uv sync

评估方法

1. 单阶段Fine-Eval： bash python evaluation/online_one_stage.py --config evaluation/config/template.json5

2. 两阶段Fine-Eval： bash python evaluation/online_two_stage.py --config evaluation/config/template.json5

贡献与许可

• 贡献：欢迎通过仓库提交问题报告
• 许可证：MIT License

搜集汇总

数据集介绍

构建方式

在组合数学领域的研究中，CombiBench作为首个基于LEAN4形式化语言的组合问题基准测试集，其构建过程体现了严谨的学术规范。研究团队采用多源数据融合策略，系统性地收集了国际数学奥林匹克竞赛（IMO）2000年以来的全部组合问题，并依据Brualdi教材的14个章节进行分层抽样，确保知识点的均衡覆盖。通过引入中学数学题库hackmath的初级题目及其他国际数学竞赛试题，构建了包含100道难度梯度分明的手工标注问题集，其中42题严格遵循教材知识体系分布，36题源自IMO真题，其余22题来自APMO、EGMO等权威赛事。

特点

该数据集最显著的特征在于其问题类型的多样性及评估维度的全面性。所有题目均采用LEAN4形式化语言表述，既包含需要先提出解再验证正确性的PutnamBench风格问题，也涵盖传统证明题和填空题。难度谱系覆盖从中学基础到国际顶级竞赛水平，其中10题为初中级难度，42题对应大学教材理论深度，48题选自各层次数学竞赛。数据集特别设计了兼容性评估框架，支持单阶段Fine-Eval和双阶段Fine-Eval两种评估模式，可灵活适应定理证明和填空补全两类任务需求。

使用方法

使用该数据集需配置LEAN≥4.15.0和Python≥3.10环境，通过kimina-lean-server建立定理证明服务器。研究人员需在配置文件中指定数据集路径、LEAN服务器参数及大语言模型API密钥（支持OpenAI、Antropic等主流接口）。评估阶段提供两种运行模式：online_one_stage.py执行单阶段评估，适用于直接证明场景；online_two_stage.py实现解耦式评估，专门处理需要分步求解的复合型问题。所有评估脚本均接受JSON5格式的配置文件，可自定义生成参数、提示模板和并行计算设置，确保评估过程的可重复性和可扩展性。

背景与挑战

背景概述

CombiBench作为首个专注于组合数学问题的基准测试数据集，由AI-MO团队基于形式化语言LEAN4构建，标志着自动化定理证明领域的重要进展。该数据集于2023年发布，汇集了从国际数学奥林匹克竞赛（IMO）、布鲁阿尔迪组合数学教材等权威来源精选的100道具有不同难度和知识层次的组合数学问题。其核心研究目标在于系统评估人工智能系统在组合数学领域的推理能力，尤其针对需要先提供解决方案再验证正确性的复杂问题类型，数据集设计参考了PutnamBench的范式。通过构建涵盖初中生竞赛题到国际顶级数学竞赛题的完整谱系，CombiBench为衡量AI系统的组合推理能力提供了标准化测试平台，对推动形式化数学和自动推理研究具有显著的学术价值。

当前挑战

在解决领域问题方面，CombiBench面临组合数学特有的高阶抽象推理挑战，包括复杂计数原理的应用、离散结构性质的证明以及非确定性解题策略的建模。数据构建过程中需克服多维度难题：源问题需从42个教材章节和12类国际竞赛中保持知识分布均衡；LEAN4形式化转换要求精确保持原始问题的数学语义；评估体系需兼容填空式和证明式两类解题范式。此外，自动证明系统在处理图论依赖型问题时存在形式化表达的固有局限，导致某道IMO图形问题不得不被排除，反映出组合数学问题形式化过程中的技术瓶颈。

常用场景

经典使用场景

在组合数学领域，CombiBench数据集为自动化定理证明系统提供了一个标准化的评估平台。该数据集精心挑选了100道难度和知识层次各异的组合数学问题，涵盖了从中学级别到国际数学奥林匹克竞赛（IMO）的高阶题目。研究人员可利用该数据集测试算法在解决组合问题时的准确性和效率，特别是在形式化语言LEAN4环境下验证数学定理的能力。

实际应用

该数据集的实际价值体现在智能教育系统和竞赛训练平台的开发中。基于CombiBench构建的自动解题系统可为数学学习者提供即时反馈，而竞赛组织者则能利用其评估题目难度分布。在工业领域，组合优化算法（如排班调度、路径规划）的开发者可通过该数据集验证模型在抽象数学问题上的泛化能力，进而提升实际业务场景中的决策质量。

衍生相关工作

受CombiBench启发，研究者已开展多项延伸工作。例如结合大语言模型的定理证明系统Kimina-Lean-Server实现了与该数据集的深度集成；部分团队借鉴其分层设计理念，开发了针对数论或几何领域的专用评测集。数据集采用的PutnamBench风格也促进了'生成-验证'双阶段评估范式在数学AI领域的普及，相关成果见于ICLR等顶会论文。