ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics

• URL: http://arxiv.org/abs/2606.10479v1
• Date: Tue, 09 Jun 2026 06:50:15 GMT
• Title: ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics
• Abstract summary: We introduce ComBench, an Olympiad-level benchmark for diagnosing and the reasoning capabilities of large language models.<n>ComBench contains 100 human-annotated competition-level problems organized around two complementary settings.<n>Experiments show that the strongest model reaches 65.4% overall Avg. and 75.3% overall Best@4.
• Score: 95.15900681087088
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.

Related papers

• Reasoning Consensus: Structural Ensembling of LLM Reasoning via Weighted DAG Aggregation [17.1797342726399]
  We propose a framework that ensembles the reasoning structure, not just the answers, of multiple Large Language Models (LLMs)<n>We weight each step by how many traces independently attest to it, to return "Consensus Reasoning"<n>Across six benchmarks spanning statutory interpretation, graduate-level science, narrative multi-hop reasoning, and first-order logic, our ensemble outperforms a matched-budget majority-vote baseline.
  arXiv  Detail & Related papers  (2026-07-30T07:14:50Z)
• AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification [41.90353470982016]
  Large language models (LLMs) have achieved remarkable performance on high-school and olympiad-style mathematics.<n>Existing benchmarks fall short in both scope and evaluation granularity.<n>We introduce AdvancedMathBench, a benchmark suite designed to evaluate advanced mathematical reasoning capabilities.
  arXiv  Detail & Related papers  (2026-07-13T17:38:22Z)
• MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis [28.906916840252077]
  MA-ProofBench is the first formal theorem-proving benchmark dedicated to Mathematical Analysis.<n>The benchmark contains 200 formalized theorems covering 6 core topics and 27 subcategories, including measure and integration theory, complex analysis, and functional analysis.<n>We evaluate a range of recent general-purpose reasoning models and formal theorem provers on MA-ProofBench.
  arXiv  Detail & Related papers  (2026-06-11T18:00:04Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
  We propose leveraging theoretical computer science (TCS) as a scalable source of rigorous proof problems.<n>We demonstrate this approach on two TCS domains: Busy Beaver problems, which involve proving bounds on Turing machine halting behavior, and Mixed Boolean Arithmetic problems, which combine logical and arithmetic reasoning.<n>Our framework automatically synthesizes problems with parallel formal (Lean4) and informal (Markdown) specifications, creating a scalable pipeline for generating verified proof challenges.
  arXiv  Detail & Related papers  (2025-08-21T14:15:40Z)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
  LLMs can tackle difficult answer-construction tasks but are prone to errors from hallucinations and unverifiable steps.<n>This raises a key understudied question: how to solve answer-construction problems while preserving both creativity and mathematical rigor?<n>We introduce the LLM-Conjecture-Prove (ECP) framework, a neuro-symbolic method integrating pattern-driven conjecturing with formal theorem proving.<n>On ConstructiveBench, ECP achieves 33.1% end-to-end state-of-the-art accuracy (up from 32.5%), demonstrating its potential to advance formal mathematical reasoning.
  arXiv  Detail & Related papers  (2025-05-24T03:52:25Z)
• PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
  We introduce PromptCoT, a novel approach for automatically generating high-quality Olympiad-level math problems.<n>The proposed method synthesizes complex problems based on mathematical concepts and the rationale behind problem construction.<n>Our method is evaluated on standard benchmarks including GSM8K, MATH-500, and AIME2024, where it consistently outperforms existing problem generation methods.
  arXiv  Detail & Related papers  (2025-03-04T06:32:30Z)
• A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation [3.003569769097376]
  Combinatorics is a cornerstone of mathematics, providing essential tools for analyzing discrete structures and solving problems.<n>To address this, we manually construct LeanComb, an automated identities benchmark in Lean.<n>We develop an Automated Theorem Generator for Combinatorial Identities, ATG4CI, which combines candidate tactics suggested by a self-improving large language model with a Reinforcement Learning Tree Search approach for prediction.
  arXiv  Detail & Related papers  (2025-02-25T04:41:49Z)
• Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models [63.31878920079154]
  We propose a benchmark specifically designed to assess large language models' mathematical reasoning at the Olympiad level.<n>Unlike existing Olympiad-related benchmarks, our dataset focuses exclusively on mathematics and comprises a vast collection of 4428 competition-level problems with rigorous human annotation.<n>Our experimental results show that even the most advanced models, OpenAI o1-mini and OpenAI o1-preview, struggle with highly challenging Olympiad-level problems, with 60.54% and 52.55% accuracy, highlighting significant challenges in Olympiad-level mathematical reasoning.
  arXiv  Detail & Related papers  (2024-10-10T14:39:33Z)
• OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems [62.06169250463104]
  We present OlympiadBench, an Olympiad-level bilingual multimodal scientific benchmark, featuring 8,476 problems from Olympiad-level mathematics and physics competitions. The best-performing model, GPT-4V, attains an average score of 17.97% on OlympiadBench, with a mere 10.74% in physics. Our analysis orienting GPT-4V points out prevalent issues with hallucinations, knowledge omissions, and logical fallacies.
  arXiv  Detail & Related papers  (2024-02-21T18:49:26Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.