LTRAG: Enhancing Autoformalization and Self-refinement for Logical Reasoning with Thought-Guided RAG

Logical reasoning is fundamental to intelligent systems. Large language models (LLMs) have demonstrated promise in natural language (NL) reasoning, especially with techniques like chain-of-thought (CoT) prompting. Neurosymbolic methods like Logic-LM and LINC further enhance performance on challenging datasets FOLIO and AR-LSAT by integrating formalization with LLMs and symbolic solvers, and possibly refinement with LLMs. However, these methods still struggle with the accurate formalization of complex NL problems. In this paper, we introduce LTRAG, a framework to enhance autoformalization and selfrefinement for logical reasoning with Retrieval-Augmented Generation (RAG), by building knowledge bases of thought-guided examples 1 . Experimental results on FOLIO and AR-LSAT show that LTRAG consistently outperforms Logic-LM and LINC across different models. On GPT-4 and AR-LSAT, it achieves an accuracy gain of 13% over Logic-LM.