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

This paper introduces Delta1 with LLM, a neuro-symbolic framework that combines the deterministic, polynomial-time theorem generation of the Automated Theorem Generator Delta1 with large language models to produce credible, auditable, and naturally explained reasoning across critical domains like healthcare and compliance.

The Gist

Imagine you are trying to build a house, but your blueprint has a hidden flaw: the instructions say the roof must be made of ice, the walls of fire, and the foundation of water. If you try to build it exactly as written, the house collapses immediately.

Now, imagine two different experts trying to help you fix this:

1. The "Math Wizard" (Symbolic Logic): This expert is incredibly precise. They look at your blueprint and say, "If you remove the 'ice roof' instruction, the house can stand." They can prove this mathematically, 100% of the time, with zero guesswork. However, they speak only in complex equations and symbols. They can tell you that the house will fall, but they can't explain why in a way a regular person understands.
2. The "Storyteller" (Large Language Model): This expert is great at speaking human language. They can look at a blueprint and say, "Oh, ice roofs melt in the sun!" But if you ask them to prove the house will fall, they might guess, hallucinate, or make up a reason that sounds good but is actually wrong.

This paper introduces a new team called "∆1 + LLM" that combines the best of both worlds.

The Core Idea: "Explainability by Construction"

Instead of building a house and then trying to explain why it fell (which is messy and often wrong), this system builds the explanation into the construction process from the very beginning.

Here is how the team works, step-by-step, using a simple analogy:

1. The Translator (The Front-End LLM)

First, you give the system a messy paragraph of rules (like a medical policy or a legal contract).

• What happens: The "Storyteller" reads your text and translates it into a clean list of simple facts (like "Patient has infection" or "Data is shared"). It turns your messy English into a structured list of ingredients.

2. The Logic Engine (The ∆1 Generator)

This is the "Math Wizard." It takes your list of ingredients and runs a special, deterministic algorithm (called FTSC).

• What happens: Instead of guessing, it mathematically constructs every possible way these ingredients could clash. It finds the smallest possible group of rules that cause the problem.
• The Magic: It doesn't just say "There is a problem." It says, "If you remove this specific rule (Rule D), the conflict disappears." It does this without any guessing, in a predictable amount of time. It guarantees that the problem it found is real and minimal.

3. The Translator (The Back-End LLM)

Now, the "Math Wizard" hands the result to the "Storyteller" again.

• What happens: The Storyteller looks at the specific rule the Math Wizard flagged and says, "Ah! This rule says 'If you have a fever, take antibiotics.' But another rule says 'If you have a virus, don't take antibiotics.' The system found that these two rules can't exist together."
• The Result: It gives you a clear, human-readable explanation: "Your policy is contradictory. You can't have both rules active at the same time. Here is how to fix it..."

Why is this a big deal?

1. No More "Black Box" Guessing
Usually, when AI finds a problem, we don't know if it's right or if the AI just made it up. With this system, the "Math Wizard" part is 100% provable. If the system says there is a contradiction, there is definitely a contradiction. The logic is ironclad.

2. From "What" to "How"
Old systems might tell you, "Your contract is invalid." This system tells you, "Your contract is invalid because Clause A conflicts with Clause B, and here is exactly how to rewrite Clause A to fix it." It turns a diagnosis into a prescription.

3. It Works in Real Life
The paper shows this working in three scary-but-important areas:

• Healthcare: Catching rules where a doctor is told to do two opposite things for a patient (e.g., "Treat with drug X" vs. "Do not give drug X if patient has condition Y").
• Law & Compliance: Finding where a company's privacy policy contradicts a government regulation (e.g., "We must share data" vs. "We must never share data").
• Contracts: Spotting clauses in a business deal that cancel each other out before anyone signs the paper.

The Bottom Line

Think of ∆1 + LLM as a super-powered editor for complex rules.

• The Math part ensures the editing is logically perfect and never makes a mistake.
• The AI part ensures the editing suggestions are written in plain English that humans can actually understand and act upon.

It bridges the gap between "cold, hard math" and "warm, human conversation," creating a system that is not only smart but also trustworthy and explainable. It moves us from "The computer says no" to "The computer says no, and here is exactly why, and here is how to fix it."

Technical Summary

1. Problem Statement

Current neuro-symbolic reasoning systems face a fundamental trade-off:

• Symbolic Logic (e.g., Automated Theorem Provers): Offers formal soundness, provable correctness, and transparent inference structures but lacks linguistic expressivity and often produces opaque, unstructured proof traces that are difficult for humans to interpret.
• Neural Models (e.g., Large Language Models - LLMs): Provide fluency, adaptability, and natural language generation but rely on stochastic processes, lacking guarantees of logical correctness or verifiable soundness.

Existing hybrid approaches often embed symbolic constraints into neural architectures or use LLMs for proof synthesis, yet they fail to provide formal guarantees of correctness while simultaneously offering human-level interpretability. There is a critical need for a framework that unifies the rigor of logic with the explainability of language by design, rather than through post-hoc approximation.

2. Methodology: The ∆1 + LLM Framework

The paper proposes an end-to-end pipeline called ∆1 + LLM, which integrates a deterministic symbolic theorem generator (∆1) with a neural language layer (LLM). The architecture operates on the principle of "Explainability by Construction."

A. The Symbolic Core: ∆1 (Automated Theorem Generator)

∆1 is a deterministic engine grounded in the Full Triangular Standard Contradiction (FTSC) schema. Unlike traditional ATPs that rely on search, resolution, or backtracking, ∆1 constructs theorems constructively.

• Input: A set of $n$ distinct, non-complementary atomic predicates ($L = \{x_1, ..., x_n\}$).
• Mechanism: ∆1 constructs a specific clause set $S$ (the FTSC) defined as:
  • $D_1 = x_1$
  • $D_2 = x_2 \lor \neg x_1$
  • ...
  • $D_t = x_t \lor \neg x_1 \lor ... \lor \neg x_{t-1}$
  • ...
  • $D_{n+1} = \neg x_1 \lor \neg x_2 \lor ... \lor \neg x_n$
• Theorem Generation: For every clause $C \in S$, ∆1 generates a theorem of the form $S \setminus \{C\} \vdash \neg C$. This proves that removing any single clause from the unsatisfiable set $S$ restores satisfiability, while the remaining clauses logically refute the removed one.
• Properties:
  • Deterministic: No search or randomness; the process is $O(n^3)$ per canonical set.
  • Minimal Unsatisfiability: Every generated theorem corresponds to a Minimal Unsatisfiable Subset (MUS) by construction.
  • Completeness: It generates exactly $n!$ non-redundant, non-equivalent theorems covering all structural permutations of the input literals.
  • Soundness: Formal validity is guaranteed by the definition of the FTSC.

B. The Neural Layer: LLM Integration

The LLM acts as a semantic interpreter and ranking engine, bridging the gap between formal logic and human understanding.

• Front-end: Converts natural language domain rules into atomic predicates (logical forms) in TPTP syntax.
• Back-end: Takes the explicit proof traces and theorems generated by ∆1 and verbalizes them into coherent natural language explanations, identifying the "why" behind contradictions and suggesting actionable remediations.
• Ranking: Optionally ranks theorems based on contextual salience, novelty, or domain importance.

C. The Pipeline Flow

1. Predicate Extraction: Natural language input $\rightarrow$ Logical predicates.
2. Deterministic Generation: ∆1 constructs FTSC and generates minimal theorems ($S \setminus \{C\} \vdash \neg C$) with explicit proof traces.
3. Verbalization: LLM translates logical dependencies into natural language rationales and remediation strategies.

3. Key Contributions

1. Explainability by Construction: The system does not explain reasoning after the fact; it generates reasoning that is inherently interpretable. Every explanation is grounded in a deterministic, verifiable proof trace.
2. Formal Guarantees in Neuro-Symbolic AI: It is the first framework to combine a formally guaranteed, non-search theorem generator with LLMs, ensuring that the output is both logically sound and linguistically intelligible.
3. Minimal Unsatisfiability as a Discovery Engine: ∆1 transforms the concept of MUS extraction from a search problem into a constructive generation problem, producing a finite, complete universe of minimal contradictions for any given set of predicates.
4. Actionable Remediation: The system moves beyond detection to prescription, offering specific, domain-aligned suggestions to resolve logical inconsistencies (e.g., adding qualifiers to rules, relaxing constraints).

4. Results and Empirical Evaluation

The framework was evaluated across high-stakes domains including Healthcare, Compliance, Regulatory Conformance, and Contract Governance.

• Medical Reasoning:
  • Scenario: Rules regarding infection, WBC count, fever, and antibiotic requirements.
  • Outcome: ∆1 identified that the combination of all four conditions created a global contradiction. The LLM explained that "asserting infection alone violates consistency" given downstream constraints and suggested adding "confirmatory tests" or "severity levels" as remediation.
• Compliance & Regulation:
  • Scenario: Conflicts between GDPR (data portability) and HIPAA (data retention).
  • Outcome: The system identified "Data Portability" as the minimal inconsistent predicate. The LLM explained the tension between "free transfer/erasure" and "storage/restricted sharing," suggesting specific policy adjustments to restore satisfiability.
• Contract Analysis:
  • Scenario: Inconsistent clauses in supply agreements (exclusivity vs. termination rights).
  • Outcome: The system detected that unconditional termination rights contradicted exclusivity and penalty clauses. It suggested conditioning termination on "just cause" to resolve the logical conflict.
• Performance: The system operates deterministically with $O(n^3)$ complexity for construction. The case studies (with $n=4$ to $n=5$) demonstrated that the pipeline produces auditable, reproducible, and domain-aligned reasoning without requiring external SAT solvers or proof verification.

5. Significance and Impact

• Bridging the Gap: This work successfully unites the "truth-preserving" nature of symbolic logic with the "meaning-seeking" nature of neural language models, addressing the "black box" problem of LLMs and the "opacity" problem of traditional ATPs.
• Trustworthy AI: By ensuring that every explanation is backed by a mathematically proven, minimal contradiction, the system provides a foundation for auditable AI in critical sectors like law, medicine, and finance.
• New Benchmark: The ∆1 generator provides a "TPTP for explainability"—a structured, ground-truth dataset of minimal contradictions that can be used to benchmark the reasoning capabilities of future neuro-symbolic systems.
• Shift in Paradigm: The paper argues for a transition from "Automated Theorem Proving" (finding proofs) to "Automated Theorem Understanding" (generating and explaining the logical structure of contradictions), paving the way for self-reflective, human-aligned AI agents.

In conclusion, ∆1–LLM represents a principled advancement in neuro-symbolic AI, demonstrating that rigorous logical soundness and human-centric explainability are not mutually exclusive but can be achieved simultaneously through constructive theorem generation.