DiLA: Enhancing LLM Tool Learning with Differential Logic Layer

TL;DR

DiLA introduces a differentiable logic layer atop LLMs to enhance logical reasoning without fully outsourcing to solvers. By translating natural language constraints into CNF via the LLM, generating an initial solution, and then iteratively refining it through a forward/backward differentiable logic layer, DiLA achieves high accuracy and significant runtime improvements over prompt-based and solver-augmented baselines. The approach shows strong performance on classic constraint problems (SAT, Graph Coloring) and scales to hard industrial benchmarks where traditional CDCL solvers struggle, while also enabling robust natural language constraint reasoning (NLCR) with 3–5 sentence high-level summaries. The results indicate substantial practical impact for real-world reasoning tasks, including improved efficiency, robustness, and interpretability through gradient-based solution refinement and unsat-core localization.

Abstract

Considering the challenges faced by large language models (LLMs) in logical reasoning and planning, prior efforts have sought to augment LLMs with access to external solvers. While progress has been made on simple reasoning problems, solving classical constraint satisfaction problems, such as the Boolean Satisfiability Problem (SAT) and Graph Coloring Problem (GCP), remains difficult for off-the-shelf solvers due to their intricate expressions and exponential search spaces. In this paper, we propose a novel differential logic layer-aided language modeling (DiLA) approach, where logical constraints are integrated into the forward and backward passes of a network layer, to provide another option for LLM tool learning. In DiLA, LLM aims to transform the language description to logic constraints and identify initial solutions of the highest quality, while the differential logic layer focuses on iteratively refining the LLM-prompted solution. Leveraging the logic layer as a bridge, DiLA enhances the logical reasoning ability of LLMs on a range of reasoning problems encoded by Boolean variables, guaranteeing the efficiency and correctness of the solution process. We evaluate the performance of DiLA on two classic reasoning problems and empirically demonstrate its consistent outperformance against existing prompt-based and solver-aided approaches.

Figures (11)

• Figure 1: Illustration of CoT (left), solver-aided approach (middle), and our logic layer-aided language modeling approach (right).
• Figure 2: Exemplar comparison of solving graph coloring problems by different approaches. Direct prompts by GPT-4 make errors when generating the color assignment step by step; SATLM, based on the Z3 symbolic solver, cannot solve parsed constraints and outputs unknown (both errors are highlighted in red). In contrast, DiLA can generate the correct answer by combining the strengths of LLMs and the differential logic layer.
• Figure 3: The overall flow of DiLA.
• Figure 4: Comparing DiLA with and without LLM initialization.
• Figure 5: Example problem from the NLCR benchmark requiring natural language understanding and constraint reasoning.