論文の概要: Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive
Synthesis using Large Language Models and Satisfiability Solving
- arxiv url: http://arxiv.org/abs/2309.16436v1
- Date: Thu, 28 Sep 2023 13:40:50 GMT
- ステータス: 処理完了
- システム内更新日: 2023-09-29 14:19:18.623918
- Title: Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive
Synthesis using Large Language Models and Satisfiability Solving
- Title(参考訳): 計画のためのニューロシンボリック推論:大規模言語モデルと満足度解法を用いた反例誘導帰納的合成
- Authors: Sumit Kumar Jha, Susmit Jha, Patrick Lincoln, Nathaniel D. Bastian,
Alvaro Velasquez, Rickard Ewetz, Sandeep Neema
- Abstract要約: インストラクショントレーニングを備えた生成型大規模言語モデル(LLM)は、プロンプトに対する人間的な応答を生成することができる。
精度が向上したにもかかわらず、これらのモデルは事実的に誤りまたは文脈的に不適切な結果をもたらすことが知られている。
この制限により、これらのモデルを使用して安全クリティカルなアプリケーションで使用される形式的なアーティファクトを合成することが困難になる。
- 参考スコア(独自算出の注目度): 23.426866969743525
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Generative large language models (LLMs) with instruct training such as GPT-4
can follow human-provided instruction prompts and generate human-like responses
to these prompts. Apart from natural language responses, they have also been
found to be effective at generating formal artifacts such as code, plans, and
logical specifications from natural language prompts. Despite their remarkably
improved accuracy, these models are still known to produce factually incorrect
or contextually inappropriate results despite their syntactic coherence - a
phenomenon often referred to as hallucination. This limitation makes it
difficult to use these models to synthesize formal artifacts that are used in
safety-critical applications. Unlike tasks such as text summarization and
question-answering, bugs in code, plan, and other formal artifacts produced by
LLMs can be catastrophic. We posit that we can use the satisfiability modulo
theory (SMT) solvers as deductive reasoning engines to analyze the generated
solutions from the LLMs, produce counterexamples when the solutions are
incorrect, and provide that feedback to the LLMs exploiting the dialog
capability of instruct-trained LLMs. This interaction between inductive LLMs
and deductive SMT solvers can iteratively steer the LLM to generate the correct
response. In our experiments, we use planning over the domain of blocks as our
synthesis task for evaluating our approach. We use GPT-4, GPT3.5 Turbo,
Davinci, Curie, Babbage, and Ada as the LLMs and Z3 as the SMT solver. Our
method allows the user to communicate the planning problem in natural language;
even the formulation of queries to SMT solvers is automatically generated from
natural language. Thus, the proposed technique can enable non-expert users to
describe their problems in natural language, and the combination of LLMs and
SMT solvers can produce provably correct solutions.
- Abstract(参考訳): gpt-4のようなインストラクショントレーニングを備えた生成型大言語モデル(llm)は、人間の指示に従って、これらのプロンプトに対する人間的な応答を生成することができる。
自然言語応答とは別に、コードや計画、論理仕様といった形式的なアーティファクトを自然言語プロンプトから生成する上でも有効であることが判明した。
精度が著しく改善されているにもかかわらず、これらのモデルは、構文的コヒーレンスにもかかわらず、事実的に誤りまたは文脈的に不適切な結果をもたらすことが知られている。
この制限により、これらのモデルを使用して安全クリティカルなアプリケーションで使用される形式的なアーティファクトを合成することが困難になる。
テキスト要約や質問回答のようなタスクとは異なり、LLMが生成するコードや計画、その他の形式的なアーティファクトのバグは破滅的です。
我々は,SMT法を導出的推論エンジンとして利用して,LLMから生成した解を解析し,解が正しくない場合に逆例を生成できることを仮定し,インストラクション学習されたLLMのダイアログ機能を利用したLLMへのフィードバックを提供する。
インダクティブLLMとインダクティブSMTソルバとのこの相互作用は、LLMを反復的に操り、正しい応答を生成する。
実験では,ブロック領域上のプランニングを,我々のアプローチを評価するための合成タスクとして利用した。
GPT-4, GPT3.5 Turbo, Davinci, Curie, Babbage, Ada をLSM, Z3 をSMTソルバとして使用する。
本手法では,smtソルバへのクエリの定式化も自然言語から自動的に生成するので,ユーザが自然言語で計画問題を伝えることができる。
提案手法により,非熟練者が自然言語で問題を記述できるようになり,LLMとSMTの解法を組み合わせることで,有効に正しい解が得られる。
関連論文リスト
- Can LLMs Converse Formally? Automatically Assessing LLMs in Translating and Interpreting Formal Specifications [21.12437562185667]
本稿では,自然言語記述と形式仕様の変換における大規模言語モデルの有用性を評価する。
本稿では,LLMの2つのコピーと既製の検証器を併用して,翻訳能力を自動評価する手法を提案する。
論文 参考訳(メタデータ) (2024-03-27T08:08:00Z) - Frugal LMs Trained to Invoke Symbolic Solvers Achieve
Parameter-Efficient Arithmetic Reasoning [36.8749786658624]
大規模言語モデル(LLM)は、スケールで発生した振る舞いとしてゼロショットの数学的推論能力を示す。
算術語問題を正規化テーマ解決タスクとして提案した場合,小さいLMでは合理的な算術的推論が可能であることを示す。
論文 参考訳(メタデータ) (2023-12-09T13:20:49Z) - LM-Polygraph: Uncertainty Estimation for Language Models [71.21409522341482]
不確実性推定(UE)手法は、大規模言語モデル(LLM)の安全性、責任性、効果的な利用のための1つの経路である。
テキスト生成タスクにおけるLLMの最先端UEメソッドのバッテリを実装したフレームワークであるLM-PolygraphをPythonで統一したプログラムインタフェースで導入する。
研究者によるUEテクニックの一貫した評価のための拡張可能なベンチマークと、信頼スコア付き標準チャットダイアログを強化するデモWebアプリケーションを導入している。
論文 参考訳(メタデータ) (2023-11-13T15:08:59Z) - Language Models can be Logical Solvers [99.40649402395725]
論理解法の推論過程を直接エミュレートする新しい言語モデルであるLoGiPTを導入する。
LoGiPTは、導出的ソルバの見えない推論過程を明らかにして精錬することから導かれる、新しく構築された命令チューニングデータセットに基づいて微調整される。
論文 参考訳(メタデータ) (2023-11-10T16:23:50Z) - Automatic Hallucination Assessment for Aligned Large Language Models via
Transferable Adversarial Attacks [98.22864957942821]
本稿では,大規模言語モデルが忠実に振る舞う既存データを適切に修正し,評価データを自動的に生成する手法を開発することを目的とする。
具体的には,LLM ベースのフレームワークである Auto Debug について述べる。
実験結果から, LLMは, インプロンプトに与えられた知識とパラメトリック知識との間に矛盾がある場合, 質問応答シナリオの2つのカテゴリに幻覚を与える可能性が示唆された。
論文 参考訳(メタデータ) (2023-10-19T06:37:32Z) - Leveraging Large Language Models to Generate Answer Set Programs [5.532477732693001]
大規模言語モデル(LLM)は、様々な自然言語処理タスクにおいて例外的な性能を示した。
本稿では,大規模言語モデルの強みと解集合プログラミングを組み合わせたニューロシンボリック手法を提案する。
論文 参考訳(メタデータ) (2023-07-15T03:40:55Z) - Evaluating Language Models for Mathematics through Interactions [116.67206980096513]
大型言語モデル(LLM)と対話し,評価するためのプロトタイププラットフォームであるCheckMateを紹介した。
我々はCheckMateと共同で3つの言語モデル(InstructGPT, ChatGPT, GPT-4)を、学部レベルの数学の証明支援として評価する研究を行った。
我々は、人間の行動の分類を導き、概して肯定的な相関にもかかわらず、正しさと知覚的有用性の間に顕著な相違点があることを明らかにする。
論文 参考訳(メタデータ) (2023-06-02T17:12:25Z) - Check Your Facts and Try Again: Improving Large Language Models with
External Knowledge and Automated Feedback [127.75419038610455]
大規模言語モデル(LLM)は、ダウンストリームタスクの多くに対して、人間のような、流動的な応答を生成することができる。
本稿では,プラグ・アンド・プレイモジュールのセットでブラックボックスのLSMを増強するLSM-Augmenterシステムを提案する。
論文 参考訳(メタデータ) (2023-02-24T18:48:43Z) - Translating Natural Language to Planning Goals with Large-Language
Models [19.738395237639136]
近年の大規模言語モデル(LLM)は,様々な自然言語処理(NLP)タスクにおいて顕著な性能を示した。
我々の中心的な問題は、LLMが自然言語で指定された目標を構造化された計画言語に翻訳できるかどうかである。
GPT 3.5 変種に対する実験結果から,LCM は計画よりも翻訳に適していることが示された。
論文 参考訳(メタデータ) (2023-02-10T09:17:52Z) - PAL: Program-aided Language Models [112.94785609781503]
自然言語問題を理解するために,プログラム支援言語モデル(PaL)を提案する。
PaLはソリューションステップをPythonインタプリタのようなプログラムランタイムにオフロードする。
私たちは12のベンチマークで新しい最先端の結果を設定しました。
論文 参考訳(メタデータ) (2022-11-18T18:56:13Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。