論文の概要: IsarStep: a Benchmark for High-level Mathematical Reasoning

• arxiv url: http://arxiv.org/abs/2006.09265v2
• Date: Wed, 24 Mar 2021 16:45:18 GMT
• ステータス: 処理完了
• システム内更新日: 2022-11-21 20:26:15.465482
• Title: IsarStep: a Benchmark for High-level Mathematical Reasoning
• Title（参考訳）: IsarStep: 高度な数学的推論のためのベンチマーク
• Authors: Wenda Li and Lei Yu and Yuhuai Wu and Lawrence C. Paulson
• Abstract要約: 本稿では,高レベルな数学的推論のためのベンチマークを提案し,ニューラルシークエンス・ツー・シーケンスモデルの推論能力について検討する。 我々は、人間の専門家が定理証明器で記述した最大の証明のリポジトリから、非合成データセットを構築した。
• 参考スコア（独自算出の注目度）: 20.96474618260995
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: A well-defined benchmark is essential for measuring and accelerating research progress of machine learning models. In this paper, we present a benchmark for high-level mathematical reasoning and study the reasoning capabilities of neural sequence-to-sequence models. We build a non-synthetic dataset from the largest repository of proofs written by human experts in a theorem prover. The dataset has a broad coverage of undergraduate and research-level mathematical and computer science theorems. In our defined task, a model is required to fill in a missing intermediate proposition given surrounding proofs. This task provides a starting point for the long-term goal of having machines generate human-readable proofs automatically. Our experiments and analysis reveal that while the task is challenging, neural models can capture non-trivial mathematical reasoning. We further design a hierarchical transformer that outperforms the transformer baseline.
• Abstract（参考訳）: 適切に定義されたベンチマークは、機械学習モデルの研究進歩の測定と加速に不可欠である。 本稿では,高レベル数学的推論のベンチマークを行い,ニューラルネットワークのシーケンスからシーケンスへの推論能力について検討する。 我々は、人間の専門家が定理証明器に書いた最大の証明のリポジトリから、非合成データセットを構築する。 このデータセットは、学部および研究レベルの数学および計算機科学の定理を幅広くカバーしている。 我々の定義したタスクでは、周囲の証明を考慮に入れた中間命題を補うためにモデルが必要である。 このタスクは、機械が自動で可読性証明を生成するという長期的な目標の出発点となる。 我々の実験と分析により、課題は難しいが、神経モデルは非自明な数学的推論を捉えることができることが明らかとなった。 さらに、トランスベースラインよりも優れた階層変換器を設計する。

関連論文リスト

• Benchmarking Large Language Models with Integer Sequence Generation Tasks [1.3108652488669736]
  本稿では,大規模言語モデル(LLM)がオンラインシーケンス百科事典(OEIS)から整数列を計算するコードを書かなければならない,新たなベンチマークを提案する。 ベンチマークの結果、OpenAI、Anthropic、Meta、Googleの他のフロンティアモデルよりも、簡単かつハードな整数シーケンス間の精度と不正なレートで、o1シリーズのモデルの方が優れていることが判明した。
  論文  参考訳（メタデータ） (2024-11-07T02:05:43Z)
• Discovering symbolic expressions with parallelized tree search [59.92040079807524]
  記号回帰は、データから簡潔で解釈可能な数学的表現を発見する能力のおかげで、科学研究において重要な役割を果たす。 既存のアルゴリズムは、複雑性の問題に対処する際の精度と効率の重要なボトルネックに直面してきた。 本稿では,限定データから汎用数学的表現を効率的に抽出する並列木探索(PTS)モデルを提案する。
  論文  参考訳（メタデータ） (2024-07-05T10:41:15Z)
• TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
  本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。 我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。 我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
  論文  参考訳（メタデータ） (2023-10-16T08:42:39Z)
• A Brain-Inspired Sequence Learning Model based on a Logic [6.653734987585243]
  本稿では,非公理論理で解釈可能なシーケンス学習モデルの設計と試験を行う。 その結果、モデルは異なるレベルの難易度でうまく機能することがわかった。
  論文  参考訳（メタデータ） (2023-08-24T01:01:41Z)
• Learning Active Subspaces and Discovering Important Features with Gaussian Radial Basis Functions Neural Networks [0.0]
  モデルの訓練が完了すると抽出できる精度行列のスペクトルに含まれる貴重な情報を示す。 回帰,分類,特徴選択タスクの数値実験を行った。 その結果,提案モデルが競合モデルに比べて魅力的な予測性能が得られるだけでなく,予測性能も向上することが示唆された。
  論文  参考訳（メタデータ） (2023-07-11T09:54:30Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。 大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
  論文  参考訳（メタデータ） (2022-12-20T18:46:16Z)
• ConvFinQA: Exploring the Chain of Numerical Reasoning in Conversational Finance Question Answering [70.6359636116848]
  本稿では,対話型質問応答における数値推論の連鎖を研究するために,新しい大規模データセットConvFinQAを提案する。 我々のデータセットは、現実世界の会話において、長距離で複雑な数値推論パスをモデル化する上で大きな課題となる。
  論文  参考訳（メタデータ） (2022-10-07T23:48:50Z)
• SynBench: Task-Agnostic Benchmarking of Pretrained Representations using Synthetic Data [78.21197488065177]
  近年、下流のタスクで大規模なデータで事前訓練された微調整大型モデルが成功し、ディープラーニングにおける重要なパラダイムシフトにつながった。 本稿では,合成データを用いて事前学習した表現の質を測定するためのタスク非依存フレームワークであるtextitSynBenchを提案する。
  論文  参考訳（メタデータ） (2022-10-06T15:25:00Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• Learning to Prove from Synthetic Theorems [41.74768503409581]
  自動定理証明に機械学習を適用する上での大きな課題は、トレーニングデータの不足である。 本稿では,一組の公理から生成される合成定理による学習に依存するアプローチを提案する。 このような定理が自動証明器の訓練に利用でき、学習された証明器が人間の生成した定理にうまく移行できることが示される。
  論文  参考訳（メタデータ） (2020-06-19T17:48:09Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。