論文の概要: Evaluating Frontier LLMs on PhD-Level Mathematical Reasoning: A Benchmark on a Textbook in Theoretical Computer Science about Randomized Algorithms

• arxiv url: http://arxiv.org/abs/2512.13978v1
• Date: Tue, 16 Dec 2025 00:34:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-17 16:49:26.529079
• Title: Evaluating Frontier LLMs on PhD-Level Mathematical Reasoning: A Benchmark on a Textbook in Theoretical Computer Science about Randomized Algorithms
• Title（参考訳）: PhD-Level Mathematical ReasoningにおけるフロンティアLLMの評価:ランダム化アルゴリズムに関する理論的コンピュータ科学における教科書のベンチマーク
• Authors: Yang Cao, Yubin Chen, Xuyang Guo, Zhao Song, Song Yue, Jiahao Zhang, Jiale Zhao,
• Abstract要約: 大規模言語モデル(LLM)は、自動数学的推論と科学的発見の突破口となった。 GP-5-Thinking、Gemini-3-Pro、Claude-Sonnet-4.5-Thinking、Grok-4の4つのフロンティアモデルのベンチマークを示す。 上位モデルの精度は高いが,他のモデルでは一貫性が著しく低下していることがわかった。
• 参考スコア（独自算出の注目度）: 14.853721511192736
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: The rapid advancement of large language models (LLMs) has led to significant breakthroughs in automated mathematical reasoning and scientific discovery. Georgiev, G${ó}$mez-Serrano, Tao, and Wagner [GGSTW+25] demonstrate that AI systems can explore new constructions and improve existing bounds, illustrating the growing potential of LLMs to accelerate mathematical discovery. Similarly, Bubeck et al. [BCE+25] show that GPT-5 can meaningfully contribute to scientific workflows, from proposing hypotheses to generating proofs and analyses. Despite these advances, a rigorous evaluation of these models on canonical, graduate-level mathematical theory remains necessary to understand their baseline reasoning capabilities. In this paper, we present a comprehensive benchmark of four frontier models: GPT-5-Thinking, Gemini-3-Pro, Claude-Sonnet-4.5-Thinking, and Grok-4 against the classic curriculum of Randomized Algorithms by Motwani and Raghavan [MR95]. We tasked each model with generating formal LaTeX proofs for a series of lemmas and exercises spanning the textbook. We find that while the top-tier models (Gemini, and Claude) achieve a high accuracy rate (approx. 66%), demonstrating a robust grasp of probabilistic method and formal logic, other models lag significantly in consistency (approx. 40%). We provide a qualitative analysis of the generated proofs, highlighting differences in conciseness, hallucination rates, and logical structure. Our results suggest that while frontier models have reached a threshold of proficiency suitable for graduate-level pedagogical assistance and formalization, significant variance exists in their reliability for rigorous mathematical derivation. The code and the full set of LLM-generated responses are open-sourced and publicly available at https://github.com/magiclinux/math_benchmark_probability.
• Abstract（参考訳）: 大規模言語モデル(LLM)の急速な進歩は、自動数学的推論と科学的発見に大きなブレークスルーをもたらした。 Georgiev, G${ó}$mez-Serrano, Tao, and Wagner [GGSTW+25] は、AIシステムが新しい構造を探求し、既存の境界を改善し、数学的発見を加速するためにLSMの増大する可能性を示す。 同様に、Bubeck et al [BCE+25] は、GPT-5が仮説の提案から証明や分析の生成まで、科学的ワークフローに有意義な貢献ができることを示した。 これらの進歩にもかかわらず、これらのモデルの標準的、大学院レベルの数学的理論に関する厳密な評価は、それらの基本的推論能力を理解するために依然として必要である。 本稿では,GPT-5-Thinking,Gemini-3-Pro,Claude-Sonnet-4.5-Thinking,Grok-4の4つのフロンティアモデルについて,Motwani と Raghavan [MR95] によるランダム化アルゴリズムの古典的カリキュラムに対する総合的なベンチマークを示す。 教科書に散在する一連のレムマと演習のための公式なLaTeX証明を生成することを各モデルに課した。 トップ層モデル(GeminiとClaude)は高い精度(約66%)を達成する一方で、確率的手法と形式論理をしっかりと把握する一方で、他のモデルでは一貫性(約40%)が著しく遅れていることがわかった。 生成した証明の質的分析を行い、簡潔さ、幻覚率、論理構造の違いを強調した。 以上の結果から,フロンティアモデルは大学院レベルの教育支援と形式化に適した習熟度に達しているが,厳密な数学的導出の信頼性には大きな差異が存在することが示唆された。 コードとLLM生成レスポンスの完全なセットは、https://github.com/magiclinux/math_benchmark_probability.comで公開されている。

関連論文リスト

• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。 この合成データセットでDeepSeekMath 7Bモデルを微調整します。 我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
  論文  参考訳（メタデータ） (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)
• Controlling Equational Reasoning in Large Language Models with Prompt Interventions [3.9735602856280132]
  本稿では,Large Language Models (LLMs) における幻覚率を,シンボルデータ生成フレームワークを用いて制御する方法を検討する。 シンボルエンジンを用いて導出タスクのデータを生成し、数学的導出の特徴を摂動させるために目的の介入を適用する。 次に、細調整されたT5モデル、GPTモデル、LLaMaモデルを含む、様々なLLMに対する迅速な介入の効果を評価する。
  論文  参考訳（メタデータ） (2023-07-19T14:13:02Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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