Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving

要約

GPT-4 などの命令トレーニングを備えた生成大規模言語モデル (LLM) は、人間が提供する命令プロンプトに従い、これらのプロンプトに対して人間のような応答を生成できます。
自然言語応答とは別に、自然言語プロンプトからコード、計画、論理仕様などの正式な成果物を生成するのにも効果的であることがわかっています。
これらのモデルは精度が著しく向上しているにもかかわらず、構文上の一貫性にもかかわらず、事実上不正確または文脈上不適切な結果を生成することが依然として知られており、これはしばしば幻覚と呼ばれる現象です。
この制限により、安全性が重要なアプリケーションで使用される正式なアーティファクトを合成するためにこれらのモデルを使用することが困難になります。
テキストの要約や質問への回答などのタスクとは異なり、コード、計画、および LLM によって生成されるその他の形式的な成果物のバグは、致命的な結果をもたらす可能性があります。
我々は、充足可能性モジュロ理論 (SMT) ソルバーを演繹的推論エンジンとして使用して、LLM から生成された解を分析し、解が正しくない場合に反例を生成し、指示訓練された対話機能を利用して LLM にそのフィードバックを提供できると仮定します。
LLM。
帰納的 LLM と演繹的 SMT ソルバー間のこの相互作用により、正しい応答を生成するように LLM を繰り返し操作できます。
私たちの実験では、アプローチを評価するための合成タスクとしてブロックの領域にわたる計画を使用します。
GPT-4、GPT3.5 Turbo、Davinci、Curie、Babbage、および Ada を LLM として使用し、Z3 を SMT ソルバーとして使用します。
私たちの方法では、ユーザーは自然言語で計画の問題を伝えることができます。
SMT ソルバーへのクエリの定式化も自然言語から自動的に生成されます。
したがって、提案された手法により、専門家でないユーザーでも自然言語で問題を説明できるようになり、LLM と SMT ソルバーの組み合わせにより、証明された正しい解決策を生成できるようになります。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google