論文の概要: Generating Natural Language Proofs with Verifier-Guided Search
- arxiv url: http://arxiv.org/abs/2205.12443v1
- Date: Wed, 25 May 2022 02:22:30 GMT
- ステータス: 処理完了
- システム内更新日: 2022-05-26 13:33:54.614413
- Title: Generating Natural Language Proofs with Verifier-Guided Search
- Title（参考訳）: Verifier-Guided Search を用いた自然言語証明の生成
- Authors: Kaiyu Yang and Jia Deng and Danqi Chen
- Abstract要約: NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
- 参考スコア（独自算出の注目度）: 74.9614610172561
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Deductive reasoning (drawing conclusions from assumptions) is a challenging
problem in NLP. In this work, we focus on proof generation: given a hypothesis
and a set of supporting facts in natural language, the model generates a proof
tree indicating how to deduce the hypothesis from supporting facts. Instead of
generating the entire proof in one shot, prior work has demonstrated the
promise of stepwise generation but achieved limited success on real-world data.
Existing stepwise methods struggle to generate proof steps that are both valid
and relevant. In this paper, we present a novel stepwise method NLProofS
(Natural Language Proof Search), which learns to generate relevant steps
conditioning on the hypothesis. At the core of our approach, we train an
independent verifier to check the validity of proof steps. Instead of
generating steps greedily, we search for proofs maximizing a global proof score
judged by the verifier. NLProofS achieves state-of-the-art performance on
EntailmentBank and RuleTaker. For example, it improves the percentage of
correctly predicted proofs from 20.9% to 33.3% in the distractor setting of
EntailmentBank. This is the first time stepwise methods have led to better
generation of challenging human-authored proofs.
- Abstract（参考訳）: 帰納的推論(仮定から結論を引き出す)はNLPにおいて難しい問題である。
本研究は, 仮説と自然言語における支援事実の集合が与えられた場合, 仮説を支持事実から導出する方法を示す証明木を生成する。
証明全体を1ショットで生成する代わりに、以前の研究はステップワイズ生成の可能性を実証したが、実際のデータでは限定的な成功を収めた。
既存のステップワイズメソッドは、正当かつ関連する証明ステップの生成に苦労している。
本稿では,新しいステップワイズ法であるnlproofs (natural language proof search) を提案する。
提案手法のコアでは,検証手順の妥当性を確認するために独立した検証器を訓練する。
強欲にステップを生成する代わりに、検証者が判断する大域的証明スコアを最大化する証明を探索する。
NLProofS は EntailmentBank と RuleTaker で最先端のパフォーマンスを達成する。
例えば、正確に予測された証明の割合を20.9%から33.3%に改善する。
ステップワイズ手法が人間による証明のより良い生成に繋がったのはこれが初めてである。
関連論文リスト
- Next-Token Prediction Task Assumes Optimal Data Ordering for LLM Training in Proof Generation [27.60611509339328]
1つのトレーニングデータサンプルの最適順序は、特定の証明ステップの関連中間監督が、その証明ステップの左側に常に配置されているときに発生すると論じる。
証明が直感的に逐次順序にある場合、トレーニングが最も効果的であることを示す。
論文 参考訳（メタデータ） (2024-10-30T18:00:04Z) - Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
証明の各ステップに先立って,非公式な思考を生成するために,言語モデルをトレーニングするフレームワークであるLean-STaRを紹介します。
Lean-STaRは、Lean定理証明環境内のminiF2F-testベンチマークで最先端の結果を達成する。
論文 参考訳（メタデータ） (2024-07-14T01:43:07Z) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10～26。
論文 参考訳（メタデータ） (2024-05-23T10:35:08Z) - Learn from Failure: Fine-Tuning LLMs with Trial-and-Error Data for Intuitionistic Propositional Logic Proving [41.23045212775232]
探索経路の失敗から学習する訓練モデルの利点を実証する。
既存のオープンソース定理証明データセットにそのような試行錯誤データが欠如しているにもかかわらず、直観論的命題論理定理のデータセットをキュレートする。
比較的短いトライアル・アンド・エラー情報(TrialMaster)で訓練されたモデルと、正しい経路でのみ訓練されたモデルを比較し、前者が低いトライアル探索でより目に見えない定理を解くことを発見した。
論文 参考訳（メタデータ） (2024-04-10T23:01:45Z) - Baldur: Whole-Proof Generation and Repair with Large Language Models [8.100054850290507]
我々は、自然言語のテキストとコードに基づいて訓練され、証明について微調整された大きな言語モデルを使用して、一度に定理のすべての証明を生成する。
我々は、この証明生成モデルと微調整の補修モデルを組み合わせて、生成した証明を修復し、さらに証明力を増強する。
本手法をプロトタイプであるBaldurで評価し、6,336 Isabelle/HOL定理とその証明のベンチマークで評価する。
論文 参考訳（メタデータ） (2023-03-08T22:00:15Z) - Natural Language Deduction with Incomplete Information [43.93269297653265]
当初,すべての前提が明記されていないような不特定設定を処理できる新しいシステムを提案する。
自然言語生成モデルを用いて、他の前提と結論が与えられた前提を誘導的に推論することにより、結論が真であるために必要な証拠の欠落を示唆することができる。
論文 参考訳（メタデータ） (2022-11-01T17:27:55Z) - NaturalProver: Grounded Mathematical Proof Generation with Language
Models [84.2064569475095]
自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。
本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。
NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
論文 参考訳（メタデータ） (2022-05-25T17:01:18Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳（メタデータ） (2021-06-02T17:58:35Z) - ProofWriter: Generating Implications, Proofs, and Abductive Statements
over Natural Language [19.917022148887273]
トランスフォーマーは自然言語理論上の論理推論をエミュレートすることが示されている。
ProofWriterと呼ばれる生成モデルは、理論の意味とそれらをサポートする自然言語の証明の両方を確実に生成できることを示しています。
論文 参考訳（メタデータ） (2020-12-24T00:55:46Z) - PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
本稿では,ルールベース上の二項質問に応答し,対応する証明を生成するトランスフォーマーモデルを提案する。
本モデルは,効率的な制約付き学習パラダイムを用いて,証明グラフに対応するノードやエッジを予測できることを学習する。
我々は、QAと証明生成のための有望な結果を示すために、合成、手書き、人文による規則ベースの実験を行う。
論文 参考訳（メタデータ） (2020-10-06T15:47:53Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。