cs.AIAug 27, 2026
SaveSymbolLKG: Towards Verifiable Logical Reasoning via Logical Knowledge Graph and Symbolic Solvers
Organizations: Shanghai JiaoTong University
Abstract
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.
Figures & tables
Figure 1: Comparison of reasoning paradigms. The input highlights constraints in green, noise in grey, and premises in orange. The Direct LLM Pipeline (left) ignores this structure. It makes a “Closed World Assumption” (CWA) error and incorrectly guesses Jamie won. The SymbolLKG Pipeline (right) converts text into a Logical Knowledge Graph. It uses symbolic verification to strictly check the premises. The system correctly concludes the answer is “Unknown”.
Figure 2: The architecture of the SymbolLKG framework. The pipeline consists of two phases: Phase 1 (LKG Construction) transforms text into an LKG, establishing a dynamic Concept-Entity hierarchy alongside reified Rule and Constraint nodes. Phase 2 (Inference) employs a hybrid retrieval strategy (combining vector search with graph traversal) to extract a context-aware subgraph. Then a topology-aware router dispatch it to the optimal symbolic solver for verifiable execution.
| Node Type | Symbol | Definition & Categories (Codebase) | Key Attributes (Class Fields) | Role in Reasoning |
|---|---|---|---|---|
| Entity | Concrete instances implemented as Entity class. IDs are generated via SHA256 hash of lemmatized name and type. | name , entity_type , id (Canonical Hash), properties | Anchors for retrieval. Hash-based IDs ensure uniqueness across the graph. | |
| Concept | Abstract categories implemented as Concept class. | name , labels | Simple taxonomy nodes supporting type grouping. | |
| Rule | Logical implications implemented as Rule class. | expression , description , embedding | Stores logic formulas; description allows vector-based retrieval of rules. | |
| Constraint | Restrictions on states, implemented as 4 subclasses: 1. Arithmetic (Math ops) 2. AllDifferent (Combinatorial) 3. Ordering (Spatial/Temporal relations like left_of , newer_than ) 4. Generic (Constraints outside the above-listed categories) | raw_expression , constraint_type , Specific: relation , operation , value | Defines solution boundaries. Ordering handles both topological and chronological constraints via relation types. |
Table 1: Node Taxonomy in the Symbolic-Cognitive Logical Knowledge Graph (SymbolLKG). The schema distinguishes between static entities, hierarchical concepts, deductive rules, and arithmetic constraints to facilitate dynamic solver routing.
| Dataset | CoT | Logic-LM | Ours |
|---|---|---|---|
| FOLIO | 70.58 | 78.92 | 71.39 |
| AR-LSAT | 35.06 | 43.04 | 57.85 |
| Logical Deduction | 75.25 | 87.63 | 90.81 |
| ProntoQA | 98.79 | 83.20 | 100.00 |
| ProofWriter | 68.11 | 79.66 | 73.60 |
| Avg. | 69.56 | 74.49 | 78.73 |
Table 2: Logical Reasoning Accuracy (%) across five benchmarks. Methods compared include Standard CoT prompting and the neuro-symbolic baseline Logic-LM.
| Type | Method | 2WikiMultiHopQA | HotpotQA | ||
|---|---|---|---|---|---|
| Recall@2 | Recall@5 | Recall@2 | Recall@5 | ||
| Single-step | BM25 | 51.8 | 61.9 | 55.4 | 72.2 |
| Contriever | 46.6 | 57.5 | 57.2 | 75.5 | |
| GTR | 60.2 | 67.9 | 59.4 | 73.3 | |
| RAPTOR | 46.3 | 53.8 | 58.1 | 71.2 | |
| Proposition | 56.4 | 63.1 | 58.7 | 71.1 | |
Table 3: Retrieval Performance (Recall@2 and Recall@5) on 2WikiMultiHopQA and HotpotQA. Baselines are categorized into Single-step and Multi-step approaches. SymbolLKG leverages topology-aware traversal to optimize evidence retrieval.
| Method | 2Wiki | HotpotQA | Musique | Average | ||||
|---|---|---|---|---|---|---|---|---|
| EM | F1 | EM | F1 | EM | F1 | EM | F1 | |
| NativeRAG | 33.4 | 43.3 | 43.4 | 57.7 | 15.5 | 26.4 | 30.8 | 42.5 |
| GraphRAG | 51.4 | 58.6 | 55.2 | 68.6 | 27.3 | 38.5 | 44.6 | 55.2 |
| IRCoT + HippoRAG | 47.7 | 62.7 | 45.7 | 59.2 | 21.9 | 33.3 | 38.4 | 51.7 |
| HippoRAG 2 | 65.0 | 71.0 | 62.7 | 75.5 | 37.2 | 48.6 | 55.0 | 65.0 |
| SymbolLKG | 70.2 | 74.9 | 73.8 | 81.5 | 48.6 | 59.4 | 64.2 | 71.9 |
Table 4: End-to-end QA Performance (EM and F1). We compare our SymbolLKG against baselines on 2WikiMultiHopQA, HotpotQA and Musique.
| Dataset | Ground-Truth Solver | Random | SymbolLKG |
|---|---|---|---|
| AR-LSAT | Z3 | 33.3 | 100.0 |
| LogicalDeduction | Z3 | 33.3 | 100.0 |
| FOLIO | PROVER9 | 33.3 | 85.0 |
| ProofWriter | PROVER9 | 33.3 | 92.0 |
| ProntoQA | PYKE | 33.3 | 53.0 |
| Average | – | 33.3 | 86.0 |
Table 5: Router classification accuracy (%) on a mixed evaluation set of 500 instances (100 per dataset). The ground-truth solver per dataset is determined by the design intent of each symbolic engine.
Appendix figures & tables9 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 3: Prompt template for Logical Knowledge Graph Construction. This prompt instructs the LLM to extract structured logic from text based on a dynamic ontology. It defines specific schemas for Entities, Concepts, and logical relationships (Rules/Constraints), enforcing a strict JSON output format to ensure graph integrity.
Figure 4: Prompt template for the Symbolic Solver (Z3) Code Generation. This prompt guides the model to translate the retrieved logical subgraph into an executable Python script utilizing the Z3 SMT solver. It enforces a structured coding process: declaring variables for entities, encoding facts as constraints, and formulating the specific query logic to verify the answer.
Figure 5: Prompt template for the Logic Pruning Module. This prompt instructs the LLM to filter the expanded candidate set.
Figure 6: Prompt template for the Adaptive Logic Router. This prompt guides the model to classify the reasoning task by evaluating the retrieved constraints and rules. It explicitly defines the decision boundaries for solver selection: Z3 is chosen for arithmetic and constraint satisfaction problems (CSPs), Prover9 for first-order logic theorem proving, and Pyke for knowledge-based relational inference.
Figure 7: Case Study: Logical Knowledge Graph Extraction Result. The figure displays the structured JSON output extracted from an AR-LSAT logical reasoning problem. It demonstrates how the system identifies entities (e.g., Office, Computer), maps concepts, and formalizes complex constraints (e.g., “AllDifferent”, “Ordering”) and logical rules from the raw text context.
Figure 8: Case Study: Inference Pipeline Log. This log trace illustrates the step-by-step execution flow: (1) Hybrid Search retrieves relevant rules regarding “Year” and “Office”; (2) Pruning filters candidates down to the essential logic; (3) The Logic Router correctly identifies the task as an arithmetic/ordering problem and selects the Z3 Solver; (4) The system generates and executes valid Z3 code to derive the final answer.
| Dataset | LKG | LLM | Total |
|---|---|---|---|
| 2Wiki | 159.2 | 6.79 | 165.96 |
| HotpotQA | 208.5 | 6.00 | 214.57 |
| MuSiQue | 395.8 | 11.35 | 407.14 |
Table 6: Per-sample wall-clock latency (seconds) on the multi-hop QA pipeline, averaged over instances per benchmark.
| Dataset | LKG | Solver | Total |
|---|---|---|---|
| AR-LSAT | 33.1 | 102.5 | 135.6 |
| LogicalDeduction | 18.9 | 103.3 | 122.2 |
| FOLIO | 23.4 | 91.8 | 115.2 |
| ProntoQA | 34.3 | 37.1 | 71.4 |
| ProofWriter | 35.1 | 131.4 | 166.5 |
| Average | 29.0 | 93.2 | 122.2 |
Table 7: Per-sample wall-clock latency (seconds) on the logical reasoning pipeline, averaged over 20 instances per dataset ( in total). “Total” reflects single-path production deployment (LKG construction plus the routed-solver path with up to three self-refining retries).