論文の概要: LeanReasoner: Boosting Complex Logical Reasoning with Lean

• arxiv url: http://arxiv.org/abs/2403.13312v1
• Date: Wed, 20 Mar 2024 05:29:06 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-21 17:58:10.474995
• Title: LeanReasoner: Boosting Complex Logical Reasoning with Lean
• Title（参考訳）: LeanReasoner: 複雑な論理的推論をリーンで促進する
• Authors: Dongwei Jiang, Marcio Fonseca, Shay B. Cohen,
• Abstract要約: 大規模言語モデル(LLM)は、論理的不整合とそのような推論の固有の難しさのために、複雑な論理的推論に苦しむことが多い。 これらの課題に対処するために、定理実証フレームワークであるLeanを使用します。 論理的推論問題をリーン内の定理にフォーマルにすることで、対応する定理を証明または証明することで、それらを解決することができる。
• 参考スコア（独自算出の注目度）: 19.486080494198724
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) often struggle with complex logical reasoning due to logical inconsistencies and the inherent difficulty of such reasoning. We use Lean, a theorem proving framework, to address these challenges. By formalizing logical reasoning problems into theorems within Lean, we can solve them by proving or disproving the corresponding theorems. This method reduces the risk of logical inconsistencies with the help of Lean's symbolic solver. It also enhances our ability to treat complex reasoning tasks by using Lean's extensive library of theorem proofs. Our method achieves state-of-the-art performance on the FOLIO dataset and achieves performance near this level on ProofWriter. Notably, these results were accomplished by fine-tuning on fewer than 100 in-domain samples for each dataset.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、論理的不整合とそのような推論の固有の難しさのために、複雑な論理的推論に苦しむことが多い。 これらの課題に対処するために、定理実証フレームワークであるLeanを使用します。 論理的推論問題をリーン内の定理にフォーマルにすることで、対応する定理を証明または証明することで、それらを解決することができる。 この方法は、リーンのシンボリック・ソルバの助けを借りて、論理的不整合のリスクを低減する。 また、Leanの広範な定理証明ライブラリを使うことで、複雑な推論タスクを扱う能力も向上します。 提案手法は,FOLIOデータセット上での最先端性能を実現し,ProofWriterのこのレベルに近い性能を実現する。 特に、これらの結果はデータセットごとに100個未満のドメインサンプルを微調整することで達成された。

関連論文リスト

• Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
  この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。 マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。 その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
  論文  参考訳（メタデータ） (2024-10-21T08:04:21Z)
• Towards Generalizable and Faithful Logic Reasoning over Natural Language via Resolution Refutation [24.584926992534346]
  本稿では,GFaiR(Generalizable and Faithful Reasoner)という新しいフレームワークを提案する。 解法の難解化は、推論規則を拡張し、矛盾による証明の原理を採用することによって、全ての一階論理推論問題を解く能力を持つ。 我々のシステムは、単純なシナリオでパフォーマンスを維持しながら、複雑なシナリオで最先端のパフォーマンスを達成することで、これまでの作業より優れています。
  論文  参考訳（メタデータ） (2024-04-02T06:28:44Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• Are LLMs Rigorous Logical Reasoner? Empowering Natural Language Proof Generation with Contrastive Stepwise Decoding [11.385103498440932]
  本稿では,論理的推論のためのモデルの能力を高めるために,負の推論経路を用いることにより,ステップワイズな証明生成に対照的な復号を導入する。 EntailmentBankの実験は、言語モデルの計画能力を実証する上で、我々の手法の成功を裏付けている。
  論文  参考訳（メタデータ） (2023-11-12T05:12:49Z)
• LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers [60.009969929857704]
  論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。 本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。 我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
  論文  参考訳（メタデータ） (2023-10-23T17:58:40Z)
• LEGO-Prover: Neural Theorem Proving with Growing Libraries [86.1191481712352]
  LEGO-Prover では,証明された補題を含むスキルライブラリを,定理証明に使用される LLM の能力を高めるためのスキルとして活用する。 LEGO-Proverは、証明をモジュール的に構築することにより、ライブラリから取得した既存のスキルを活用し、証明プロセス中に新しいスキルを作成することができる。 我々のアブレーション研究は、これらの新たなスキルが定理の証明に役立つことを示唆し、47.1%から50.4%に改善した。
  論文  参考訳（メタデータ） (2023-10-01T12:47:59Z)
• LeanDojo: Theorem Proving with Retrieval-Augmented Language Models [72.54339382005732]
  大規模言語モデル(LLM)は、Leanのような証明アシスタントを使って形式的な定理を証明することを約束している。 既存のメソッドは、プライベートコード、データ、計算要求のために、複製や構築が難しい。 本稿では、ツールキット、データ、モデルからなるオープンソースのリーンツールキットであるLeanDojoを紹介します。 本研究では,LLM ベースの証明器 ReProver を開発した。
  論文  参考訳（メタデータ） (2023-06-27T17:05:32Z)
• Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning [101.26814728062065]
  大規模言語モデル(LLM)は人間のような推論能力を示しているが、それでも複雑な論理的問題に悩まされている。 本稿では,論理問題の解法を改善するために,LLMとシンボリックソルバを統合した新しいフレームワークであるLogic-LMを紹介する。
  論文  参考訳（メタデータ） (2023-05-20T22:25:38Z)

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

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