神经符号推理用于规划：通过大型语言模型和可满足性求解的反例引导归纳合成

Sep, 2023

神经符号推理用于规划：通过大型语言模型和可满足性求解的反例引导归纳合成

Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving

PDF

Sumit Kumar Jha, Susmit Jha, Patrick Lincoln, Nathaniel D. Bastian, Alvaro Velasquez...

TL;DR使用方便的自然语言进行交流，结合生成式大型语言模型和可满足模理论求解器，可以生成可验证的正确解决方案。

Abstract

generative large language models (LLMs) with instruct training such as GPT-4 can follow human-provided instruction prompts and generate human-like responses to these prompts. Apart from natural language responses, they have also been found to be effective at generating formal artifacts

generative large language models hallucination satisfiability modulo theory solvers inductive llms deductive smt solvers

发现论文，激发创造

利用大型语言模型生成答案集程序

本文提出了一种神经符号方法，将大型语言模型和答案集编程的优势相结合，以将逻辑谜题的自然语言描述转化为答案集程序。

Jul, 2023

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

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

May, 2023

元推理：针对大型语言模型的语义符号解构

本文提出了元推理（Meta-Reasoning）的概念，通过符号解构，最大限度地将某些推理任务的不同问题转化为类似的自然语言表达式，从而使得大语言模型 (LLMs) 能够通过类比学习和促进数据有效的上下文学习，从而显著地提高推理能力，GPT-3 (text-davinci-002) 在使用一个元推理演示的情况下可以达到超过 99％的准确率。

Jun, 2023

语言模型是贪心推理器：对思维链的系统形式分析

本文通过介绍一种新的合成问答数据集 PrOntoQA，旨在通过对 LLMs 的系统探索，该数据集是通过使用一阶逻辑表示的合成世界模型生成的。作者对 InstructGPT 和 GPT-3 进行了分析，表明 LLMs 能够进行正确的逻辑推理，但在方案规划方面存在困难。

Oct, 2022

使用 Transformers 生成符号化计划

本文介绍了 Plansformer，这是一个进行了微调的 LLM，可用于自动化规划，并且具有强大的转移学习能力，可适用于解决不同复杂度的规划领域，其中一个 Plansformer 的配置可实现 97% 有效计划，其中 95% 为汉诺塔谜题的最优解。

Dec, 2022

基于符号规划和代码生成的实地对话

使用大型语言模型与符号规划器和基于代码执行的系统组成的模块化可解释的对话系统，在处理任务导向对话中解决了大型语言模型难于引导到任务目标和处理新颖基础的问题，并在具有抽象散点图的协作参考解决任务中显著优于之前的最新技术，包括在最具挑战性的情境中将人工评估的任务成功率从 56% 提高到 69%。

Oct, 2023

生成符合 PDDL 标准的神经符号规划器框架

本文介绍了 Teriyaki 框架，将大型语言模型（LLMs）训练为与规划领域定义语言（PDDL）兼容的神经符号规划器，验证了这种基于 LLMs 的规划器的正确性，并将其与现有的 PDDL 规划器进行了比较。

Mar, 2023

异步计划推理中的图增强大语言模型

异步计划推理对于优化时间成本需要进行顺序和并行规划，这是具有挑战性的。本研究首次对大型语言模型（LLMs）在此任务上的成功进行了大规模研究。我们发现，代表性的闭源和开源 LLMs，包括 GPT-4 和 LLaMA-2，在缺乏关于任务解决过程的说明时表现不佳。我们提出了一种新颖技术，称为 Plan Like a Graph (PLaG)，它将图形与自然语言提示相结合，取得了最先进的结果。我们表明，尽管 PLaG 可以提升模型性能，但在任务复杂性增加时，LLMs 仍然会遭受严重退化，凸显了利用 LLMs 模拟数字设备的局限性。我们认为这项研究是将 LLMs 用作高效自治代理的一个令人兴奋的步骤。

Feb, 2024

大型语言模型的符号能力研究

研究证实，大型语言模型在处理基于符号的任务时面临符号复杂度上升的挑战，强调了需要专门的训练、内存和架构调整以提高它们在符号推理任务中的熟练度。

May, 2024

Logic-LM: 使用符号求解器增强大型语言模型进行可靠的逻辑推理

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

May, 2023