构建首个覆盖博士考题难度的代数定理证明基准，揭示大模型在形式化推理中的严重短板。
FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels
- 设计FATE-H与FATE-X两个代数难题集，涵盖本科到博士级难度
- 顶尖模型在FATE-H上仅3%准确率，FATE-X为0%，暴露出形式化能力不足
- 揭示自然语言推理优于形式化转化，适合研究形式化数学推理的团队
大型语言模型在数学竞赛类定理证明任务（如IMO）中表现优异，但这些竞赛无法反映现代数学研究的深度、广度与抽象性。为此，我们提出FATE（Formal Algebra Theorem Evaluation），一个面向形式代数的新基准系列，旨在推动高级数学推理的发展。本工作包含两个新组件：FATE-H与FATE-X，各含100道抽象代数与交换代数问题，难度覆盖从本科练习题到超过博士资格考试水平的问题。值得注意的是，FATE-X是首个在难度和数学库覆盖范围上均超越博士级考试与Mathlib库的正式基准。对当前先进大模型证明器的评估显示，在FATE-H上最佳模型仅达3%（pass@64）准确率，在FATE-X上为0%。两阶段评估表明，模型的自然语言推理能力显著高于其形式化推理能力。我们系统归类了形式化过程中的常见错误。此外，对比研究发现，专用证明器在自然语言阶段的反思能力反而低于通用模型，导致整体准确率下降。我们认为FATE提供了一个强大且具有挑战性的基准，为迈向研究级形式化数学推理设立了关键里程碑。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。