JetBrains推出基于大语言模型生成证明的插件CoqPilot

共计 1538 个字符，预计需要花费 4 分钟才能阅读完成。

近年来，形式化软件验证在确保软件可靠性方面的重要性日益增加，特别是在航空航天工程、金融和医疗保健等关键领域。Coq 作为一种流行的证明助手，通过使开发者能够创建数学证明来验证其代码，已经成为确保软件正确性的关键工具。

• GitHub：https://github.com/JetBrains-Research/coqpilot

然而，编写这些形式化证明是一项劳动密集型且耗时的任务，需要相当的专业知识。为了解决这一挑战，JetBrains 研究人员推出了 CoqPilot——一个 VS Code 扩展，用于自动化生成 Coq 证明。

CoqPilot 的主要特点

1. 自动化生成证明：
   • 收集证明洞 ：CoqPilot 收集在 Coq 文件中标记为admit 策略的不完整证明片段，称为证明洞。
   • 生成解决方案：使用大型语言模型（LLMs）和传统方法生成可能的解决方案。
   • 验证和替换：验证生成的证明是否正确，并在成功时自动替换证明洞。
2. 模块化架构：
   • 集成多种生成方法：CoqPilot 集成了流行的 LLMs（如 GPT- 4 和 GPT-3.5）以及自动化工具（如 CoqHammer 和 Tactician），允许用户结合多种方法。
   • 适应性强：其模块化特性使其易于适应新模型或甚至 Coq 以外的不同语言。
3. 用户友好的界面：
   • 自动解决证明洞：CoqPilot 允许自动解决证明洞，并在必要时利用多轮错误处理和重试来提高生成证明的正确性。
   • 设置简单：CoqPilot 的设置要求最低，使对形式验证感兴趣的用户无需进行广泛的工具配置即可访问。

技术细节

1. 证明生成方法：
   • LLMs：CoqPilot 集成了 GPT-4、GPT-3.5、Anthropic Claude 和 LLaMA- 2 等 LLMs，这些模型在生成 Coq 证明方面表现出色。
   • 自动化工具：CoqPilot 还集成了 CoqHammer 和 Tactician 等自动化工具，这些工具在特定任务中表现出色。
2. 验证和完成服务：
   • 模型参数：CoqPilot 提供了使用不同模型参数（包括提示结构和 LLMs 的温度设置）进行证明验证和完成的服务。
   • 多轮处理：在必要时，CoqPilot 会进行多轮错误处理和重试，以提高生成证明的正确性。

性能评估

JetBrains 研究人员对 CoqPilot 进行了广泛的评估，试验了几种 LLMs，包括 GPT-4、GPT-3.5、Anthropic Claude 和 LLaMA-2，比较了它们在生成 Coq 证明方面的性能。结果如下：

• GPT-4：成功生成了 34% 的证明。
• 多种模型：使用多种模型的集体努力在其数据集中证明了 39% 的定理。
• 集成工具：当与 Tactician 和 CoqHammer 等工具集成时，总体成功率为 51%。

这些结果展示了 CoqPilot 在简化证明编写过程方面的潜力，使开发者能够专注于更高层次的问题，而插件处理更多重复的任务。

意义和影响

1. 提高效率：CoqPilot 显著提高了 Coq 用户的证明生成效率，减少了形式验证所需的时间和精力。
2. 提高质量：通过自动化生成和验证证明，CoqPilot 提高了证明的质量，减少了人为错误。
3. 易用性：CoqPilot 的用户友好界面和简单的设置要求使其成为初学者和经验丰富的开发者都能使用的工具。
4. 模块化和适应性：其模块化架构和对多种工具的支持使其能够适应不断发展的技术和方法。

CoqPilot 代表了 Coq 用户自动化证明生成过程的重大进步。通过利用 LLMs 并集成各种证明生成工具，CoqPilot 不仅减少了形式验证所需的时间和精力，还提高了证明的质量。其模块化架构和对一系列工具的支持使其成为希望自动化形式验证过程的开发者和研究人员的绝佳选择。凭借其与各种模型和工具无缝工作的能力，CoqPilot 为生成形式化证明相关的挑战提供了强大的解决方案，使其成为在软件可靠性和形式验证领域工作的宝贵工具。