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

📄 arXiv: 2603.12953v1 📥 PDF

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

分类: cs.LO, cs.AI

发布日期: 2026-03-13

备注: 12 pages, 1 figure, 3 tables, accepted oral presentation at AAAI2026 Bridge Program on Logic & AI

💡 一句话要点

Delta1与LLM结合，实现可信且可解释的神经符号推理

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 神经符号推理 可解释AI 自动定理生成 大型语言模型 知识推理

📋 核心要点

  1. 神经符号推理需要兼顾逻辑的严谨性和LLM的可解释性，现有方法难以同时满足这两个需求。
  2. 论文提出Delta1框架，结合自动定理生成器和LLM，通过构造确保推理的可靠性和可解释性。
  3. 实验表明，该框架在医疗、合规等领域实现了可解释、可审计且领域对齐的推理。

📝 摘要（中文）

本文提出了一种端到端的、通过构建实现可解释性的流程，该流程集成了基于完全三角标准矛盾(FTSC)的自动定理生成器Delta1与大型语言模型(LLM)。Delta1以确定性的方式在多项式时间内构建最小不可满足子句集和完整定理，通过构造确保了可靠性和最小性。LLM层将每个定理和证明轨迹转化为连贯的自然语言解释和可操作的见解。在医疗保健、合规性和监管领域的实证研究表明，Delta1和LLM能够实现可解释、可审计和领域对齐的推理。这项工作推进了逻辑、语言和学习的融合，将建设性定理生成定位为神经符号可解释AI的原则性基础。

🔬 方法详解

问题定义：现有的神经符号推理方法难以同时保证逻辑推理的严谨性和结果的可解释性。传统方法可能缺乏对推理过程的明确解释，而基于LLM的方法可能存在幻觉问题，导致推理结果不可靠。因此，需要一种能够提供可信且可解释推理的框架。

核心思路：论文的核心思路是将自动定理生成器Delta1与LLM相结合。Delta1负责进行严谨的逻辑推理，生成最小不可满足子句集和完整定理，保证推理的可靠性。LLM则负责将Delta1的推理过程和结果转化为自然语言解释，提高可解释性。通过这种结合，可以同时实现推理的可靠性和可解释性。

技术框架：该框架包含两个主要模块：Delta1自动定理生成器和LLM解释器。Delta1基于完全三角标准矛盾(FTSC)算法，以确定性的方式构建最小不可满足子句集和完整定理。然后，LLM接收Delta1生成的定理和证明轨迹，并将其转化为连贯的自然语言解释和可操作的见解。整个流程是端到端的，通过构造确保了可解释性。

关键创新：该方法最重要的创新点在于将自动定理生成器Delta1与LLM相结合，实现了可信且可解释的神经符号推理。Delta1保证了推理的可靠性，LLM提高了可解释性。与现有方法相比，该方法能够提供更严谨、更可信、更易于理解的推理结果。

关键设计：Delta1的关键设计在于其基于FTSC算法的自动定理生成过程，该算法能够在多项式时间内构建最小不可满足子句集和完整定理。LLM的关键设计在于其自然语言生成能力，能够将Delta1的推理过程和结果转化为易于理解的解释。论文中没有明确说明具体的参数设置、损失函数或网络结构等技术细节，这些可能取决于所使用的具体LLM模型。

📊 实验亮点

论文在医疗保健、合规性和监管领域进行了实证研究，结果表明Delta1和LLM能够实现可解释、可审计和领域对齐的推理。具体性能数据和对比基线未在摘要中明确给出，但强调了该方法在实际应用中的有效性。

🎯 应用场景

该研究成果可应用于需要高度可信和可解释推理的领域，如医疗诊断、金融合规、法律法规解释等。通过提供可解释的推理过程，该方法可以帮助领域专家更好地理解和信任AI系统的决策，从而提高AI系统的应用价值和接受度。未来，该方法还可以扩展到更复杂的推理任务和领域。

📄 摘要（原文）

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.