論文の概要: ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics

• arxiv url: http://arxiv.org/abs/2606.10479v1
• Date: Tue, 09 Jun 2026 06:50:15 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-10 15:40:58.358128
• Title: ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics
• Title（参考訳）: ComBench: Olympiad-Level Combinatoricsにおける厳格な推論と構成的実現のためのベンチマーク
• Authors: Shunkai Zhang, Haoran Zhang, Yun Luo, Qianjia 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, Yu Cheng,
• Abstract要約: 我々は,Olympiadレベルの診断用ベンチマークであるComBenchと,大規模言語モデルの推論機能を紹介する。 ComBenchには、補完的な2つの設定で整理された100の人間注釈の競合レベルの問題が含まれている。 実験の結果、最強モデルはAvg.全体65.4%、Best@4.3%に達した。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: コンビニティクスはオリンピアドレベルの数学的問題解決の中心であり、深い離散的推論、創造的な構成、厳密な構造的洞察を必要とする。 最近の証拠は、今日の最強フロンティアモデルでさえオリンピアード組合せ論において不均一であり続けており、創造的な数学的推論のギャップが明らかになっていることを示唆している。 我々は,大言語モデルの組合せ推論能力の評価と診断を行うための,OlympiadレベルのコンビネータベンチマークであるComBenchを紹介する。 ComBenchには、厳密な数学的議論を必要とする分析中心問題と、正当性の正当性に加えて明示的な構成を必要とする建設中心問題という、2つの相補的な設定で整理された100の人間注釈の競合レベル問題が含まれている。 評価プロトコルは、ルーブリック誘導による証明グレーディングと決定論的構成検証を組み合わせ、証明品質と構築妥当性がばらばらなケースを明らかにする。 フロンティアのオープンソースモデルとクローズドソースモデルの実験では、コムベンチは飽和状態には程遠いことが示され、最強のモデルはAvg全体の65.4%に達する。 全体の75.3%がBest@4。 Kimi-K2.6 は解析中心の証明グレーディングで GPT-5.5 をパスするが、構成中心の Best@4 では上回っている。

関連論文リスト

• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  大規模言語モデル(LLM)は、強力な非公式な数学的推論を示すが、リーンのような形式言語で検証可能な証明を生成するのに苦労している。 本稿では,汎用基礎モデルによる自動形式定理証明の最先端性能を実現するためのエージェントフレームワークであるLEAPを提案する。
  論文  参考訳（メタデータ） (2026-06-02T08:16:42Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。 新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。 このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
  論文  参考訳（メタデータ） (2026-04-02T08:22:17Z)
• Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs [41.29431283264807]
  本稿では、厳密な証明問題のスケーラブルな情報源として理論計算機科学(TCS)を活用することを提案する。 本稿では,2つのTCS領域に対して,チューリング機械停止動作の証明を含むベイジービーバー問題(Busy Beaver problem)と,論理と算術の推論を組み合わせた混合ブール算術問題(Mixed Boolean Arithmetic problem)を提案する。 我々のフレームワークは,並列形式 (Lean4) と非公式 (Markdown) 仕様で問題を自動生成し,検証問題を生成するスケーラブルなパイプラインを作成する。
  論文  参考訳（メタデータ） (2025-08-21T14:15:40Z)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
  LLMは難解な解答作業に対処できるが、幻覚や不可解なステップの誤りを生じやすい。 創造性と数学的厳密性の両方を保ちながら、どのように解答-構成問題を解決するか? 本稿では,パターン駆動型推論と形式的定理証明を統合したニューロシンボリックな手法であるLLM-Conjecture-Prove(ECP)フレームワークを紹介する。 ConstructiveBenchでは、ECPは33.1%の最先端の精度(32.5%から)を達成し、公式な数学的推論を前進させる可能性を示している。
  論文  参考訳（メタデータ） (2025-05-24T03:52:25Z)
• PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
  本稿では,高品質なオリンピアードレベルの数学問題を自動生成する新しい手法であるPromptCoTを紹介する。 提案手法は,問題構築の背景にある数学的概念と理論的根拠に基づいて複雑な問題を合成する。 提案手法は, GSM8K, MATH-500, AIME2024などの標準ベンチマークで評価され, 既存の問題生成手法を一貫して上回っている。
  論文  参考訳（メタデータ） (2025-03-04T06:32:30Z)
• A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation [3.003569769097376]
  コンビニティクスは数学の基盤であり、離散構造の分析と問題解決に不可欠なツールを提供する。 これを解決するために、手動でLeanCombを構築しました。 我々は,自己改善型大規模言語モデルによって提案される候補戦略と,予測のための強化学習木探索アプローチを組み合わせた,コンビニアル・アイデンティティのための自動定理ジェネレータATG4CIを開発した。
  論文  参考訳（メタデータ） (2025-02-25T04:41:49Z)
• OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems [62.06169250463104]
  我々はOlympiadレベルのバイリンガル・マルチモーダル・サイエンス・ベンチマークであるOlympiadBenchを紹介し、Olympiadレベルの数学と物理学のコンペティションの8,476の問題を特徴とする。 最も優れたモデルであるGPT-4Vはオリンピアドベンチで平均17.97%を獲得し、物理学ではわずか10.74%である。 GPT-4Vの分析では、幻覚、知識欠失、論理的誤信などの問題が指摘されている。
  論文  参考訳（メタデータ） (2024-02-21T18:49:26Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。