論文の概要: MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
- arxiv url: http://arxiv.org/abs/2109.00110v1
- Date: Tue, 31 Aug 2021 23:21:12 GMT
- ステータス: 処理完了
- システム内更新日: 2021-09-02 14:28:53.695200
- Title: MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics
- Title（参考訳）: minif2f: 形式的オリンピアドレベル数学のためのクロスシステムベンチマーク
- Authors: Kunhao Zheng, Jesse Michael Han, Stanislas Polu
- Abstract要約: miniF2Fは、ニューラル定理証明のための統一されたクロスシステムベンチマークを提供することを目的とした、オリンピアードレベルの公式な数学問題のデータセットである。
miniF2Fベンチマークは現在Metamath、Lean、Isabelleをターゲットにしており、AIME、AMC、International Mathematical Olympiad (IMO)から引き出された488の問題文で構成されている。
GPT-3に基づくニューラル定理証明器であるGPT-fを用いてベースライン結果を報告し,その性能解析を行った。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present miniF2F, a dataset of formal Olympiad-level mathematics problems
statements intended to provide a unified cross-system benchmark for neural
theorem proving. The miniF2F benchmark currently targets Metamath, Lean, and
Isabelle and consists of 488 problem statements drawn from the AIME, AMC, and
the International Mathematical Olympiad (IMO), as well as material from
high-school and undergraduate mathematics courses. We report baseline results
using GPT-f, a neural theorem prover based on GPT-3 and provide an analysis of
its performance. We intend for miniF2F to be a community-driven effort and hope
that our benchmark will help spur advances in neural theorem proving.
- Abstract（参考訳）: ニューラル定理証明のための一貫したクロスシステムベンチマークを提供することを目的として,オリンピアードレベルの数学問題のデータセットである miniF2F を提案する。
miniF2Fベンチマークは、現在Metamath、Lean、Isabelleをターゲットにしており、AIME、AMC、国際数学オリンピアード(IMO)から引き出された488の問題文と、高校や学部の数学コースの資料で構成されている。
GPT-3に基づくニューラル定理証明器であるGPT-fを用いてベースライン結果を報告し,その性能解析を行った。
MiniF2Fはコミュニティ主導の取り組みであり、私たちのベンチマークが神経定理の証明の進歩を促進することを期待しています。
関連論文リスト
- PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition [6.971356163199923]
パットナムベンチ (PutnamBench) は、ウィリアム・ローウェル・パットナム数学コンペティション (William Lowell Putnam Mathematical Competition) から導かれる640の定理を1697年に手作りで定式化したものである。
すべての定理はLean 4 と Isabelle の形式化を持ち、かなりの部分集合は Coq の形式化も持つ。
パットナムベンチを用いて、確立されたニューラルおよびシンボリック定理証明器の評価を行う。
論文 参考訳（メタデータ） (2024-07-15T19:57:15Z) - A Critical Analysis of the Theoretical Framework of the Extreme Learning Machine [1.9503475832401784]
ELM学習アルゴリズムに反例を与える2つの主要な文とデータセットの証明を論じる。
我々は、いくつかの理論的ケースにおいて、EMMの効率を正当化する基礎の代替的なステートメントを提供する。
論文 参考訳（メタデータ） (2024-06-25T10:06:07Z) - DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
本稿では,高校・学部レベルの数学競争問題から得られたリーン4証明データを生成する手法を提案する。
この合成データセットでDeepSeekMath 7Bモデルを微調整します。
我々のモデルは、Lean 4 Formalized International Mathematical Olympiad (FIMO)ベンチマークで148の問題を5つ証明しましたが、GPT-4は証明できませんでした。
論文 参考訳（メタデータ） (2024-05-23T09:03:42Z) - MathBench: Evaluating the Theory and Application Proficiency of LLMs with a Hierarchical Mathematics Benchmark [82.64129627675123]
MathBenchは、大規模言語モデルの数学的能力を厳格に評価する新しいベンチマークである。
MathBenchは幅広い数学の分野にまたがっており、理論的な理解と実践的な問題解決のスキルの両方を詳細に評価している。
論文 参考訳（メタデータ） (2024-05-20T17:52:29Z) - ConceptMath: A Bilingual Concept-wise Benchmark for Measuring
Mathematical Reasoning of Large Language Models [67.32868432113587]
本稿では,Large Language Models (LLMs) の概念的数学的推論を評価するための詳細なベンチマークであるConceptMathを紹介する。
一般的な数学的推論を平均精度で評価する従来のベンチマークとは異なり、ConceptMathは数学の問題を数学的概念の階層の下に体系的に整理する。
論文 参考訳（メタデータ） (2024-02-22T16:06:49Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - Llemma: An Open Language Model For Mathematics [46.557804525919785]
数学のための大きな言語モデルであるLlemmaを紹介します。
MATHベンチマークでは、Llemmaはすべての既知のオープンベースモデルより優れている。
レムマは道具の使用と公式な定理を証明することができるが、それ以上の微調整は行わない。
論文 参考訳（メタデータ） (2023-10-16T17:54:07Z) - FIMO: A Challenge Formal Dataset for Automated Theorem Proving [31.695624833932577]
FIMOは、IMOレベルでの高度な自動定理証明を容易にするように設計されている。
公式な問題文は149で、非公式な問題記述とそれに対応する非公式な証明の両方を伴っている。
論文 参考訳（メタデータ） (2023-09-08T12:34:28Z) - ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics [7.607254619341369]
本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。
ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。
テキスト内学習による文の自動書式化のベースライン結果について報告する。
論文 参考訳（メタデータ） (2023-02-24T03:28:46Z) - Generalization Guarantee of Training Graph Convolutional Networks with
Graph Topology Sampling [83.77955213766896]
グラフ畳み込みネットワーク(GCN)は近年,グラフ構造化データの学習において大きな成功を収めている。
スケーラビリティ問題に対処するため、Gsの学習におけるメモリと計算コストを削減するため、グラフトポロジサンプリングが提案されている。
本稿では,3層GCNのトレーニング(最大)におけるグラフトポロジサンプリングの最初の理論的正当性について述べる。
論文 参考訳（メタデータ） (2022-07-07T21:25:55Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。