FATE (Formal Algebra Theorem Evaluation)

FATE数据集是形式代数领域的新基准系列，旨在推动高级数学推理的发展。该系列包括FATE-H和FATE-X两个新组件，每个组件包含100个问题，涵盖从本科练习到超出博士资格考试的问题。FATE-X是第一个超过博士水平考试难度和Mathlib库覆盖范围的正式基准。该数据集由专家数学家选择并正式化，以确保质量和原创性，适用于评估从本科到博士资格考核的正式推理。The FATE dataset is a new benchmark series in the field of formal algebra, aimed at advancing advanced mathematical reasoning. This series comprises two novel components, FATE-H and FATE-X, each consisting of 100 problems ranging from undergraduate-level exercises to questions beyond the difficulty of doctoral qualifying examinations. FATE-X is the first formal benchmark that surpasses both the difficulty of doctoral-level qualifying exams and the coverage breadth of the Mathlib library. This dataset is curated and formalized by expert mathematicians to guarantee quality and originality, and is tailored for evaluating formal reasoning across undergraduate to doctoral qualifying exam levels.

原始信息汇总

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文件。

使用警告

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

• 难度级别显著不同
• 形式化特征存在明显差异

问题分布

数学类别分布图：https://raw.githubusercontent.com/frenzymath/FATE/main/assets/FATE-H&X-sunburst.svg

附加信息

FATE-M基准是以下论文中引用基准的重构版本： https://arxiv.org/abs/2505.20613

搜集汇总

数据集介绍

构建方式

在代数形式化验证领域，FATE数据集的构建遵循严谨的专家协作流程。研究团队从超过20部权威教材、博士资格考试题及前沿研究文献中筛选出400个候选问题，通过纯代数领域的博士后与博士专家团队进行四轮联合评审，最终确定200个问题进入形式化阶段。由五位Mathlib核心贡献者组成的专业团队通过五次专题研讨会，将精选问题转化为Lean语言的形式化表述，并经过双重专家审核确保数学严谨性与形式化准确性。整个过程融合了数学深度与形式化专业性的双重标准，建立了从本科到博士资格考试的渐进式难度体系。

特点

FATE系列最显著的特征在于其阶梯式难度架构与前沿研究导向。数据集涵盖抽象代数与交换代数两大核心领域，其中FATE-H聚焦研究生层次的荣誉课程难题，FATE-X则突破性地达到博士资格考试难度并超越Mathlib库现有覆盖范围。该数据集特别设计了新型定义前置的独特形式化特征，要求模型在解决过程中自主推导引理并构建数学对象。问题分布呈现从群论、域论向深度交换代数的结构性转变，通过合成分析与递归结构分析等复杂推理模式，有效模拟了现代数学研究中的抽象思维过程。

使用方法

该数据集采用双阶段评估框架进行模型验证。研究者在输入阶段同时提供问题的自然语言描述与Lean形式化语句，观察模型首先生成自然语言证明链、继而转化为形式化代码的推理过程。评估时分别采用专家人工评审与Lean内核自动验证的双重机制：对自然语言推理阶段使用Pass@1指标由代数专家评估逻辑严谨性，对形式化代码阶段使用Pass@64指标通过Lean REPL进行多进程并行验证。这种解耦式评估方法能精准定位模型在数学推理与形式化转换中的能力瓶颈，为研究级数学推理的系统性评测提供标准化范式。

背景与挑战

背景概述

FATE（Formal Algebra Theorem Evaluation）基准系列由西湖大学、北京大学等机构的研究团队于2025年提出，旨在弥合竞赛数学与现代数学研究之间的鸿沟。该系列包含FATE-M、FATE-H与FATE-X三个难度递增的代数基准，覆盖从本科习题到超越博士资格考试的数学问题。研究团队通过数学家与形式化专家的协同工作，从经典教材、博士资格考试题及前沿研究文献中筛选并形式化问题，聚焦抽象代数与交换代数领域，强调抽象证明与结构研究，为评估形式化数学推理能力提供了系统化工具。

当前挑战

FATE基准面临双重挑战：在领域问题层面，其旨在解决高级数学推理的形式化验证难题，要求模型掌握深层次抽象概念与递归结构分析能力，而当前最优模型在博士级难度的FATE-X上准确率仍为零；在构建过程中，需克服数学专家与形式化专家协同工作的复杂性，确保问题在保持数学深度的同时具备可形式化特性，且需处理Mathlib库未覆盖的新定义，要求模型具备自主构建辅助引理的能力。

常用场景

经典使用场景

在形式化代数定理证明领域，FATE数据集作为前沿基准测试系列，其经典使用场景聚焦于评估大型语言模型在抽象代数与交换代数中的形式化推理能力。该数据集通过构建从本科习题到博士资格考试级别的渐进难度结构，系统性地检验模型在代数结构研究中的定理形式化表现，特别是对群论、环论和域论等核心代数分支的覆盖深度。

解决学术问题

FATE数据集有效解决了形式化数学推理领域的关键学术问题，填补了竞赛数学与现代数学研究之间的评估鸿沟。通过设计超越Mathlib库覆盖范围的前沿代数问题，该数据集揭示了当前模型在高级数学形式化中的核心瓶颈——自然语言推理与形式化代码生成之间的能力断层，为研究级数学自动证明提供了关键的评估基准。

衍生相关工作

基于FATE数据集衍生的经典工作主要集中在形式化定理证明的方法论创新上。深度强化学习在形式化证明中的应用研究通过该数据集验证了子目标分解策略的有效性，同时催生了专门针对代数结构的形式化证明器开发。这些工作进一步推动了自然语言推理与形式化生成解耦的研究方向，为构建下一代数学推理系统奠定了基础。