Con-NF

Con-NF是一个基于Lean 4 Con(NF)构建的新型自动形式化基准，包含961个基于不同于Mathlib 4的理论基础的定理，以及1,348个形式对象及其非形式化版本。

Con-NF is a novel automated formalization benchmark built upon Lean 4 Con(NF). It contains 961 theorems based on a theoretical foundation distinct from that of Mathlib 4, as well as 1,348 formal objects along with their informal counterparts.

原始信息汇总

Rethinking Statement Autoformalization Dataset Overview

数据集简介

本文提供了对研究论文《Rethinking and Improving Autoformalization: Towards a Faithful Metric and a Dependency Retrieval-based Approach》的官方实现数据集的概述。该数据集旨在评估自动形式化语句的准确性和依赖检索方法。

数据集组成

• Autoformalization Benchmarks: 包含基于Lean 4 Con(NF)构建的新型自动形式化基准Con-NF，以及现有基准ProofNet、MiniF2F、PutnamBench。Con-NF基准包含961个定理和1348个形式对象及其非形式化描述。
• Human Equivalence Benchmark: 包含200个类型检查的模型生成形式语句及其地面真实对照。
• Library: 包含形式对象及其非形式化描述的库。

数据集结构

• Autoformalization Benchmarks (data/{connf, proofnet}/benchmark.jsonl):

  • informal_stmt: 非形式化语句
  • formal_stmt: 形式化语句
  • header: 形式化语句的头部信息
  • proof_state: 形式化语句的初始证明状态
  • mathlib_dependencies: 导入库的依赖
  • hard_dependencies: 导入库外的依赖
  • source: 问题来源
  • problem_name: 问题的原始名称
  • full_name: 问题的完整名称

• Human Equivalence Benchmark (data/human_equivalence/{o1-generated, rautoformalizer-generated}):

  • autoformalization.json: 组织样本为ProofNet基准的自动形式化结果
  • labels.json: 存储每个样本的人类注释等价标签

• Library (data/{connf, proofnet}/library.jsonl):

  • full_name: 形式对象的完整名称
  • url: 对象文档页面的URL
  • code_src: 对象的源代码
  • ptype: 对象的类型
  • header: 对象的声明
  • code: 对象的源代码
  • additional_info: 额外信息
  • used_premises: 对象的依赖
  • def_path: 对象源文件的路径
  • pos: 源代码在源文件中的位置
  • informalization: 对象的非形式化描述

评估指标

• Equivalence Metrics: 评估人类等价性基准的指标，包括精确度、召回率和准确率。
• Dependency Retrieval: 评估依赖检索的指标，包括Recall@5和Precision@5。

使用说明

• 数据集的使用和评估需要安装特定的Python依赖和Lean 4依赖。
• 提供了详细的评估命令和参数设置。

引用

• 如果您的研究中使用了这个数据集，请引用相应的论文。

许可

• 该项目遵循Apache 2.0许可。

联系方式

• 如有疑问或讨论，可通过问题/电子邮件与作者联系。

搜集汇总

数据集介绍

构建方式

Con-NF数据集的构建基于Lean 4的Con(NF)理论，涵盖了961个定理及1348个形式对象和它们的非形式化描述。这些定理基于与Mathlib 4不同的理论体系，旨在评估自动化形式化工具在研究级数学上的泛化能力。

特点

Con-NF数据集的特点在于它包含基于不同理论基础的形式化定理，这为评估自动化形式化工具在非Mathlib 4理论基础上的性能提供了可能。数据集提供了形式语句、非形式描述、依赖关系等多种信息，有助于深入研究形式化方法。

使用方法

使用Con-NF数据集，研究者可以复制相应的autoformalization.json文件到输出路径，并根据需要调整环境变量和模型路径。通过运行提供的Python脚本，可以评估不同方法在数据集上的性能，例如BEq、Def Equiv等评价指标。

背景与挑战

背景概述

Con-NF数据集是在上海交通大学计算机科学与人工智能学院的研究背景下创建的，由Qi Liu、Xinhao Zheng、Xudong Lu、Qinxiang Cao和Junchi Yan等研究人员共同工作成果。该数据集的构建旨在评估自动化语句自动形式化的性能，特别是在数学领域的研究级数学问题上。Con-NF基于Lean 4的Con(NF)理论，包含了961个定理及其形式对象和它们的非正式描述，为自动化形式化提供了一个新的基准。这一数据集的创建对于推动数学自动化形式化领域的发展具有重要意义。

当前挑战

Con-NF数据集在构建过程中遇到的挑战主要包括：1) 如何确保所选定理的代表性，以覆盖不同难度级别的数学问题；2) 如何准确捕捉和表示数学定理的非正式描述，以利于机器学习模型的训练和推理；3) 在构建自动化形式化指标时，如何处理和评估形式化语句与人类生成的语句之间的一致性。此外，数据集在解决领域问题，如数学定理的自动化形式化时，也面临着如何提高形式化准确性和效率的挑战。

常用场景

经典使用场景

Con-NF数据集是针对自动形式化任务的评估而构建的，其经典使用场景在于为自动形式化系统提供一套基于Lean 4理论的不同于Mathlib 4的定理，以评估这些系统在非分布一般化能力和研究级数学上的表现。该数据集包含了961个定理和1348个形式对象及其非正式描述，为研究者提供了一个全面且具有挑战性的测试平台。

实际应用

在实际应用中，Con-NF数据集可用于训练和评估自动形式化工具，帮助研究者开发出能够准确地将自然语言数学表述转化为形式化语言的算法。此外，它还可以作为教育工具，帮助学生学习形式化方法和 Lean 4 的使用。

衍生相关工作

基于Con-NF数据集，研究者已经进行了一系列相关工作，包括开发了新的自动形式化工具、提出了改进的评估指标，以及探索了依赖检索在自动形式化中的应用。这些衍生工作进一步扩展了Con-NF数据集的应用范围，并推动了数学自动化领域的发展。