Delta1 with LLM: symbolic and neural integration for credible and explainable reasoning

Yang Xu; Jun Liu; Shuwei Chen; Chris Nugent; Hailing Guo

cs.LOMar 13, 2026

Delta1 with LLM: symbolic and neural integration for credible and explainable reasoning

Authors: Yang Xu, Jun Liu, Shuwei Chen, Chris Nugent, Hailing Guo

Organizations: School of Mathematics, Southwest Jiaotong University, Chengdu 611756, China · National–Local Joint Engineering Laboratory of System Credibility Automatic Verification, Southwest Jiaotong University, Chengdu 611756, Sichuan, China · School of Computing, Ulster University, Belfast, Northern Ireland, UK

Abstract

Neuro-symbolic reasoning increasingly demands frameworks that unite the formal rigor of logic with the interpretability of large language models (LLMs). We introduce an end to end explainability by construction pipeline integrating the Automated Theorem Generator Delta1 based on the full triangular standard contradiction (FTSC) with LLMs. Delta1 deterministically constructs minimal unsatisfiable clause sets and complete theorems in polynomial time, ensuring both soundness and minimality by construction. The LLM layer verbalizes each theorem and proof trace into coherent natural language explanations and actionable insights. Empirical studies across health care, compliance, and regulatory domains show that Delta1 and LLM enables interpretable, auditable, and domain aligned reasoning. This work advances the convergence of logic, language, and learning, positioning constructive theorem generation as a principled foundation for neuro-symbolic explainable AI.

Figures & tables

Panel of Figure 1 — Figure 1: Architecture of the $\Delta_{1}$ + LLM pipeline. Natural‐language policy text is first processed by the front-end LLM to extract atomic predicates. The $\Delta_{1}$ generator deterministically constructs all minimal unsatisfiable clause sets and corresponding theorems ( $S\setminus\{C\}\vdash\neg C$ ), producing explicit proof traces. A back-end LLM module then translates each theorem into natural‐language explanations and remediation suggestions, enabling explainability by construction : formal correctness from $\Delta_{1}$ and interpretive clarity from the LLM.

Domain	Atomic Predicates ( $\mathcal{L}$ )
Contract	$\{\textit{Supplies}(s,p),\textit{DeliversOnTime}(s,p),\textit{ExclusiveSupplier}(s,p),\textit{CanTerminate}(b,s),\textit{HasPenalty}(s,p)\}$
Contract	$\{\textit{Delivers}(s,p,t),\textit{Insures}(s,p),\textit{PaysPenalty}(s,p),\textit{ForceMajeure}(t),\textit{Renews}(c)\}$
Contract	$\{\textit{Confidential}(d),\textit{Shares}(p,d),\textit{HasNDA}(p),\textit{Audits}(p),\textit{Discloses}(p,d)\}$
Healthcare	$\{\textit{HoldsData}(h,p),\textit{SharesData}(h,r,p),\textit{HasConsent}(p),\textit{Encrypts}(h,p),\textit{Retains}(h,p,t)\}$
Healthcare	$\{\textit{Diagnoses}(d,p),\textit{Prescribes}(d,p,m),\textit{Approves}(a,m),\textit{Reports}(d,p),\textit{Publishes}(a,m)\}$
Healthcare	$\{\textit{Treats}(h,p),\textit{UsesData}(h,p),\textit{HasConsent}(p),\textit{Charges}(h,p),\textit{Transfers}(h,p,r)\}$

Table 1: Atomic predicate sets (

L

) for each domain corresponding to the examples in Table 2 . Each

L

serves as input to

\Delta_{1}

for FTSC construction. Given

|L|=n

\Delta_{1}

deterministically generates

n\!+\!1

dependency clauses

(D_{1},\dots,D_{n+1})

, forming a canonical unsatisfiable set and minimal contradictions

S\setminus\{D_{i}\}\vdash\neg D_{i}

Domain	$\Delta_{1}$ Theorem	LLM Explanation (Semantic Interpretation)	Remediation / Policy Fix
Contract	$S\!\setminus\!\{D_{4}\}\!\vdash\!\neg D_{4}$	Termination without cause contradicts exclusivity and penalty dependencies in the FTSC chain.	Restrict termination rights to “for cause” or require notice/compensation.
Contract	$S\!\setminus\!\{D_{3}\}\!\vdash\!\neg D_{3}$	Strict penalty enforcement becomes inconsistent when ForceMajeure negations are active.	Qualify penalties with force‐majeure exceptions.
Contract	$S\!\setminus\!\{D_{5}\}\!\vdash\!\neg D_{5}$	Disclosure clause violates confidentiality unless NDA dependency ( $\neg x_{3}$ ) is resolved.	Add NDA precondition to disclosure permissions.
Healthcare	$S\!\setminus\!\{D_{3}\}\!\vdash\!\neg D_{3}$	Data sharing without consent ( HasConsent $(p)$ ) produces a minimal contradiction in the FTSC sequence.	Require explicit consent or anonymization before sharing.
Healthcare	$S\!\setminus\!\{D_{5}\}\!\vdash\!\neg D_{5}$	Publishing approvals without anonymization conflict with prior encryption and consent relations.	Anonymize or redact identifying data before publication.
Healthcare	$S\!\setminus\!\{D_{6}\}\!\vdash\!\neg D_{6}$	Transferring patient data contradicts consent, billing, and retention dependencies in the FTSC.	Add consent clause or lawful transfer basis.

Table 2: Ten representative

\Delta_{1}

contradiction theorems with corresponding LLM interpretations and remediations. For each atomic predicate set

L

of size

n

\Delta_{1}

generates

n\!+\!1

dependency clauses

(D_{1},\dots,D_{n+1})

composing the FTSC. Each minimal entailment

S\setminus\{D_{i}\}\vdash\neg D_{i}

reveals a domain‐specific inconsistency, which the LLM then explains and resolves in natural language.

Domain	Theorem	Priority	LLM‐Suggested Remediation
Contract	$S\setminus\{D_{4}\}\vdash\neg D_{4}$	High	Restrict termination rights to “for cause” or require notice/compensation.
Contract	$S\setminus\{D_{3}\}\vdash\neg D_{3}$	Medium	Qualify penalty clauses with force‐majeure exceptions.
Contract	$S\setminus\{D_{5}\}\vdash\neg D_{5}$	Low	Add NDA precondition to disclosure permissions.
Healthcare	$S\setminus\{D_{3}\}\vdash\neg D_{3}$	High	Require explicit patient consent or anonymization before data sharing.
Healthcare	$S\setminus\{D_{5}\}\vdash\neg D_{5}$	Medium	Anonymize or redact identifying data prior to publication.
Healthcare	$S\setminus\{D_{6}\}\vdash\neg D_{6}$	Low	Add lawful‐basis clause permitting compliant data transfer.

Table 3: Ranked summary of

\Delta_{1}

+ LLM reasoning outputs across domains. For each predicate set of size

n

\Delta_{1}

generates

n\!+\!1

FTSC clauses

(D_{1},\dots,D_{n+1})

. Each contradiction theorem

S\setminus\{D_{i}\}\vdash\neg D_{i}

is assigned a qualitative priority (High, Medium, Low) based on the LLM’s interpretation of practical impact and remediation urgency.

Neuro-Symbolic Reasoning

Neuro-symbolic reasoning combines learned neural models with explicit logic, rules, knowledge structures, or executable tools to solve structured tasks.

See all 270 papers

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification
Aug 9, 2026Wenyao Cui, Huaping Zhang, Yongyi Huang +6CoT Faithfulness LLM Answer Verification
Beijing Institute of Technology Beijing, China · Zhongguancun Academy Beijing, China · Xinjiang Future Enterprise Incubator Co., Ltd. Xinjiang, China +1
Neurosymbolic Language Reasoning as Satisfiability Modulo Theory
Feb 20, 2026Hyunseok Oh, Sam Stern, Youngki Lee +1Constraint-Guided Reasoning in Language Models Neuro-Symbolic Reasoning
Seoul National University · U. Mass. Amherst · Microsoft
TRUE: A Trustworthy Unified Explanation Framework for Large Language Model Reasoning
Feb 21, 2026Yujiao YangLLM Interpretability Faithfulness of Language Model Explanations
Dalian University of Technology, Dalian, China

Aug 9, 2026J/K move · Enter open · S save

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification

Wenyao Cui, Huaping Zhang, Yongyi Huang, Qiuchi Li+5

Beijing Institute of Technology Beijing, China · Zhongguancun Academy Beijing, China · Xinjiang Future Enterprise Incubator Co., Ltd. Xinjiang, China+1

CoT Faithfulness LLM Answer Verification Symbolic Reasoning Neuro-Symbolic Reasoning

Open paper AskPDF arXiv

Large language models (LLMs) increasingly serve as data-driven reasoners, yet their chains-of-thought (CoT) can be unfaithful even when final answers are correct. Most existing

verification'' signals are not diagnostic: answer matching observes only the outcome, LLM-as-judge provides subjective and non-verifiable critiques, and scalar rewards (e.g., PRMs/RMs) offer little insight into where a multi-step derivation fails.We propose **SymDiag**, a neuro-symbolic framework that **reframes reasoning verification as structured failure diagnosis**. SymDiag translates natural-language CoT into symbolic constraints and performs step-level satisfiability/entailment checks to (i) localize failing steps and (ii) produce verifiable diagnostic evidence, including counterexamples, inconsistency witnesses, and missing-premise indicators. A central challenge is that apparent

logic violations'' can be caused either by genuine reasoning defects or by neural-to-symbolic translation noise. SymDiag therefore incorporates a Self-Auditor that disentangles TranslationError from ReasoningError via dual symbolic encodings consistency checks, enabling robust diagnosis under partial observability. Across diverse mathematical, logical, scientific, and general reasoning benchmarks, SymDiag improves detection of unfaithful reasoning and provides substantially more effective feedback for multi-round reasoning repair than outcome-only verification and LLM-based judging, offering a principled foundation for trustworthy and scalable reasoning diagnosis.

Abstract

Neuro-Symbolic Reasoning

Explore similar work

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification

Neurosymbolic Language Reasoning as Satisfiability Modulo Theory

TRUE: A Trustworthy Unified Explanation Framework for Large Language Model Reasoning