miniF2F-rocq

一个包含高中级别数学问题的数据集，该数据集已经被形式化在Lean、Isabelle/HOL和MetaMath中，现在本项目旨在将其形式化在Rocq中，以扩展其作为未来研究自动化证明评估基准的效用。

A dataset containing high-school level mathematical problems has been formalized in Lean, Isabelle/HOL, and MetaMath. The present project aims to formalize this dataset in Rocq, thereby extending its utility as a benchmark for automated theorem proving evaluation in future research.

原始信息汇总

数据集概述：miniF2F-rocq

数据集简介

• 数据集名称：miniF2F-rocq
• 研究领域：大型语言模型（LLMs）在形式化证明中的应用
• 数据集用途：评估机器学习基于自动证明技术的性能

数据集特点

• 数据集来源：miniF2F
• 包含内容：高中水平数学问题的形式化定理
• 支持的证明系统：Lean, Isabelle/HOL, MetaMath, Rocq（正在进行形式化）

数据集形式化

• 目标：在Rocq系统中形式化miniF2F数据集，以便作为自动化证明评估的可靠基准
• 形式化进度：正在审计过程中，目前进度为0%

数据集审计

• 审计目的：确保Rocq版本miniF2F的定理表述对证明开发尽可能友好
• 审计进度：正在进行中
• 贡献者：感谢所有参与审计和精炼定理表述的贡献者

相关链接

• miniF2F原始数据集

搜集汇总

数据集介绍

构建方式

miniF2F-rocq数据集的构建旨在将数学定理从一种证明辅助系统自动翻译至另一种。该数据集以miniF2F为基础，该基础数据集包含了高中学水平的数学问题，并已在Lean、Isabelle/HOL和MetaMath中形式化。本项目通过人工审核及修正，确保了在Rocq中的形式化准确性与可靠性。

特点

该数据集的特点在于其跨证明辅助系统的可翻译性，以及为机器学习自动证明技术提供了一个多元化的评估标准。此外，经过严格审核，其定理表述对于证明开发尤为友好，增强了数据集的实用性和在自动化证明评估中的可靠性。

使用方法

使用miniF2F-rocq数据集时，研究者可以将其作为训练或评估自动证明技术的基准。数据集包含的定理已通过类型检查，确保了与原始自然语言及Isabelle和Lean中定理表述的一致性。用户需遵循项目提供的审核流程，以进一步优化定理表述，提高证明效率。

背景与挑战

背景概述

miniF2F-rocq数据集的构建源于对大型语言模型（LLMs）在自动证明生成领域的研究。该数据集的创建旨在探索LLMs是否能够实现不同证明助手之间的形式化定理自动翻译。该数据集由Facebook研究团队开发，以miniF2F为基础，该基础数据集已在学校级别的数学问题上得到广泛应用，并作为评估机器学习辅助证明技术的标准。miniF2F-rocq数据集的创建进一步拓宽了其在自动化证明评估中的效用，并针对Rocq证明系统进行了专门的适配。

当前挑战

该数据集面临的挑战主要包括：不同证明助手之间的翻译准确性和效率问题，以及确保定理表述对证明开发尽可能友好。此外，构建过程中需进行严格的审核流程，以保证翻译定理的正确性和可靠性。目前，审核进度尚未完成，仍需领域专家的参与和贡献。

常用场景

经典使用场景

在机器学习与形式化证明领域交叉的研究中，miniF2F-rocq数据集被广泛作为评价基准，用于检验大型语言模型在不同证明助手之间的定理翻译能力。该数据集选取了高中级别的数学问题，这些问题已被形式化在Lean、Isabelle/HOL和MetaMath等证明辅助系统中，研究者可借此数据集评估模型在形式化证明翻译任务上的表现。

实际应用

实际应用中，miniF2F-rocq数据集不仅为机器学习算法的训练和评估提供了标准平台，其形式化的数学定理库还可用于教育领域，辅助学生和教师理解和掌握数学证明的原理和方法。

衍生相关工作

基于miniF2F-rocq数据集的研究已经催生了多项相关工作，包括但不限于对翻译后定理的审计流程优化、新型证明辅助系统的开发，以及针对特定数学领域的问题进行模型定制化训练等，进一步拓宽了该数据集在学术研究和实际应用中的影响。