論文の概要: Automated Theorem Provers Help Improve Large Language Model Reasoning

• arxiv url: http://arxiv.org/abs/2408.03492v1
• Date: Wed, 7 Aug 2024 01:03:56 GMT
• ステータス: 処理完了
• システム内更新日: 2024-08-08 14:16:39.507356
• Title: Automated Theorem Provers Help Improve Large Language Model Reasoning
• Title（参考訳）: 大規模言語モデルの推論を改善するための自動定理証明器
• Authors: Lachlan McGinness, Peter Baumgartner,
• Abstract要約: ニューロシンボリック・アーキテクチャーによっていかに精度が向上できるかを示す。 構文的および意味的エラーカテゴリのフレームワークを定義する。 我々は,構文的および意味的誤りを自動的に修正する機能を備えた手法を拡張した。
• 参考スコア（独自算出の注目度）: 0.18416014644193066
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this paper we demonstrate how logic programming systems and Automated first-order logic Theorem Provers (ATPs) can improve the accuracy of Large Language Models (LLMs) for logical reasoning tasks where the baseline performance is given by direct LLM solutions. We first evaluate LLM reasoning on steamroller problems using the PRONTOQA benchmark. We show how accuracy can be improved with a neuro-symbolic architecture where the LLM acts solely as a front-end for translating a given problem into a formal logic language and an automated reasoning engine is called for solving it. However, this approach critically hinges on the correctness of the LLM translation. To assess this translation correctness, we secondly define a framework of syntactic and semantic error categories. We implemented the framework and used it to identify errors that LLMs make in the benchmark domain. Based on these findings, we thirdly extended our method with capabilities for automatically correcting syntactic and semantic errors. For semantic error correction we integrate first-order logic ATPs, which is our main and novel contribution. We demonstrate that this approach reduces semantic errors significantly and further increases the accurracy of LLM logical reasoning.
• Abstract（参考訳）: 本稿では,論理プログラミングシステムと一階述語論理系(ATP)が,LLMソリューションによって基本性能が与えられる論理的推論タスクにおいて,Large Language Models(LLMs)の精度を向上させる方法を示す。 本稿ではまず,PRONTOQAベンチマークを用いて,蒸気ローラー問題に対するLCM推論の評価を行った。 我々は、LLMが与えられた問題を形式論理言語に翻訳するためのフロントエンドとしてのみ機能し、それを解決するために自動推論エンジンが呼び出されるニューロシンボリックアーキテクチャにおいて、いかに精度が向上できるかを示す。 しかし、このアプローチはLLM翻訳の正確性に批判的に依存している。 この翻訳精度を評価するために,構文的・意味的誤り分類の枠組みを第2に定義する。 我々は、このフレームワークを実装し、LLMがベンチマークドメインで犯したエラーを識別するために使用しました。 これらの結果に基づき,構文的および意味的誤りを自動的に修正する機能を備えた第3に手法を拡張した。 セマンティックな誤り訂正のために、我々は主かつ新しい貢献である一階述語論理ATPを統合する。 提案手法は意味的誤りを著しく低減し,LLM論理的推論の精度をさらに高めることを示す。

関連論文リスト

• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• LLM-ARC: Enhancing LLMs with an Automated Reasoning Critic [2.1073328551105623]
  LLM-ARCは,Large Language Models (LLM) の論理的推論能力を高めるために設計された,ニューロシンボリックなフレームワークである。 LLM-ARC は Actor-Critic 方式を採用しており、LLM アクターは宣言論理プログラムと意味的正当性テストを生成し、Automated Reasoning Critic はコードを評価し、テストを実行し、反復的洗練のためのテスト失敗に対するフィードバックを提供する。 実験では,LLMのみのベースラインよりも大幅に改善され,論理的テスト生成と反復的自己精製の重要性が強調された。
  論文  参考訳（メタデータ） (2024-06-25T15:52:15Z)
• NL2FOL: Translating Natural Language to First-Order Logic for Logical Fallacy Detection [45.28949266878263]
  本研究では,自然言語を一階論理に変換することによって,論理的誤りを確実に検出する手法を設計する。 次に、満足度モデュロ理論(SMT)を用いて、式の有効性を推論する。 私たちのアプローチは堅牢で解釈可能で、トレーニングデータや微調整は必要ありません。
  論文  参考訳（メタデータ） (2024-04-18T00:20:48Z)
• LogicAsker: Evaluating and Improving the Logical Reasoning Ability of Large Language Models [63.14196038655506]
  大規模言語モデル(LLM)の論理的推論能力を評価・拡張するための新しいアプローチであるLogicAskerを紹介する。 提案手法は, LLMが論理規則を学習する際の大きなギャップを明らかにし, 異なるモデル間で29%から90%の推論失敗を識別する。 GPT-4oのようなモデルにおける論理的推論を最大5%向上させることで、これらの知見を活用して、ターゲットとなる実演例と微調整データを構築した。
  論文  参考訳（メタデータ） (2024-01-01T13:53:53Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  本稿では,新しいタスク,CLOMO(Counterfactual Logical Modification)と高品質な人間アノテーションベンチマークを紹介する。 このタスクでは、LLMは所定の論理的関係を維持するために、与えられた議論的テキストを順応的に変更しなければなりません。 LLMの自然言語出力を直接評価する革新的な評価指標である自己評価スコア(SES)を提案する。
  論文  参考訳（メタデータ） (2023-11-29T08:29:54Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning [101.26814728062065]
  大規模言語モデル(LLM)は人間のような推論能力を示しているが、それでも複雑な論理的問題に悩まされている。 本稿では,論理問題の解法を改善するために,LLMとシンボリックソルバを統合した新しいフレームワークであるLogic-LMを紹介する。
  論文  参考訳（メタデータ） (2023-05-20T22:25:38Z)
• SatLM: Satisfiability-Aided Language Models Using Declarative Prompting [68.40726892904286]
  本研究では,大規模言語モデル (LLM) の推論能力を向上させるために,新しい満足度支援言語モデリング (SatLM) 手法を提案する。 我々はLLMを用いて命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終解を導出する。 我々はSATLMを8つの異なるデータセット上で評価し、命令パラダイムにおいてプログラム支援されたLMよりも一貫して優れていることを示す。
  論文  参考訳（メタデータ） (2023-05-16T17:55:51Z)

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

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