FATE benchmarks

FATE（形式代数定理评估）基准包含三个抽象代数和交换代数基准：FATE-M（150个练习）、FATE-H（100个练习）和FATE-X（100个练习）。所有练习都用Lean形式化，问题来源于本科和研究生教材、期末考试和博士资格考试以及研究文献。三个基准的难度逐渐增加：FATE-M主要是标准教科书练习（基础级别），FATE-H包含抽象/交换代数期末考试中的挑战性问题，FATE-X包括博士资格考试级别及更高难度的问题。

FATE (Formal Algebraic Theorem Evaluation) benchmark includes three abstract and commutative algebra benchmarks: FATE-M (150 exercises), FATE-H (100 exercises), and FATE-X (100 exercises). All exercises are formalized in Lean, with problems sourced from undergraduate and graduate textbooks, final examinations, doctoral qualifying examinations, and research literature. The three benchmarks feature increasing difficulty: FATE-M mainly comprises standard textbook exercises at the basic level, FATE-H includes challenging problems from abstract/commutative algebra final examinations, and FATE-X covers problems at the doctoral qualifying examination level and above.

原始信息汇总

FATE 数据集概述

数据集简介

FATE（Formal Algebra Theorem Evaluation）基准测试集包含抽象代数和交换代数领域的三个基准测试：

• FATE-M（150道习题）
• FATE-H（100道习题）
• FATE-X（100道习题）

所有习题均使用Lean语言形式化。

数学难度级别

• FATE-M：主要包含标准教材习题（基础水平）
• FATE-H：包含抽象代数/交换代数期末考试中的挑战性问题
• FATE-X：包含博士资格考试级别及更高难度的问题

问题来源包括：

• 本科和研究生教材
• 期末考试和博士资格考试
• 研究文献

基准结构

每个基准的Lean文件包含：

• 一个完全形式化的陈述
• 单个sorry占位符
• 开头适当的开放命名空间
• 陈述前的自然语言注释

结构差异：

• FATE-M和FATE-H：不包含额外定义
• FATE-X：在陈述前形式化了最小依赖定义

使用建议

为方便用户，每个基准提供PDF文件和JSON文件以便阅读和使用。

强烈建议不要合并这些基准，原因：

• 难度级别显著不同
• 形式化特征各异

问题分布

附加信息

FATE-M基准是以下文献中引用基准的重构版本： REAL-Prover: Retrieval-Augmented Lean Prover for Mathematical Reasoning

搜集汇总

数据集介绍

构建方式

在抽象代数与交换代数领域，FATE基准数据集通过系统化采集与严谨形式化构建而成。其问题来源涵盖本科至研究生教材习题、期末考试与博士资格考题以及前沿研究文献，确保数学内容的广度与深度。所有问题均采用Lean定理证明器进行形式化编码，每个文件包含完整的形式化陈述、单一待证明目标及自然语言注释，FATE-X还额外引入了最小依赖定义以支持高阶问题表达。

特点

该数据集最显著的特征在于其分层难度设计与学科专业性。FATE-M聚焦基础教科书习题，FATE-H收录抽象代数考试难题，FATE-X则涉及博士水平及以上的高阶理论问题。三者均配备自然语言注释与形式化语句的双重表达，并通过可视化图表展示数学范畴分布。数据集严格避免难度混合，每个基准保持独立的形式化特性与数学逻辑一致性，为代数推理研究提供精准评估维度。

使用方法

使用者可通过提供的PDF文件快速浏览自然语言问题描述，或利用JSON文件进行程序化数据处理。建议根据研究目标选择单一基准开展实验：基础教育验证可选用FATE-M，高阶推理任务则适配FATE-H或FATE-X。所有问题均以Lean代码形式呈现，需在定理证明环境中加载相关命名空间后，针对标记为`sorry`的待证明目标开展形式化验证。数据集支持机器学习模型在代数自动推理领域的性能评估与对比研究。

背景与挑战

背景概述

FATE基准数据集由形式代数定理评估研究团队于2025年创建，专注于抽象代数与交换代数领域的定理形式化验证。该数据集包含FATE-M、FATE-H和FATE-X三个难度递增的子集，涵盖从本科教材习题到博士资格考试的数学问题，全部采用Lean定理证明器进行形式化表述。作为数学自动化推理领域的重要资源，FATE为形式化数学和机器学习交叉研究提供了标准化评估框架，显著推动了定理自动证明技术的发展。

当前挑战

该数据集核心挑战在于解决高阶数学定理的形式化验证问题，需要克服数学概念的形式化表示、复杂代数结构的机器可读编码以及跨难度级别的统一评估标准建立等难题。在构建过程中，研究团队面临数学知识的多层次标注、Lean语言规范的一致性维护以及不同来源习题的难度分级等具体挑战，特别是如何保持原始数学语义与形式化表述之间的精确对应关系。

常用场景

经典使用场景

在形式化数学与自动定理证明领域，FATE benchmarks作为代数定理的形式化评估基准，其经典应用场景主要集中于测试和验证定理自动证明系统的性能。研究者利用FATE-M、FATE-H和FATE-X三个难度递增的子集，系统评估证明助手在抽象代数与交换代数问题上的推理能力，尤其适用于衡量基于检索增强或大语言模型的自动证明方法在严格数学语境下的效果。

解决学术问题

FATE benchmarks有效解决了形式化数学中自动定理证明的评估标准化问题，为学术界提供了难度分级明确、来源权威的代数问题集。它使得研究者能够量化比较不同证明系统的代数推理能力，尤其缓解了以往评估中缺乏高质量、可复现形式化问题集的困境。该数据集推动了自动推理领域在严谨数学分支上的科学评估方法发展，对形式化数学与人工智能交叉研究具有奠基性意义。

衍生相关工作

FATE benchmarks已催生多项重要研究工作，其中最显著的是REAL-Prover（检索增强的Lean证明器），该系统利用FATE-M进行训练与评估，实现了检索增强技术与定理证明的深度融合。该数据集还促进了形式化数学领域对大语言模型代数推理能力的系统性评估，衍生出多个结合神经网络与符号推理的混合证明框架，推动了自动定理证明在代数结构处理方面的前沿探索。