論文の概要: AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
- arxiv url: http://arxiv.org/abs/2607.11849v1
- Date: Mon, 13 Jul 2026 17:38:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-07-14 17:47:21.576021
- Title: AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
- Title（参考訳）: AdvancedMathBench: 高度な数学的証明生成と検証のためのベンチマークスイート
- Abstract要約: 大型言語モデル (LLM) は、高校やオリンピックスタイルの数学において顕著な性能を発揮している。
既存のベンチマークはスコープと評価の粒度の両方で不足している。
本稿では,高度な数学的推論能力を評価するためのベンチマークスイートであるAdvancedMathBenchを紹介する。
- 参考スコア（独自算出の注目度）: 41.90353470982016
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Large language models (LLMs) have achieved remarkable performance on high-school and olympiad-style mathematics, yet their capabilities on advanced mathematics remain poorly understood. Existing benchmarks, however, fall short in both scope and evaluation granularity: they provide limited disciplinary coverage and often rely on final-answer correctness or coarse judgments, leaving the validity of the reasoning process inadequately assessed. To bridge this gap, we introduce AdvancedMathBench, a benchmark suite designed to evaluate advanced mathematical reasoning capabilities. Its core proof-generation benchmark, ProverBench, contains 296 problems spanning undergraduate and doctoral qualifying-exam levels. To provide reliable evaluation of the proofs, we develop a dedicated automatic verification pipeline trained on large-scale expert annotations to produce both correctness verdicts and fine-grained assessments of proof errors, which exhibits strong agreement with human experts on held-out proof trajectories. We further introduce VerifierBench, consisting of 888 model-generated proof trajectories paired with expert ground truth, to evaluate whether models can correctly judge proof validity and provide sound verification rationales. Experiments show that AdvancedMathBench remains challenging for frontier models. On proof generation, the best-performing model, GPT-5.5-xhigh, achieves only 75.8 and 66.1 on the UGD and QE splits, respectively, indicating substantial room for improvement on advanced mathematical proof construction. On proof verification, the best model attains a Balanced F1 of only 65.1, and models generally exhibit low true negative rates, suggesting that critical error detection remains a major bottleneck.
- Abstract（参考訳）: 大規模言語モデル(LLM)は、高校やオリンピックスタイルの数学において顕著な性能を発揮しているが、高度な数学におけるそれらの能力はいまだに理解されていない。
しかし、既存のベンチマークは、範囲と評価の粒度の両方において不足しており、限定的な懲戒的カバレッジを提供し、しばしば最終回答の正しさや粗い判断に依存し、推論プロセスの妥当性を不十分に評価する。
このギャップを埋めるために、高度な数学的推論能力を評価するために設計されたベンチマークスイートであるAdvancedMathBenchを導入する。
コアとなる証明生成ベンチマークであるProverBenchには、学部と博士の資格試験レベルにまたがる296の問題がある。
証明の信頼性を評価するため,大規模な専門家アノテーションに基づいて訓練された自動検証パイプラインを開発し,検証誤差の正確性評価ときめ細かな評価の両立を図った。
さらに、888個のモデル生成された証明軌跡と専門家の真実を組み合わせて構成したVerifierBenchを導入し、モデルが妥当性を正しく判断し、音響的検証の合理性を提供するかどうかを評価する。
実験によると、AdvancedMathBenchはフロンティアモデルでは依然として挑戦的である。
証明生成において、最高の性能モデルである GPT-5.5-xhigh は、それぞれ UGD と QE の分割で 75.8 と 66.1 しか達成していない。
証明検証において、最良のモデルは65.1のバランスF1に達し、モデルは一般に真の負のレートが低く、臨界誤差検出が主要なボトルネックであることを示している。
関連論文リスト
- ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
我々は,Olympiadレベルの診断用ベンチマークであるComBenchと,大規模言語モデルの推論機能を紹介する。
ComBenchには、補完的な2つの設定で整理された100の人間注釈の競合レベルの問題が含まれている。
実験の結果、最強モデルはAvg.全体65.4%、Best@4.3%に達した。
論文 参考訳（メタデータ） (2026-06-09T06:50:15Z) - FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models [0.0]
我々はtextbfFormalRewardBenchを紹介します。これはLean 4.0で証明された形式的定理で報酬モデルを評価するための最初のベンチマークです。
その結果,フロンティア LLM は最高性能 (59.8%) を達成し,特殊定理証明器は最低性能 (24.4%) を達成した。
textbfFormalRewardBenchを公開し、形式数学における報酬モデルの開発についてさらなる研究を奨励する。
論文 参考訳（メタデータ） (2026-05-11T07:51:15Z) - LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
研究レベルの数学的推論のための動的多重選択ベンチマークであるLiveMathematicianBenchを提案する。
新たに発表された定理で評価を基礎づけることで、記憶されたパターンを超えた現実的なテストベッドを提供する。
このパイプラインは、高レベルな証明戦略を使用して、妥当だが無効な解選択を構築する。
論文 参考訳（メタデータ） (2026-04-02T08:22:17Z) - FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified? [0.04324039930655099]
本稿では、AIモデルが正式に検証された数学的証明を生成できるかどうかを評価するために設計されたプライベートベンチマークであるFormalProofBenchを紹介する。
各タスクは、自然言語とLean4の形式的なステートメントをペアリングし、モデルはLean 4チェッカーが受け入れるリーンの証明を出力する必要があります。
エージェントハーネスを用いたフロンティアモデルの評価を行い,最も優れた基礎モデルが33.5%の精度で達成できることを見出した。
論文 参考訳（メタデータ） (2026-03-27T21:14:53Z) - Reliable Fine-Grained Evaluation of Natural Language Math Proofs [30.992321135182905]
本稿では,0-7スケールの微粒なスコアをモデル生成数学の証明に割り当てる評価器を開発するための体系的手法を提案する。
ProofBenchは,6つの主要な数学コンペティションから145の問題にまたがる,詳細な証明評価のエキスパートによる最初のデータセットである。
本稿では,強力な推論バックボーンLMと参照解とマーキングスキームからのリッチコンテキストを組み合わせた評価器ProofGraderと,シンプルなアンサンブル手法を提案する。
論文 参考訳（メタデータ） (2025-10-14T02:59:07Z) - Reasoning or Memorization? Unreliable Results of Reinforcement Learning Due to Data Contamination [67.67725938962798]
大規模なWebスケールコーパスの事前トレーニングは、広く使用されているベンチマークでデータ汚染の影響を受けやすいQwen2.5が残る。
我々はRandomCalculationと呼ばれる任意の長さと難易度を持つ完全クリーンな算術問題を生成するジェネレータを導入する。
精度の高い報酬信号のみがベースモデルの性能境界を超える安定した改善をもたらすことを示す。
論文 参考訳（メタデータ） (2025-07-14T17:55:15Z) - Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models [11.250861762443801]
RFMDataset(Reveal Failure Modes)は200種類の数学的証明問題の集合である。
先進モデルの性能を徹底的に評価する。
解析により,現在の大規模推論モデルの基本的制約を示す10種類のきめ細かい誤差型が明らかになった。
論文 参考訳（メタデータ） (2025-06-20T16:14:18Z) - Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad [4.573289946657861]
我々は2025年のUSAMOの6つの問題に対する推論モデルを評価する。
Gemini-2.5-Proのみが25%という非自明なスコアを達成している。
以上の結果から,現在のLLMは厳密な数学的推論作業には不十分であることが示唆された。
論文 参考訳（メタデータ） (2025-03-27T19:21:05Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。