Considering the challenges faced by large language models (LLMs) on logical
reasoning, prior efforts have sought to transform problem-solving through tool
learning. While progress has been made on small-scale problems, solving
industrial cases remains difficult due to their large scale and intricate
expressions. In this paper, we propose a novel solver-layer adaptation (SoLA)
method, where we introduce a solver as a new layer of the LLM to differentially
guide solutions towards satisfiability. In SoLA, LLM aims to comprehend the
search space described in natural language and identify local solutions of the
highest quality, while the solver layer focuses solely on constraints not
satisfied by the initial solution. Leveraging MaxSAT as a bridge, we define
forward and backward transfer gradients, enabling the final model to converge
to a satisfied solution or prove unsatisfiability. The backdoor theory ensures
that SoLA can obtain accurate solutions within polynomial loops. We evaluate
the performance of SoLA on various datasets and empirically demonstrate its
consistent outperformance against existing symbolic solvers (including Z3 and
Kissat) and tool-learning methods in terms of efficiency in large-scale
problem-solving.

对大型语言模型（LLMs）在逻辑推理中所面临的挑战，以及利用工具学习改变问题求解的过程进行了探讨。本文提出了一种新颖的解算器层自适应（SoLA）方法，通过将解算器作为 LLMs 的新层，以不同的方式引导解决方案朝着可满足性发展。通过利用 MaxSAT 作为桥梁，定义正向和反向转移梯度，使最终模型能够收敛到满足的解决方案或证明不可满足性。通过验证 SoLA 在各种数据集上的性能，实证证明了其在大规模问题求解的效率上相对于现有的符号求解器（包括 Z3 和 Kissat）和工具学习方法的持续优势。