論文の概要: PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
- arxiv url: http://arxiv.org/abs/2407.11214v2
- Date: Sun, 3 Nov 2024 17:14:37 GMT
- ステータス: 処理完了
- システム内更新日: 2024-11-08 21:21:36.800324
- 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の定理の、1692年の手作りの形式化からなる。
パットナムベンチは、学部数学コースで教えられる幅広いトピックにおいて、重大な問題解決能力と熟練度を必要とする。
- 参考スコア（独自算出の注目度）: 6.971356163199923
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present PutnamBench, a new multi-language benchmark for evaluating the ability of neural theorem-provers to solve competition mathematics problems. PutnamBench consists of 1692 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 problems have formalizations in Lean 4 and Isabelle; a substantial subset also has Coq formalizations. PutnamBench 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)は、ニューラル定理プロデューサが競合数学の問題を解く能力を評価するための新しい多言語ベンチマークである。
パットナムベンチは、1692年、北アメリカの大学レベルの数学コンペティションであるウィリアム・ローウェル・パットナム数学コンペティション(William Lowell Putnam Mathematical Competition)から得られた640の定理を手作りで定式化したものである。
すべての問題はLean 4とIsabelleで形式化されている。
パットナムベンチは、学部数学コースで教えられる幅広いトピックにおいて、重大な問題解決能力と熟練度を必要とする。
パットナムベンチを用いて、確立されたニューラルおよびシンボリック定理証明器の評価を行う。
これらのアプローチはパットナムベンチ問題のごく一部しか解決できず、このベンチマークをニューラル定理証明の研究の難しいオープンチャレンジとして確立する。
PutnamBenchはhttps://github.com/trishullab/PutnamBench.comで入手できる。
関連論文リスト
- An unholy trinity: TFNP, polynomial systems, and the quantum satisfiability problem [0.0]
複素系の研究に基づいて, 完全関数NP (TFNP) の2つの新しいサブクラスを定義する。
我々の研究の中心は、SDR(System of Distinct Representatives)を用いた量子SAT(Quantum SAT)として知られる計算問題である。
本稿では, SFTA がゼロエラー版 SDR に含まれることから, 疎度・高次複雑さの根源を SDR で QSAT に埋め込む方法を示す。
論文 参考訳（メタデータ） (2024-12-27T12:57:06Z) - Proposing and solving olympiad geometry with guided tree search [63.824930029019995]
木探索に基づくガイド付き問題解決を支援するユークリッド幾何学システムであるTongGeometryを紹介する。
TongGeometryは、補助的な構成を必要とする67億の幾何学定理を発見した。
トンゲメトリーはIMO-AG-30ですべての国際数学オリンピック幾何学を解き、金メダリストを初めて上回った。
論文 参考訳（メタデータ） (2024-12-14T04:20:47Z) - 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) - 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。