論文の概要: FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
- arxiv url: http://arxiv.org/abs/2511.02872v2
- Date: Thu, 06 Nov 2025 03:30:44 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-07 13:46:06.499775
- 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が研究レベルの公式な数学的推論への道筋に不可欠なチェックポイントを確立する、堅牢で挑戦的なベンチマークを提供すると考えている。
関連論文リスト
- From Abstract to Contextual: What LLMs Still Cannot Do in Mathematics [79.81905350372067]
我々は文脈的数学的推論を通してギャップを研究する。
AIMEとMATH-500の問題を2つのコンテキスト設定に再利用するベンチマークであるContextMATHを紹介する。
オープンソースモデルはSGとCSで13、34ポイント減少し、プロプライエタリモデルは13、20ポイント減少している。
論文 参考訳（メタデータ） (2026-01-30T14:56:04Z) - RIDE: Difficulty Evolving Perturbation with Item Response Theory for Mathematical Reasoning [26.91583214616048]
大規模言語モデル (LLM) は数学的推論において高い性能を達成する。
現在の規則に基づく摂動法は、しばしば不適切な質問を発生させる。
本稿では,新しい逆問題書き換えフレームワーク RIDE を提案する。
論文 参考訳（メタデータ） (2025-11-06T07:10:17Z) - Proof2Hybrid: Automatic Mathematical Benchmark Synthesis for Proof-Centric Problems [9.041749463376599]
本稿では,自然言語の数学的コーパスから高品質な証明中心ベンチマークを合成するフレームワークProof2Hybridを提案する。
我々のフレームワークとベンチマークは、AIシステムの数学的インテリジェンスに関する、より深い研究の波の道を開く。
論文 参考訳（メタデータ） (2025-08-04T08:59:36Z) - Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving [48.22540519786074]
最近の研究では、非公式な精度は80%を超え、公式な成功はPutnamBenchのようなベンチマークで8%以下である。
低レベルの証明生成から高レベルの推論を分離する新しいフレームワークを提案する。
提案手法は,2000年以降のIMO問題に対して,従来のオープンソース証明者が未報告の課題として評価した。
論文 参考訳（メタデータ） (2025-07-07T22:38:49Z) - 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) - Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem
Understanding [74.12405417718054]
本稿では,中国初の数学的事前学習言語モデル(PLM)を提示することにより,機械の数学的知性向上を目指す。
他の標準のNLPタスクとは異なり、数学的テキストは問題文に数学的用語、記号、公式を含むため理解が難しい。
基礎課程と上級課程の両方からなる数学PLMの学習を改善するための新しいカリキュラム事前学習手法を設計する。
論文 参考訳（メタデータ） (2022-06-13T17:03:52Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。