Answering Questions with ATP and LLMs

Abstract

This talk describes a process for answering natural language questions using ATP and LLMs. The natural language question is translated to logic using the ShZZaM tool, an ATP system is used to find a refutation that that there is an answer to the question, Taelja is used to convert the refutation to a proof that answers the questions, and an LLM translates the proof to a natural language answer. The answer found using that process is compared with the answer that comes directly from the LLM.