Divide and Translate: Compositional First-Order Logic Translation and Verification for Complex Logical Reasoning

要約

複雑な論理的推論タスクには長い推論シーケンスが必要ですが、思考連鎖プロンプトを備えた大規模言語モデル (LLM) ではまだ不十分です。
この問題を軽減するために、ニューロシンボリックなアプローチにはシンボリック ソルバーが組み込まれています。
具体的には、LLM は自然言語の問題を一次論理式で構成される充足可能性 (SAT) 問題に変換するだけであり、健全なシンボリック ソルバーは数学的に正しい解を返します。
しかし、LLM では、翻訳中に自然言語に隠された複雑な論理意味論を捕捉するのが難しいことがわかりました。
この制限を解決するために、構成的一次論理変換を提案します。
LLM は、まず自然言語文を解析して、アトミックな部分文とその依存部分から構成される新しく定義された論理依存構造に変換し、次に解析された部分文を順番に翻訳します。
単一の文に対して複数の論理依存構造と逐次翻訳が可能であるため、より信頼性の高い結果を保証するために 2 つの検証アルゴリズムも導入しています。
SAT ソルバーを利用して、生成された 1 次論理式のセマンティクスを厳密に比較し、最も可能性の高いものを選択します。
CLOVERと呼ばれる提案された方法を7つの論理的推論ベンチマークで評価し、それが以前の神経象徴的アプローチを上回り、新しい最先端の結果を達成することを示します。

要約(オリジナル)

Complex logical reasoning tasks require a long sequence of reasoning, which a large language model (LLM) with chain-of-thought prompting still falls short. To alleviate this issue, neurosymbolic approaches incorporate a symbolic solver. Specifically, an LLM only translates a natural language problem into a satisfiability (SAT) problem that consists of first-order logic formulas, and a sound symbolic solver returns a mathematically correct solution. However, we discover that LLMs have difficulties to capture complex logical semantics hidden in the natural language during translation. To resolve this limitation, we propose a Compositional First-Order Logic Translation. An LLM first parses a natural language sentence into newly defined logical dependency structures that consist of an atomic subsentence and its dependents, then sequentially translate the parsed subsentences. Since multiple logical dependency structures and sequential translations are possible for a single sentence, we also introduce two Verification algorithms to ensure more reliable results. We utilize an SAT solver to rigorously compare semantics of generated first-order logic formulas and select the most probable one. We evaluate the proposed method, dubbed CLOVER, on seven logical reasoning benchmarks and show that it outperforms the previous neurosymbolic approaches and achieves new state-of-the-art results.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google