論文の概要: NaturalProver: Grounded Mathematical Proof Generation with Language Models

• arxiv url: http://arxiv.org/abs/2205.12910v1
• Date: Wed, 25 May 2022 17:01:18 GMT
• ステータス: 処理完了
• システム内更新日: 2022-05-26 13:54:06.193550
• Title: NaturalProver: Grounded Mathematical Proof Generation with Language Models
• Title（参考訳）: NaturalProver: 言語モデルを用いた数学的証明生成
• Authors: Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, Yejin Choi
• Abstract要約: 自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。 本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。 NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
• 参考スコア（独自算出の注目度）: 84.2064569475095
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Theorem proving in natural mathematical language - the mixture of symbolic and natural language used by humans - plays a central role in mathematical advances and education, and tests aspects of reasoning that are core to intelligence. Yet it has remained underexplored with modern generative models. We study large-scale language models on two new generation tasks: suggesting the next step in a mathematical proof, and full proof generation. Naively applying language models to these problems yields proofs riddled with hallucinations and logical incoherence. We develop NaturalProver, a language model that generates proofs by conditioning on background references (e.g. theorems and definitions that are either retrieved or human-provided), and optionally enforces their presence with constrained decoding. On theorems from the NaturalProofs benchmark, NaturalProver improves the quality of next-step suggestions and generated proofs over fine-tuned GPT-3, according to human evaluations from university-level mathematics students. NaturalProver is capable of proving some theorems that require short (2-6 step) proofs, and providing next-step suggestions that are rated as correct and useful over 40% of the time, which is to our knowledge the first demonstration of these capabilities using neural language models.
• Abstract（参考訳）: 自然数理言語の証明 - 人間によって使用される記号と自然言語の混合 - は、数学の進歩と教育において中心的な役割を果たし、知性の中核となる推論の側面をテストする。 しかし、現代の世代モデルでは未熟である。 本研究では,2つの新世代タスクにおいて,数学的証明の次のステップと完全証明生成の2つの課題について,大規模言語モデルについて検討する。 これらの問題に言語モデルを適用することは、幻覚と論理的不整合によって取り除かれた証明をもたらす。 背景参照(例えば、検索されたり、人間が提供されたりする定理や定義)を条件付けして証明を生成する言語モデルである naturalprover を開発し、制約付きデコードでその存在を任意に強制する。 NaturalProofsベンチマークの定理では、NaturalProverは次のステップの提案の質を改善し、微調整されたGPT-3に対する証明を生成する。 naturalproverは、短い(2～6ステップ)証明を必要とするいくつかの定理を証明でき、40%以上の時間に正確かつ有用と評価された次のステップの提案を提供することができる。

関連論文リスト

• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。 Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
  論文  参考訳（メタデータ） (2024-07-14T01:43:07Z)
• Language Models as Inductive Reasoners [125.99461874008703]
  本稿では,帰納的推論のための新しいパラダイム(タスク)を提案し,自然言語の事実から自然言語規則を誘導する。 タスクのための1.2kルールファクトペアを含むデータセットDEERを作成し,ルールと事実を自然言語で記述する。 我々は、事前訓練された言語モデルが自然言語の事実から自然言語規則をいかに誘導できるかを、初めてかつ包括的な分析を行う。
  論文  参考訳（メタデータ） (2022-12-21T11:12:14Z)
• Towards a Mathematics Formalisation Assistant using Large Language Models [5.485439959027125]
  リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。 コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。 新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
  論文  参考訳（メタデータ） (2022-11-14T16:52:32Z)
• Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
  NLProofS (Natural Language Proof Search) を提案する。 NLProofSは仮説に基づいて関連するステップを生成することを学習する。 EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2022-05-25T02:22:30Z)
• NaturalProofs: Mathematical Theorem Proving in Natural Language [132.99913141409968]
  数学的ステートメントの多領域コーパスであるNaturalProofsとその証明を開発した。 NaturalProofsは広範なカバレッジ、深いカバレッジ、低リソースの数学的ソースを統一する。 数式参照検索と生成タスクに関する強力なニューラルネットワーク手法をベンチマークする。
  論文  参考訳（メタデータ） (2021-03-24T03:14:48Z)
• ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language [19.917022148887273]
  トランスフォーマーは自然言語理論上の論理推論をエミュレートすることが示されている。 ProofWriterと呼ばれる生成モデルは、理論の意味とそれらをサポートする自然言語の証明の両方を確実に生成できることを示しています。
  論文  参考訳（メタデータ） (2020-12-24T00:55:46Z)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)

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

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