大语言模型 和语言服务器协议：上下文中的匹配

本文介绍 Eiffel-tools，它是 Eiffel 编程语言的语言服务器协议 (LSP) 实现，它使用 大语言模型 (LLM) 来帮助开发静态验证的软件。该工具提供各种交互式和非交互式命令来生成代码和规范。它使用语言和项目特定知识来精确指导 LLM 并使用静态验证器验证输出。它为输入制作丰富的程序化提示，并纠正或拒绝输出。此外，它还会处理重试，直到程序通过验证。该工具的错误修复能力是使用 3 个模型在 2 个公共数据集上进行评估的。通过结合 LLM 和形式验证器，该工具可以修复 76% 到 95% 的错误，具体取决于所使用的模型和提示。结果显示了修复尝试次数和成功率之间的权衡。