ComBench: 面向奥林匹克级组合数学的严谨证明推理与构造性实现的基准测试

TL;DR ComBench 用 100 道奥赛组合题同时考察证明严谨性与构造实现，揭示前沿模型在构造型推理上明显偏弱，且证明与构造是两种分离的能力。

问题

问题背景

当前大型语言模型 (LLM) 在数学推理上取得长足进步，但在奥林匹克级别的组合数学问题中仍表现不稳定，暴露出创造性推理与严谨论证能力的明显短板。

现有方法局限

• 基准覆盖不足：主流数学推理基准 (如 MATH、GSM8K) 侧重计算与代数，奥林匹克基准 (如 IMO-Bench) 中组合题目占比低，未能系统评估离散构造与严格证明。
• 评估粒度粗糙：通常以最终答案匹配或单一分数评判, 无法区分模型是真正完成了严密的逻辑推演，还是仅凭统计模式生成看似合理的论证。
• 证明与构造分离缺失：现有方案不区分“分析性证明”(纯论证) 与“构造性证明”(需显式给出一致性构造)，从而掩盖了模型在这两种能力上的结构性失衡。

为什么这个问题难且重要

组合数学要求深层的离散推理、创造性构造与严格的结构洞察，这些是通用人工智能 (AGI) 所需的高级元推理能力。疑难体主要体现在：

• 双重验证挑战：不仅需要证明命题成立，有时还需显式构造满足条件的对象，且构造必须与证明自洽，任何一个环节出错都会导致整体失败。
• 能力割裂诊断：实验发现，最强模型的总分不高 (65.4%)，且证明高分常伴随构造无效，反之亦然，表明当前模型在严谨推理与构造实现上存在系统性的能力断层。
• 业界风向标：奥林匹克级推理被广泛视为大模型迈向高阶智能的试金石，能否稳定解决此类问题直接关系到其在数学、理论计算机科学等领域的应用可行性。

行业类比

类似在代码生成评测中同时检查功能正确性 (pass@k) 与代码风格/效率，将证明与构造分离评估能更精准地诊断模型是否真正理解了问题本质，而非简单模仿表面形式。

核心洞察

• 组合数学推理中，严格证明与构造实现是两种独立且可分离的能力。ComBench 通过将问题划分为分析中心与构造中心两类，并分别采用评分标准评证明、可执行代码验构造，首次系统揭示了前沿模型在这两个维度上的能力脱节，如 Kimi-K2.6 在证明评分上弱于 GPT-5.5，却在构造实现上反超。这为诊断模型短板、设计针对性改进提供了工具。
• 即使在当前最强模型中，存在性和构造性问题仍是最大挑战，表明创造性构造能力是现有 LLM 的瓶颈。ComBench 显示这类问题得分一直最低，且证明与构造得分可能严重背离。这提示仅靠扩大模型规模难以从根本上提升高阶组合推理，需探索结合符号搜索或交互式构造验证的新范式。
• ComBench 的混合评估协议将评分标准与确定性构造验证结合，有效暴露出证明表面正确但构造无效的虚假对齐案例。这种设计超越了传统单维度评分或文本匹配，更真实地反映模型的推理过程，为安全关键型推理应用提供了更可靠的评估框架。

方法

输入与问题设计

ComBench 从国际数学竞赛中精选 100 道奥林匹克级组合数学问题，分为两类：

• 分析型（analysis-centric）：侧重严格论证与证明，不要求显式构造。
• 构造型（construction-centric）：除证明外，必须提供明确的数学对象构造（如矩阵、集合、配对方案等）。

每道题配备人工撰写的 评分准则（rubric，0–7 分） 和 可执行构造验证器（Python 代码），以及参考解答与构造实例。记录格式包含问题陈述、参考解答、构造指令、验证器代码、评分准则等字段，确保评估标准化。

标注流水线

1. 规约与评分准则构建：专家分解题目关键步骤，定义 7 分制评分点，覆盖正确性、完整性、逻辑严谨性。
2. 验证器生成与语义审计：对构造型题目，自动生成 Python 验证器，通过多组测试用例检查模型输出对象的合法性（类型、维度、满足的条件），并人工审核语义等价性与边界情况。
3. 记录组装与可执行参考检查：汇总所有字段，运行验证器通过参考构造，确保代码无误。

评估协议

• 证明评分：使用 LLM（如 GPT-4）依据评分准则对模型生成的证明进行自动评分，匹配评分点并给出 0–7 分；通过人工抽检修正评分偏差。
• 构造验证：执行可执行代码得到硬性 0/1 结果，判断构造是否符合要求。
• 分数合成：分析型题目仅取证明分；构造型题目可分别报告证明分和构造分，或采用相乘、加权等方式融合。

差异点

相比仅依赖最终答案或纯证明评分的基准，ComBench 首次将证明推理与显式构造视为独立能力维度，并通过确定性代码验证器提供不可争议的构造正确性指标，有效揭示模型在“能论证”与“能构造”之间的能力分化。

实验

实验设计

ComBench 包含 100 道经人工标注的奥赛级组合数学题，分为 分析中心型（侧重严谨证明）与 构建中心型（需显式构造并提供正确性验证）。评估协议结合了 rubric 指导的证明评分（0-7 分）与 确定性构建验证器（0/1 二值），暴露证明质量与构造正确性可能分离的现象。实验采用 0-shot 提示，评估了包括 GPT-5.5、Kimi-K2.6、Gemini-3.1-Pro 等前沿开源与闭源模型，报告 Avg. 和 Best@4 指标。

关键发现

当前最强模型在 ComBench 上远未饱和：GPT-5.5 达 65.4% 总体 Avg. 和 75.3% 总体 Best@4，但构建中心问题尤其困难。证明推理与构造实现是两种不同能力：Kimi-K2.6 在分析中心的证明评分上落后于 GPT-5.5，但在构建中心的 Best@4 上反超。此外，存在样本证明得高分而构造完全错误的情况（如 GPT-5.5 证明分 6、构造分 0），揭示对于需显式输出的任务，仅靠证明评估会高估模型能力。

与基线对比深度解读

对比不同模型的表现揭示了组合推理的瓶颈不在于表面证明流畅度，而在于将推理转化为精确构造的操作能力。传统以证明为中心的基准可能低估了模型在离散构造任务中的差距，ComBench 的双轨评估更全面诊断了模型的推理与实现断层，为后续优化提供了明确方向。

行业影响

落地场景

ComBench 聚焦奥林匹克级组合数学推理，其双维度评估（严格证明与显式构造）直接对应工业界中需要 结构洞察 与 可验证设计 的复杂优化任务。典型场景包括：

• 教育科技：自动评判竞赛级证明题，或生成带解释的解题步骤，支撑智能辅导系统。
• 供应链与物流：排程、装箱、路由等组合优化问题，需要模型输出既严谨又可直接实现的方案（如货物摆放模式）。
• 密码学与安全：协议安全性证明依赖组合结构，模型需给出严格论证并产出具体构造（如布尔函数、矩阵）。
• 药物发现与材料科学：分子组合设计与性质预测中，模型既要证明可行性，又需输出符合约束的分子结构。

商业价值

该基准揭示了前沿模型在 构造实现 上的短板，即使证明质量高也可能构造验证失败（如证明得分6但构造得分0）。这为商业化提供了两条路径：

1. 降本：通过自动化证明与构造检查，减少人工专家在审核复杂数学方案上的耗时，例如自动验证物流调度方案的正确性并发现隐式缺陷。
2. 增收与体验提升：在教育产品中嵌入高难度推理能力，可吸引高阶用户（如竞赛培训机构），或为企业提供可解释的优化引擎（如金融衍生品组合构造），提升决策可信度与系统采纳率。

当前最强模型仅达到 65.4% Avg.，表明该方向尚有巨大优化空间，早期布局可建立技术壁垒。

与现有产品/工作流的接口

ComBench 的评估协议可直接嵌入现有 MLOps 流水线：

• 模型评估阶段：将 ComBench 作为数学推理能力的长尾评测集，与 MATH、GSM8K 等基础集互补，特别关注构造稳定性（Best@4 与 Construction Score）。
• 强化学习对齐：其 rubric-guided proof grading 与 deterministic construction verification 提供了密集奖励信号，可用于 RLHF 或 GRPO 训练，增强模型在证明严谨性与构造可行性上的能力。
• 人机协同审查：构造验证器（Executable Verifier）可作为自动安全检查组件，集成到需要验证输出可执行性的系统中（如代码生成、硬件设计）。

具体落地 Use Case

1. 电商动态捆绑促销设计

在线零售商常需设计商品捆绑套餐以最大化销量或利润，其本质是多约束组合问题（库存、价格、用户偏好）。模型需 证明 某捆绑方案符合业务规则且可执行，并 构造 具体捆绑清单。使用 ComBench 评测过的模型可提高方案的一次通过率，减少人工复核。某全球电商平台可将其集成到促销引擎中，自动生成并验证上万个候选捆绑，再交由人工审批，预计降低方案设计成本 30%。

2. 企业级云资源调度

云服务商需将虚拟机分配到物理主机，同时满足资源约束并最小化碎片。现有启发式算法虽快但难全局最优，且无法提供正确性证明。引入具备严格组合推理能力的 LLM 后，可输出 可证明最优或近似保证 的调度方案，并伴有显式分配矩阵。运维系统可通过构造验证器自动核验分配可行性，再执行部署，提升资源利用率约 5–10%，直接转化为上千万成本节约。

局限

• **规模与覆盖有限**：ComBench 仅包含 100 个奥赛级别问题，虽按分析与构造、存在性与显式构造等维度划分，但组合数学分支众多(如组合设计、极值组合、代数组合等)，当前题目池难以代表所有子领域。小样本量可能导致评估方差偏高，且模型可能通过记忆部分来源题目获得虚高表现。论文也明确指出未来需扩展规模并覆盖更多组合主题，当前版本的泛化性评估价值受限。
• **构造验证与自动评分的局限**：构造验证依赖人工编写的可执行检查器，虽然能机械验证结构的正确性，但对非标准但正确的输出形式容忍度低，可能产生假阴性。证明评分使用基于 rubric 的自动打分，尽管与人工审计一致性良好，但在边界情形下仍会偏离人类专家判断(附录I审计报告显示部分案例评分漂移)。此外，验证器无法检查构造的最优性、简洁性或美学质量，而这些是奥赛中重要的隐性评判维度。
• **与已有基准的重叠与定位**：ComBench 与 IMO-Bench 存在约 20% 的题目重叠(附录H)，尽管二者侧重于不同的评分纬度，但部分题目重复可能导致对未来模型出现“污染”争议。同时基准严格限定于奥赛题源，反映的是模型在高难度、长证明链场景下的极限能力，无法直接衡量在常规组合推理或应用数学中的实用表现，限制了其作为下游任务代理指标的参考价值。