LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers

要約

論理的推論、つまり一連の前提から結論の真理値を演繹的に推測することは、科学、数学、社会に広範な潜在的な影響を与える人工知能にとって重要なタスクです。
大規模言語モデル (LLM) がそのような推論をより効果的に実行できるようにするために、多くのプロンプトベースの戦略が提案されていますが、依然として満足のいくものではなく、微妙で予測不可能な方法で失敗することがよくあります。
この研究では、代わりにモジュール式神経記号プログラミング (LINC: Logical Inference via Neurosymbolic Computation) と呼ばれるタスクを再定式化することの妥当性を調査します。
LINC では、LLM はセマンティック パーサーとして機能し、前提と結論を自然言語から一次論理の式に変換します。
これらの式は、外部の定理証明器にオフロードされ、演繹的推論が記号的に実行されます。
このアプローチを活用することで、評価したほぼすべての実験条件において、3 つの異なるモデルについて FOLIO とバランスのとれた ProofWriter のサブセットで大幅なパフォーマンスの向上が観察されました。
ProofWriter では、比較的小規模なオープンソース StarCoder+ (15.5B パラメーター) を LINC で強化すると、思考連鎖 (CoT) プロンプトを備えた GPT-3.5 と GPT-4 をそれぞれ絶対 38% と 10% 上回ります。
GPT-4 と併用すると、LINC スコアは ProofWriter で CoT より 26% 高くなりますが、FOLIO では比較的高いパフォーマンスを発揮します。
さらに分析を進めると、このデータセットではどちらの方法も平均してほぼ同じ頻度で成功しますが、異なる相補的な故障モードを示すことが明らかになりました。
したがって、私たちは、記号証明者と LLM を共同利用することで、自然言語に対する論理的推論にどのように取り組むことができるかについて、有望な証拠を提供します。
対応するすべてのコードは https://github.com/benlipkin/linc で公開されています。

要約(オリジナル)

Logical reasoning, i.e., deductively inferring the truth value of a conclusion from a set of premises, is an important task for artificial intelligence with wide potential impacts on science, mathematics, and society. While many prompting-based strategies have been proposed to enable Large Language Models (LLMs) to do such reasoning more effectively, they still appear unsatisfactory, often failing in subtle and unpredictable ways. In this work, we investigate the validity of instead reformulating such tasks as modular neurosymbolic programming, which we call LINC: Logical Inference via Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser, translating premises and conclusions from natural language to expressions in first-order logic. These expressions are then offloaded to an external theorem prover, which symbolically performs deductive inference. Leveraging this approach, we observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate. On ProofWriter, augmenting the comparatively small open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5 and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%, respectively. When used with GPT-4, LINC scores 26% higher than CoT on ProofWriter while performing comparatively on FOLIO. Further analysis reveals that although both methods on average succeed roughly equally often on this dataset, they exhibit distinct and complementary failure modes. We thus provide promising evidence for how logical reasoning over natural language can be tackled through jointly leveraging LLMs alongside symbolic provers. All corresponding code is publicly available at https://github.com/benlipkin/linc

arxiv情報

提供元, 利用サービス

arxiv.jp, Google