論文の概要: 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ドル以上のエントリーがあり、これは現在、機械学習可能な形式における公式な数学的知識のコレクションとして最大である。
関連論文リスト
- Library Learning Doesn't: The Curious Case of the Single-Use "Library" [20.25809428140996]
LEGO-ProverとTroVEの2つのライブラリ学習システムについて検討した。
機能再利用は miniF2F と MATH では極めて稀である。
我々の追跡実験は、再利用よりも自己補正と自己整合が、観察されたパフォーマンス向上の主要な要因であることを示唆している。
論文 参考訳（メタデータ） (2024-10-26T21:05:08Z) - DiscoveryBench: Towards Data-Driven Discovery with Large Language Models [50.36636396660163]
我々は、データ駆動探索の多段階プロセスを形式化する最初の包括的なベンチマークであるDiscoveryBenchを紹介する。
我々のベンチマークには、社会学や工学などの6つの分野にまたがる264のタスクが含まれている。
私たちのベンチマークでは、自律的なデータ駆動型発見の課題を説明し、コミュニティが前進するための貴重なリソースとして役立ちます。
論文 参考訳（メタデータ） (2024-07-01T18:58:22Z) - PromptReps: Prompting Large Language Models to Generate Dense and Sparse Representations for Zero-Shot Document Retrieval [76.50690734636477]
本稿では,PmptRepsを提案する。このPmptRepsは,トレーニングを必要とせず,コーパス全体から検索できる機能である。
検索システムは、高密度テキスト埋め込みとスパースバッグ・オブ・ワード表現の両方を利用する。
論文 参考訳（メタデータ） (2024-04-29T04:51:30Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - A New Approach Towards Autoformalization [7.275550401145199]
オートフォーマル化(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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。