論文の概要: 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で入手できる。
関連論文リスト
- 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) - Connecting classical finite exchangeability to quantum theory [69.62715388742298]
交換性は確率論と統計学の基本的な概念である。
有限交換可能な列に対するデ・フィネッティのような表現定理は、量子論と正式に等価な数学的表現を必要とすることを示す。
論文 参考訳（メタデータ） (2023-06-06T17:15:19Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳（メタデータ） (2023-05-21T17:51:35Z) - Representer Theorems for Metric and Preference Learning: A Geometric
Perspective [0.0]
計量学習と選好学習を同時に行うための新しい代表者定理を得る。
本稿では,三重項比較によるメートル法学習の課題に対して,本フレームワークが適用可能であることを示す。
カーネル・ヒルベルト・スペースを再現する場合、学習問題の解をカーネル用語で表現できることを実証する。
論文 参考訳（メタデータ） (2023-04-07T16:34:25Z) - Connes implies Tsirelson: a simple proof [91.3755431537592]
コンヌ埋め込み問題は同期的ツィレルソン予想を意味することを示す。
また、コンネスの代数 $mathcalRomega$ の異なる構成もコンネス埋め込み問題に現れる。
論文 参考訳（メタデータ） (2022-09-16T13:59:42Z) - Discussion of Foundation of Mathematics and Quantum Theory [0.0]
古典数学と有限数学の異なる側面について論じる。
特性$p$の有限環に基づく量子論は、標準量子論よりも一般的である。
論文 参考訳（メタデータ） (2022-03-09T18:46:57Z) - 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) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z) - A refinement of Reznick's Positivstellensatz with applications to
quantum information theory [72.8349503901712]
ヒルベルトの17番目の問題において、アルティンはいくつかの変数の任意の正定値が2つの平方和の商として書けることを示した。
レズニックはアルティンの結果の分母は常に変数の平方ノルムの$N$-次パワーとして選択できることを示した。
論文 参考訳（メタデータ） (2019-09-04T11:46:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。