PaperlayerView exact revision on arXiv

Source-linked AI summary

SymbolLKG: Towards Verifiable Logical Reasoning via Logical Knowledge Graph and Symbolic Solvers

Haizhao Fan, Yuchi Xiong, Jize Wang, Xinping Guan, Xinyi Le

arXiv:2608.26836v1cs.AIcs.CL

TL;DR

LLMs struggle with reliable, verifiable multi-step logical reasoning, while CoT lacks rigorous verification and standard RAG misses structural dependencies. SymbolLKG represents rules and constraints as explicit LKG nodes, retrieves topology-aware contexts, and routes tasks to symbolic solvers; it significantly outperforms prompting and RAG baselines while producing deterministic proof traces. The framework remains dependent on accurate natural-language grounding, and semantic misinterpretations can propagate to the solver.

  • Problem

    LLMs struggle with strict multi-step reasoning, while CoT lacks rigorous verification and standard RAG misses structural dependencies in logical tasks.

  • Method

    SymbolLKG parses text into an LKG with explicit rule and constraint nodes, uses hybrid retrieval, and dynamically routes subgraphs to suitable symbolic solvers.

  • Results

    SymbolLKG significantly outperforms standard prompting and retrieval baselines on complex reasoning benchmarks while providing deterministic proof traces.

  • Takeaways & Limitations

    The framework combines LLM semantic flexibility with symbolic deterministic precision for transparent, verifiable reasoning paths.

  • Takeaways & Limitations

    Semantic misinterpretations during natural-language extraction can propagate to the solver, which validates argument structure but not the truth of flawed premises.

Abstract

from arXiv · show

Large Language Models (LLMs) have demonstrated remarkable proficiency in natural language understanding, yet they struggle with strict multi-step reasoning, frequently suffering from hallucinations and inconsistency. Existing solutions like Chain-of-Thought (CoT) lack rigorous verification mechanisms, while standard Retrieval-Augmented Generation (RAG) often misses the complex, structural dependencies inherent in logical tasks. To bridge this gap, we propose a Neuro-Symbolic architecture that integrates a Logical Knowledge Graph (LKG) with dynamic solver routing. Specifically, we introduce an ontology-based LKG that treats logical rules and constraints as first-class topological nodes, enabling explicit modeling of dependencies extracted from text. We further design a Logic Router to dynamically dispatch tasks to the optimal symbolic engine, which is supported by a topology-aware hybrid retrieval mechanism. Experimental results on logical reasoning benchmarks demonstrate that our framework significantly outperforms state-of-the-art prompting and RAG baselines, delivering higher accuracy and verifiable reasoning paths.

1 Introduction

SymbolLKG addresses unreliable multi-step logical reasoning by representing rules and constraints explicitly in a Logical Knowledge Graph and routing problems to symbolic solvers. It combines structured retrieval, adaptive solver selection, and symbolic verification, outperforming prompting and baseline RAG methods on logical reasoning and multi-hop QA datasets.

  • LLMs can generate plausible but incorrect reasoning steps and fail to maintain consistency across long contexts.
  • CoT may propagate errors without symbolic grounding, while standard RAG can miss directional dependencies in logical rules.
  • Existing graph-based approaches often represent logical rules as unstructured text or implicit edge attributes, limiting deterministic symbolic verification and solver routing.
  • SymbolLKG treats logical rules and constraints as first-class LKG nodes while combining LLM parsing with deterministic external solvers.
  • The framework retrieves a topologically connected subgraph and dynamically routes each problem to an appropriate symbolic solver.
  • SymbolLKG significantly outperforms standard LLM prompting and baseline RAG methods on logical reasoning and multi-hop QA datasets.

2 Related Works

Related work combines neural language understanding, symbolic execution, retrieval, and graph structure, but existing methods generally use static solvers or underrepresent logical rules. These limitations motivate explicit logical structure and adaptive reasoning in SymbolLKG.

  • Pure neural reasoning methods improve multi-step generation but still suffer from hallucinations and unfaithful explanations.
  • Neuro-symbolic systems translate text into formal code or logic rules and execute them with external solvers, but most assign one solver to an entire dataset.
  • Standard RAG can retrieve semantically similar but logically irrelevant documents, producing semantic drift in logical reasoning tasks.
  • Graph-based methods support multi-hop reasoning, yet they commonly treat knowledge graphs as entity lists while ignoring complex logical rules.

3 Methodology

SymbolLKG constructs a heterogeneous logical graph, retrieves a complete but compact reasoning context, and routes that context to a suitable symbolic solver. An LLM then generates and self-refines solver-specific code for verifiable execution.

  • The workflow parses unstructured text into an LKG, retrieves relevant premises, selects a solver from graph topology, and performs self-refining symbolic execution.
  • LKG Construction: The LKG is a directed heterogeneous multigraph whose nodes are typed and extracted through an LLM-based OpenIE pipeline.
  • LKG Construction: Schema-on-Read dynamically creates Concept and Entity nodes according to their roles in the text.
  • LKG Construction: Logical dependencies become explicit Rule and Constraint nodes connected to their relevant entities.
  • LKG Construction: Rules receive vector embeddings and remain distinct from assertions, while context-specific Concepts define the domain of discourse.
  • Hybrid Retrieval and Pruning: Hybrid retrieval combines query-entity matching and dense similarity to identify anchor nodes.
  • Hybrid Retrieval and Pruning: Graph traversal expands anchors along mention, type, and application edges to include nearby rules and constraints, forming a logically complete hull.
  • Hybrid Retrieval and Pruning: An LLM pruning module removes distractor constraints from the expanded hull to produce a compact final subgraph.

4 Experiments

Experiments evaluate SymbolLKG across logical reasoning, multi-hop retrieval, end-to-end question answering, and solver routing benchmarks, with implementation details and baselines specified for comparison. Results show strong overall accuracy, retrieval, QA, and routing performance, while latency remains dominated by LLM calls.

  • Datasets: The evaluation covers eight benchmarks spanning formal logical reasoning, multi-hop retrieval, and open-domain question answering.Logical reasoning benchmarks assess translation and deduction, while retrieval and QA benchmarks test evidence aggregation, noise filtration, bridge-entity identification, and compositional reasoning.
  • Baselines: SymbolLKG is compared with Standard CoT, Logic-LM, single-step retrievers, multi-step retrieval systems, and three RAG frameworks.The comparisons include BM25, Contriever, GTR, NativeRAG, RAPTOR, Proposition, HippoRAG, IRCoT, GraphRAG, and HippoRAG 2.
  • Logical Reasoning Performance: 78.73% average accuracy across five logical reasoning benchmarks exceeds Logic-LM’s 74.49% and Standard CoT’s 69.56%.Typed constraint subclasses help select Z3 on AR-LSAT, yielding 57.85%, while the three-attempt self-refining loop reaches 100.00% on ProntoQA.
  • Multi-hop Retrieval Performance: SymbolLKG attains Recall@2/Recall@5 of 79.4/88.2 on 2WikiMultiHopQA and 68.5/84.1 on HotpotQA.The retrieval evaluation measures whether top-k documents contain the complete ground-truth supporting-fact set; topology-aware traversal helps surface distractor-buried evidence.
  • Question Answering Performance: SymbolLKG leads every prior baseline on all reported EM/F1 cells: 70.2/74.9 on 2Wiki, 73.8/81.5 on HotpotQA, and 48.6/59.4 on MuSiQue.The end-to-end QA evaluation uses Exact Match and token-overlap F1 across three multi-hop datasets.
  • Router and Efficiency Performance: The router reaches 86.0% overall accuracy, including 100.0% on both AR-LSAT and LogicalDeduction, while full-pipeline latency averages 122.2 seconds per logical problem.Multi-hop QA queries take 166–407 seconds; fixed corpora permit offline LKG construction and reduce inference to retrieval below 0.1 seconds plus approximately 10 seconds for answer generation.

5 Limitations & Conclusion

SymbolLKG combines Logical Knowledge Graphs with adaptive symbolic solvers to provide deterministic, transparent proof traces. Its main limitations concern extraction accuracy, ambiguity in natural language, and computational overhead.

  • SymbolLKG treats logical rules as topological nodes and routes tasks to Z3, Prover9, or Pyke, producing deterministic proof traces.The framework is presented as bridging LLM semantic flexibility with symbolic precision and verifiability.
  • Semantic misinterpretations during LLM extraction can propagate to the solver, which guarantees argument validity but not premise soundness.
  • Ambiguous language, including vague quantifiers or metaphorical expressions, may be oversimplified by the LKG’s rigid schema.
  • Graph construction and external solvers make the pipeline computationally heavier than direct single-pass generation.

A Prompt Templates

Appendix A documents the prompts that support LKG construction, solver-code generation, logic pruning, and adaptive solver routing. These templates impose structured representations and guide the framework’s modular interactions with the LLM.

  • A Prompt Templates: Appendix A provides prompt templates to facilitate reproducibility and illustrate interactions between SymbolLKG and the LLM.
  • A.1 Prompt for LKG Construction: The LKG-construction prompt extracts structured logic using a dynamic ontology and schemas for Entities, Concepts, Rules, and Constraints.
  • A.1 Prompt for LKG Construction: It enforces strict JSON output to preserve graph integrity.
  • A.2 Prompt for Solvers: The solver task description requires processing logfile information and generating complete Z3 code encoding the given information.
  • A.2 Prompt for Solvers: The Z3 prompt translates a retrieved logical subgraph into executable Python by declaring entity variables, encoding facts as constraints, and formulating query logic.
  • A.3 Prompt for Pruner: The logic-pruning prompt filters the expanded candidate set before downstream reasoning.
  • A.3 Prompt for Pruner: The adaptive router selects Z3 for arithmetic and CSP tasks, Prover9 for first-order theorem proving, and Pyke for relational inference.

B Case Study

The AR-LSAT case study illustrates SymbolLKG’s end-to-end workflow, from extracting structured graph components to retrieving, pruning, routing, and executing solver code. The example routes an arithmetic/ordering problem to Z3 and derives the final answer.

  • The case study demonstrates the complete lifecycle of an AR-LSAT logical reasoning task through SymbolLKG.It covers intermediate outputs from LKG extraction through final executable reasoning.
  • The extracted representation identifies entities, concepts, rules, and constraints from the natural-language problem.
  • The example models offices, computers, and printers while formalizing AllDifferent and Ordering constraints.
  • Hybrid search retrieves rules and constraints concerning the queried computers, offices, printers, and years.
  • Pruning reduces the retrieved candidates to the essential logic before solver selection.
  • The Logic Router identifies the task as arithmetic/ordering reasoning and selects the Z3 solver.
  • Generated Z3 code is executed to derive the final answer from the routed logical representation.

C.1 Empirical Latency

SymbolLKG incurs substantial per-sample latency, with LKG construction and routed solver execution dominating the pipeline. Multi-hop QA is slower than logical reasoning in the reported ranges, and dataset runtimes vary with program complexity and retries.

  • Per-sample wall-clock time is profiled on N = 100 instances per benchmark.
  • Multi-hop QA: 166.0–407.1 s: Multi-hop QA end-to-end latency spans 2WikiMultiHopQA to MuSiQue.LKG construction accounts for 159.2–395.8 s, while answer generation takes 6.0–11.4 s.
  • Multi-hop QA: Table 6 reports multi-hop QA latency in seconds, averaged over N = 100 instances per benchmark.
  • Logical Reasoning: 122.2 s: Logical reasoning averages this end-to-end latency per problem, comprising 29.0 s for LKG construction and 93.2 s for routed solving.
  • Logical Reasoning: 166.5 s and 135.6 s: ProofWriter and AR-LSAT have the longest mean logical-reasoning times.The passage attributes these times to longer Prover9/Z3 programs and higher retry rates.
  • Logical Reasoning: 71.4 s: ProntoQA has the shortest mean logical-reasoning time because of its lightweight Pyke path.
  • Logical Reasoning: Table 7 reports logical-reasoning latency in seconds, averaged over 20 instances per dataset and N = 100 overall.“Total” represents single-path production deployment with up to three self-refining retries.

C.2 Discussion

LLM API latency, not graph operations, dominates the framework’s runtime, but offline LKG construction, bounded retries, and smaller backbones constrain its practical impact.

  • Over 99% of wall-clock time comes from two recurring LLM calls, while retrieval and BFS together remain below 0.1 s per query.
  • For fixed deployment corpora, offline LKG construction eliminates the 155–494 s per-question construction cost in multi-hop QA.After amortisation, inference costs retrieval below 0.1 s plus one answer-generation call of approximately 10 s.
  • The self-refining loop permits at most three retries, bounding worst-case solver latency at three times the single-attempt cost.
  • Routing and pruning use bounded-length prompts and can run on a smaller, cheaper backbone without materially affecting accuracy.
Loading 2608.26836v1…