Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
Large Language Models (LLMs) have shown human-like reasoning abilities but still struggle with complex logical problems. This paper introduces a novel framework, LOGICLM, which integrates LLMs with symbolic solvers to improve logical problem-solving. Our method first utilizes LLMs to translate a natural language problem into a symbolic formulation. Afterward, a deterministic symbolic solver performs inference on the formulated problem. We also introduce a self refinement module, which utilizes the symbolic solver’s error messages to revise symbolic formalizations.

Language Models for Logical Reasoning. Recent works in adapting LLMs for logical reasoning tasks can be broadly categorized into two groups: 1) fine-tuning approaches that optimize LLMs’ reasoning ability through fine-tuning or training specialized modules (Clark et al., 2020; Tafjord et al., 2022; Yang et al., 2022), and 2) in-context learning approaches that design special prompts to elicit LLMs’ step-by-step reasoning capabilities. Typical methods include chain-of-thought prompting (Wei et al., 2022b; Wang et al., 2023) that generates explanations before the final answer and the least-to most prompting (Zhou et al., 2023) that breaks the problem down into simpler components that can be solved individually. Both the above approaches perform reasoning directly over natural language (NL), providing greater flexibility than symbolic based reasoning. However, the intrinsic complexity and ambiguity of NL also bring undesired issues such as unfaithful reasoning and hallucinations.
we use symbolic language as the basic unit of reasoning. This effectively transfers the burden of executing complex, precise reasoning from LLMs to more reliable, interpretable external symbolic solvers. Simultaneously, we leverage the strong in-context learning ability of LLMs to formulate the NL-based problem into suitable symbolic representations, thus maintaining the benefit of flexibility.

Lines of inquiry this paper opens 24
Research framings built by reading the notes related to this paper — the questions it feeds into.
How effectively do deterministic tools improve language model reasoning on formal tasks?- Can symbolic solvers rescue language models from logical reasoning failures?
- Would hybrid systems combining LLMs with symbolic solvers overcome the retraction limitation?
- How do deterministic symbolic solvers improve the reliability of language model reasoning?
- Can symbolic solvers reliably replace LLM reasoning for logical tasks?
- What happens when LLMs grade other LLMs in closed evaluation loops?
- Why do LLMs fail inter-annotator agreement tests on argument evaluation?
- Can LLMs translate between natural language and formal logic faithfully?
- Why can LLMs interpret formal logic better than they generate it?
- Why do LLMs struggle to translate natural language into logical formalizations?
- Can LLMs successfully translate natural language into formal solver specifications?
- What concrete problems do LLMs solve at the computational level?
- How do LLMs lose information when translating natural language to formal logic?
- Why do LLMs fail at faithful autoformalisation of reasoning problems?
- Why do LLMs struggle with negation and exception handling?
- Why can't LLMs reason from first principles or initial commitments?
- Does LLM reasoning always match the outputs it generates?
- Can LLMs simultaneously reason and optimize their own modules?
- Why do LLMs fall for and deploy logical fallacies with equal confidence?