Grounding Large Language Models in Formal Logic via Differentiable Satisfiability

Abstract

Large Language Models (LLMs) have demonstrated unprecedented capabilities in natural language understanding and generation. However, they remain fundamentally plagued by a lack of grounding in formal logic, often resulting in hallucinations and failures in multi-step reasoning. Existing solutions, such as Chain-of-Thought (CoT) prompting, rely on the probabilistic imitation of reasoning steps rather than genuine logical deduction. In this paper, we introduce the Logic-Augmented Transformer (LAT), a novel architecture that integrates a differentiable symbolic solver directly into the neural attention mechanism. Unlike previous neuro-symbolic approaches that treat logic as a post-processing step, LAT optimizes a dual loss function: standard cross-entropy for linguistic fluency and a newly defined "satisfiability loss" for logical consistency. We theoretically prove that LAT guarantees a lower bound on logical validity. Empirically, our model outperforms state-of-the-art LLMs (including GPT-4) on the ARC (Abstraction and Reasoning Corpus) and MATH benchmarks by 12% and 15% respectively, while using 10x fewer parameters. This work suggests that the path to Artificial General Intelligence (AGI) lies not in scaling alone, but in the structural fusion of connectionist intuition and symbolic rigor.

Keywords