PaperlayerView exact revision on arXiv

Source-linked AI summary

LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers

Theo X. Olausson, Alex Gu, Benjamin Lipkin, Cedegao E. Zhang, Armando Solar-Lezama, Joshua B. Tenenbaum, Roger Levy

arXiv:2310.15164v2cs.CLcs.AI

TL;DR

LLM prompting has not made natural-language logical reasoning reliably robust, motivating a modular neurosymbolic alternative. LINC parses premises and conclusions into first-order logic and delegates deduction to a theorem prover, producing significant gains across nearly all evaluated conditions. The results support combining language models with symbolic provers while recognizing limits in formalization and scalability.

  • Problem

    Prompting-based strategies have not made LLM logical reasoning reliably robust, despite the importance of deductive reasoning for AI and NLP.

  • Method

    LINC uses an LLM as a semantic parser from natural language to first-order logic, then delegates deductive inference to an external theorem prover.

  • Results

    LINC yields significant performance gains in nearly every evaluated setting, except GPT-4 on FOLIO, and its errors differ from Chain-of-Thought errors.

  • Takeaways & Limitations

    The findings provide evidence that neurosymbolic systems integrating language models and theorem provers are promising for natural-language logical reasoning.

  • Takeaways & Limitations

    LINC depends on accurate natural-language-to-first-order-logic formalization, which becomes harder for longer paragraph-form premises and can cause incorrect deductions when information is lost.

Abstract

from arXiv · show

Logical reasoning, i.e., deductively inferring the truth value of a conclusion from a set of premises, is an important task for artificial intelligence with wide potential impacts on science, mathematics, and society. While many prompting-based strategies have been proposed to enable Large Language Models (LLMs) to do such reasoning more effectively, they still appear unsatisfactory, often failing in subtle and unpredictable ways. In this work, we investigate the validity of instead reformulating such tasks as modular neurosymbolic programming, which we call LINC: Logical Inference via Neurosymbolic Computation. In LINC, the LLM acts as a semantic parser, translating premises and conclusions from natural language to expressions in first-order logic. These expressions are then offloaded to an external theorem prover, which symbolically performs deductive inference. Leveraging this approach, we observe significant performance gains on FOLIO and a balanced subset of ProofWriter for three different models in nearly all experimental conditions we evaluate. On ProofWriter, augmenting the comparatively small open-source StarCoder+ (15.5B parameters) with LINC even outperforms GPT-3.5 and GPT-4 with Chain-of-Thought (CoT) prompting by an absolute 38% and 10%, respectively. When used with GPT-4, LINC scores 26% higher than CoT on ProofWriter while performing comparatively on FOLIO. Further analysis reveals that although both methods on average succeed roughly equally often on this dataset, they exhibit distinct and complementary failure modes. We thus provide promising evidence for how logical reasoning over natural language can be tackled through jointly leveraging LLMs alongside symbolic provers. All corresponding code is publicly available at https://github.com/benlipkin/linc

1 Introduction

LLM prompting can produce unreliable logical reasoning, motivating LINC, which combines natural-language parsing into first-order logic with symbolic theorem proving. The paper evaluates this approach against established LLM strategies and reports broad gains plus complementary failure modes.

  • Prompting-based LLM reasoning remains unreliable for tasks involving out-of-domain reasoning and negation.
  • Logical reasoning is important for AI and NLP because it can support more truthful chatbots, automated theorem proving, knowledge discovery, and consistent tutoring systems.
  • LINC converts natural-language premises and conclusions into first-order logic, uses a symbolic theorem prover to determine truth values, and applies majority voting.
  • The study compares LINC with three baseline LLM strategies across StarCoder+, GPT-3.5, GPT-4, FOLIO, and ProofWriter.
  • LINC improves performance in nearly every experimental condition except GPT-4 on FOLIO.
  • LINC and Chain-of-Thought exhibit distinct failure modes, suggesting potential synergy between the methods.

2 LINC: Logical Inference via Neurosymbolic Computation

LINC reformulates end-to-end natural-language reasoning as a modular pipeline: an LLM produces formal logic expressions, and an automated prover performs deduction. This trades flexible natural-language representations for strict formulas and exposes complementary precision-recall behavior relative to Chain-of-Thought.

  • LINC translates natural-language statements into first-order logic and passes the resulting expressions to Prover9 for symbolic deduction.
  • The reformulation replaces flexible natural-language reasoning with syntactically strict formulas that support symbolic algorithms with guarantees about deductive chains within the intermediate representation.
  • Compared with Chain-of-Thought, LINC has worse recall but better precision on True/False predictions.
  • The distinct error patterns suggest that LINC and in-context reasoning could complement one another.

3 Experiments

The experiments evaluate LINC and three controlled baselines across two challenging logical-reasoning datasets and three language models. They use balanced evaluation data, in-context examples, autoregressive generation, and primarily ten-way majority voting.

  • Datasets: The evaluation uses FOLIO and a balanced 360-example OWA subset of ProofWriter.FOLIO contributes 182 error-filtered validation examples; ProofWriter is balanced across proof depths and True, False, and Uncertain labels.
  • Evaluation procedure: Reported accuracies generally use K=10-way majority voting, selecting the modal prediction from ten independent samples.Ties between two labels are resolved by selecting the first generated label.
  • Evaluation procedure: The prompting workflow concatenates the original problem, in-context examples encoded in an intermediate markup language, and the evaluation problem before sampling to a stop token.
  • Models: The models are GPT-3.5, GPT-4, and StarCoder+, all pretrained on natural language and code and decoded at temperature T = 0.8.StarCoder+ is free and open access, unlike the other evaluated models.
  • Baselines: The baselines are Naïve direct labeling, Scratchpad logical-form generation with model-based solving, and Chain-of-Thought reasoning.Scratchpad ablates LINC’s symbolic solver by replacing it with the language model’s own prediction.

4 Results & Discussion

LINC improves logical-reasoning accuracy across the evaluated models and datasets, with especially strong gains on ProofWriter. Performance patterns vary by model and dataset, while proof-depth results suggest benefits for longer deductive chains.

  • Benchmark results: 14.2 points separate StarCoder+ LINC from its closest FOLIO baseline, reaching 56.0% versus 41.8% with Chain-of-Thought.For GPT-3.5, the corresponding FOLIO comparison is 62.6% versus 54.9%.
  • Benchmark results: LINC significantly improves performance across models on the balanced ProofWriter subset, with GPT-3.5 and GPT-4 reaching 96.4% and 98.3% mean accuracy.The results are shown alongside three baselines, grouped by StarCoder+, GPT-3.5, and GPT-4.
  • Benchmark results: GPT-4 reverses the FOLIO trend, with LINC underperforming Chain-of-Thought, but the difference is not significant (p = 0.58).The figure reports bootstrapped 10-way majority-vote accuracies with ±1 bootstrapped standard-deviation error bars.
  • Discussion: The authors propose synthetic short sentences and baseline difficulty with irrelevant premises and longer deductive chains as plausible reasons for LINC’s ProofWriter advantage.They note that the symbolic solver robustly handles irrelevant premises and long deductive chains after the LLM translates sentences into FOL.
  • Proof depth: On ProofWriter, LINC remains far above chance for StarCoder+ as proof depth increases, though its performance drops somewhat on deeper problems.The authors interpret this decline as evidence that StarCoder+ struggles with larger natural-language-to-FOL translations.
  • Proof depth: GPT-3.5 with LINC achieves near-perfect performance across ProofWriter proof depths, whereas its baselines quickly fall toward chance after shallow proofs.Chain-of-Thought completes some depth-1 tasks but is equivalent to chance within one standard deviation at higher depths.

5 Error Analysis

The error analysis finds distinct failure modes for LINC and Chain-of-Thought, with LINC’s mistakes often arising during natural-language-to-FOL formalization and producing complementary errors.

  • LINC failure modes: LINC can fail when FOL omits implicit information needed for deduction, such as encoding that Harry is a person.
  • LINC failure modes: LINC can also lose explicitly stated information through the chosen FOL representation, as with merging “Nazi German politician” into one symbol.
  • LINC failure modes: FOL generations contain syntax errors in 38% of StarCoderPlus, 24% of GPT-3.5, and 13% of GPT-4 generations.
  • CoT failure modes: CoT failures include conclusions that contradict the reasoning, incorrect deductions such as the converse fallacy, and failure to complete complex reasoning paths.
  • Quantitative comparison: LINC predicts Uncertain more often than CoT (57% vs. 41%), while achieving higher True/False precision (93% vs. 81%) but lower recall (60% vs. 75%).
  • Quantitative comparison: LINC’s misprediction similarity with other methods is 0.14, 0.21, and 0.22, versus 0.52, 0.54, and 0.56 among in-context methods.

6 Related Work

The related-work discussion situates LINC among research on eliciting reasoning, neurosymbolic methods, autoformalization, and tool-augmented language models.

  • Reasoning in LLMs: Prior work elicits natural-language reasoning through methods including Scratchpad, Chain-of-Thought, least-to-most prompting, and selection-inference.
  • Neurosymbolic reasoning: Neurosymbolic approaches combine neural networks with symbolic techniques for knowledge-base consistency and algorithmic reasoning over symbolically grounded inputs.
  • Neurosymbolic reasoning: Related logical-reasoning systems differ in how language models generate facts, invoke symbolic reasoners, or determine whether inference rules apply.
  • Autoformalization: Autoformalization research translates natural language into structured symbolic representations for theorem provers and system specifications.
  • Tool usage: Tool-usage work augments language models with calculators, code interpreters, retrieval systems, simulators, or predefined post-generation tools.

7 Conclusion

The conclusion reports that LINC improves logical reasoning across nearly all evaluated settings and produces errors that differ substantially from in-context reasoning methods.

  • LINC yields significant performance gains in nearly every evaluated setting and generalizes to larger premise sets than shown in in-context examples.
  • Quantitative and qualitative analyses indicate that LINC may complement Chain-of-Thought because the methods differ in the types and frequencies of their mistakes.
  • The authors present these findings as evidence supporting neurosymbolic approaches to natural-language reasoning and combining language models with symbolic reasoning engines.

8 Limitations

The paper identifies limitations involving task scope, natural-language formalization, scalability, logic expressiveness, computational cost, and uncertain generalization of qualitative findings.

  • Task scope: LINC evaluates only truth-value prediction from relatively short natural-language premises and conclusions, limiting its scope.Longer paragraph-form premises make formalization more difficult because relevant information requires pragmatic inference.
  • Generalizability: LINC’s qualitative finding of complementary errors may not generalize to related reasoning tasks using different intermediate languages.The authors identify this as an open question for settings such as PAL, Logic-LM, and SATLM.
  • Future methods: Traditional Chain-of-Thought, tree-of-thoughts, program-of-thoughts, retrieval, and self-repair methods remain possible alternatives for addressing reasoning failure modes.The paper leaves systematic evaluation of these more sophisticated techniques as future work.
  • Scalability: As premises increase, formalization errors become more likely and theorem proving may become slow because general logical deduction is NP-hard.The authors note that fast forward- and backward-chaining algorithms exist, but the general problem remains computationally difficult.
  • Logic coverage: First-order logic cannot express problems requiring higher-order or non-classical logics, which would require alternative theorem provers.LINC may extend to these settings, but its performance there remains untested.
  • Computational cost: Using GPT models and StarCoder+ with majority voting requires costly API requests, dedicated GPUs, and many generations per query.These requirements increase the computational resources needed to implement the approach.

A Future Directions

The paper localizes LINC’s errors primarily to semantic parsing, especially on naturalistic language, and proposes several strategies for improving parsing faithfulness and robustness.

  • Error analysis: LINC errors are primarily semantic-parsing errors, with relatively unimpeded performance on synthetic ProofWriter but more room for improvement on naturalistic FOLIO.The authors identify naturalistic language handling as the key opportunity for improvement.
  • Proposed improvements: Implicit premise rediscovery could improve performance when naturalistic communication leaves relevant information unstated.The proposed strategy explores the logical neighborhood of existing explicit premises.
  • Proposed improvements: Restricting LLM sampling to context-free-grammar-consistent term expansions would eliminate syntax errors.The proposal addresses samples currently lost because generated outputs are syntactically invalid.
  • Proposed improvements: Back-translating candidate FOL expressions into natural language could identify translations that more faithfully preserve sentence semantics.Forward translations ranking highly after back-translation would be favored as better semantic matches.
  • Conclusion: The authors expect naturalistic evaluations and these improvement strategies to advance neurosymbolic approaches to formal reasoning.This conclusion is stated as a forward-looking research direction rather than a demonstrated result.
  • Model details: GPT-3.5 and GPT-4 allow up to 1024 tokens for FOLIO and 4096 for ProofWriter, while StarCoder+ uses its 8192-token context window.Decoding stops early when </EVALUATE> is produced, and local experiments use NVIDIA A100 GPUs.
  • Model details: GPT-3.5 and GPT-4 use API-based checkpoints, while StarCoder+ is an open-access 15.5B model run locally with bf16 precision.The implementation uses different deployment settings across the evaluated models.

C FOLIO Dataset Preprocessing

The experiments preprocess FOLIO by removing erroneous validation samples and use structured few-shot prompting for multiple reasoning methods, including LINC and Chain-of-Thought.

  • Dataset preprocessing: The evaluation uses FOLIO’s validation split, while its testing split is unavailable publicly.Few-shot examples are selected from the publicly available training split.
  • Dataset preprocessing: 22 of FOLIO’s 204 validation examples were removed because of malformed expressions, mismatched labels, or premise-expression count errors, leaving 182 examples.The errors were independently checked using Prover9 and manual inspection where applicable.
  • Prompting: Few-shot prompts use 1–8 manually structured examples with PREMISES, CONCLUSION, and EVALUATE tags to scaffold generation and post-processing.The same format supports naïve, scratchpad, Chain-of-Thought, and neurosymbolic methods.
  • Task format: The task represents premises as a set of FOL sentences and evaluates a single conclusion as True, False, or Uncertain.For the neurosymbolic method, both premises and conclusions are translated into FOL before theorem-prover evaluation.
  • Prompt examples: The example formalizes each natural-language premise and conclusion into FOL before returning the answer Uncertain.The Chain-of-Thought example reaches the same answer by verbally tracing the premise implications.

E.2 GPT-4 LINC Failure Modes

GPT-4 LINC errors primarily arise when the translation to first-order logic omits implicit facts or represents explicit information incorrectly. These translation failures can leave Prover9 unable to derive conclusions that are true or false in the original natural-language task.

  • L1: Implicit information: FOL fails to capture implicit information needed for correct deductions, such as that Harry is a person, Walden is a book, or KiKi is an animal.The analysis also identifies an implicit identity fact, SameAirport(LGA, LGA), as necessary in one example.
  • Consequences: The LINC pipeline can therefore return Uncertain when missing information breaks the formal proof path, even though the natural-language premises support a definite conclusion.This mechanism is illustrated by the KiKi, Susan, and Harry examples.
  • L2: Representation choice: FOL can lose explicitly stated information when the model chooses an inadequate representation, such as omitting that Barutin Cove is a cove.Other examples involve failing to encode Tom’s license plate as a license plate or using inconsistent predicates for four sides.
  • Translation errors: GPT-4 produces very few FOL translation mistakes, although the broader analysis still identifies cases where incorrect formalization yields Uncertain instead of the ground-truth label.For example, Prover9 returns Uncertain for the true conclusion that Heinrich Schmidt was either German or Russian and for the false Istanbul license-plate conclusion.

F Proofwriter StarCoder+ Errors

StarCoder+ errors on ProofWriter are usually caused by syntax or improper logical representations rather than lossy translation. Representative failures include malformed quantification, incorrect argument structure, and conjunctions that do not encode the intended fact.

  • Error pattern: Most StarCoder+ errors on ProofWriter arise from syntax or improper representations because the dataset’s premises are relatively simple and direct.The analysis states that lossy translation is rarer on this dataset.
  • Quantification: StarCoder+ omits universal quantification when translating rules such as “All quiet people are round” and “If something is furry then it is quiet.”The ground-truth forms explicitly quantify over all x.
  • Argument structure: StarCoder+ reverses a relational statement by translating “The cow eats the dog” as Cow(Eats(Dog)) instead of Eats(Cow, Dog).The error changes the intended binary relation into an invalid nested form.
  • Predicate representation: StarCoder+ translates “The cow is blue” as Cow(x) & Blue(x), introducing an unbound variable instead of the ground-truth fact Blue(Cow).This representation does not preserve the intended individual-level predicate.

G StarCoderPlus FOLIO Error Analysis

StarCoder+ exhibits distinct FOLIO error patterns under CoT and LINC, with CoT tending toward True predictions and LINC benefiting from increased majority-vote samples. The two methods’ mispredictions differ more for StarCoder+ than for GPT-4.

  • Prediction patterns: StarCoder+ CoT primarily predicts True on FOLIO, whereas LINC predicts Uncertain more often and shows a different misprediction pattern.The authors attribute the CoT tendency as likely related to StarCoder+’s code-heavy training and limited sophisticated textual chain-of-thought capability.
  • Error overlap: StarCoder+’s CoT and LINC mistakes differ much more than GPT-4’s, indicating less overlap between their error sets for the smaller model.The comparison is made in the qualitative analysis of Figure 6.
  • K-way voting: LINC’s gains from larger K are partly explained by majority voting reducing predictions caused by solver errors from invalid FOL generations.This rationale is stated for the K-sensitivity analysis on FOLIO.
  • K-way voting: Increasing K benefits LINC accuracy on FOLIO but not CoT, with the effect especially useful for weaker models that more often generate syntactically invalid FOL expressions.Majority voting over more samples reduces the risk of predicting Error, which is always incorrect.
Loading 2310.15164v2…