論文の概要: PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
- arxiv url: http://arxiv.org/abs/2407.11214v1
- Date: Mon, 15 Jul 2024 19:57:15 GMT
- ステータス: 処理完了
- システム内更新日: 2024-07-17 19:21:30.815310
- Title: PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
- Title（参考訳）: パットナムベンチ:パットナム数学コンペティションにおける神経理論者の評価
- Authors: George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Amitayush Thakur, Swarat Chaudhuri,
- Abstract要約: パットナムベンチ (PutnamBench) は、ウィリアム・ローウェル・パットナム数学コンペティション (William Lowell Putnam Mathematical Competition) から導かれる640の定理を1697年に手作りで定式化したものである。
すべての定理はLean 4 と Isabelle の形式化を持ち、かなりの部分集合は Coq の形式化も持つ。
パットナムベンチを用いて、確立されたニューラルおよびシンボリック定理証明器の評価を行う。
- 参考スコア（独自算出の注目度）: 6.971356163199923
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present PutnamBench, a new multilingual benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1697 hand-constructed formalizations of 640 theorems sourced from the William Lowell Putnam Mathematical Competition, the premier undergraduate-level mathematics competition in North America. All the theorems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations. Proving the theorems requires significant problem-solving ability and proficiency in a broad range of topics taught in undergraduate mathematics courses. We use PutnamBench to evaluate several established neural and symbolic theorem-provers. These approaches can only solve a handful of the PutnamBench problems, establishing the benchmark as a difficult open challenge for research on neural theorem-proving. PutnamBench is available at https://github.com/trishullab/PutnamBench.
- Abstract（参考訳）: パットナムベンチ(PatnamBench)は、ニューラル定理プロデューサが競合数学の問題を解く能力を評価するための新しい多言語ベンチマークである。
パットナムベンチは、1697年、北アメリカの大学レベルの数学コンペティションであるウィリアム・ローウェル・パットナム数学コンペティション(William Lowell Putnam Mathematical Competition)から得られた640の定理を手作りで定式化したものである。
すべての定理はLean 4 と Isabelle の形式化を持ち、かなりの部分集合は Coq の形式化も持つ。
定理の証明には、学部数学コースで教えられる幅広いトピックにおいて、重大な問題解決能力と習熟性が必要である。
パットナムベンチを用いて、確立されたニューラルおよびシンボリック定理証明器の評価を行う。
これらのアプローチはパットナムベンチ問題のごく一部しか解決できず、このベンチマークをニューラル定理証明の研究の難しいオープンチャレンジとして確立する。
PutnamBenchはhttps://github.com/trishullab/PutnamBench.comで入手できる。
関連論文リスト
- FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI [2.0608396919601493]
FrontierMath(フロンティアマス、フロンティアマス、FrontierMath)は、数学者が考案し検証した何百もの数学問題のベンチマークである。
現在の最先端のAIモデルは、問題の2%未満を解決し、AI能力と数学的コミュニティの長所との間に大きなギャップが浮かび上がっている。
AIシステムが専門家レベルの数学的能力に向かって進むにつれ、FrontierMathは彼らの進歩を定量化する厳格なテストベッドを提供する。
論文 参考訳（メタデータ） (2024-11-07T17:07:35Z) - Another quantum version of Sanov theorem [53.64687146666141]
我々は、サノフの定理を量子集合に拡張する方法を研究する。
我々は、経験的分布の量子アナログを考慮することで、サノフの定理の別の量子バージョンを提案する。
論文 参考訳（メタデータ） (2024-07-26T07:46:30Z) - MathBench: Evaluating the Theory and Application Proficiency of LLMs with a Hierarchical Mathematics Benchmark [82.64129627675123]
MathBenchは、大規模言語モデルの数学的能力を厳格に評価する新しいベンチマークである。
MathBenchは幅広い数学の分野にまたがっており、理論的な理解と実践的な問題解決のスキルの両方を詳細に評価している。
論文 参考訳（メタデータ） (2024-05-20T17:52:29Z) - Rigor with Machine Learning from Field Theory to the Poincar\'e
Conjecture [0.0]
本稿では,機械学習を用いた自然科学における厳密性獲得手法について論じる。
非厳密な手法は、予想生成や強化学習による検証を通じて厳密な結果をもたらす可能性がある。
また、機械学習理論と数学または理論物理学の間に直接の橋渡しを構築することも想像できる。
論文 参考訳（メタデータ） (2024-02-20T19:00:59Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳（メタデータ） (2023-05-21T17:51:35Z) - Connes implies Tsirelson: a simple proof [91.3755431537592]
コンヌ埋め込み問題は同期的ツィレルソン予想を意味することを示す。
また、コンネスの代数 $mathcalRomega$ の異なる構成もコンネス埋め込み問題に現れる。
論文 参考訳（メタデータ） (2022-09-16T13:59:42Z) - JiuZhang: A Chinese Pre-trained Language Model for Mathematical Problem
Understanding [74.12405417718054]
本稿では,中国初の数学的事前学習言語モデル(PLM)を提示することにより,機械の数学的知性向上を目指す。
他の標準のNLPタスクとは異なり、数学的テキストは問題文に数学的用語、記号、公式を含むため理解が難しい。
基礎課程と上級課程の両方からなる数学PLMの学習を改善するための新しいカリキュラム事前学習手法を設計する。
論文 参考訳（メタデータ） (2022-06-13T17:03:52Z) - MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics [0.0]
miniF2Fは、ニューラル定理証明のための統一されたクロスシステムベンチマークを提供することを目的とした、オリンピアードレベルの公式な数学問題のデータセットである。
miniF2Fベンチマークは現在Metamath、Lean、Isabelleをターゲットにしており、AIME、AMC、International Mathematical Olympiad (IMO)から引き出された488の問題文で構成されている。
GPT-3に基づくニューラル定理証明器であるGPT-fを用いてベースライン結果を報告し,その性能解析を行った。
論文 参考訳（メタデータ） (2021-08-31T23:21:12Z) - A refinement of Reznick's Positivstellensatz with applications to
quantum information theory [72.8349503901712]
ヒルベルトの17番目の問題において、アルティンはいくつかの変数の任意の正定値が2つの平方和の商として書けることを示した。
レズニックはアルティンの結果の分母は常に変数の平方ノルムの$N$-次パワーとして選択できることを示した。
論文 参考訳（メタデータ） (2019-09-04T11:46:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。