Jun, 2024

DafnyBench: 形式软件验证基准

PDF
TL;DR我们介绍了 DafnyBench，这是一个用于训练和评估形式软件验证的机器学习系统的最大基准测试。我们测试了 LLM（如 GPT-4 和 Claude 3）生成足够的提示来让 Dafny 形式验证引擎成功验证 750 多个程序，代码行数约为 53,000 行。最佳模型和提示方案的成功率达到 68%，我们量化了通过错误信息反馈重试时成功率的提高，以及所需代码和提示数量的恶化。我们希望 DafnyBench 能够在 LLMs 和验证技术质量提高时，从这个基准得到快速改进。
dafnybenchmachine learning systemsformal software verificationllmsdafny formal verification engine
发现论文，激发创造
  • Laurel：使用大型语言模型生成 Dafny 断言

    Laurel 是一种使用大型语言模型（LLMs）自动生成 Dafny 程序的辅助断言的工具，通过两种领域特定的提示技术，能够提高 LLMs 在此任务中的成功率，从而使 LLMs 成为进一步自动化实际程序验证的可用且经济实惠的工具。

    May, 2024

  • DevBench：软件开发综合基准

    最近的大型语言模型 (LLMs) 的进展显著增强了它们的编码能力。然而，现有的基准主要关注编程的简化或隔离方面，如单文件代码生成或存储库问题调试，无法全面衡量真实世界编程活动引发的各种挑战。为此，我们提出了 DevBench，这是一个全面的基准，评估 LLMs 在软件开发生命周期的各个阶段，包括软件设计、环境设置、实施、验收测试和单元测试。DevBench 涵盖了广泛的编程语言和领域，具备高质量的数据收集，并为每个任务设计和验证了仔细设计的指标。经验证实证研究表明，包括 GPT-4-Turbo 在内的当前 LLMs 未能解决 DevBench 中提出的挑战。分析显示，模型在理解存储库中的复杂结构、管理编译过程和掌握高级编程概念方面存在困难。我们的发现为未来 LLMs 的真实世界编程应用的发展提供了可行的洞察。我们的基准可以在此 https URL 获取。

    Mar, 2024

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

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

    Jun, 2024

  • AssertionBench: 用于评估大语言模型的断言生成基准

    使用大型语言模型（LLMs）生成断言的有效性和适用性的定量评估。

    Jun, 2024

  • DiscoveryBench：基于大型语言模型的数据驱动发现

    快速提取、调用函数和数据分析是大型语言模型 (LLMs) 快速生成代码，从提供的数据集中自动化搜索和验证假设的关键。我们通过 DiscoveryBench 这一全面的基准测试来评估这个问题，该基准测试形式化了数据驱动发现的多步骤过程。该基准测试的设计是为了系统评估当前模型在发现任务中的能力，并为改进这些能力提供有用的资源。

    Jul, 2024

  • BigCodeBench：多样化函数调用和复杂指令的代码生成基准

    基于大型语言模型 (LLMs) 的自动化软件工程在最近的进展中得到了极大的增强。尽管当前的基准测试表明 LLMs 可以完成各种软件工程任务，如人类开发人员一样，但它们的大多数评估仅限于简短的、自包含的算法任务。解决具有挑战性和实际意义的编程任务需要利用多种函数调用作为工具，以有效地实现数据分析和 Web 开发等功能。此外，使用多个工具来解决一个任务需要通过准确理解复杂的指令来进行组合推理。同时实现这两个特征对于 LLMs 来说是一个巨大的挑战。为了评估 LLMs 解决具有挑战性和实际意义的编程任务的能力，我们引入了一个基准测试集 Bench，其中挑战 LLMs 以从 139 个库和 7 个领域中选择 1,140 个细粒度的编程任务中调用多个函数调用作为工具。为了对 LLMs 进行严格评估，每个编程任务包括 5.6 个测试用例，平均分支覆盖率达到 99%。此外，我们提出了 Bench 的自然语言导向变体 Benchi，它将原始的文档字符串自动转换为仅具有基本信息的简短指令。我们对 60 个 LLMs 进行了广泛评估，结果显示 LLMs 还不能准确地遵循复杂指令来使用函数调用，得分最高仅为 60%，明显低于人类的 97%。这些结果强调了在这个领域进一步改进的需要。

    Jun, 2024

  • DeepSeek-Prover: 通过大规模合成数据推进 LLMs 中的定理证明

    基于大规模合成数据，使用 Lean 4 proof 数据生成方法，我们的模型在定理生成和解决题目方面取得了卓越的成果，证明了合成数据对提高 LLMs 中的定理证明能力的潜力。

    May, 2024

  • FormAI 数据集：基于形式验证的软件安全生成式 AI

    FormAI 数据集利用动态零 - shot 提示技术构建，包含 11.2 万个 AI 生成的可以编译和独立运行的 C 程序，按漏洞类型进行了分类，并采用 SMT-based Bounded Model Checker 方法进行了验证，检测出漏洞并提供反例，用于评估各种静态和动态分析工具的效果以及用于训练大型语言模型和机器学习算法。

    Jul, 2023

  • Hints-In-Browser：针对编程反馈生成的语言模型基准测试

    通过在浏览器中进行推理的新范式，基于生成技术的人工智能和大型语言模型能够在编程教育中生成个性化反馈和提示，本文通过基准测试语言模型在编程反馈生成中的质量、成本、时间和数据隐私等多个性能标准，展示了与浏览器推理引擎兼容的小型模型的反馈质量提升，并使用 WebLLM 的浏览器推理引擎在三个不同的 Python 编程数据集上展示了经过精调的 Llama3-8B 和 Phi3-3.8B 4 位量化模型的有效性，同时提供完整的实现、Web 应用和数据集以促进进一步的浏览器语言模型研究。

    Jun, 2024

  • TaskBench: 用于任务自动化的大型语言模型基准测试

    最近，大型语言模型的不断进展引发了任务自动化的火花，其将用户指令描述的复杂任务分解为子任务，并调用外部工具执行它们，在自主代理中起着核心作用。然而，缺乏一个系统的和标准化的基准来促进 LLM 在任务自动化中的发展。为此，我们引入了 TaskBench 来评估 LLM 在任务自动化中的能力。具体而言，任务自动化可以分为三个关键阶段：任务分解，工具调用和参数预测以实现用户意图。这种复杂性使得数据收集和评估与常见的自然语言处理任务相比更具挑战性。为了生成高质量的评估数据集，我们引入了工具图的概念来表示用户意图中的分解任务，并采用反指导方法来模拟用户指令和注释。此外，我们提出了 TaskEval 来从任务分解、工具调用和参数预测等不同方面评估 LLM 的能力。实验结果表明，TaskBench 能够有效地反映 LLM 在任务自动化中的能力。借助自动化数据构建和人工验证的综合，TaskBench 相对于人工评估具有高一致性，可以作为 LLM-based 自主代理的全面而可靠的基准。

    Nov, 2023