Oct, 2023

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

PDF
TL;DR使用 LLM4nl2post 将非正式自然语言转化为形式化方法的后置条件，并通过验证度量在质量和生成的后置条件的可区分性方面进行比较。结果显示，这些后置条件通常是正确的且能够区分错误的代码，并且通过 LLMs 进行 LLM4nl2post 有潜力在实践中发挥重要作用，在 Defects4J 中成功捕获了 70 个真实世界历史 BUG。
informal natural languagecode functionalityfault localizationdebuggingllm4nl2post
发现论文，激发创造
  • 朝着大型语言模型辅助的程序优化

    使用 GPT4、Coq 和 Coqhammer 实现的 LLM4PR 工具将正式程序细化技术与非正式 LLM 方法相结合，通过将规范转换为前置条件和后置条件，基于细化演算自动生成提示，并与 LLM 进行交互以生成代码，最后验证生成的代码是否符合细化演算的条件，从而确保代码的正确性。

    Jun, 2024

  • 自然语言编程学习

    使用自然语言作为一种新的编程语言来描述任务过程，让其易于被人类和 LMMs 理解，并进一步借助 Learning to Program (LP) 方法通过学习来自训练集中的自然语言程序，优化复杂任务的问题解决能力，该方法在 AMPS 和数学两个数据集上的有效性得到验证，证明其性能超过直接零样本测试表现 18.3%。

    Apr, 2023

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

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

    Mar, 2024

  • 评估基于 LLM 驱动的用户意图形式化对于具备验证意识的语言

    通过符号测试规范来评估和验证音而语言中用户意图的质量与大型语言模型生成的和人工标注的 Dafny 规范数据集基本接近，但也显示了人工标注存在不完善的情况。我们的工作为程序用户意图形式化问题的建立基准和研究议程铺平了道路。

    Jun, 2024

  • 超越自然语言：利用替代格式增强推理与沟通的 LLM

    通过探索非自然语言表达的实用性，本文挑战了大型语言模型默认使用自然语言的做法，并展示了在单个语言模型推理和多智能体通信方面，让语言模型自主选择最合适的表达形式可以提高 3.3% 至 5.7% 的推理效率以及多智能体通信中高达 72.7% 的记号使用减少，并保持沟通有效性。同时，综合分析揭示了语言模型可以从有限的任务指令中设计一种格式，并且所设计的格式可以有效地在不同的语言模型之间转换。该研究还发现，语言模型决定的结构化通信格式与已建立的智能体通信语言存在显著的相似性，显示出在智能体通信中向高效、结构化通信的自然演化。

    Feb, 2024

  • 使用大型语言模型执行自描述算法：一项调查研究

    研究表明，目前的大型语言模型（LLMs），特别是 GPT-4，能够有效地执行用自然语言描述的程序，只要不涉及繁重的数值计算。

    Feb, 2024

  • 从自然语言问题描述生成功能正确的代码编辑

    本文提出了将自然语言编程描述翻译为正确代码修改的任务 NL2Fix，为此引入了包含高级 Bug 修复描述的 Defects4J-NL2Fix 数据集，并对多种最先进的 LLMs 进行了实证评估，结果表明这些 LLMs 能够对 64.6% 的错误生成合理的修复，并且最佳 LLM 技术在此基准测试中可以达到 21.20% 的 top-1 和 35.68% 的 top-5 精度。

    Apr, 2023

  • 正式 - LLM：将正式语言和自然语言整合为可控制的基于 LLM 的代理人

    该篇论文提出了一种名为 ``Formal-LLM'' 的新型框架用于基于 LLM 的代理，通过结合自然语言的表现力和形式语言的准确性，使规划过程具有控制性，从而防止代理生成无效和不成功的计划，并且通过实验验证了该框架在任务性能上取得的超过 50% 的整体性能提升，为在规划的有效性至关重要的应用场景中更广泛地利用 LLM 提供了可能性。

    Feb, 2024

  • 利用大语言模型将自然语言转换为计划目标

    本研究探讨了大型语言模型是否能够将自然语言的目标翻译成结构化的计划语言。我们使用 GPT 3.5 变种进行了实验，结果表明大型语言模型更适合进行翻译而不是规划，虽然这些模型能够利用常识知识和推理填补自然语言目标中缺失的细节，但在涉及到数字或物理推理的任务中，它们可能会出现失败，并且对所使用的提示信息很敏感。

    Feb, 2023

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

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

    Jul, 2023