AI·新世界

近年来，形式化软件验证在确保软件可靠性方面的重要性日益增加，特别是在航空航天工程、金融和医疗保健等关键领域。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为生成形式化证明相关的挑战提供了强大的解决方案，使其成为在软件可靠性和形式验证领域工作的宝贵工具。