論文の概要: MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis

• arxiv url: http://arxiv.org/abs/2606.13782v2
• Date: Mon, 15 Jun 2026 05:26:47 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-16 13:45:31.22235
• Title: MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis
• Title（参考訳）: MA-ProofBench:数学解析における理論証明のためのLLMの2段階評価
• Authors: Lushi Pu, Weiming Zhang, Xinheng Xie, Zixuan Fu, Bingxiang He, Hongya Lyu, Xin Li, Jie Zhou, Yudong Wang,
• Abstract要約: MA-ProofBenchは数学解析に特化した最初の公式な定理証明ベンチマークである。 ベンチマークには6つのコアトピックと27のサブカテゴリをカバーする200の形式化された定理が含まれており、測定と積分理論、複素解析、関数解析が含まれる。 我々は、MA-ProofBench上での最近の汎用推論モデルと形式定理プロバーについて評価する。
• 参考スコア（独自算出の注目度）: 28.906916840252077
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large Language Models (LLMs) have made notable progress in automated theorem proving, yet existing formal benchmarks remain limited in both mathematical coverage and difficulty. Most are concentrated in areas that are easier to formalize, such as algebra and elementary number theory, and provide limited coverage of subfields that require deeper reasoning, including mathematical analysis. To address this gap, we introduce MA-ProofBench, to the best of our knowledge, the first formal theorem-proving benchmark dedicated to Mathematical Analysis. The benchmark contains 200 formalized theorems covering 6 core topics and 27 subcategories, including measure and integration theory, complex analysis, and functional analysis. The problems are divided into two difficulty levels, an undergraduate level (Level I, 100 problems) and a Ph.D. qualifying level (Level II, 100 problems), to evaluate how well LLMs perform formal reasoning at different mathematical depths. Each problem is constructed through a human-led, LLM-assisted formalization pipeline followed by independent expert review, ensuring that the formal statements remain faithful to the original mathematics. We evaluate a range of recent general-purpose reasoning models and formal theorem provers on MA-ProofBench. However, most models perform poorly: even the best-performing model, GPT-5.5, achieves only 16% Pass@8 on Level I and 5% on Level II, while most models stay close to 0% on Level II. Further analysis identifies Mathlib hallucinations and incomplete proofs as the two dominant failure modes, while an evaluation on the natural-language version of the benchmark exposes a clear gap between informal and formal reasoning. MA-ProofBench is intended to serve as a reliable reference for tracking progress in formal mathematical reasoning in advanced domains.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、自動定理証明において顕著な進歩を遂げているが、既存の公式ベンチマークは、数学的カバレッジと難易度の両方で制限されている。 多くは代数や素数理論などの形式化が容易な領域に集中しており、数学的解析を含むより深い推論を必要とする部分体を限定的にカバーしている。 このギャップに対処するため、我々はMA-ProofBenchを紹介します。 ベンチマークには6つのコアトピックと27のサブカテゴリをカバーする200の形式化された定理が含まれており、測定と積分理論、複素解析、関数解析が含まれる。 問題は2つの難易度、学部レベル(レベルI、100問題)とPh.D.予選レベル(レベルII、100問題)に分けられ、LLMが数学的深度で形式的推論をいかにうまく行うかを評価する。 それぞれの問題は、人間主導のLSM支援形式化パイプラインを通じて構築され、その後独立した専門家によるレビューによって、形式的ステートメントが元の数学に忠実であることを保証する。 我々は、MA-ProofBench上での最近の汎用推論モデルと形式定理プロバーについて評価する。 GPT-5.5はレベルIでは16%のPass@8しか達成せず、レベルIIでは5%、レベルIIでは0%近くにとどまっている。 さらなる分析では、Mathlibの幻覚と不完全証明を2つの支配的な失敗モードとして特定し、一方、ベンチマークの自然言語版に対する評価は、非公式な推論と形式的な推論の間に明確なギャップを露呈している。 MA-ProofBenchは、高度な領域における公式な数学的推論の進捗を追跡するための信頼性の高い基準として機能することを意図している。

関連論文リスト

• 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)
• Solving Inequality Proofs with Large Language Models [42.667163027148916]
  不等式証明は様々な科学・数学分野において不可欠である。 これにより、大きな言語モデル(LLM)の需要が高まるフロンティアとなる。 我々は、Olympiadレベルの不平等を専門家が計算したデータセットであるIneqMathをリリースした。
  論文  参考訳（メタデータ） (2025-06-09T16:43:38Z)
• DeepTheorem: Advancing LLM Reasoning for Theorem Proving Through Natural Language and Reinforcement Learning [67.93945726549289]
  DeepTheoremは、数学的推論を強化するために自然言語を活用する包括的な非公式な定理証明フレームワークである。 DeepTheoremには、121Kの高品質なIMOレベルの非公式な定理と証明からなる大規模なベンチマークデータセットが含まれている。 我々は、証明された定理の変種を利用して堅牢な数学的推論を動機付けることによって、非公式な定理証明に適した新しい強化学習戦略(RL-Zero)を考案する。
  論文  参考訳（メタデータ） (2025-05-29T17:59:39Z)
• FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models [17.919212265668783]
  本稿では,高校のオリンピアード問題から学部レベルの定理まで,5,560の公証問題からなる大規模Lean4ベンチマークであるFormalMATHを提案する。 本稿では,文の自動形式化,セマンティック検証,否定に基づく無防備なフィルタリング戦略を統合した,新たなオートフォーマル化パイプラインを提案する。 現状のLSMに基づく定理証明器の評価は, 重大な限界を呈する。
  論文  参考訳（メタデータ） (2025-05-05T15:37:00Z)
• 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)

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

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