Using Language Models For Knowledge Acquisition in Natural Language Reasoning Problems

TL;DR

This paper compares direct problem-solving with fact extraction plus theorem proving using LLMs, concluding that the latter approach yields better results for natural language reasoning puzzles.

Contribution

It demonstrates that combining language models for fact extraction with theorem provers outperforms direct problem-solving in natural language reasoning tasks.

Findings

Fact extraction plus theorem proving outperforms direct solving.

GPT-4 and ChatGPT effectively extract facts for reasoning.

The approach improves accuracy on logic puzzles.

Abstract

For a natural language problem that requires some non-trivial reasoning to solve, there are at least two ways to do it using a large language model (LLM). One is to ask it to solve it directly. The other is to use it to extract the facts from the problem text and then use a theorem prover to solve it. In this note, we compare the two methods using ChatGPT and GPT4 on a series of logic word puzzles, and conclude that the latter is the right approach.