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.

翻译：对于需要一定推理才能解决的自然语言问题，至少有两种使用大型语言模型（LLM）的方法。一种是直接要求模型解决问题。另一种是利用模型从问题文本中提取事实，然后使用定理证明器来求解。在本报告中，我们通过一系列逻辑文字谜题，使用ChatGPT和GPT4对这两种方法进行了比较，并得出结论：后者是更合适的方法。