Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning

• LLMs struggle with complex logical problems and can produce unfaithful reasoning, while symbolic solvers offer transparent inference but depend on accurate translation from natural language.Logic-LM combines LLM language understanding with symbolic solvers’ logical faithfulness and transparency.Source: §1 · p. 1
• The framework has three stages: LLM problem formulation, deterministic symbolic reasoning, and result interpretation that maps solver output to an answer.Self-refinement iteratively revises generated logical forms using symbolic-solver error messages as feedback.Source: §1 · p. 2
• Evaluations span five datasets covering deductive reasoning, first-order logic, constraint satisfaction, and analytical reasoning.The datasets are ProofWriter, PrOntoQA, FOLIO, AR-LSAT, and LogicalDeduction.Source: §1 · p. 2
• The framework uses four solver types: logic programming, first-order logic inference, finite-domain constraint optimization, and SAT solving for analytical reasoning.Source: §1 · p. 2
• Logic-LM improves average performance by 39.2% over standard prompting and 18.4% over chain-of-thought prompting.The introduction also reports that Logic-LM becomes increasingly effective as required reasoning depth increases.Source: §1 · p. 2

Language Models for Logical Reasoning

• Fine-tuning and in-context prompting methods reason directly in natural language, which is flexible but can produce unfaithful reasoning and hallucinations.Examples include chain-of-thought prompting (Wei et al., 2022b; Wang et al., 2023) and least-to-most prompting (Zhou et al., 2023); fine-tuning examples include Clark et al. (2020), Tafjord et al. (2022), and Yang et al. (2022).Source: §2 · p. 2
• Logic-LM uses LLMs to formulate symbolic representations, then delegates precise inference to external symbolic solvers while retaining in-context flexibility.This shifts complex reasoning from the LLM to solvers described as more reliable and interpretable.Source: §2 · p. 2
• Prior neuro-symbolic methods can require hand-crafted or specialized modules or be brittle to optimize; Logic-LM aims for generality without training or problem-specific modules.Prior approaches include Mao et al. (2019), Gupta et al. (2020), Manhaeve et al. (2021), Cai et al. (2021), Tian et al. (2022), and Pryor et al. (2023).Source: §2 · p. 2

Tool-augmented Language Models

• Tool-augmented LLMs have used generated Python for arithmetic reasoning (Gao et al., 2023; Chen et al., 2022), but nonlinear logical procedures resist direct representation as functional programs.Logic-LM instead describes the problem symbolically and offloads reasoning to external solvers; cited tools also include retrievers (Shi et al., 2023), calculators (Cobbe et al., 2021), code interpreters, and planners (Liu et al., 2023a).Source: §2 · p. 3

Auto-Formalization

• LLMs have formalized mathematical problems for tools such as SymPy, Isabelle/HOL, and Lean, while Logic-LM extends auto-formalization to broader logical reasoning tasks.Mathematical problems are described as more readily formalized because they focus on numeric deductions; broader logical tasks may require world knowledge and commonsense (Wu et al., 2022; Drori et al., 2022; He-Yueya et al., 2023; Jiang et al., 2023).Source: §2 · p. 3

3 LOGIC-LM

• Logic-LM separates problem formulation from deterministic symbolic inference, aiming for faithful answers when the formulation is correct and shifting the LLM’s focus from step-by-step reasoning to symbolic representation.A result interpreter then translates the solver’s answer into natural language.Source: §3 · p. 4

3.1 Problem Formulator

• The formulator uses four task-specific grammars—Prolog-style facts, rules, and queries; FOL premises and conclusions; CSP variables, domains, and constraints; and SAT constraints and queries—and can add formulations for other tasks.LLMs receive grammar instructions and few-shot examples to identify entities, facts, and rules and encode them in symbolic languages.Source: §3.1 · pp. 4–5

3.2 Symbolic Reasoner

• Task-matched deterministic solvers execute the symbolic representations: Pyke for deductive reasoning, Prover9 for FOL, python-constraint3 for CSPs, and Z3 for SAT.Pyke uses forward- and backward-chaining; Prover9 converts formulas to CNF and applies resolution.Source: §3.2 · p. 5

3.3 Self-Refiner

• The self-refiner prompts the LLM with an erroneous logical form, solver error message, and demonstrations of common errors and remedies, repeating revisions until errors stop or the revision limit is reached.This module addresses the difficulty of generating correct logical forms for complex problems.Source: §3.3 · pp. 5–6

3.4 Result Interpreter

• The result interpreter uses rules or an LLM to turn solver outputs into natural-language answers, with rule mappings for simple cases and more complex translation for CSP assignments.For example, a CSP assignment can be rendered as a sentence identifying which vehicle is oldest.Source: §3.4 · p. 6

4 Experiments

• Evaluation covers hardest 5-hop PrOntoQA and depth-5 ProofWriter (600 balanced samples), plus full test sets for FOLIO (204), LogicalDeduction (300), and AR-LSAT (231).FOLIO problems are expert-written and real-world aligned; AR-LSAT contains multiple-choice analytical reasoning questions from 1991 to 2016.Source: §4 · p. 6
• All models use the same 1–5 in-context examples and multiple-choice format, with temperature 0; comparisons cover standard prompting and CoT using ChatGPT, GPT-3.5, and GPT-4.Performance is measured by answer accuracy, with LLM responses selected at the highest probability.Source: §4 · p. 6

4.1 Main Results

• 39.2% average improvement over standard LLMs and 18.4% over CoT: LOGIC-LM with GPT-3.5 outperforms both baselines across all five datasets.The reported LOGIC-LM results use no self-refinement; unexecutable symbolic formulations fall back to CoT.Source: Table 2 · p. 7, §4.1 · p. 7
• GPT-4 improves over GPT-3.5 by 48.46% with standard prompting, and LOGIC-LM further improves GPT-4 by 24.98% over standard prompting and 10.44% over CoT.CoT gains vary by dataset: 51.59% on PrOntoQA and 33.82% on ProofWriter, but 11.75% on FOLIO, 9.41% on LogicalDeduction, and -3.2% on AR-LSAT; LOGIC-LM exceeds CoT by 21.85%, 45.67%, and 24.14% on the latter three, respectively.Source: §4.1 · p. 7

4.3 Robustness of Reasoning

• On ProofWriter, LOGIC-LM’s advantage over CoT rises from 7.1% at depth 0 to 39.4% at depth 5, while standard and CoT performance declines more sharply as reasoning depth increases.The evaluation sampled 300 examples from each reasoning-depth subset with balanced labels; the trend supports the approach of delegating multi-step inference to symbolic solvers.Source: Figure 3 · p. 8, §4.3 · p. 8

4.2 Effectiveness of Problem Formulator

• GPT-4’s executable-formulation rate is 79.9% on FOLIO and 32.6% on AR-LSAT, despite near-100% rates on synthetic PrOntoQA and ProofWriter and LogicalDeduction.Executable rate measures grammar correctness, whereas executable accuracy measures semantic correctness; GPT-4 generally has high executable accuracy, including on AR-LSAT.Source: §4.2 · p. 8

4.4 Impact of Self-Refinement

• Self-refinement increases executable-formulation rate by 5.01 on average, and further rounds on FOLIO raise executability and final performance even as accuracy stagnates.Solver error messages can repair invalid representations but do not ensure that a valid representation accurately captures the problem.Source: §4.4 · pp. 8–9, Figure 4 · p. 8

Conclusion and Future Work

• Logic-LM combines large language models with symbolic solvers and significantly improves performance over pure LLMs and chain-of-thought prompting.The paper presents Logic-LM as one instantiation of this framework.Source: §5 · p. 9
• Future extensions could integrate statistical relational learning systems, including Markov logic networks and probabilistic soft logic, to support reasoning under uncertainty.The authors also identify commonsense reasoning over complex and ambiguous rules as a significant challenge and potential extension.Source: §5 · p. 9

Limitations

• LOGIC-LM’s reliance on symbolic encoding bounds applicability by solver expressiveness, though integrating diverse solvers could mitigate this limitation.Not all problems are easily encoded in first-order logic; the framework’s flexible design supports integration of additional solvers.Source: Limitations · p. 10
• In-context learning with self-refinement may struggle to map natural-language problems into symbolic forms with intricate grammars, such as probabilistic soft logic.The paper attributes this to the difficulty of conveying complex grammatical rules through limited demonstrations within a constrained context size.Source: Limitations · p. 10
• Future work could develop specialized natural-language-to-symbolic mapping modules, including fine-tuning LLMs on synthetic data generated by symbolic solvers.Source: Limitations · p. 10

Ethics Statement

• Few-shot in-context learning gives this work a lower energy footprint than training models from scratch, but inference APIs—especially GPT-4—consume significant energy.The authors note that LLM training requires substantial computational energy and contributes to global warming.Source: Ethics Statement · p. 10

• Table 4 is titled “First-Order Logic Grammar.”Source: Table 4 · p. 14

B Dataset Statistics

• Table 5 reports statistics for the logical-reasoning datasets.The supplied passage identifies the table’s scope but does not provide its cell values.Source: Table 5 · p. 14

C Prompt Examples

• The prompt examples use two demonstrations per setting, with standard prompting, chain-of-thought, and Logic-LM differing in their included components.Standard prompts include context, question, and options; chain-of-thought and Logic-LM add a task description and respectively a reasoning chain or symbolic program.Source: C Prompt Examples · p. 14

Chain-of-Thought Prompting

• A prompt example specifies parsing a problem and question into first-order logic, with a grammar covering connectives and universal and existential quantification.Its listed operators include conjunction, disjunction, negation, implication, and biconditional.Source: Chain-of-Thought Prompting · p. 16
• A chain-of-thought example reasons from ordering clues that the raven is not rightmost and selects the quail as the rightmost object.The example concludes with option A.Source: Chain-of-Thought Prompting · p. 17
• A vehicle-ordering example represents the problem as a constraint-satisfaction task with a finite domain, variables, an all-different constraint, and a queried position.The example uses values 1 through 3 and tests whether the minivan is second-newest.Source: Chain-of-Thought Prompting · p. 17
• A constraint-satisfaction task is parsed by defining its domain, variables, and constraints; the example declares story and assistant sorts and checks whether named assignments to Tuscany are unsatisfiable.Source: Chain-of-Thought Prompting · p. 18

Standard In-Context Learning

• The standard in-context example supplies a context, asks whether a statement is true, false, or unknown, and presents three answer options.The sample question asks whether “The tiger is not young.”Source: Standard In-Context Learning · p. 15
• The standard in-context example marks option B as correct.Source: Standard In-Context Learning · p. 15

Chain-of-Thought Prompting

• The chain-of-thought example provides intermediate reasoning about the tiger and concludes with option B.Its displayed reasoning says the tiger likes the cow and squirrel, then states that the tiger is young.Source: Chain-of-Thought Prompting · p. 15
• The structured chain-of-thought task asks the model to define predicates, parse rules, list facts, and translate the question into logic.Source: Chain-of-Thought Prompting · p. 15
• The symbolic example defines predicates including Quiet, Furry, White, and Young, with typed arguments indicating entities and truth values.Source: Chain-of-Thought Prompting · p. 15
• The example represents Anne as quiet and Harry as white using facts, and gives “All red people are young” as a rule.Source: Chain-of-Thought Prompting · p. 15
• The symbolic example includes a rule that young people are furry and represents the question “Anne is white” as White(Anne, True).Source: Chain-of-Thought Prompting · p. 15

D Result Interpreter Implementation

• For PrOntoQA and ProofWriter, Pyke returns a query-variable value or Unknown, which the interpreter compares with the goal statement to determine whether the goal is True or False.For example, Pyke may return x = True for ConductElectricity(Nail, x), which is compared with ConductElectricity(Nail, False).Source: D Result Interpreter Implementation · p. 18
• For FOLIO, the interpreter maps the FOL engine’s ENTAILMENT, CONTRADICTION, and CONTINGENT labels to True, False, and Unknown, respectively.Source: D Result Interpreter Implementation · p. 18
• For LogicalDeduction, it checks whether each option’s parsed value appears among the solver’s possible assignments; for AR-LSAT, it separately proves each option.Source: D Result Interpreter Implementation · p. 18

• Figure 6 shows generated symbolic representations and predicted answers, highlighting incorrect segments and their problem correspondences in red and correct revisions in green.Source: Figure 6 · p. 19