論文の概要: 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はコミュニティ主導の取り組みであり、私たちのベンチマークが神経定理の証明の進歩を促進することを期待しています。
関連論文リスト
- Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - Omni-MATH: A Universal Olympiad Level Mathematic Benchmark For Large Language Models [63.31878920079154]
Olympiadレベルでの大規模言語モデルの数学的推論を評価するためのベンチマークを提案する。
既存のOlympiad関連のベンチマークとは異なり、我々のデータセットは数学にのみ焦点をあてている。
実験の結果,最も先進的なモデルであるOpenAI o1-miniとOpenAI o1-previewでさえ,高度に難解なオリンピアドレベルの問題に悩まされていることが明らかとなった。
論文 参考訳（メタデータ） (2024-10-10T14:39:33Z) - Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement [71.46993852662021]
Qwen2.5-Math と Qwen2.5-Math-Instruct-1.5B/7B/72B である。
Qwen2.5-Math-Instructは中国語と英語の両方をサポートし、高度な数学的推論能力を持っている。
論文 参考訳（メタデータ） (2024-09-18T16:45:37Z) - SubgoalXL: Subgoal-based Expert Learning for Theorem Proving [37.115856591703974]
SubgoalXLは、正規の定理証明を強化するために、専門家の学習とサブゴールベースの証明を相乗化する新しいアプローチである。
SubgoalXLは、標準のminiF2Fデータセット上で、Isabelleで56.1%の最先端パフォーマンスを実現する。
論文 参考訳（メタデータ） (2024-08-20T20:10:53Z) - PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition [6.971356163199923]
パットナムベンチ (PutnamBench) は、ウィリアム・ローウェル・パットナム数学コンペティション (William Lowell Putnam Mathematical Competition) から導かれる640の定理の、1692年の手作りの形式化からなる。
パットナムベンチは、学部数学コースで教えられる幅広いトピックにおいて、重大な問題解決能力と熟練度を必要とする。
論文 参考訳（メタデータ） (2024-07-15T19:57:15Z) - 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) - FIMO: A Challenge Formal Dataset for Automated Theorem Proving [31.695624833932577]
FIMOは、IMOレベルでの高度な自動定理証明を容易にするように設計されている。
公式な問題文は149で、非公式な問題記述とそれに対応する非公式な証明の両方を伴っている。
論文 参考訳（メタデータ） (2023-09-08T12:34:28Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳（メタデータ） (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。