DafnyBench: 形式软件验证基准
原文中文，约400字，阅读约需1分钟。发表于：。我们介绍了 DafnyBench，这是一个用于训练和评估形式软件验证的机器学习系统的最大基准测试。我们测试了 LLM（如 GPT-4 和 Claude 3）生成足够的提示来让 Dafny 形式验证引擎成功验证 750 多个程序，代码行数约为 53,000 行。最佳模型和提示方案的成功率达到 68%，我们量化了通过错误信息反馈重试时成功率的提高，以及所需代码和提示数量的恶化。我们希望...
最近的大型语言模型 (LLMs) 的进展显著增强了编码能力，但现有基准无法全面衡量真实世界编程活动的挑战。我们提出了 DevBench，一个全面的基准，评估 LLMs 在软件开发生命周期的各个阶段。验证研究表明，包括 GPT-4-Turbo 在内的当前 LLMs 未能解决 DevBench 中的挑战。我们的发现为未来 LLMs 的真实世界编程应用提供了洞察。
