MLFMF: Data Sets for Machine Learning for Mathematical Formalization

要約

証明アシスタントによる数学の形式化をサポートするために使用されるベンチマーク推奨システムのデータ セットのコレクションである MLFMF を紹介します。
これらのシステムは、人間が新しい定理の証明や新しい構築の実行に関連する以前のエントリ (定理、構築、データ型、公準) を識別するのに役立ちます。
各データ セットは、証明アシスタント Agda または Lean で記述された形式化された数学のライブラリから派生します。
このコレクションには、最大の Lean~4 ライブラリ Mathlib と、最大の Agda ライブラリのいくつか (標準ライブラリ、一価数学ライブラリ Agda-unimath、および TypeTopology ライブラリ) が含まれています。
各データ セットは、対応するライブラリを 2 つの方法で表します。1 つは異種ネットワークとして、もう 1 つはライブラリ内のすべてのエントリの構文ツリーを表す 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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google