Proof-Carrying Neuro-Symbolic Reasoning for Non-Monotonic Legal Decision Support with LLMs
Large language models (LLMs) and retrieval-augmented generation (RAG) are increasingly used in legal decision support, but retrieved evidence and fluent explanations do not guarantee valid normative inference. This paper proposes a proof-carrying neuro-symbolic method for non-monotonic legal reasoning. The LLM component is restricted to source-linked extraction of facts, defeasible rules, defeaters, priorities, citations, and operational confidence scores, while a deterministic symbolic engine computes the conclusion. Evidence is represented as a finite defeasible normative theory and compiled into a Dung-style argumentation framework; accepted conclusions are obtained from the grounded extension and returned with proof graphs showing support, attacks, and priority-based defeats. Under gold formalization, the symbolic engine achieved 99.3% accuracy on a 600-case controlled benchmark. In a 240-scenario LLM-to-logic experiment, the GPT-4o extractor followed by symbolic reasoning achieved 86.7% downstream accuracy versus 75.8% for a direct LLM over the same retrieved evidence; the paired difference was supported by an exact McNemar test after Holm correction (adjusted p = 0.016). Differences from the PDL and simpler symbolic baselines were not statistically established. Validation-triggered repair yielded 90.4% observed accuracy. Public-contract, Russian-law, stress-test, scalability, and lawyer-verification experiments further delimit the feasibility and current limitations of proof-carrying legal decision support.