論文の概要: NaturalProofs: Mathematical Theorem Proving in Natural Language

• arxiv url: http://arxiv.org/abs/2104.01112v2
• Date: Mon, 7 Jun 2021 21:58:06 GMT
• ステータス: 処理完了
• システム内更新日: 2023-04-06 23:34:49.919655
• Title: NaturalProofs: Mathematical Theorem Proving in Natural Language
• Title（参考訳）: NaturalProofs: 自然言語で証明する数学的理論
• Authors: Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, Kyunghyun Cho
• Abstract要約: 数学的ステートメントの多領域コーパスであるNaturalProofsとその証明を開発した。 NaturalProofsは広範なカバレッジ、深いカバレッジ、低リソースの数学的ソースを統一する。 数式参照検索と生成タスクに関する強力なニューラルネットワーク手法をベンチマークする。
• 参考スコア（独自算出の注目度）: 132.99913141409968
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Understanding and creating mathematics using natural mathematical language - the mixture of symbolic and natural language used by humans - is a challenging and important problem for driving progress in machine learning. As a step in this direction, we develop NaturalProofs, a multi-domain corpus of mathematical statements and their proofs, written in natural mathematical language. NaturalProofs unifies broad coverage, deep coverage, and low-resource mathematical sources, allowing for evaluating both in-distribution and zero-shot generalization. Using NaturalProofs, we benchmark strong neural methods on mathematical reference retrieval and generation tasks which test a system's ability to determine key results that appear in a proof. Large-scale sequence models show promise compared to classical information retrieval methods, yet their performance and out-of-domain generalization leave substantial room for improvement. NaturalProofs opens many avenues for research on challenging mathematical tasks.
• Abstract（参考訳）: 自然数理言語による数学の理解と作成 シンボリック言語と自然言語の組み合わせ - 機械学習の進歩を推進する上で、挑戦的で重要な問題である。 この方向への一歩として、数学的ステートメントの多領域コーパスであるNaturalProofsを開発し、その証明を自然言語で記述する。 naturalproofsは広い範囲、深い範囲、低リソースの数学的情報源を統一し、内分布とゼロショットの一般化の両方を評価することができる。 NaturalProofsを用いて、証明に現れる重要な結果を決定するシステムの能力をテストする数学的参照検索および生成タスクについて、強力なニューラルネットワーク手法をベンチマークする。 大規模シーケンスモデルでは、従来の情報検索手法と比較すると期待できるが、その性能とドメイン外一般化は改善の余地を残している。 NaturalProofsは、挑戦的な数学的タスクの研究のための多くの道を開く。

関連論文リスト

• LeanAgent: Lifelong Learning for Formal Theorem Proving [85.39415834798385]
  フォーマルな定理証明のための新しい生涯学習フレームワークであるLeanAgentを紹介する。 LeanAgentは継続的に一般化し、拡張可能な数学的知識を改善します。 以前、23のリーンリポジトリで人間が公式に証明していなかった155の定理の証明に成功した。
  論文  参考訳（メタデータ） (2024-10-08T17:11:24Z)
• Artifical intelligence and inherent mathematical difficulty [0.0]
  まず、計算可能性と複雑性理論による制限的な結果が証明発見が本質的に難しい問題であることを示す従来の議論の更新版を提示する。 次に、人工知能にインスパイアされた最近のいくつかの応用が、数学的な証明の性質に関する新しい疑問を実際に提起する方法について説明する。
  論文  参考訳（メタデータ） (2024-08-01T20:08:31Z)
• Tree-Based Representation and Generation of Natural and Mathematical Language [77.34726150561087]
  科学コミュニケーションと教育シナリオにおける数学的言語は重要であるが、比較的研究されている。 数学言語に関する最近の研究は、スタンドアローンな数学的表現や、事前訓練された自然言語モデルにおける数学的推論に焦点をあてている。 テキストと数学を共同で表現・生成するために,既存の言語モデルに対する一連の修正を提案する。
  論文  参考訳（メタデータ） (2023-02-15T22:38:34Z)
• Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs [5.045988012508899]
  オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。 本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
  論文  参考訳（メタデータ） (2023-01-05T17:56:00Z)
• A Survey of Deep Learning for Mathematical Reasoning [71.88150173381153]
  我々は過去10年間の数学的推論とディープラーニングの交差点における重要なタスク、データセット、方法についてレビューする。 大規模ニューラルネットワークモデルの最近の進歩は、新しいベンチマークと、数学的推論にディープラーニングを使用する機会を開放している。
  論文  参考訳（メタデータ） (2022-12-20T18:46:16Z)
• NaturalProver: Grounded Mathematical Proof Generation with Language Models [84.2064569475095]
  自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
  論文  参考訳（メタデータ） (2022-05-25T17:01:18Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• Natural Language Premise Selection: Finding Supporting Statements for Mathematical Text [3.42658286826597]
  提案するNLPタスクは,サポート定義の検索や提案の支持に使用される自然前提選択である。 また、NL-PSというデータセットを利用可能にすることで、自然環境選択タスクに対する様々なアプローチを評価することができる。
  論文  参考訳（メタデータ） (2020-04-30T17:08:03Z)

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

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