論文の概要: 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で公開されている。
関連論文リスト
- LeanConjecturer: Automatic Generation of Mathematical Conjectures for Theorem Proving [6.220998637943786]
LeanConjecturerは、Large Language Models(LLMs)を使用して、Lean 4で大学レベルの数学予想を自動的に生成するパイプラインである。
反復生成と評価により、LeanConjecturerは40のMathlibシードファイルから12,289の予想を生成し、3,776は構文的に有効で非自明であると同定された。
論文 参考訳（メタデータ） (2025-06-27T08:17:18Z) - Solving Inequality Proofs with Large Language Models [42.667163027148916]
不等式証明は様々な科学・数学分野において不可欠である。
これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。
我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
論文 参考訳（メタデータ） (2025-06-09T16:43:38Z) - FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。
本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。
現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
論文 参考訳（メタデータ） (2025-05-05T15:37:00Z) - Automating Mathematical Proof Generation Using Large Language Model Agents and Knowledge Graphs [2.534053759586253]
KGプロデューサは、数学的証明の構築と形式化のために汎用LLMを拡張している。
汎用LLMはKG-Proverと組み合わせてミニF2Fテストで最大21%向上した。
KG-ProverはProofNetの2-11%、miniF2F-test、MUSTARDデータセットなど、さらなるスケーリングなしで一貫した改善を実現している。
論文 参考訳（メタデータ） (2025-02-04T07:17:34Z) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - SIaM: Self-Improving Code-Assisted Mathematical Reasoning of Large Language Models [54.78329741186446]
本稿では,コードに基づく批判モデルを用いて,質問コードデータ構築,品質管理,補完的評価などのステップをガイドする新しいパラダイムを提案する。
英語と中国語におけるドメイン内ベンチマークとドメイン外ベンチマークの両方の実験は、提案したパラダイムの有効性を実証している。
論文 参考訳（メタデータ） (2024-08-28T06:33:03Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - 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) - math-PVS: A Large Language Model Framework to Map Scientific
Publications to PVS Theories [10.416375584563728]
本研究では,大規模言語モデル(LLM)の高度な数学的概念の定式化への適用性について検討する。
我々は、研究論文から数学的定理を抽出し、形式化する、Emphmath-PVSと呼ばれる自動過程を構想する。
論文 参考訳（メタデータ） (2023-10-25T23:54:04Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。