Herald Statements, Herald Proofs

从README中的描述来看，这是Mathlib 4的注释数据集和最新翻译模型，用于自动形式化。

As described in the README, this is an annotated dataset of Mathlib 4 and the latest translation model for automated formalization.

原始信息汇总

Herald: A Natural Language Annotated Lean 4 Dataset

数据集概述

• 数据集名称：Herald
• 数据集类型：自然语言注释的Lean 4数据集
• 数据集来源：Mathlib 4

数据集下载

数据集	下载链接
Herald Statements	HuggingFace
Herald Proofs	HuggingFace

模型

模型	下载链接
Herald Translator	HuggingFace

评估结果

模型	miniF2F-test	miniF2F-valid	extract-theorems	college-math-CoT
TheoremLlama	50.1%	55.6%	4.0%	3.0%
InternLM2-Math-Plus-7B	73.0%	80.1%	7.5%	6.5%
Herald	96.7%	96.3%	23.5%	16.0%

快速开始

环境要求

1. 代码测试环境为 vllm >= 0.6.6
2. 运行推理需要 leantest 环境，包含 repl 用于Lean编译器检查。代码测试版本为 v4.11.0，可在此获取 链接

简单推理

1. 在 config.py 中配置偏好模型和设置，用于回译和NLI检查。测试环境使用 InternLM2-Math-Plus 7B 进行回译，Deepseek V2.5 进行NLI检查。

2. 使用脚本运行模型。

   bash

   翻译并验证翻译后的陈述

   python -m run_translate_verify example/test.json example/test_result.json

   进行回译和NLI检查

   python -m run_backtrans_nli example/test_result.json

在数据集上实验

完成 config.py 中的配置，并运行脚本 bash run_pipeline.sh <data.json>。可以将自己的数据集放在 ./data 目录下。结果检查在 ./data/results。

搜集汇总

数据集介绍

构建方式

Herald Statements与Herald Proofs数据集，系从Mathlib 4中提取并注解而构建。该数据集旨在为自动形式化提供支持，通过数学库的语句及证明过程，为机器学习模型提供训练素材。

特点

该数据集具备以下特点：一是来源权威，源自Mathlib 4的原始数据；二是包含丰富的数学语句与证明，为研究提供了多样化的样本；三是经过专业注解，提高了数据集的质量与可用性。

使用方法

使用该数据集，用户需配置适当的编程环境，如vllm版本不低于0.6.6，以及包含repl的leantest环境。用户可通过修改config.py文件来设置模型和参数，使用提供的脚本进行翻译验证和反向翻译以及NLI检查。此外，用户亦可自行添加数据至./data目录下，并执行脚本进行实验。

背景与挑战

背景概述

在数学形式化领域，自动形式化技术的研究正日益受到重视。Herald数据集在这样的背景下应运而生，由FrenzyMath团队于近期创建并发布。该数据集源自Mathlib 4，旨在通过注释的自然语言文本促进自动形式化模型的开发。Herald数据集的推出，不仅提供了丰富的实验资源，而且对于促进数学知识的形式化表示与自动化推理研究具有重要意义。

当前挑战

Herald数据集在构建过程中面临的挑战主要包括两个方面：一是如何确保自然语言注释的准确性与一致性，这对于提高自动形式化模型的性能至关重要；二是如何处理数学证明中的复杂结构和逻辑关系，这是自动形式化技术中的核心难题。此外，数据集在解决数学领域问题时，还需克服如何有效评估模型性能的问题，这在Herald数据集的评估结果中可见一斑，例如在college-math-CoT任务上的表现仍有提升空间。

常用场景

经典使用场景

在数学公式自动形式化的研究领域，Herald数据集及其配套的翻译模型，被广泛用于评估和提升自然语言到形式化数学表述的转换能力。该数据集通过Mathlib 4的注释，提供了丰富的自然语言表述与对应的形式化数学定理，成为检验自动形式化系统性能的标准资源。

衍生相关工作

基于Herald数据集，研究者们进一步开展了诸如定理自动证明、数学公式理解与生成等经典工作，推动了形式化数学语言处理技术的发展，并促进了数学与计算机科学的深度融合。

数据集最近研究

最新研究方向

在数学公式自动化领域，Herald数据集以其对Mathlib 4的详尽注释，以及搭配的Herald Translator模型，成为当前研究的热点。该数据集的发布，旨在推进数学公式自动化的进程，特别是在自然语言处理与形式化验证的交叉领域。近期研究集中于提高模型在自动化证明生成和定理提取方面的性能，如Herald在college-math-CoT指标上达到的16.0%的正确率，显著优于其他模型，这对于数学教育以及自动化推理系统的发展具有重要的实际意义。