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

📄 arXiv: 2406.14408v2 📥 PDF

作者: Xiaohan Lin, Qingxing Cao, Yinya Huang, Haiming Wang, Jianqiao Lu, Zhengying Liu, Linqi Song, Xiaodan Liang

分类: cs.AI, cs.CL, cs.LG

发布日期: 2024-06-20 (更新: 2024-06-21)

🔗 代码/项目: PROJECT_PAGE

💡 一句话要点

提出FVEL以解决形式验证中的灵活性与效率问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式验证 大型语言模型 自动定理证明 Isabelle 神经网络 软件验证 程序合成

📋 核心要点

  1. 现有形式验证方法主要依赖符号验证器和手工规则，缺乏灵活性和广泛适用性。
  2. FVEL通过将代码转换为Isabelle格式，结合LLMs进行神经自动定理证明，提升验证效率。
  3. 实验结果显示，FVEL在SV-COMP中显著提高了问题解决率，并减少了证明错误的比例。

📝 摘要（中文）

形式验证（FV）在当前程序合成中愈发重要，但现有方法主要依赖符号验证器或手工规则，导致验证的灵活性和广泛性受限。本文提出FVEL，一个结合大型语言模型（LLMs）的交互式形式验证环境。FVEL将待验证代码转换为Isabelle格式，并通过神经自动定理证明进行验证。为此，研究团队构建了大规模的FVELER数据集，包含758个理论、29,125个引理和200,646个证明步骤。实验结果表明，经过FVELER微调的Llama3-8B在SV-COMP中解决了17.39%的更多问题，Mistral-7B则提高了12%。

🔬 方法详解

问题定义：本文旨在解决现有形式验证方法在灵活性和效率上的不足，特别是依赖符号验证器和手工规则的局限性。

核心思路：FVEL通过将待验证代码转换为Isabelle格式，利用大型语言模型进行神经自动定理证明，从而实现高效且灵活的形式验证。这样的设计使得可以充分利用Isabelle中丰富的规则和定理，同时便于引入最新的LLMs。

技术框架：FVEL的整体架构包括三个主要模块：首先是代码转换模块，将待验证代码转换为Isabelle格式；其次是神经自动定理证明模块，利用LLMs进行验证；最后是结果评估模块，分析验证结果和性能表现。

关键创新：FVEL的主要创新在于将大型语言模型与形式验证相结合，通过神经自动定理证明提升验证的灵活性和效率，这是与传统方法的本质区别。

关键设计：在FVELER数据集中，包含758个理论、29,125个引理和200,646个证明步骤，确保了验证过程中的深度依赖关系。微调过程中，使用特定的损失函数和参数设置，以优化LLMs在验证任务中的表现。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果显示，经过FVELER微调的Llama3-8B在SV-COMP中解决了17.39%（从69个问题提升至81个问题）更多的问题，而Mistral-7B则提高了12%（从75个问题提升至84个问题）。此外，证明错误的比例也显著降低，表明FVEL在形式验证中的有效性和可靠性。

🎯 应用场景

该研究的潜在应用领域包括软件验证、智能合约安全性分析以及自动化程序合成等。通过提升形式验证的灵活性和效率，FVEL有望在确保软件质量和安全性方面发挥重要作用，推动相关领域的技术进步。未来，FVEL可能会与其他AI技术结合，进一步拓展其应用范围。

📄 摘要（原文）

Formal verification (FV) has witnessed growing significance with current emerging program synthesis by the evolving large language models (LLMs). However, current formal verification mainly resorts to symbolic verifiers or hand-craft rules, resulting in limitations for extensive and flexible verification. On the other hand, formal languages for automated theorem proving, such as Isabelle, as another line of rigorous verification, are maintained with comprehensive rules and theorems. In this paper, we propose FVEL, an interactive Formal Verification Environment with LLMs. Specifically, FVEL transforms a given code to be verified into Isabelle, and then conducts verification via neural automated theorem proving with an LLM. The joined paradigm leverages the rigorous yet abundant formulated and organized rules in Isabelle and is also convenient for introducing and adjusting cutting-edge LLMs. To achieve this goal, we extract a large-scale FVELER3. The FVELER dataset includes code dependencies and verification processes that are formulated in Isabelle, containing 758 theories, 29,125 lemmas, and 200,646 proof steps in total with in-depth dependencies. We benchmark FVELER in the FVEL environment by first fine-tuning LLMs with FVELER and then evaluating them on Code2Inv and SV-COMP. The results show that FVEL with FVELER fine-tuned Llama3- 8B solves 17.39% (69 -> 81) more problems, and Mistral-7B 12% (75 -> 84) more problems in SV-COMP. And the proportion of proof errors is reduced. Project page: https://fveler.github.io/.