論文の概要: CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics

• arxiv url: http://arxiv.org/abs/2505.03171v1
• Date: Tue, 06 May 2025 04:32:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-07 18:50:11.203562
• Title: CombiBench: Benchmarking LLM Capability for Combinatorial Mathematics
• Title（参考訳）: CombiBench: 組合せ数学のためのLLM能力のベンチマーク
• Authors: Junqi Liu, Xiaohan Lin, Jonas Bayer, Yael Dillies, Weijie Jiang, Xiaodan Liang, Roman Soletskyi, Haiming Wang, Yunzhou Xie, Beibei Xiong, Zhengfeng Yang, Jujian Zhang, Lihong Zhi, Jia Li, Zhengying Liu,
• Abstract要約: 100の問題をまとめた総合的なベンチマークであるCombiBenchを紹介します。 CombiBenchは2000年以降の問題解決に適している(画像を含むIMO 2004 P3を除く)。 また、フォーマル数学のための包括的で標準化された評価フレームワーク「ファイン・エバル」も提供する。
• 参考スコア（独自算出の注目度）: 45.32204834230928
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Neurosymbolic approaches integrating large language models with formal reasoning have recently achieved human-level performance on mathematics competition problems in algebra, geometry and number theory. In comparison, combinatorics remains a challenging domain, characterized by a lack of appropriate benchmarks and theorem libraries. To address this gap, we introduce CombiBench, a comprehensive benchmark comprising 100 combinatorial problems, each formalized in Lean~4 and paired with its corresponding informal statement. The problem set covers a wide spectrum of difficulty levels, ranging from middle school to IMO and university level, and span over ten combinatorial topics. CombiBench is suitable for testing IMO solving capabilities since it includes all IMO combinatorial problems since 2000 (except IMO 2004 P3 as its statement contain an images). Furthermore, we provide a comprehensive and standardized evaluation framework, dubbed Fine-Eval (for $\textbf{F}$ill-in-the-blank $\textbf{in}$ L$\textbf{e}$an Evaluation), for formal mathematics. It accommodates not only proof-based problems but also, for the first time, the evaluation of fill-in-the-blank questions. Using Fine-Eval as the evaluation method and Kimina Lean Server as the backend, we benchmark several LLMs on CombiBench and observe that their capabilities for formally solving combinatorial problems remain limited. Among all models tested (none of which has been trained for this particular task), Kimina-Prover attains the best results, solving 7 problems (out of 100) under both ``with solution'' and ``without solution'' scenarios. We open source the benchmark dataset alongside with the code of the proposed evaluation method at https://github.com/MoonshotAI/CombiBench/.
• Abstract（参考訳）: 大規模言語モデルと形式的推論を統合するニューロシンボリックアプローチは、代数、幾何学、数論における数学の競合問題における人間レベルの性能を最近達成している。 比較すると、組合せ論は、適切なベンチマークと定理ライブラリの欠如を特徴とする、挑戦的な領域のままである。 このギャップに対処するために、100の組合せ問題からなる包括的なベンチマークであるCombiBenchを紹介します。 問題セットは、中学からIMO、大学レベルまで幅広い難易度をカバーし、10以上の総合的なトピックにまたがる。 CombiBenchは2000年以来のIMO組合せ問題(画像を含むIMO 2004 P3を除く)を含むため、IMO解決機能をテストするのに適している。 さらに,Fine-Eval($\textbf{F}$ill-in-the-blank $\textbf{in}$ L$\textbf{e}$an Evaluation)と呼ばれる包括的で標準化された評価フレームワークを提供する。 証明に基づく問題だけでなく、初めて、補題付き質問の評価にも対応している。 評価手法としてFine-Eval、バックエンドとしてKimina Lean Serverを使用し、CombiBench上で複数のLLMをベンチマークし、組合せ問題を正式に解く能力が制限されていることを観察する。 テストされたすべてのモデル(いずれもこの特定のタスクのためにトレーニングされたものではない)の中で、Kimina-Proverは最高の結果を得、 `with Solution' と `without Solution' のシナリオの両方で 7 つの問題 (100点中) を解決する。 提案された評価手法のコードとともに、ベンチマークデータセットをhttps://github.com/MoonshotAI/CombiBench/でオープンソース化しました。

関連論文リスト

• Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models [86.45058529521258]
  OlymMATHは、LLMの複雑な推論能力を厳格にテストするために設計された、Olympiadレベルの新しい数学ベンチマークである。 OlymMATHは200の厳密にキュレートされた問題があり、それぞれが手動で検証され、英語と中国語の並行バージョンで利用可能である。
  論文  参考訳（メタデータ） (2025-03-27T11:20:17Z)
• PromptCoT: Synthesizing Olympiad-level Problems for Mathematical Reasoning in Large Language Models [59.920971312822736]
  本稿では,高品質なオリンピアードレベルの数学問題を自動生成する新しい手法であるPromptCoTを紹介する。 提案手法は,問題構築の背景にある数学的概念と理論的根拠に基づいて複雑な問題を合成する。 提案手法は, GSM8K, MATH-500, AIME2024などの標準ベンチマークで評価され, 既存の問題生成手法を一貫して上回っている。
  論文  参考訳（メタデータ） (2025-03-04T06:32:30Z)
• UGMathBench: A Diverse and Dynamic Benchmark for Undergraduate-Level Mathematical Reasoning with Large Language Models [11.964085209696051]
  UGMathBenchは16の被験者5,062の課題と111のトピックで構成され、10の異なる回答タイプが特徴である。 それぞれの問題には3つのランダム化バージョンが含まれており、主要なオープンソース LLM が UGMathBench で飽和するにつれて、リリースに向けて追加バージョンが計画されている。 LLMを23個評価した結果, OpenAI-o1-mini による EAcc のロバスト性は 56.3% であり,それぞれ異なるモデルで大きな$Delta$値が観測された。
  論文  参考訳（メタデータ） (2025-01-23T15:46:43Z)
• UTMath: Math Evaluation with Unit Test via Reasoning-to-Coding Thoughts [7.856746367263317]
  本稿では,大規模言語モデルの評価を目的とした頑健な評価フレームワークであるUTMath Benchmarkを紹介する。 これは9つの数学領域にまたがる1053個の最先端問題を含み、平均68個のテストケースがある。 最高の性能モデルであるo1-miniはわずか32.57%の問題を解き、o1-previewは27.16%、GPT-4oは26.93%であった。
  論文  参考訳（メタデータ） (2024-11-11T18:59:02Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAPは、それらの算術的証明構造に関する仕様に従って、問題文と連鎖推論トレースを生成する。 MathGAP を用いて, LLM はより深く, より広くなるにつれて, 性能が著しく低下することがわかった。
  論文  参考訳（メタデータ） (2024-10-17T12:48:14Z)
• FLARE: Faithful Logic-Aided Reasoning and Exploration [50.9814063216852]
  タスク分解を用いて問題空間をトラバースする新しい手法を提案する。 我々はLarge Language Modelsを使ってソリューションを計画し、クエリを事実に軟式化し、論理プログラミングコードを使って述語する。 提案手法は,生成したコードに対する推論プロセスの忠実度を計算し,外部の解法に頼らずにマルチホップ探索のステップを解析する。
  論文  参考訳（メタデータ） (2024-10-14T19:39:11Z)
• GSM-Plus: A Comprehensive Benchmark for Evaluating the Robustness of LLMs as Mathematical Problem Solvers [68.77382332826167]
  大規模言語モデル (LLM) は、様々な数学的推論ベンチマークで顕著な性能を達成している。 1つの必須かつ頻繁な証拠は、数学の質問がわずかに変更されたとき、LLMは誤って振る舞うことができることである。 このことは, LLMの数学推論能力の頑健性を評価するために, 幅広い質問のバリエーションを試すことによるものである。
  論文  参考訳（メタデータ） (2024-02-29T15:26:14Z)
• CHAMP: A Competition-level Dataset for Fine-Grained Analyses of LLMs' Mathematical Reasoning Capabilities [25.857946070979576]
  概念とHint-Annotated Math Problems (CHAMP) は、概念に注釈を付けた高校数学の競争問題である。 このベンチマークは困難で、最高のモデルは標準設定で58.1%しか得点できない。 モデルはしばしば、間違った推論ステップを通じて、正しい最終回答に到達します。
  論文  参考訳（メタデータ） (2024-01-13T03:18:16Z)

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

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