Satisfiability-Aided Language Models Using Declarative Prompting

要約

これまでの研究では、大規模言語モデル (LLM) での思考連鎖プロンプトとプログラム表現を組み合わせて、効果的かつ透過的な推論を実行していました。
このようなアプローチは、前向き推論のみを必要とするタスク (単純な算術など) では非常にうまく機能しますが、より高度な計画と検索を必要とする制約解決タスクではあまり効果的ではありません。
この論文では、LLM の推論能力を向上させるための新しい充足可能性支援言語モデリング アプローチを提案します。
LLM を使用して命令型プログラムではなく宣言型タスク仕様を生成し、既製の自動定理証明器を利用して最終的な答えを導き出します。
このアプローチには 2 つの重要な利点があります。
宣言的仕様は推論ステップよりも問題の説明に近いため、LLM はそれをより正確に解析できます。
さらに、実際の推論タスクを自動化された定理証明者にオフロードすることにより、私たちのアプローチは、解析された仕様に対する答えの正しさを保証し、推論プロセスにおける計画エラーを回避できます。
6 つの異なるデータセットで SATLM を評価し、命令型パラダイム (PROGLM) におけるプログラム支援 LM よりも一貫して優れていることを示しました。
特に、SATLM は、GSM の困難なサブセットにおいて PROGLM よりも 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 tasks that require more sophisticated planning and search. In this paper, we propose a new satisfiability-aided language modeling 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 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 reasoning process. We evaluate SATLM on 6 different datasets and show that it consistently outperforms program-aided LMs in an imperative paradigm (PROGLM). In particular, SATLM outperforms PROGLM by 23% on a challenging subset of GSM; SATLM also achieves a new SoTA on LSAT, surpassing previous models that are trained on the full training set.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google