ComBench：一个用于奥林匹克级组合数学严谨证明推理与构造实现的基准

# ComBench：奥林匹克级组合数学中严格证明推理与构造实现的基准测试

来源：https://arxiv.org/html/2606.10479

Shunkai Zhang²,¹,\*Haoran Zhang³,¹,\*Yun Luo¹,†\daggerQianjia Cheng¹ Haodi Lei¹Yizhuo Li¹Runzhe Zhan¹Zhilin Wang¹Bangjie Xu⁴ Yucheng Su⁴Xinmiao Han⁴Xiaoye Qu¹Dongrui Liu¹Zhouchen Lin² Yu Qiao¹Ning Ding⁴, ¹Yafu Li¹, ⁵,†\daggerYu Cheng¹,†\dagger

¹上海人工智能实验室²北京大学³上海交通大学 ⁴清华大学⁵香港中文大学

\*同等贡献。†\dagger通讯作者

###### 摘要

组合数学是奥林匹克级数学问题求解的核心，需要深入的离散推理、创造性构造和严谨的结构洞察。近期证据表明，即使当前最强的前沿模型在奥林匹克组合数学上仍表现不均衡，暴露出创造性数学推理方面的差距。我们提出ComBench，一个用于评估大语言模型组合推理能力的奥林匹克级组合数学基准。ComBench包含100道人工标注的竞赛级问题，围绕两个互补设置组织：分析型问题，主要需要严格的数学论证；构造型问题，除了正确性证明外还需要明确的构造。评估协议结合了基于评分标准的证明评分与确定性构造验证，揭示了证明质量与构造有效性可能不一致的情况。对前沿开源与闭源模型的实验表明，ComBench远未饱和：最强模型在总分平均上达到65.4%，在总分Best@4上达到75.3%。我们进一步发现，**严格证明推理**与**构造实现**是两种不同的能力：Kimi-K2.6在分析型证明评分上落后于GPT-5.5，但在构造型Best@4上超越它；而**存在性与构造**问题在代表性前沿模型中始终是最难的。

## 1 引言

大语言模型（LLM）近期在数学推理方面取得了快速进展，前沿系统在多个竞赛级基准上接近精英人类水平 (Luong et al., 2025; An et al., 2025)。然而，它们在与奥林匹克级组合数学相关的领域表现仍不均衡，该领域不仅需要长程逻辑推理，还需要离散结构洞察和创造性构造。例如，Gemini Deep Think和DeepSeekMath-V2 (Shao et al., 2025) 在IMO 2025中获得了金牌级表现，解决了六个问题中的五个，但在最难的组合题上失败 (Luong et al., 2025)。这表明，当前模型可能仍缺乏构造性和创造性数学推理的关键成分。

![图1](https://arxiv.org/html/2606.10479#S1.F1)
图1：IMO 2025 P6，一个具有挑战性的组合题，所有评估模型均未解决。图中显示了原题陈述、参考答案以及参考构造的示意图。

现有的奥林匹克级基准 (Luong et al., 2025; An et al., 2025) 为研究此类进展提供了重要工具，但它们并未单独隔离组合数学的构造性。基于答案的基准可以规模化评估，但很少揭示模型是否产生了有效的数学论证。IMO-Bench风格的证明评估通过评判证明质量和部分进展来解决这一局限，非常适合测量**严格证明推理**：即根据奥林匹克评分标准编写完整解决方案的能力。然而，许多组合问题还需要另一种能力。模型不仅需要论证对象存在，还必须明确实现它。我们将这第二种能力称为**构造实现**：即将存在性或构造性论证转化为完整、明确且可机器检查的离散证据。这些证据可以是染色、拼贴、图、族集、策略、矩阵、排列或反例。这些对象的自然语言描述往往难以可靠评估，因为其有效性依赖于整个对象的全局约束。例如，在IMO 2025问题6（图1）中，完整的解决方案不仅需要证明最优值，还需要展示一个达到该值的瓷砖分布。

在本研究中，我们提出**ComBench**，一个包含100道奥林匹克级组合问题的基准，旨在同时评估**严格证明推理**和**构造实现**。ComBench通过可执行的构造验证扩展了IMO-Bench风格的证明评估。它包含两种类型记录。**分析型**记录使用基于评分标准的证明评分来评估原始数学解答。**构造型**记录保留原证明任务，但增加了一个构造任务，模型必须以规定表示输出具体证据，并由特定问题的验证器确定性检查该证据。区别在于评估目标。ComBench从主要的奥林匹克型竞赛中精选问题，包括IMO、USAMO、选拔测试、地区奥林匹克和IMO Shortlist问题。每个问题都按照0/1/6/7分制评分指南进行标注。构造型记录还配备了构造说明、参考证据、验证器计划和确定性Python验证器。多位数学专家提供了严格且经过仔细验证的标注，涉及评分指南、组合构造说明和确定性验证器。这种设计使我们能够分别评估证明质量和构造有效性，然后通过验证器门控评分（当需要构造时）将两者结合。

我们评估了一系列前沿闭源和开源LLM在ComBench上的表现，几个发现说明了该基准的诊断价值。总体而言，奥林匹克级组合数学远未饱和：最强模型GPT-5.5在我们基于评分标准和验证器门控的评估下，总分平均达到65.4%，总分Best@4达到75.3%。模型行为在两个目标能力上也差异显著。Kimi-K2.6在分析型证明评分上明显弱于GPT-5.5，但在构造型Best@4上取得最佳表现，超越了GPT-5.5。在类别层面，**存在性与构造**问题对于代表性前沿模型始终是最难的，而**计数**和**图论**问题相对容易。这些发现表明，**严格证明推理**和**构造实现**是相关但不同的能力，在奥林匹克级组合数学上取得进展需要证明层面的严格性和显式证据实现。

#### 贡献。本工作做出以下贡献：

- • 我们提出**ComBench**，一个包含100道奥林匹克级组合问题的基准，用于**严格证明推理**和**构造实现**。
- • 我们开发了一个评估协议，结合了IMO-Bench风格的基于评分标准的证明评分与显式构造证据的确定性验证。
- • 我们提供了前沿闭源和开源LLM在ComBench上的系统实证评估，揭示了证明层面推理与显式构造能力之间的明显分离，以及奥林匹克级组合数学中特定类别的弱点。

## 2 相关工作

#### 数学推理评估。数学基准已从GSM8K和MATH (Cobbe et al., 2021; Hendrycks et al., 2021) 发展到奥林匹克级和前沿级评估 (He et al., 2024; Balunović et al., 2026; Glazer et al., 2025; Phan et al., 2025; Wang et al., 2026)，主要由三种协议主导：如AMO-Bench和OlymMATH中的纯答案匹配 (An et al., 2025; Sun et al., 2026)；如IMO-Bench和ProofGrader中的基于评分标准的0–7分证明评分 (Luong et al., 2025; Ma et al., 2026)；以及基于Lean的形式化证明基准，如CombiBench (Liu et al., 2025)，它在Lean 4中形式化组合问题，评估定理证明和填空形式化解答。然而，奥林匹克组合数学中，解答依赖于全局约束的证据（如染色、族集或反例），这些协议仍不充分：答案匹配无法揭露无效证据，证明评分器只评论文本而不检查构造本身。作为Lean形式化路线的补充，ComBench保留了自然语言解答，但增加了显式证据的可执行验证。

#### 用于奥林匹克级推理的LLM。在早期的神经符号和形式证明系统达到IMO奖牌级表现之后 (Chervonyi et al., 2025; Hubert et al., 2025)，大规模强化学习后训练，并通过关于规模、训练策略和工具集成推理的方案进一步优化，显著提升了通用LLM的数学能力 (Guo et al., 2025; Team et al., 2026; Yang et al., 2025; Cheng et al., 2026; Zhang et al., 2026)。沿着这一轨迹，近期的思考系统已在竞赛条件下达到IMO金牌级的自然语言表现 (Luong et al., 2025; Huang and Yang, 2025; Chen et al., 2025; Yang et al., 2026; Li et al., 2026)，但最难的组合问题仍未解决：没有模型在IMO 2025 P6上获得分数。ComBench正是为了解耦并精确测量这一差距而设计。

## 3 ComBench数据集

### 3.1 概述

![图2](https://arxiv.org/html/2606.10479#S3.F2)
图2：ComBench类别分布。

我们提出ComBench，一个包含100道奥林匹克级组合问题的基准，旨在评估超越最终答案正确性的数学推理。它在50道分析型问题和50道构造型问题之间保持平衡。该基准涵盖2000年至2025年的15个竞赛来源，包括国际数学奥林匹克（IMO）、美国数学奥林匹克（USAMO）、选拔测试、地区奥林匹克和IMO Shortlist问题。这种来源多样性将经典国际问题与国家及选拔测试问题相结合，扩大了构造性、极值、图论、计数和策略驱动型组合学的覆盖范围。图2可视化了这种构成：100道问题在分析型和构造型记录中均分，并分为五个主要组合类别。两种问题类型对应本文的两个目标能力：分析型记录评估**严格证明推理**，而构造型记录额外通过显式、可机械检查的证据评估**构造实现**。来源、年份、类别和问题类型的聚合统计见附录A。

![图3](https://arxiv.org/html/2606.10479#S3.F3)
图3：ComBench的构造型数据构建流程。

### 3.2 记录设计与问题分类

我们选择以离散结构、极值推理、计数、图论论证、策略或显式构造为核心的奥林匹克级组合问题。所选问题包括标准的奥林匹克风格证明任务，以及其自然解答需要显式证据（如染色、排列、图、表格、集合系统、拼贴、策略或反例）的任务。为了更好地针对组合推理，我们排除了核心困难非组合的问题，即使它们涉及少量计数或离散元素。

每个ComBench记录包含基于评分标准的证明评估所需信息：原始问题陈述、来源元数据、参考答案、参考解答（如有）、主要问题类别、问题类型以及特定问题的评分指南。评分指南遵循0/1/6/7分制，并规定了无进展、最小进展、接近完成和完整解答的标准。构造型记录包含额外字段，定义了可执行的构造任务：特定问题的构造说明、参考证据、非正式验证器计划以及确定性Python验证器代码。附录C.2给出了一个完整的构造型记录格式化示例。对于每个构造型问题，**证据**是构造说明所要求的具体离散对象。它不是证明草图或自然语言说明；而是其表示和数学有效性可由验证器检查的对象。这种设计使构造任务明确，而不是依赖可能难以解析或再现的自由形式对象描述。代表性证据格式见附录C.3。

ComBench使用五个主要问题类别：极值问题、存在性与构造、操作与策略、图论和计数。这些类别提供了一种稳定的方式来分析重复出现的推理模式，而非互斥的数学子领域。类别定义及类别与类型的交叉分布见附录A。

### 3.3 标注流程

分析型和构造型记录都需要标注。对于分析型记录，主要标注是用于基于评分标准的证明评估的特定问题0/1/6/7分制评分指南。构造型记录使用相同的证明评分标注，但额外需要构造说明、参考证据、非正式验证器计划、确定性验证器代码和语义审计。由于评分构建是两种记录类型共有的，下面我们专注于完整的构造型流程，它通过证据规范和可执行验证扩展了证明评分标注，如图3所示。

#### 阶段1：规范和评分构建。输入包括原始问题、参考答案和人类解答。对于构造型问题，还需要指定所需的证据类型（例如，一个0-1矩阵、一个排列、一个图邻接表等）和验证逻辑。然后，专家编写评分指南，定义不同分数水平的证明质量。