PaperlayerView exact revision on arXiv

Source-linked AI summary

Faithful Logical Reasoning via Symbolic Chain-of-Thought

Jundong Xu, Hao Fei, Liangming Pan, Qian Liu, Mong-Li Lee, Wynne Hsu

arXiv:2405.18357v2cs.CL

TL;DR

LLMs may struggle with logical reasoning that depends on symbolic expressions and rigid deduction rules. SymbCoT combines symbolic representations, planning, solving, and verification within an LLM, and experiments show improvements over vanilla CoT across five benchmarks.

  • Problem

    Natural-language CoT can struggle with logical reasoning that depends on symbolic expressions and rigid deduction rules, while natural-language intermediate steps can lose information on complex tasks.

  • Method

    SymbCoT translates natural-language contexts into symbolic formats, derives a step-by-step plan using symbolic rules, solves the problem, and verifies the translation and reasoning chain entirely with an LLM.

  • Results

    SymbCoT significantly enhances vanilla CoT across five logical reasoning datasets evaluated with First-Order Logic and Constraint Optimization expressions.

  • Takeaways & Limitations

    The framework is reported to provide more faithful reasoning, more robust symbolic syntax handling, human-readable explanations, and fuller information utilization.

  • Takeaways & Limitations

    The evaluation covers only First-Order Logic and Constraint Optimization, and the extended reasoning chains increase token generation and API costs.

Abstract

from arXiv · show

While the recent Chain-of-Thought (CoT) technique enhances the reasoning ability of large language models (LLMs) with the theory of mind, it might still struggle in handling logical reasoning that relies much on symbolic expressions and rigid deducing rules. To strengthen the logical reasoning capability of LLMs, we propose a novel Symbolic Chain-of-Thought, namely SymbCoT, a fully LLM-based framework that integrates symbolic expressions and logic rules with CoT prompting. Technically, building upon an LLM, SymbCoT 1) first translates the natural language context into the symbolic format, and then 2) derives a step-by-step plan to solve the problem with symbolic logical rules, 3) followed by a verifier to check the translation and reasoning chain. Via thorough evaluations on 5 standard datasets with both First-Order Logic and Constraint Optimization symbolic expressions, SymbCoT shows striking improvements over the CoT method consistently, meanwhile refreshing the current state-of-the-art performances. We further demonstrate that our system advances in more faithful, flexible, and explainable logical reasoning. To our knowledge, this is the first to combine symbolic expressions and rules into CoT for logical reasoning with LLMs. Code is open at https://github.com/Aiden0526/SymbCoT.

1 Introduction

SymbCoT addresses the difficulty of applying natural-language CoT to symbolic logical reasoning by combining symbolic expressions, natural-language context, planning, solving, and verification in an LLM-based framework.

  • LLM-based symbolic reasoning systems can be limited by translation errors, information omission, and unexplainability.
  • SymbCoT performs translation, planning, solving, and verification entirely with an LLM rather than external reasoners or tools.
  • SymbCoT combines symbolic expressions with natural language to support precise logical calculations while retaining implicit intentions and contextual information.
  • Its plan-then-solve architecture decomposes complex problems into smaller sub-problems, making the reasoning process more trackable and structured.
  • Across five logical reasoning datasets using First-Order Logic and Constraint Optimization expressions, SymbCoT significantly improves vanilla CoT and outperforms current state-of-the-art solutions.
  • The verifier checks translations and reasoning chains, while the framework integrates symbolic rules with CoT prompting for more faithful reasoning.

2 Related work

Prior work combines LLMs with symbolic reasoning, but natural-language intermediate reasoning can lose information and translator-only systems do not inherently improve logical reasoning.

  • CoT methods improve reasoning by prompting LLMs to make intermediate steps and rationales explicit, with extensions including self-consistency and Tree-of-Thought.
  • Natural-language-only intermediate reasoning can cause significant information loss on complex logical reasoning tasks.
  • Existing symbolic reasoning approaches use rule-based, neural, or LLM-integrated methods to interpret and solve symbolic representations.
  • Using LLMs merely as translators does not inherently enhance logical reasoning capabilities.
  • Compared with external-reasoner approaches, SymbCoT is presented as more robust to syntax errors, more human-friendly in explanation, and better able to combine symbolic and natural-language reasoning.

3 SymbCoT for Symbolic Reasoning

SymbCoT converts natural-language logical problems into hybrid symbolic representations, plans and solves them with formal rules, and verifies both translations and deductions.

  • 3.1 Task Definition: Logical reasoning determines whether a statement is true, false, or unknown from a set of premises and their logical inferences.
  • 3.2 Modules: The Solver applies symbolic inference rules, such as Modus Tollens, to derive a conclusion classified as true, false, or uncertain.
  • 3.2 Modules: The Verifier checks semantic equivalence between natural-language and symbolic translations, then validates each reasoning step and refines invalid translations or deductions.
  • 3.2 Modules: The Translator converts premises and the question statement into symbolic formats and concatenates natural-language and symbolic versions into hybrid contexts.
  • 3.2 Modules: The Planner decomposes the problem into sequential intermediate steps that connect the premises to the question statement.
  • 3.3 Reasoning Steps: Table 1 reports First-Order Logic performance, while Table 2 reports GPT-4 results using Constraint Optimization representations.

4 Experiments

Experiments evaluate SymbCoT with GPT-3.5 and GPT-4 across five logical reasoning datasets using FOL and CO symbolic structures, against established baselines. Results include broad performance gains, module ablations, reasoning-depth analysis, and execution-rate comparisons.

  • Settings: Experiments use GPT-3.5 and GPT-4 with identical model parameters for evaluating baselines and SymbCoT.The specified models are gpt-3.5-turbo-0613 and gpt-4-0613.
  • Settings: Five datasets evaluate logical reasoning accuracy, spanning FOL for PrOntoQA, ProofWriter, and FOLIO and CO expressions for LogicalDeduction and AR-LSAT.Accuracy measures multiple-choice correctness.
  • Main Result: SymbCoT gains 21.56%, 6.11%, and 3.53% over Naive, CoT, and Logic-LM on GPT-3.5, and 22.08%, 9.31%, and 7.88% on GPT-4.The GPT-3.5 comparison has one reported FOLIO exception against Logic-LM, while GPT-4 surpasses all baselines across both datasets discussed.
  • Main Result: On CO symbolic expressions, SymbCoT surpasses CoT and Logic-LM by 13.32% and 3.12%, demonstrating versatility across symbolic reasoning expressions.These results are reported on LogicalDeduction and AR-LSAT.
  • Model Ablation: As reasoning depth increases on ProofWriter, SymbCoT’s improvement over vanilla CoT becomes more pronounced.The analysis treats greater reasoning depth as indicating more complex problems.
  • Model Ablation: Planner and Solver together improve performance by an average of 10.4%, while Translator contributes a further 6.3% improvement in the GPT-4 ablation study.The Solver depends on the Planner, so they are ablated simultaneously.

5 Analysis and Discussion

The analysis examines SymbCoT’s performance, execution reliability, reasoning faithfulness, model scaling, and illustrative cases. It reports stronger gains on deeper reasoning tasks, reduced translation errors, and elimination of unfaithful reasoning with verification.

  • As reasoning depth increases, SymbCoT’s improvement over CoT becomes more pronounced, while remaining best at depth 5.
  • SymbCoT achieves up to 100% symbolic-expression execution success, improving over Logic-LM by an average of 17.7 percentage points.
  • 73.3% of external-solver translation errors were reduced, including declines of 53.8% in information loss and 19.5% in information error.
  • Verifier-based SymbCoT eliminated unfaithful reasoning on FOLIO, compared with 6% for CoT and 2% without the Verifier.
  • Upgrading from GPT-3.5 to GPT-4 produced a 24.3% performance boost with SymbCoT across three FOL datasets.
  • A case study shows SymbCoT rejects affirming the consequent and correctly preserves an unknown conclusion when the required premise is absent.

6 Conclusion

The conclusion presents SymbCoT as a framework that combines symbolic reasoning with CoT prompting to improve LLM logical reasoning. Evaluations across five benchmarks using FOL and CO show stronger performance than vanilla CoT.

  • SymbCoT translates natural-language contexts into symbolic form, plans reasoning with symbolic rules, and verifies the translation and reasoning chain.
  • Across five standard benchmarks using FOL and Constraint Optimization expressions, SymbCoT strikingly enhances vanilla CoT on logical reasoning.
  • The framework integrates symbolic expressions and logical rules with CoT prompting to improve LLM logical reasoning abilities.

Limitations

The paper identifies limited symbolic-language coverage and substantial implementation expense as potential limitations of SymbCoT.

  • The evaluation covers only First-Order Logic and Constraint Optimization, leaving additional symbolic languages for future assessment.
  • SymbCoT incurs considerable costs because symbolic rules lengthen reasoning chains and increase token generation, API usage, or computational-resource requirements.

Ethics Statement

The paper describes ethical commitments centered on transparency, fairness, responsible AI development, privacy, bias mitigation, and explainability. It also frames SymbCoT as potentially beneficial across several technical fields while calling for continued evaluation.

  • The study emphasizes transparency, fairness, responsible AI development, data privacy, bias mitigation, and explainable AI decisions.
  • SymbCoT is presented as potentially contributing to natural language processing, knowledge representation, and automated reasoning.
  • The authors encourage responsible use of the findings and ongoing evaluation of their societal and ethical implications.

C Dataset Statistics

The study uses the same records as Logic-LM to ensure consistency and facilitate comparative analysis, with dataset statistics presented in Table 3.

  • The experiments adopt identical records to Logic-LM for consistent comparative analysis.Table 3 presents the statistics for each dataset.

D Baseline Specification

The study compares direct prompting, CoT variants, symbolic reasoning baselines, and the proposed method. On FOLIO, the proposed method achieves the highest reported F1 score and differs in prediction behavior from Logic-LM.

  • Naive Prompting directly answers questions using few-shot demonstrations without explicit reasoning.
  • CoT generates step-by-step reasoning with in-context demonstrations, while CoT-SC selects among multiple chains by majority vote.
  • Logic-LM translates natural-language inputs into symbolic representations and uses external solvers to deduce answers.
  • Ours achieves the highest F1 score on FOLIO, exceeding CoT by 6% and Logic-LM by 3%.Logic-LM predicts more Unknown cases, which the authors attribute to information loss during translation.

F.1 F1 Score Analysis

On FOLIO, the proposed method achieves the strongest F1 score among the compared approaches, indicating the best reported balance between precision and recall.

  • 85% F1: Ours achieves the highest F1 score among the compared models.The paper describes F1 as balancing precision and recall.
  • 82 F1: Logic-LM ranks below Ours in the reported comparison.
  • 79 F1: CoT records the lowest F1 score among the three models.

F.2 Recall Analysis

The proposed method has the highest reported recall on FOLIO, while Logic-LM has the lowest and CoT falls between them.

  • 81 recall: Ours achieves the highest recall among the three models.
  • 72 recall: Logic-LM has the lowest recall rate among the compared models.The authors note that this may limit its utility where high recall is critical.
  • 75 recall: CoT falls between Ours and Logic-LM in recall.

F.3 Precision Analysis

The supplied examples combine precision analysis with symbolic logical deduction, planning, verification, and multiple final-answer demonstrations. Results include precision comparisons, a balanced F1 conclusion, and worked reasoning outcomes.

  • Precision Analysis: 89 precision is reported for the authors’ methodology, while Logic-LM reaches 95 and CoT reaches 81.The three values are presented as precision scores for ours, Logic-LM, and CoT.
  • Precision Analysis: The authors’ methodology is summarized as having the highest F1 score and balanced precision and recall.The supplied analysis characterizes Logic-LM as precision-oriented and CoT as trailing in both precision and recall.
  • Output Examples: A worked deduction concludes that the statement about Rock being cute and still implying turtle and skittish is false.The reasoning uses Still(rock), derives that Rock is not skittish, and concludes the target conjunction cannot hold.
  • Symbolic Reasoning Process: The framework translates natural language into symbolic form, derives a plan with First-Order Logic rules, solves the problem, and verifies the process.The supplied prompt material explicitly separates translation, planning, solving, and verification stages.
  • Output Examples: Other supplied examples report valid or determined outcomes, including that Alex is not sour and that the quail is rightmost.These examples provide final answers without a shared evaluation metric.

I.1.2 ProofWriter

The ProofWriter examples illustrate SymbCoT’s staged First-Order Logic workflow and show how the solver and verifier handle both derivable and underdetermined conclusions. In the Anne example, the queried whiteness remains unknown despite deriving redness.

  • I.1.2 ProofWriter: SymbCoT’s ProofWriter workflow defines predicates and facts, parses logic rules and questions, derives a plan, executes inferences, and verifies the conclusion.The supplied passages enumerate these stages across translation, planning, solving, and verification prompts.
  • I.1.2 ProofWriter: Anne’s quietness supports an inference that Anne is red through the supplied conditional rule.The execution identifies Quite(Anne, True) as a fact and applies Modus Ponens to infer redness.
  • I.1.2 ProofWriter: White(Anne, True) is judged unknown because the provided First-Order Logic rules do not directly infer it.The same unknown conclusion is repeated in the original execution and its verification.
  • I.1.2 ProofWriter: Verification finds the context and query semantically consistent and confirms the unknown conclusion is logically consistent with the available premises.The verification separately checks context correspondence, inference validity, assumptions, and consistency.
  • I.1.2 ProofWriter: The verification flags a typo and variable mismatch in the rule connecting Anne’s quietness to redness.It recommends using Quiet(Anne, True) → Red(Anne, True) for the intended interpretation.

I.2.2 ProofWriter

This ProofWriter example derives that the tiger is young from its likes, visits, niceness, and seeing relations, supporting the supplied answer choice B. The chain demonstrates multi-step rule application.

  • I.2.2 ProofWriter: The tiger’s liking both the cow and the squirrel implies that it visits the tiger.This applies the rule requiring both likes relations.
  • I.2.2 ProofWriter: Visiting the tiger implies that the tiger is nice.The example explicitly applies the visits-to-nice rule after deriving the visit.
  • I.2.2 ProofWriter: Being nice and seeing the tiger implies that the tiger is young.The example states the resulting young conclusion after the preceding derivation.
  • I.2.2 ProofWriter: The supplied reasoning selects option B for the question about whether the tiger is not young.The passage reports the option label after deriving that the tiger is young.
Loading 2405.18357v2…