Mar, 2023

nl2spec：使用大型语言模型将非结构化自然语言交互地翻译为时间逻辑

PDF
TL;DR通过使用大型语言模型从自然语言中推导出严格的正式说明的方法，解决了手动编写正式规范的困难，从而提出了一个框架 nl2spec。
发现论文，激发创造
  • NL2TL: 利用大型语言模型将自然语言转换为时间逻辑

    提出了一种使用大型语言模型进行自然语言到时间逻辑（Temporal Logic）转换的框架，实现了跨领域通用模型的构建，提高了模型泛化能力，并在五个不同领域上进行了测试，效果良好。

    May, 2023

  • LLM 能够正式对话吗？自动评估 LLM 在翻译和解释正式规范中的表现

    利用大型语言模型 (LLMs) 将自然语言描述转换为形式化规范的能力进行了评估，提出了一种使用两个 LLMs 与现成验证程序结合的方法来自动评估其翻译能力，结果显示目前最先进的 LLMs 无法充分解决这个任务，限制了它们在复杂系统设计中的实用性。

    Mar, 2024

  • Lang2LTL：将自然语言命令转换为时间机器人任务规范

    Lang2LTL 是一个基于大型语言模型的新型系统，能够提取自然语言指令中的相关表达并将其转化为机器人的任务规范，使任何机器人系统能够在无需额外训练的情况下解释自然语言导航命令并执行多步骤的导航任务，以 88.4% 的平均准确性在 22 个未见过的环境下进行翻译，并成功整合进一个计划工具，驱动四足移动机器人在实验室中执行多步导航任务。

    Feb, 2023

  • 机器人任务规范的自然语言到线性时间逻辑翻译器的高效数据学习

    本文提出一种基于学习的方法，通过算法生成 LTL 公式，并将其转换为结构化英语进而利用现代大型语言模型的改写功能来合成自然语言命令，从而减少人工数据依赖，以 75％的准确率将自然语言命令翻译成 LTL 规范，并发现该翻译的公式能够用于长视距的，多阶段任务的规划（以 12D 四旋翼为例）。

    Mar, 2023

  • 通过大型语言模型将自然语言意图正式化为程序规范

    使用 LLM4nl2post 将非正式自然语言转化为形式化方法的后置条件，并通过验证度量在质量和生成的后置条件的可区分性方面进行比较。结果显示，这些后置条件通常是正确的且能够区分错误的代码，并且通过 LLMs 进行 LLM4nl2post 有潜力在实践中发挥重要作用，在 Defects4J 中成功捕获了 70 个真实世界历史 BUG。

    Oct, 2023

  • 通过 LLM - 符号定理证明验证和改进自然语言解释

    通过将大型语言模型（LLMs）与定理证明器（TPs）相结合，本文研究了自然语言解释的验证和改进，提出了一个名为 Explanation-Refiner 的神经符号框架，用于生成和形式化解释句子，并为自然语言推理（NLI）提供潜在的推理策略。同时，定理证明器用于提供解释逻辑有效性的形式保证，并针对改进提供反馈。展示了如何共同使用 Explanation-Refiner 来评估最先进的 LLMs 的解释推理、自动形式化和错误纠正机制，以及自动提高不同领域中复杂性不同的人工注释解释的质量。

    May, 2024

  • 基于大型语言模型的软件规格自动综合

    本文提出了一个能从自然语言来源中自动生成软件规格说明的框架 SpecSyn，并证明其性能明显更强于之前的同类工具。

    Apr, 2023

  • 利用大型语言模型进行一致的时态逻辑规划：知道什么时候做什么和什么时候寻求帮助

    针对移动机器人在完成多个高级子任务中的新运动规划问题，本文提出了 HERACLEs，一个层次化一致性自然语言规划器，通过自动机理论确定机器人下一步应完成的子任务，使用大型语言模型设计满足这些子任务的机器人计划，并通过符合预测推理出计划的正确性和任务满足程度，并确定是否需要外部协助。

    Sep, 2023

  • 使用信号时间逻辑从自然语言和演示中进行交互式学习

    该研究介绍了一种交互式学习方法，能够从自然语言描述中学习正确、简洁的统一信号时序逻辑公式，并使用深度 Q 学习算法确定机器人的最优控制策略。

    Jul, 2022

  • 通过迭代符号细化增强大型语言模型的伦理解释

    本研究探讨如何利用混合神经符号技术来增强大型语言模型在伦理自然语言推理中的逻辑有效性和一致性，通过整合外部的向后求解器，改进逐步自然语言解释的过程，验证解释的正确性，减少不完整性和冗余性，并生成支持模型推理的形式证明，从而提高在多步伦理自然语言推理任务中解释的质量。

    Feb, 2024