ComBench: Um Benchmark para Raciocínio de Prova Rigorosa e Realização Construtiva em Combinatória de Nível Olímpico

Resumo

A combinatória é central para a resolução de problemas matemáticos de nível olímpico, exigindo raciocínio discreto profundo, construções criativas e visão estrutural rigorosa. Evidências recentes sugerem que mesmo os modelos de fronteira mais fortes atuais permanecem irregulares em combinatória olímpica, revelando uma lacuna no raciocínio matemático criativo. Apresentamos o ComBench, um benchmark de combinatória de nível olímpico para avaliar e diagnosticar as capacidades de raciocínio combinatório de grandes modelos de linguagem. O ComBench contém 100 problemas de nível competitivo anotados por humanos, organizados em dois cenários complementares: problemas centrados em análise, que exigem primordialmente argumentos matemáticos rigorosos, e problemas centrados em construção, que exigem construções explícitas além de justificativas de correção. O protocolo de avaliação combina gradação de provas orientada por rubrica com verificação determinística de construção, expondo casos onde a qualidade da prova e a validade da construção divergem. Experimentos com modelos de fronteira de código aberto e fechado mostram que o ComBench está longe de estar saturado: o modelo mais forte alcança 65,4% de Média geral e 75,3% de Best@4 geral. Descobrimos ainda que Raciocínio de Prova Rigorosa e Realização Construtiva são capacidades distintas: Kimi-K2.6 fica atrás do GPT-5.5 na gradação de provas centradas em análise, mas o supera no Best@4 centrado em construção, enquanto problemas de Existência e Construção permanecem consistentemente os mais difíceis entre os modelos de fronteira representativos.

English

Combinatorics is central to Olympiad-level mathematical problem solving, requiring deep discrete reasoning, creative constructions, and rigorous structural insight. Recent evidence suggests that even today's strongest frontier models remain uneven on Olympiad combinatorics, revealing a gap in creative mathematical reasoning. We introduce ComBench, an Olympiad-level combinatorics benchmark for evaluating and diagnosing the combinatorial reasoning capabilities of large language models. ComBench contains 100 human-annotated competition-level problems organized around two complementary settings: analysis-centric problems, which primarily require rigorous mathematical arguments, and construction-centric problems, which require explicit constructions in addition to correctness justifications. The evaluation protocol combines rubric-guided proof grading with deterministic construction verification, exposing cases where proof quality and construction validity diverge. Experiments on frontier open- and closed-source models show that ComBench is far from saturated: the strongest model reaches 65.4% overall Avg. and 75.3% overall Best@4. We further find that Rigorous Proof Reasoning and Constructive Realization are distinct capabilities: Kimi-K2.6 trails GPT-5.5 on analysis-centric proof grading but surpasses it on construction-centric Best@4, while Existence and Construction problems remain consistently hardest across representative frontier models.