論文の概要: FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels

• arxiv url: http://arxiv.org/abs/2511.02872v1
• Date: Tue, 04 Nov 2025 03:25:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-06 18:19:32.183448
• Title: FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
• Title（参考訳）: FATE: 複数難易度のフロンティア代数のためのフォーマルベンチマークシリーズ
• Authors: Jiedong Jiang, Wanyi He, Yuefeng Wang, Guoxiong Gao, Yongle Hu, Jingting Wang, Nailing Guan, Peihao Wu, Chunbo Dai, Liang Xiao, Bin Dong,
• Abstract要約: FATE (Formal Algebra Theorem Evaluation) は形式代数学の新しいベンチマークシリーズである。 我々はFATE-H と FATE-X という2つの新しい成分を示し、それぞれ抽象代数学と可換代数学における100の問題を解く。 FATE-XはPhDレベルの試験の難しさとMathlibライブラリのカバレッジを超えた最初の正式なベンチマークである。
• 参考スコア（独自算出の注目度）: 7.8395206631845324
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Recent advances in large language models (LLMs) have demonstrated impressive capabilities in formal theorem proving, particularly on contest-based mathematical benchmarks like the IMO. However, these contests do not reflect the depth, breadth, and abstraction of modern mathematical research. To bridge this gap, we introduce FATE (Formal Algebra Theorem Evaluation), a new benchmark series in formal algebra designed to chart a course toward advanced mathematical reasoning. We present two new components, FATE-H and FATE-X, each with 100 problems in abstract and commutative algebra. The FATE series spans a difficulty spectrum from undergraduate exercises to problems exceeding PhD qualifying exams. Notably, FATE-X is the first formal benchmark to surpass both PhD-level exam difficulty and the coverage of the Mathlib library. Our evaluations of state-of-the-art LLM provers on this new benchmark reveal a stark performance gap compared to contest math: the best model achieves only 3% (pass@64) accuracy on FATE-H and 0% on FATE-X. Our two-stage evaluation reveals that models' natural-language reasoning is notably more accurate than their ability to formalize this reasoning. We systematically classify the common errors that arise during this formalization process. Furthermore, a comparative study shows that a specialized prover can exhibit less effective reflection than general-purpose models, reducing its accuracy at the natural-language stage. We believe FATE provides a robust and challenging benchmark that establishes essential checkpoints on the path toward research-level formal mathematical reasoning.
• Abstract（参考訳）: 大規模言語モデル(LLM)の最近の進歩は、特にIMOのような競合ベースの数学的ベンチマークにおいて、形式的定理証明における印象的な能力を示している。 しかし、これらのコンテストは現代の数学研究の深さ、幅、抽象化を反映していない。 このギャップを埋めるために、フォーマル代数の新しいベンチマークシリーズである FATE (Formal Algebra Theorem Evaluation) を導入する。 我々はFATE-H と FATE-X という2つの新しい成分を示し、それぞれ抽象代数学と可換代数学における100の問題を解く。 FATEシリーズは、学部のエクササイズからPhDの資格試験を超える問題まで、難易度の範囲にまたがっている。 特に、FATE-XはPhDレベルの試験の難しさとMathlibライブラリのカバレッジを超えた最初の正式なベンチマークである。 提案手法は,FATE-Hでは3%(pass@64),FATE-Xでは0%の精度しか得られない。 我々の2段階評価では、モデルの自然言語推論は、この推論を形式化する能力よりも顕著に正確であることが示されている。 この形式化プロセスで発生する共通エラーを体系的に分類する。 さらに、比較研究により、特殊証明器は汎用モデルよりも効果の低い反射を示し、自然言語の段階での精度を低下させることが示されている。 我々は、FATEが研究レベルの公式な数学的推論への道筋に不可欠なチェックポイントを確立する、堅牢で挑戦的なベンチマークを提供すると考えている。

関連論文リスト

• 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)
• 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)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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