NuSym-R: Self-Contained Neuro-Symbolic Verification with DAG-Structured Proof Graphs

While Large Language Models (LLMs) demonstrate impressive fluency in reasoning tasks, their intermediate steps remain largely opaque, often harboring undetected logical fallacies and arithmetic hallucinations. Existing neuro-symbolic approaches tackle this by translating LLM rationales into formal specifications and deferring verification to external solvers (e.g., Z3, Prover9, or Lean). However, this creates tight coupling, limits portability across diverse deployment environments, and often constrains reasoning into rigid, linear proof chains that fail to capture the shared sub-structures inherent in complex deduction. We present NuSym-R, a completely self-contained neuro-symbolic verification framework that eliminates the need for external theorem provers. NuSym-R implements a five-stage architecture centered around three core components: (1) a typed first-order logic (FOL) parser that translates natural-language reasoning steps into formal facts and rules; (2) a native forward-chaining verification engine that unifies these elements to construct DAG-structured proof graphs, preserving shared intermediate derivations; and (3) a structured feedback mechanism that intercepts verification failures to deliver precise, predicate-level diagnostic signals back to the LLM, driving an iterative self-correction loop. We evaluate NuSym-R across multi-hop arithmetic (GSM8K), first-order logic natural language inference (FOLIO), and deductive reasoning (ProofWriter). In addition to standard metrics, we introduce four novel diagnostic metrics, including Error Detection Rate (EDR) and Self-Correction Rate (SCR), to isolate the direct impact of symbolic verification. Extensive experiments, supported by rigorous paired bootstrap and McNemar's significance tests, reveal that NuSym-R dramatically enhances answer reliability and proof soundness while yielding machine-checkable artifacts – achieving this entirely within a self-contained, highly portable framework.