FormalML

FormalML是一个用于评估机器学习理论中形式子目标完成的基准数据集。

FormalML is a benchmark dataset designed to evaluate the achievement of formal sub-objectives in machine learning theory.

原始信息汇总

FormalML数据集概述

数据集基本信息

• 名称：FormalML
• 类型：机器学习理论中的形式化子目标完成评估基准
• 相关论文：NeurIPS25 (Datasets and Benchmarks Track) submission "FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theory"
• 托管平台：
  • GitHub: https://github.com/njuyxw/FormalML
  • Hugging Face: https://huggingface.co/datasets/zzhisthebest/LeanBenchmark

数据来源

数据集基于以下两个库构建：

1. optlib (fork版本): https://github.com/Lizn-zn/optlib
2. lean-rademacher: https://github.com/njuyxw/lean-rademacher

数据提取工具

依赖项

• lean-repl: https://github.com/leanprover-community/repl

安装步骤

1. 更新并构建AutoML
2. 更新并构建lean-repl
3. 运行提取脚本run_all.sh

输出目录

• 生成的基准文件保存在: ./AutoML/FormalML

目录结构

extraction/ ├── AutoML/ │ ├── FormalML/ # 输出基准文件 │ └── ... # AutoML相关代码 ├── repl/ # lean-repl依赖 ├── run_all.sh # 定理提取脚本

注意事项

• 需要安装Python以运行提取脚本
• 需要正确安装Lean和lake并添加到PATH中

评估框架

评估步骤

1. 证明生成 bash cd evaluation python generation.py --prover_name deepseek_v15_rl --gpu 4 --dataset_path "zzhisthebest/LeanBenchmark" --n 32

2. 评估设置

   • 使用修改版的kimina-lean-server(适配Lean 4.18.0)

3. 运行评估 bash python eval.py --input_file file_name

搜集汇总

数据集介绍

构建方式

在机器学习理论的形式化子目标完成评估领域，FormalML数据集的构建体现了严谨的学术方法论。研究团队通过精心设计的自动化流程，从optlib和lean-rademacher两个核心数学库中提取定理数据。技术实现上采用Lean定理证明器的生态系统，包括lean-repl依赖和lake构建工具，通过Python脚本实现批量提取。数据生成过程严格遵循形式化验证规范，最终输出结构化的基准测试文件，为机器学习理论的形式化验证建立了标准化评估体系。

特点

该数据集作为机器学习理论形式化验证的基准测试平台，具有鲜明的专业特性。其核心价值在于收录了经过严格形式化验证的数学定理集合，覆盖优化理论和概率论等机器学习基础领域。数据集采用层次化存储结构，支持模块化访问和扩展。特别值得注意的是，数据集与Lean4.18.0证明环境深度集成，确保验证过程的数学严谨性，同时提供与HuggingFace平台的无缝对接，极大提升了数据可及性和研究复现效率。

使用方法

研究人员可通过标准化工作流高效利用该数据集。使用前需配置Lean证明环境及GPU计算资源，通过专用脚本实现定理数据的批量生成与提取。评估框架采用模块化设计，分阶段执行证明生成和环境验证：首先生成阶段调用深度学习证明器处理基准数据，随后通过定制化的kimina-lean-server进行形式化验证。整个流程支持分布式计算和参数调优，输出结果包含详尽的验证指标，为比较不同证明方法的有效性提供量化依据。

背景与挑战

背景概述

FormalML数据集作为机器学习理论领域的重要基准，由NeurIPS'25数据集与基准赛道的提交团队开发，旨在评估形式化子目标完成的能力。该数据集基于optlib和lean-rademacher等开源库构建，专注于形式化验证与定理证明在机器学习理论中的应用。其核心研究问题在于如何通过形式化方法验证机器学习算法的理论性质，为研究者提供了一个标准化的评估平台，推动了形式化验证与机器学习交叉领域的发展。

当前挑战

FormalML数据集面临的挑战主要体现在两个方面：其一，在解决领域问题上，形式化验证在机器学习理论中的应用仍处于探索阶段，如何准确捕捉和验证复杂的理论性质成为关键难题；其二，在构建过程中，数据集的生成依赖于多源库的整合与自动化脚本的执行，确保数据的一致性与可复现性需要克服技术上的复杂性。此外，评估框架的搭建涉及对Lean等专业工具的深度定制，进一步增加了技术实现的难度。

常用场景

经典使用场景

在机器学习理论研究中，FormalML数据集为评估形式化子目标完成提供了一个标准化的测试平台。该数据集通过提取optlib和lean-rademacher等库中的定理，构建了一个丰富的数学形式化任务集合。研究人员可以借助这一基准，系统地评估不同自动证明方法在形式化数学子目标上的表现，从而推动机器学习与形式化方法的交叉研究。

实际应用

在实际应用中，FormalML数据集可广泛应用于自动定理证明系统的开发与优化。工业界的研究团队可利用该数据集训练和验证新型神经网络证明器，提升其在数学软件辅助验证中的实用性。教育领域也可借助这一资源，设计更高效的形式化数学教学工具，帮助学生理解抽象数学概念的形式化表达过程。

衍生相关工作

基于FormalML数据集，学术界已衍生出多项重要研究工作。其中包括改进的神经网络证明架构、新型交互式定理证明界面，以及结合大语言模型的形式化方法。这些工作不仅扩展了数据集的应用边界，也为形式化数学与机器学习的深度融合开辟了新方向，推动了整个领域的技术进步。