論文の概要: MLFMF: Data Sets for Machine Learning for Mathematical Formalization
- arxiv url: http://arxiv.org/abs/2310.16005v1
- Date: Tue, 24 Oct 2023 17:00:00 GMT
- ステータス: 処理完了
- システム内更新日: 2023-10-25 17:41:17.452681
- Title: MLFMF: Data Sets for Machine Learning for Mathematical Formalization
- Title(参考訳): MLFMF:数学的形式化のための機械学習のためのデータセット
- Authors: Andrej Bauer, Matej Petkovi\'c, Ljup\v{c}o Todorovski
- Abstract要約: MLFMF(MLFMF)は、証明アシスタントを用いた数学の形式化を支援するために使用されるベンチマークシステムのためのデータセットの集合である。
各データセットは、AgdaやLeanの証明アシスタントで書かれた形式化された数学のライブラリから導かれる。
合計25万ドル以上のエントリーがあり、これは現在、機械学習可能な形式における公式な数学的知識のコレクションとして最大である。
- 参考スコア(独自算出の注目度): 0.18416014644193068
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: 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.
- Abstract(参考訳): MLFMFは,証明アシスタントを用いた数学の形式化を支援するために使用される推薦システムベンチマークのためのデータセットの集合である。
これらのシステムは、新しい定理の証明や新しい構成の実行に関係した以前のエントリ(理論、構造、データタイプ、仮定)を特定するのに役立つ。
各データセットは、AgdaやLeanの証明アシスタントで書かれた形式化された数学のライブラリから導かれる。
このコレクションには、最大のLean~4ライブラリMathlibと、最大規模のAgdaライブラリ(標準ライブラリ、Agda-Unimathの一価数学ライブラリ、TypeTopologyライブラリ)が含まれている。
各データセットは対応するライブラリを2つの方法で表現する: ヘテロジニアスネットワークとして、そしてライブラリ内のすべてのエントリの構文木を表すs表現のリストとして。
ネットワークにはライブラリの(モジュール的な)構造とエントリ間の参照が含まれており、s式はエントリごとに完全かつ容易に解析される情報を提供する。
標準グラフと単語埋め込み,ツリーアンサンブル,インスタンスベースの学習アルゴリズムを用いて,ベースライン結果について報告する。
MLFMFデータセットは、形式化された数学に対する多くの機械学習アプローチのさらなる調査のために、確固たるベンチマークサポートを提供する。
ネットワークとs-表現を抽出する手法は他のライブラリにも容易に適用でき、他の証明アシスタントにも適用できる。
合計250,000ドル以上のエントリーがあり、これは現在、機械学習可能な形式における公式な数学的知識のコレクションとして最大である。
関連論文リスト
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - LILO: Learning Interpretable Libraries by Compressing and Documenting Code [72.90003911433905]
LILOは、反復的に合成、圧縮、文書化を行う、ニューロシンボリックなフレームワークである。
LILOは、LLM誘導プログラム合成と、Stitchから自動化された最近のアルゴリズムの進歩を組み合わせたものである。
LILOのシンセサイザーが学習した抽象化を解釈し、デプロイするのを手助けすることで、AutoDocがパフォーマンスを向上させることが分かりました。
論文 参考訳(メタデータ) (2023-10-30T17:55:02Z) - A New Approach Towards Autoformalization [8.176989532546632]
オートフォーマル化(Autoformalization)は、自然言語をプログラムで検証可能な形式言語に変換するタスクである。
研究論文は大量の背景と文脈を必要とする。
本稿では,研究レベルの数学の自己形式化に取り組み,タスクをより容易に,より親しみやすいサブタスクに分割する手法を提案する。
論文 参考訳(メタデータ) (2023-10-12T00:50:24Z) - LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。
既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。
本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。
本研究では,LLM ベースの証明器 ReProver を開発した。
論文 参考訳(メタデータ) (2023-06-27T17:05:32Z) - FuzzyLogic.jl: a Flexible Library for Efficient and Productive Fuzzy
Inference [5.584060970507507]
本稿では,ファジィ推論を行うJuliaライブラリであるtextscFuzzyLogic.jlを紹介する。
ライブラリは完全にオープンソースで、パーミッシブライセンスでリリースされている。
論文 参考訳(メタデータ) (2023-06-17T10:43:09Z) - BERT is not The Count: Learning to Match Mathematical Statements with
Proofs [34.61792250254876]
この課題は、数学的情報検索に関する現在の研究や、より一般的には、数学的記事分析に当てはまる。
現代数学研究論文から抽出した180k以上の文対からなるデータセットについて述べる。
本稿では,文と証明を効果的にマッチングする双線形類似モデルと2つの復号法を提案する。
論文 参考訳(メタデータ) (2023-02-18T14:48:20Z) - Deep Learning Symmetries and Their Lie Groups, Algebras, and Subalgebras
from First Principles [55.41644538483948]
ラベル付きデータセットに存在する連続した対称性群の検出と同定のためのディープラーニングアルゴリズムを設計する。
完全に接続されたニューラルネットワークを用いて、変換対称性と対応するジェネレータをモデル化する。
また,Lie群とその性質の数学的研究に機械学習アプローチを使うための扉を開く。
論文 参考訳(メタデータ) (2023-01-13T16:25:25Z) - GRAD-MATCH: A Gradient Matching Based Data Subset Selection for
Efficient Learning [23.75284126177203]
我々は、トレーニングや検証セットの勾配と密接に一致する部分集合を見つける汎用フレームワークgrad-matchを提案する。
GRAD-MATCHは、最近のデータ選択アルゴリズムよりも大きく、一貫して優れていることを示す。
論文 参考訳(メタデータ) (2021-02-27T04:09:32Z) - Learning Aggregation Functions [78.47770735205134]
任意の濃度の集合に対する学習可能なアグリゲータであるLAF(Learning Aggregation Function)を紹介する。
半合成および実データを用いて,LAFが最先端の和(max-)分解アーキテクチャより優れていることを示す実験を報告する。
論文 参考訳(メタデータ) (2020-12-15T18:28:53Z) - A Graph Representation of Semi-structured Data for Web Question
Answering [96.46484690047491]
本稿では、半構造化データとそれらの関係の構成要素の体系的分類に基づいて、Webテーブルとリストのグラフ表現を提案する。
本手法は,最先端のベースラインに対してF1スコアを3.90ポイント向上させる。
論文 参考訳(メタデータ) (2020-10-14T04:01:54Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。