MLFMF：用于数学形式化的机器学习数据集
MLFMF: Data Sets for Machine Learning for Mathematical Formalization
AI总结：
本文提出 MLFMF 数据集，用于基准测试支持数学形式化的推荐系统，涵盖 Agda 和 Lean 库的异构网络与 s-表达式，并基于多种算法提供基线结果，是目前最大的机器可读形式化数学知识集合。
摘要：
我们引入了 MLFMF，这是一组用于对推荐系统进行基准测试的数据集，这些推荐系统用于支持使用证明助手进行数学形式化。这些系统帮助人类识别哪些先前的条目（定理、构造、数据类型和公设）与证明新定理或进行新构造相关。每个数据集均源自使用证明助手 Agda 或 Lean 编写的形式化数学库。该集合包括最大的 Lean 4 库 Mathlib，以及一些最大的 Agda 库：标准库、一元数学库 Agda-unimath 和 TypeTopology 库。每个数据集以两种方式表示相应的库：作为异构网络，以及作为表示库中所有条目语法树的 s-表达式列表。网络包含库的（模块化）结构和条目之间的引用，而 s-表达式提供关于每个条目的完整且易于解析的信息。我们报告了使用标准图和词嵌入、树集成以及基于实例的学习算法的基线结果。MLFMF 数据集为进一步研究形式化数学的众多机器学习方法提供了坚实的基准测试支持。用于提取网络和 s-表达式的方法论可直接应用于其他库，并适用于其他证明助手。总条目超过 250,000 个，这是目前机器可读格式中最大的形式化数学知识集合。
英文摘要：
We introduce MLFMF, a collection of data sets for benchmarking recommendation systems used to support formalization of mathematics with proof assistants. These systems help humans identify which previous entries (theorems, constructions, datatypes, and postulates) are relevant in proving a new theorem or carrying out a new construction. Each data set is derived from a library of formalized mathematics written in proof assistants Agda or Lean. The collection includes the largest Lean~4 library Mathlib, and some of the largest Agda libraries: the standard library, the library of univalent mathematics Agda-unimath, and the TypeTopology library. Each data set represents the corresponding library in two ways: as a heterogeneous network, and as a list of s-expressions representing the syntax trees of all the entries in the library. The network contains the (modular) structure of the library and the references between entries, while the s-expressions give complete and easily parsed information about every entry. We report baseline results using standard graph and word embeddings, tree ensembles, and instance-based learning algorithms. The MLFMF data sets provide solid benchmarking support for further investigation of the numerous machine learning approaches to formalized mathematics. The methodology used to extract the networks and the s-expressions readily applies to other libraries, and is applicable to other proof assistants. With more than $250\,000$ entries in total, this is currently the largest collection of formalized mathematical knowledge in machine learnable format.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
