FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving

正式验证（FV）在当前新兴的大型语言模型（LLMs）演进的程序合成中变得越来越重要。然而，当前的正式验证主要依赖于符号验证器或手工制定规则，导致验证的广泛性和灵活性受到限制。另一方面，用于自动定理证明的形式语言（如Isabelle）作为另一种严格验证的方法，是通过全面的规则和定理来维护的。在本文中，我们提出了一个名为FVEL的交互式正式验证环境，其中包含LLMs。具体而言，FVEL将待验证的给定代码转换为Isabelle，然后通过LLMs进行神经自动定理证明来进行验证。这种联合范式利用了Isabelle中严谨而丰富的规则和组织方式，也方便引入和调整尖端的LLMs。为了实现这个目标，我们提取了一个大规模的FVELER3。FVELER数据集包括在Isabelle中制定的代码依赖关系和验证过程，总共包含758个理论、29,125个引理和200,646个证明步骤，具有深入的依赖关系。我们在FVEL环境中对FVELER进行基准测试，首先使用FVELER微调LLMs，然后在Code2Inv和SV-COMP上对它们进行评估。结果显示，使用FVELER微调的Llama3-8B在SV-COMP中解决了17.39%（69-> 81）更多的问题，Mistral-7B解决了12%（75-> 84）更多的问题，并且证明错误的比例降低了。项目页面：https://fveler.github.io/。

论文提出了FVEL，一种基于大型语言模型（LLMs）的交互式形式验证环境，旨在解决当前形式验证的限制和不足。

FVEL将待验证的代码转换为Isabelle，并通过神经自动定理证明与LLMs进行验证，利用Isabelle中丰富的规则和定理。

论文提出了FVELER数据集，包含了758个理论、29,125个引理和200,646个证明步骤，用于评估FVEL。实验中使用了Code2Inv和SV-COMP数据集，证明了FVEL可以有效地解决更多的问题并减少证明错误。项目页面提供了开源代码。

相关研究包括当前形式验证的符号验证器和手工规则，以及Isabelle等自动定理证明的形式语言。