Feb, 2024

SoLA：基于求解器层适应的 LLM 在逻辑推理中的应用

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

    Logic-LM 是一种将大型语言模型与符号推理相结合的框架，通过首先使用大型语言模型将自然语言问题转化为符号形式，然后进行确定性符号求解，以及自我精炼阶段来修正符号形式，在 ProofWriter、PrOntoQA、FOLIO 和 LogicalDeduction 等四个逻辑推理数据集上的结果表明，与仅使用大型语言模型相比，我们的方法可以显著提高逻辑推理的性能。

    May, 2023

  • 语言模型可作为逻辑求解器

    LoGiPT 是一种新颖的语言模型，通过直接模拟逻辑求解器的推理过程并严格遵守求解器的语法规则，绕过分析错误，并在竞争的语言模型上表现出优异的性能。

    Nov, 2023

  • 利用可满足性辅助的语言模型与声明性提示

    本文提出了一种新的满足性辅助语言建模方法，利用自然语言处理模型生成任务的声明性规范，使用现成的自动定理证明器进行推理并验证答案的正确性，在解决需要更复杂的规划与搜索任务时比基于编程范式的模型更加有效。

    May, 2023

  • 深度研究逻辑推理与 LLM：工具选择的重要性

    通过将大型语言模型 (LLMs) 与各种符号求解器相结合，我们对 Z3、Pyke 和 Prover9 三个符号求解器的性能进行实验证明，其中与 LLMs 相结合时，Pyke 的性能明显低于 Prover9 和 Z3，Z3 的总体准确性略高于 Prover9，但 Prover9 能够处理更多问题。

    Jun, 2024

  • 利用深度学习构建带性能界限的随机局部搜索 SAT 求解器

    利用图神经网络训练适用于布尔可满足性问题的 SLS 求解器，可显著提高性能，平均解决比例更高、步骤更少，具有性能保证。

    Sep, 2023

  • SATNet: 使用可微可满足性求解器桥接深度学习与逻辑推理

    本文提出了一种新的路线，即通过引入可微（平滑）的最大可满足性（MAXSAT）求解器，将逻辑推理纳入更大的深度学习系统的循环中，从而在端到端学习系统中学习有挑战性的问题的逻辑结构，表现出集成逻辑结构于深度学习的潜力。

    May, 2019

  • LogicLLM: 探索基于自监督逻辑增强训练的大型语言模型

    本篇论文主要介绍了如何通过自监督后训练和上下文学习来增加逻辑知识，从而提高语言模型的逻辑推理能力，取得了比现有基线更好的效果。

    May, 2023

  • SAAS：增强大型语言模型数学推理的解决能力放大策略

    本研究提出了一种新颖的学习方法，旨在增强大型语言模型的数学推理和问题解决能力。通过整合思维链和思维方案的学习，以解决数学问题为重点，提出了一种名为 SAAS 的顺序学习方法。经过广泛的性能比较实证研究，结果表明我们的 SAAS 在数学推理领域取得了最先进的性能。

    Apr, 2024

  • 小语言模型微调以协调更大的语言模型，提升复杂推理

    引入 DaSLaM，使用分解生成器将复杂问题分解为需要更少推理步骤的子问题，由求解器回答。我们的方法在多个不同推理数据集上进行评估，表明 1750 亿参数 LM（text-davinci-003）可以产生与规模更大的 GPT-4 相比具有竞争力甚至更好的性能。

    Oct, 2023

  • 通过将语言模型与符号求解器相结合解决数学语言问题

    通过将大型语言模型与外部符号求解器相结合，我们提出了一种能够将单词问题逐步规范化为一组变量和方程的方法，并使用符号求解器解决问题，相较于 PAL 在解决代数类问题上性能提升了 20%。

    Apr, 2023