PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Liangming Pan, Alon Albalak, Xinyi Wang, William Yang Wang

arXiv:2305.12295v2cs.CLcs.AI

TL;DR

LLMs struggle with complex logical problems and lack guaranteed reasoning faithfulness. Logic-LM translates natural-language problems into symbolic forms, delegates inference to deterministic solvers, and uses self-refinement to revise formalizations. Across five datasets, it reports average improvements of 39.2% over standard prompting and 18.4% over chain-of-thought prompting.

  • Problem

    LLMs struggle with complex logical reasoning and can generate conclusions that do not follow their reasoning chains.

  • Method

    Logic-LM uses LLMs to formulate symbolic representations, deterministic solvers to perform inference, and self-refinement to revise erroneous formalizations.

  • Results

    39.2% average improvement over standard prompting and 18.4% over chain-of-thought prompting are reported across five logical reasoning datasets.

  • Takeaways & Limitations

    Logic-LM delegates complex reasoning to external symbolic solvers while retaining LLM flexibility for translating natural language into symbolic representations.

  • Takeaways & Limitations

    Logic-LM’s applicability is bounded by symbolic-solver expressiveness, and intricate symbolic grammars may challenge its in-context formulation process.

Abstract

from arXiv · show

Large Language Models (LLMs) have shown human-like reasoning abilities but still struggle with complex logical problems. This paper introduces a novel framework, Logic-LM, 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. We demonstrate Logic-LM's effectiveness on five logical reasoning datasets: ProofWriter, PrOntoQA, FOLIO, LogicalDeduction, and AR-LSAT. On average, Logic-LM achieves a significant performance boost of 39.2% over using LLM alone with standard prompting and 18.4% over LLM with chain-of-thought prompting. Our findings suggest that Logic-LM, by combining LLMs with symbolic logic, offers a promising avenue for faithful logical reasoning. Code and data are publicly available at https://github.com/teacherpeterpan/Logic-LLM.

1 Introduction

LLMs can produce human-like reasoning but still struggle with complex logical problems and may generate unfaithful reasoning. Logic-LM addresses this by combining LLM-based symbolic formulation with deterministic symbolic inference and self-refinement.

  • Motivation: LLMs still struggle with complex logical reasoning and can produce conclusions that do not follow their generated reasoning chains.Their probabilistic, black-box nature lacks a mechanism guaranteeing reasoning faithfulness.
  • Approach: Logic-LM decomposes logical problem solving into Problem Formulation, Symbolic Reasoning, and Result Interpretation.An LLM formulates the problem symbolically, a deterministic solver performs inference, and an interpreter maps the result to the answer.
  • Approach: Self-refinement revises generated logical forms using error messages from the symbolic solver as feedback.This module incrementally improves symbolic formalizations when solver interactions expose errors.
  • Evaluation: Logic-LM is evaluated on five datasets spanning deductive, first-order logic, constraint satisfaction, and analytical reasoning problems.The study uses ProofWriter, PrOntoQA, FOLIO, AR-LSAT, and LogicalDeduction, alongside four types of symbolic inference tools.
  • Results: 39.2% average improvement over standard prompting and 18.4% over chain-of-thought prompting are reported for integrating LLMs with symbolic solvers.The reported gains measure performance in logical reasoning across the evaluation datasets.

2 Related Work

Logic-LM differs from prior language-model and neuro-symbolic approaches by using symbolic language as the reasoning unit while retaining LLM flexibility for problem formulation. It extends tool-augmented reasoning to logical problems by delegating inference to external symbolic solvers rather than encoding procedures as programs.

  • Language Models for Logical Reasoning: Prior LLM approaches use fine-tuning or in-context prompts, including chain-of-thought, to improve logical reasoning.These methods elicit step-by-step reasoning capabilities through training or prompt design.
  • Neuro-Symbolic Reasoning: Logic-LM transfers complex, precise reasoning from LLMs to reliable, interpretable symbolic solvers while using in-context learning for symbolic formulation.This preserves flexibility while changing the basic unit of reasoning to symbolic language.
  • Neuro-Symbolic Reasoning: Unlike prior neuro-symbolic methods, Logic-LM does not require training or complex problem-specific modules.The paper characterizes earlier approaches as limited by specialized designs or optimization brittleness.
  • Tool-Augmented Language Models: Tool-augmented language models have improved arithmetic reasoning by generating executable programs, but logical reasoning has been harder to represent procedurally.Logical reasoning can involve hypothesizing, case analysis, and elimination rather than a straightforward sequence of commands.
  • Tool-Augmented Language Models: Logic-LM describes logical problems in symbolic language and offloads reasoning to external solvers instead of parsing problem-solving procedures as programs.This provides a tool-augmented route for handling nonlinear logical reasoning.
  • Auto-Formalization: Auto-formalization work shows that LLMs can translate many mathematical problems into formal specifications used by systems such as SymPy, Isabelle/HOL, and Lean.The paper positions mathematical reasoning as a numeric-specific subset of logical reasoning.

3 LOGIC-LM

Logic-LM formulates natural-language problems and goals in task-specific symbolic languages, applies deterministic external solvers, and translates their outputs into natural-language answers. It supports multiple reasoning types through corresponding formulations and solvers, with self-refinement for erroneous logical forms.

  • Framework: Logic-LM takes a natural-language problem P and goal G, then follows a problem formulation-and-reasoning paradigm.The inputs may include a multiple-choice or free-form question.
  • Framework: An LLM translates the problem and goal into a task-specific symbolic language before a deterministic solver obtains a symbolic answer.The framework shifts the LLM’s role from step-by-step problem solving to symbolic representation.
  • Problem Formulator: Four symbolic formulations cover deductive reasoning, first-order logic, constraint satisfaction, and analytical reasoning.The framework can accommodate additional tasks by defining further problem-specific formulations.
  • Problem Formulator: Logic-programming representations use facts, rules, and queries to express deductive reasoning problems.Facts are predicate-argument statements, rules derive facts from other facts, and queries are facts to prove.
  • Problem Formulator: FOL formulations divide parsed formulas into premises and a conclusion, while CSP formulations specify variables, domains, and constraints.SAT formulations represent a problem as constraints under a theory together with a query of interest.
  • Symbolic Reasoner: After symbolic parsing, task-specific deterministic solvers produce answers, including Pyke, Prover9, python-constraint, and Z3.These tools support logic programming, first-order logic, finite-domain CSPs, and SAT or SMT-style reasoning, respectively.
  • Self-Refinement: Self-refinement modifies inaccurate logical forms using symbolic-reasoner error messages as feedback.The LLM receives the erroneous form, the solver’s error message, and demonstrations of common error cases.
  • Result Interpreter: The result interpreter converts symbolic solver outputs into natural-language answers using rule-based or LLM-based interpretation.Rule-based mappings can handle simple outputs, while CSP results may require more complex translation.

4 Experiments

Experiments evaluate LOGIC-LM across five logical reasoning datasets and show stronger performance than standard prompting and chain-of-thought baselines. Analyses attribute these gains to solver-based reasoning, improved problem formulation, and self-refinement, while identifying semantic translation as a remaining challenge.

  • 4.1 Main Results: LOGIC-LM significantly outperforms standard LLMs and chain-of-thought across all five datasets.With GPT-3.5, it improves over standard prompting by 39.2% on average and over chain-of-thought by 18.4% on average.
  • 4.1 Main Results: GPT-4 improves over GPT-3.5 by 48.46% on average for standard prompting, while LOGIC-LM further improves GPT-4 by 24.98% over standard prompting and 10.44% over chain-of-thought.These results show gains from solver integration even with the stronger base model.
  • 4.1 Main Results: CoT gains are larger on PrOntoQA and ProofWriter, whereas symbolic solvers yield larger improvements on FOLIO, LogicalDeduction, and AR-LSAT.The reported LOGIC-LM improvements over CoT are 21.85% on FOLIO, 45.67% on LogicalDeduction, and 24.14% on AR-LSAT.
  • 4.2 Effectiveness of Problem Formulator: GPT-4’s executable-formulation rate is near 100% on synthetic datasets but falls to 79.9% on FOLIO and 32.6% on AR-LSAT.Executable rate measures grammar correctness, while executable accuracy measures semantic correctness; GPT-4 generally achieves high executable accuracy, including on AR-LSAT.
  • 4.3 Robustness of Reasoning: LOGIC-LM’s advantage increases with reasoning depth on ProofWriter, exceeding CoT by 7.1%, 5.0%, 12.7%, 20.0%, and 39.4% at depths 0, 1, 2, 4, and 5.Standard and CoT performance declines more sharply as problem complexity increases, while external solvers mitigate this degradation.
  • 4.4 Impact of Self-Refinement: Self-refinement increases executable formulation rates by 5.01 on average and generally improves final performance, although accuracy stagnates in later rounds.Solver error messages can repair invalid representations, but validity does not guarantee that the formulation correctly captures the problem semantics.

5 Conclusion and Future Work

The conclusion presents Logic-LM as a framework combining large language models with symbolic solvers, while identifying expressiveness, representation, and computational limitations for future work.

  • Logic-LM combines large language models with symbolic solvers to address logical reasoning problems.
  • Logic-LM could be extended with statistical relational learning systems and to commonsense reasoning problems involving complex and ambiguous rules.
  • The framework’s applicability is bounded by the expressiveness of the symbolic solver, because not all problems are easily encoded in first-order logic.The authors suggest integrating a more diverse set of symbolic solvers as a mitigation.
  • In-context learning and self-refinement may struggle with logical representations containing intricate grammar structures.The authors attribute this difficulty to conveying complex grammatical rules through limited demonstrations in a constrained context.
  • Using large language models for inference consumes significant energy, although few-shot in-context learning has a lower footprint than training models from scratch.

A Syntax for First-order Logic (FOL)

Table 4 presents the syntax for first-order logic.

  • Table 4 presents a first-order logic grammar.
  • The table is titled “First-Order Logic Grammar.”
  • The section provides a syntax reference for first-order logic.

B Dataset Statistics

Table 5 presents statistics of the logical reasoning datasets.

  • Table 5 presents statistics for the logical reasoning datasets.
  • The table summarizes dataset-level information for logical reasoning benchmarks.
  • The dataset statistics are collected in a dedicated table.

C Prompt Examples

The prompt examples show how standard in-context learning, chain-of-thought prompting, and Logic-LM structure logical reasoning tasks across several datasets. They include natural-language contexts, questions, answer options, reasoning or logic representations, and solver-oriented outputs.

  • C.1 PrOntoQA Prompts Standard In-Context Learning: Standard in-context prompts use two demonstrations containing a context, question, options, and the correct option.The examples cover PrOntoQA, FOLIO, LogicalDeduction, and AR-LSAT-style tasks.
  • Chain-of-Thought Prompting: Chain-of-thought prompts add a task description and explicit reasoning to the context, question, options, and answer format.Examples show intermediate deductions before selecting the correct option.
  • Chain-of-Thought Prompting: First-order-logic prompts specify conjunction, disjunction, exclusive disjunction, negation, implication, biconditional, and quantification in the output grammar.The grammar is paired with an output format containing a logic form and description.
  • Chain-of-Thought Prompting: Constraint-satisfaction prompts define domains and variables, then encode ordering relations and all-different constraints before testing answer options.The vehicle-ordering example assigns values from oldest to newest and represents each option as a constraint check.
  • C.5 AR-LSAT Prompts Standard In-Context Learning: For tour-scheduling questions, chain-of-thought reasoning fixes Thursday and Friday consequences, narrows the remaining days, and identifies option C as impossible.The corresponding standard prompt asks which schedule statement cannot be true.

C.2 ProofWriter Prompts Standard In-Context Learning

The ProofWriter standard in-context example presents a logical context, a three-way truth-status question, answer options, and the selected option.

  • C.2 ProofWriter Prompts Standard In-Context Learning: The example supplies facts and a conditional rule before asking whether the tiger is not young.The answer choices are True, False, and Unknown.
  • C.2 ProofWriter Prompts Standard In-Context Learning: The demonstrated answer is option B.The example labels the selected option as False.

Chain-of-Thought Prompting

Chain-of-thought prompting augments logical reasoning examples with task descriptions, intermediate reasoning, and structured symbolic representations. The examples span truth-status, first-order-logic, and predicate-based formulations.

  • Chain-of-Thought Prompting: The prompts frame the task as answering a logical reasoning question from a problem statement and context.This framing appears in the task descriptions accompanying the examples.
  • Chain-of-Thought Prompting: The tiger example includes intermediate deductions linking likes and observations to the conclusion that the tiger is young.The demonstrated answer remains option B for the statement that the tiger is not young.
  • Chain-of-Thought Prompting: A predicate-based formulation names predicates such as Quiet, Furry, White, and Young and records corresponding facts.The example also represents rules such as red people being young and young people being furry.
  • Chain-of-Thought Prompting: The symbolic example encodes facts and implications in a logic-oriented notation paired with natural-language descriptions.The representation includes Anne’s quietness, Harry’s whiteness, and rules connecting Red, Young, and Furry.

D Result Interpreter Implementation

The result interpreter uses different solver outputs for rule-based and first-order-logic datasets, then compares those outputs with the goal statement or maps them directly to veracity labels.

  • D Result Interpreter Implementation: For PrOntoQA and ProofWriter, Pyke returns the query variable’s inferred value or Unknown when it cannot be determined.The inferred value is compared with the goal statement to determine whether the goal is true or false.
  • D Result Interpreter Implementation: For FOLIO, the first-order-logic inference engine directly returns ENTAILMENT, CONTRADICTION, or CONTINGENT for the goal.These outputs serve as the goal’s veracity labels.

E Example Generations of LOGIC-LM

The examples show generated symbolic representations and predicted answers for a wild-turkey classification problem, with incorrect segments and their revisions identified.

  • The example asks whether Tom is an Ocellated wild turkey based on stated exclusions and the fact that Tom is a wild turkey.
  • The wild-turkey instance lists six possible types and explicitly excludes Eastern, Osceola, Gould's, Merriam's, and Rio Grande wild turkeys for Tom.
  • Figure 6 compares incorrect symbolic-representation segments with their corresponding problem text and correct revisions.
Loading 2305.12295v2…