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

• LLMs can generate plausible but incorrect steps and lose consistency across long contexts, challenging trustworthy reasoning in high-stakes domains such as healthcare, law, finance [3], and scientific discovery.Source: §1 · p. 1
• CoT lacks symbolic verification [10] and standard RAG misses directional dependencies in logical rules [9], while implicit rule representations impede deterministic verification and solver routing.Source: §1 · pp. 1–2
• SymbolLKG pairs LLM parsing of natural-language problems into an LKG with deterministic external solvers for reasoning.Source: §1 · p. 2
• Its Schema-on-Read LKG makes rules and constraints independent nodes, then combines vector search, graph traversal, and LLM pruning to form a minimal Logical Hull.Source: §1 · p. 2
• A Logic Router selects solvers from problem structure and uses solver error traces to refine generated code.Source: §1 · p. 2
• SymbolLKG significantly outperforms standard LLM prompting and baseline RAG on standard logical-reasoning and multi-hop QA datasets.Source: §1 · p. 2

Large Language Models for Logical Reasoning

• CoT [7], Zero-Shot CoT [19], Self-Consistency [20], and ToT [8] improve reasoning, but neural models still face unfaithful explanations, weak compositional generalization, and difficult self-correction [21] [22] [23] [24].These limitations motivate robust external verification mechanisms.Source: §2 · p. 2

Neuro-Symbolic AI and Auto-formalization

• Existing neuro-symbolic systems such as Logic-LM [27] and LINC [28] use external solvers, but static solver assignment fails on complex queries combining arithmetic and relational logic.SymbolLKG instead analyzes each query at runtime to select a solver, reflecting that tool effectiveness depends on problem structure [29].Source: §2 · p. 3

Retrieval-Augmented Generation for Structured Knowledge

• Standard RAG uses dense vector similarity and can retrieve semantically similar but logically irrelevant documents, causing semantic drift in logical reasoning tasks [9].It can also fail at multi-hop reasoning, which requires following logical chains rather than matching similar words.Source: §2 · p. 3
• Graph-guided methods Think-on-Graph [14], RoG [15], StructGPT [31], and GraphRAG [16] support reasoning over graph structures, but typically treat knowledge graphs as static entity lists and ignore complex rules.SymbolLKG makes rules and constraints primary graph nodes and combines vector search with Logical Hull Expansion to retrieve implicit axioms for the solver.Source: §2 · p. 3

3.1 Logical Knowledge Graph Construction

• The LKG represents concepts, entities, rules, and constraints as typed graph nodes, with context-specific concepts and logical rules or constraints modeled explicitly.OpenIE extracts graph elements from text; Schema-on-Read adapts concept and entity nodes to their roles. Rule embeddings support semantic search, while separating rules from assertions keeps the reasoning structure stable as entity data changes and enables translation into first-order logic.Source: §3.1 · p. 4

3.2 Hybrid Retrieval and Pruning

• Hybrid retrieval combines query-entity and embedding-based anchors with graph traversal to include nearby rules and constraints, then prunes irrelevant nodes into a compact subgraph.Traversal follows MENTIONS, IS_A, and APPLIES_TO edges to recover logically related rules and constraints, supporting logical completeness before LLM-based pruning.Source: §3.2 · pp. 4–5

3.3 Solver Selection via Logic Router

• The topology-aware router selects Z3 for constraint-heavy arithmetic or uniqueness tasks, Prover9 for rule-heavy first-order proofs, and Pyke for direct relational queries.This routes computation to symbolic engines rather than relying on the LLM for arithmetic.Source: §3.3 · p. 5

3.4 Code Generation

• The LLM compiles the pruned graph into solver-specific code and uses execution errors to refine it until success or timeout, yielding a formal proof or logically valid assignment.For Z3, entities become variables, concepts set domains, and constraints become assertions.Source: §3.4 · pp. 5–6

4.1 Experimental Settings

• Evaluation spans eight benchmarks: five for logical reasoning and three for multi-hop retrieval and QA.The logical set is FOLIO, AR-LSAT, ProofWriter, LogicalDeduction, and ProntoQA; the retrieval/QA set is 2WikiMultiHopQA, HotpotQA, and Musique. Llama-3.3-70B-Instruct serves as the extraction and translation backbone and primary baseline backbone, with temperature 0; solvers are Z3, Prover9, and Pyke, and hybrid retrieval combines BGE-M3 dense embeddings with topology-aware graph traversal.Source: §4.1 · p. 6

4.2 Logical Reasoning Performance

• 78.73% average accuracy beats Logic-LM (74.49%) and Standard CoT (69.56%), with 57.85% on AR-LSAT and 100.00% on ProntoQA.Typed constraint subclasses guide Z3 selection on AR-LSAT, while a three-attempt self-refining loop returns compiler errors to the LLM on ProntoQA; SymbolLKG lags Logic-LM on FOLIO and ProofWriter, where dataset-specific prompts and weaker router signals limit recovery.Source: Table 2 · p. 6, §4.2 · pp. 6–7

4.3 Multi-hop Retrieval Performance

• Recall@2 / Recall@5 is 79.4 / 88.2 on 2WikiMultiHopQA and 68.5 / 84.1 on HotpotQA.Hybrid anchoring unions three thresholded vector queries with a BM25 entity-name pass, and Logical Hull traversal surfaces distractor-buried HotpotQA facts; the single-pass anchor-and-prune strategy cannot restore evidence rejected initially, unlike IRCoT.Source: Table 3 · p. 7, §4.3 · p. 7

4.4 Question Answering Performance

• 70.2 EM / 74.9 F1 on 2Wiki, 73.8 EM / 81.5 F1 on HotpotQA, and 48.6 EM / 59.4 F1 on MuSiQue lead every prior baseline on every cell.The largest gain on MuSiQue is attributed to hash-based entity canonicalization and Logical Hull expansion; the +6.0 F1 on HotpotQA reflects topologically bounded retrieval among distractors, while the narrower 2Wiki gap is attributed to dense baselines already covering much of the evidence.Source: Table 4 · p. 8, §4.4 · p. 8

4.5 Router Performance

• 86.0% overall routing accuracy across 500 instances is more than 2.5× random, with 100.0% on AR-LSAT and LogicalDeduction, 85.0% on FOLIO, 92.0% on ProofWriter, and 53.0% on ProntoQA.Typed constraint cues and three-valued question wording guide routing; ProntoQA’s “true or false” phrasing can confuse Pyke with Prover9, though both engines support Horn-clause forward chaining.Source: §4.5 · pp. 8–9, Table 5 · p. 9

4.6 Computational Cost Analysis

• The full pipeline averages 122.2 s per logical reasoning problem and 166–407 s per multi-hop QA query, with LLM API calls taking more than 99% of wall-clock time.For fixed corpora, the LKG can be built offline and reused, reducing inference-time latency to retrieval under 0.1 s plus one answer-generation call of about 10 s.Source: §4.6 · p. 9

Conclusion

• SymbolLKG models logical rules as graph nodes and routes tasks to Z3, Prover9, or Pyke, producing deterministic proof traces and outperforming standard prompting and retrieval baselines.The framework is presented as bridging LLM semantic flexibility with symbolic solver precision; its proof traces are contrasted with opaque Chain-of-Thought generation.Source: §5 · p. 9

Limitations & Future Work

• Semantic misinterpretations during LLM extraction can propagate to the solver, which validates argument structure but cannot ensure premise truth when initial grounding is flawed.A self-refining loop mitigates syntax errors, but not this semantic translation bottleneck.Source: §5 · p. 9
• Vague quantifiers and metaphorical expressions can challenge the LKG’s rigid schema, risking oversimplification of natural-language nuance.The limitation arises because formal logic requires precise definitions while natural language is inherently ambiguous.Source: §5 · p. 9
• Graph construction and external solvers make SymbolLKG computationally heavier than single-pass generation, motivating work on extraction latency and end-to-end differentiable alignment.The proposed alignment aims to reduce dependence on intermediate discrete translation.Source: §5 · p. 9

A Prompt Templates

• The appendix presents prompt templates to make SymbolLKG’s LLM interaction mechanisms reproducible.Source: A Prompt Templates · p. 14

A.1 Prompt for LKG Construction

• The LKG construction prompt directs the LLM to extract structured logic from text using a dynamic ontology.Source: Figure 3 · p. 14
• It specifies schemas for entities, concepts, and logical relationships, including rules and constraints.Source: Figure 3 · p. 14

A.2 Prompt for Solvers

• The solver prompt translates a retrieved logical subgraph into an executable Python script using Z3.Source: Figure 4 · p. 15
• Its structured coding process declares entity variables, encodes facts as constraints, and formulates query logic to verify answers.Source: Figure 4 · p. 15

A.3 Prompt for Pruner; A.4 Prompt for Router

• The pruning prompt filters the expanded candidate set, while the router classifies tasks and selects Z3 for arithmetic or CSPs, Prover9 for first-order theorem proving, or Pyke for relational inference.Source: Figure 6 · p. 16, Figure 5 · p. 16

B Case Study

• The AR-LSAT case study demonstrates SymbolLKG’s end-to-end workflow, from extracting LKG components through dynamic inference to executable Z3 code.The workflow includes intermediate outputs at each stage.Source: B Case Study · p. 17
• The extracted LKG represents entities and concepts alongside formalized rules and constraints, including AllDifferent and Ordering.The example entities include Office and Computer.Source: Figure 7 · p. 17
• The inference trace retrieves and prunes relevant rules, routes the arithmetic/ordering task to Z3, and executes generated code to derive the final answer.Hybrid Search retrieves rules about Year and Office before pruning candidates to the essential logic.Source: Figure 8 · p. 18

C.1 Empirical Latency

• Latency is measured as per-sample wall-clock time; the profile uses 100 instances per benchmark, while Table 7 averages 20 instances per dataset, 100 total.Table 7 reports the single-path production pipeline with up to three self-refining retries.Source: §C.1 · p. 18, Table 7 · p. 19
• 166.0–407.1 s is the end-to-end per-sample latency range across the three multi-hop QA datasets, from 2WikiMultiHopQA to MuSiQue.Per-question LKG construction accounts for 159.2–395.8 s of that latency.Source: §C.1 · p. 18, Table 6 · p. 18
• 159.2–395.8 s is spent on per-question LKG construction over each question’s 8–10 paragraph context, while answer generation takes 6.0–11.4 s.Construction extracts entities, rules, and constraints.Source: §C.1 · p. 18, Table 6 · p. 18
• 122.2 s is the average end-to-end latency per logical reasoning problem, comprising 29.0 s for LKG construction and 93.2 s for the routed solver.The production path includes up to three self-refining retries.Source: §C.1 · p. 18, Table 7 · p. 19
• 166.5 s for ProofWriter and 135.6 s for AR-LSAT are the longest logical-reasoning mean latencies, reflecting longer Prover9/Z3 programs and higher retry rates.Source: §C.1 · p. 18, Table 7 · p. 19
• 71.4 s is ProntoQA’s mean latency, attributed to its lightweight Pyke forward-chaining path.Source: §C.1 · p. 18, Table 7 · p. 19

C.2 Discussion

• The two recurring LLM calls account for over 99% of wall-clock time, while retrieval and BFS together take below 0.1 s per query.The calls are LKG extraction plus solver-code generation or answer generation.Source: §C.2 · p. 19
• For fixed deployment corpora, building the LKG offline eliminates 155–494 s per-question construction, reducing inference to retrieval (<0.1 s) plus one answer-generation call (∼10 s).Source: §C.2 · p. 19
• The self-refining loop is capped at three retries, limiting worst-case solver latency to 3× the single-attempt cost.Source: §C.2 · p. 19
• Routing and pruning use bounded-length prompts that can run on a smaller, cheaper backbone without materially affecting accuracy.Source: §C.2 · p. 19