SoLA：基于求解器层适应的 LLM 在逻辑推理中的应用
内容提要
该文综述大语言模型与符号推理结合的进展，涵盖Logic-LM（先转符号再求解并自省）、LoGiPT（模拟求解器推理）、SAT辅助语言建模（用定理证明器验证）、Elemental Cognition平台（处理约束优化）、图神经网络提升SAT求解器、可微MAXSAT（将逻辑纳入深度学习）、自监督后训练增强逻辑知识、DaSLaM（分解子问题）、LLM结合符号求解器解代数题提升20%、SYRELM（用强化学习实现算术推理）。
延伸解读
神经符号推理的两种路径
文章展示了神经符号推理的两种主要路径：一是将自然语言转化为符号形式后交由求解器处理，如Logic-LM；二是让语言模型模拟求解器行为，如LoGiPT。前者依赖外部求解器的确定性，后者则试图内化推理过程。两种路径各有侧重，但都旨在弥补纯语言模型在逻辑严谨性上的不足。
求解器与语言模型的融合方式
除了直接调用求解器，研究还探索了更紧密的融合方式。例如，可微MAXSAT将逻辑推理嵌入深度学习循环，图神经网络则用于改进SAT求解器。这些尝试表明，符号求解器不仅可以作为外部工具，还能与神经网络结合，形成端到端可训练的系统，为复杂推理任务提供新思路。
性能提升与评估基准
多项工作在特定任务上报告了性能提升。例如，Logic-LM在四个逻辑推理数据集上显著优于纯语言模型；结合符号求解器的方法在代数问题上比PAL提升20%；DaSLaM使1750亿参数模型达到与GPT-4竞争的水平。这些结果基于不同基准，但共同指向符号推理对语言模型能力的增强作用。
实际应用与可解释性
Elemental Cognition平台展示了神经符号方法在约束满足和优化问题上的应用潜力。SYRELM则强调其方法易于诊断和解释，且大多数研究人员可使用。这表明，除了提升准确性，神经符号系统还注重实用性和透明度，为实际部署提供了可能。
Q&A
Logic-LM 是如何提升逻辑推理性能的？
Logic-LM 首先使用大型语言模型将自然语言问题转化为符号形式，然后进行确定性符号求解，并通过自我精炼阶段修正符号形式。在 ProofWriter、PrOntoQA、FOLIO 和 LogicalDeduction 四个数据集上，该方法比仅使用大型语言模型显著提高了逻辑推理性能。
LoGiPT 与 Logic-LM 在方法上有什么不同？
LoGiPT 通过直接模拟逻辑求解器的推理过程并严格遵守求解器的语法规则来绕过分析错误，而 Logic-LM 则是先将自然语言转化为符号形式再进行确定性符号求解。LoGiPT 在竞争的语言模型上表现出优异的性能。
SAT 辅助语言建模如何验证答案的正确性？
SAT 辅助语言建模利用自然语言处理模型生成任务的声明性规范，然后使用现成的自动定理证明器进行推理并验证答案的正确性。在解决需要复杂规划与搜索的任务时，它比基于编程范式的模型更有效。
Elemental Cognition 平台在处理约束满足和优化问题上有何优势？
Elemental Cognition 平台通过神经符号化方法，使用大型语言模型进行知识获取和用户交互，在处理约束满足和优化问题方面优于传统的大型语言模型，具有更高的有效性和性能。
DaSLaM 如何让较小规模的语言模型达到与 GPT-4 竞争的性能？
DaSLaM 使用分解生成器将复杂问题分解为需要更少推理步骤的子问题，然后由求解器回答。在多个推理数据集上评估表明，1750 亿参数的 LM（text-davinci-003）可以产生与规模更大的 GPT-4 相比具有竞争力甚至更好的性能。
SYRELM 架构如何实现算术推理？
SYRELM 通过采用符号求解器将自然语言算术问题转化为形式化语言描述，然后通过一个小型冻结的 LM 生成包含自然语言描述的形式化表达式，并通过策略梯度强化学习训练适应的 LM，从而实现合理的算术推理。该方法在准确性上取得了巨大改进，且易于诊断、解释和使用。
