FATE：面向多难度层级的前沿代数形式化基准系列
FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
AI总结：
FATE是一个面向多难度层级的前沿代数形式化基准系列，旨在评估和推动高级数学推理能力。
摘要：
近年来，大语言模型（LLMs）在形式化定理证明方面的进展令人印象深刻，特别是在像IMO这样的竞赛型数学基准测试中。然而，这些竞赛并不能反映现代数学研究的深度、广度和抽象性。为弥合这一差距，我们引入了FATE（Formal Algebra Theorem Evaluation），一个新的形式化代数基准系列，旨在为高级数学推理开辟道路。我们提出了两个新组件，FATE-H和FATE-X，每个组件包含100道抽象和交换代数问题。FATE系列覆盖了从本科生练习到超过博士资格考试难度的难度范围。值得注意的是，FATE-X是首个超过博士级别考试难度并覆盖Mathlib库的正式基准。我们对最先进的LLM证明者在该新基准上的评估揭示了与竞赛数学相比的显著性能差距：最佳模型在FATE-H上仅达到3%（pass@64）的准确率，在FATE-X上为0%。我们的两阶段评估显示，模型的自然语言推理准确性明显高于其形式化这一推理的能力。我们系统地分类了在这一形式化过程中出现的常见错误。此外，一项比较研究显示，专门的证明者在自然语言阶段的准确性可能低于通用模型，从而减少其准确性。我们相信FATE提供了一个稳健且具有挑战性的基准，为研究级形式化数学推理建立了必要的检查点。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
