Satisfiability-Aided Language Models Using Declarative Prompting

要約

これまでの研究では、大規模言語モデル (LLM) での思考連鎖プロンプトとプログラム表現を組み合わせて、効果的かつ透過的な推論を実行していました。
このようなアプローチは、前向き推論のみを必要とするタスク (単純な算術など) には非常にうまく機能しますが、より高度な計画と検索を必要とする制約解決問題にはあまり効果的ではありません。
この論文では、LLM の推論能力を向上させるための新しい充足可能性支援型言語モデリング (SATLM) アプローチを提案します。
LLM を使用して命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終的な答えを導き出します。
このアプローチには 2 つの重要な利点があります。
宣言的仕様は推論ステップよりも問題の説明に近いため、LLM は説明からそれをより正確に解析できます。
さらに、実際の推論タスクを自動化された定理証明者にオフロードすることにより、私たちのアプローチは、解析された仕様に対する答えの正確さを保証し、解決プロセスにおける計画エラーを回避できます。
私たちは 6 つの異なるデータセットで SATLM を評価し、命令型パラダイムにおいてプログラム支援 LM よりも一貫して優れたパフォーマンスを示すことを示しました。
特に、SATLM は、GSM 算術推論データセットの困難なサブセットにおいて、プログラム支援 LM よりも 23% 優れたパフォーマンスを発揮します。
SATLM は、LSAT 上で新しい SoTA も実現し、完全なトレーニング セットでトレーニングされた以前のモデルを上回ります。

要約(オリジナル)

Prior work has combined chain-of-thought prompting in large language models (LLMs) with programmatic representations to perform effective and transparent reasoning. While such an approach works very well for tasks that only require forward reasoning (e.g., straightforward arithmetic), it is less effective for constraint solving problems that require more sophisticated planning and search. In this paper, we propose a new satisfiability-aided language modeling (SATLM) approach for improving the reasoning capabilities of LLMs. We use an LLM to generate a declarative task specification rather than an imperative program and leverage an off-the-shelf automated theorem prover to derive the final answer. This approach has two key advantages. The declarative specification is closer to the problem description than the reasoning steps are, so the LLM can parse it out of the description more accurately. Furthermore, by offloading the actual reasoning task to an automated theorem prover, our approach can guarantee the correctness of the answer with respect to the parsed specification and avoid planning errors in the solving process. We evaluate SATLM on 6 different datasets and show that it consistently outperforms program-aided LMs in an imperative paradigm. In particular, SATLM outperforms program-aided LMs by 23% on a challenging subset of the GSM arithmetic reasoning dataset; SATLM also achieves a new SoTA on LSAT, surpassing previous models that are trained on the full training set.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google