这篇文档属于类型a，是一篇关于原创研究的学术论文。以下是针对该研究的详细学术报告：

作者及机构
本研究的核心作者团队包括Xiaohan Lin（中山大学深圳校区）、Qingxing Cao（中山大学深圳校区）、Yinya Huang（香港城市大学）、Haiming Wang（中山大学）、Jianqiao Lu（香港大学）、Zhengying Liu（华为诺亚方舟实验室）、Linqi Song（香港城市大学）及Xiaodan Liang（中山大学深圳校区/DarkMatter AI Research）。论文发表于第38届NeurIPS 2024会议的Datasets and Benchmarks专题。

学术背景
研究领域为形式化验证（Formal Verification, FV）与大型语言模型（LLMs）的结合。随着LLMs在代码生成领域的快速发展，传统形式化验证方法（如符号验证器或手工规则）面临灵活性和扩展性不足的问题。同时，自动化定理证明（Automated Theorem Proving, ATP）系统（如Isabelle）虽具备严格的逻辑框架，但尚未充分与LLMs的推理能力结合。本研究旨在提出一种交互式形式化验证环境FVEl，通过将代码验证问题转化为Isabelle中的定理证明任务，利用LLMs的推理能力提升验证效率。

研究流程与方法
1. 环境设计（FVEl）
- 输入处理：将待验证的C代码通过C-parser和AutoCorres工具转换为Isabelle中的函数定义，生成中间表示Simpl。
- 交互机制：LLMs接收Isabelle定义后生成规范描述（Lemma），并通过PISA环境与Isabelle证明器交互。LLMs逐步生成证明步骤，Isabelle反馈验证状态（如错误信息），直至完成证明或超时。
- 输出：验证结果以“成功/失败”标志输出，并附带中间证明状态。

1. 数据集构建（FVElEr）

   • 数据来源：基于seL4微内核的形式化验证项目，提取Isabelle理论文件（.thy）、引理及证明步骤。
     
   • 依赖关系提取：构建理论依赖图，记录理论文件间的多跳引用关系，最深依赖路径达156层。
     
   • 数据规模：包含758个理论文件、29,304条引理及201,498个证明步骤，按引理随机划分为训练/验证/测试/测试-困难集。
     

2. 实验验证

   • 基准测试：在Code2Inv（133个C程序）和SV-Comp（1,000个C程序）数据集上评估。
     
   • 模型调优：使用LoRA方法微调Mistral-7B和Llama3-8B模型，输入为Isabelle引理，输出为完整证明。
     
   • 对比方法：包括符号求解器（UAutomizer、ESBMC）和LLM-based方法（Lemur）。
     

主要结果
1. 性能提升
- Llama3-8B在SV-Comp上验证通过率从69提升至81（+17.39%），Mistral-7B从75提升至84（+12%）。
- Code2Inv任务中，微调后的模型验证通过率与Lemur-GPT-4（107）接近，但优于符号求解器（ESBMC仅68）。

1. 错误分析

   • Code2Inv的错误主要来自规范生成（70.8%），而SV-Comp中证明错误占比更高（50.3%）。微调后，证明错误比例显著下降（如Llama3-8B从47%降至38.2%）。
     

2. 泛化性验证

   • 在Python代码翻译任务中（93个样本），GPT-4生成的C99代码解析成功率达84%，微调后模型验证通过数进一步提升（如Mistral-7B从35增至42）。
     

结论与价值
1. 科学价值
- 提出首个将LLMs与Isabelle ATP深度结合的交互式验证框架，弥补了传统符号验证与手工规则的局限性。
- 构建的大规模依赖数据集FVElEr为后续研究提供了基准资源。

1. 应用价值
   
   • 可扩展至工业级代码验证场景（如操作系统内核），提升自动化验证效率。
     
   • 为LLMs在形式化数学领域的应用提供了新范式。
     

研究亮点
1. 方法创新：通过ATP框架将代码验证转化为定理证明问题，利用LLMs的动态推理能力。
2. 数据深度：FVElEr包含深度依赖的引理网络（50%引理依赖深度>78），支持复杂验证任务。
3. 性能突破：微调后的轻量级模型（如Llama3-8B）在标准测试中超越符号求解器。

其他发现
- 研究揭示了LLMs在规范生成（Lemma Specification）上的瓶颈，为未来改进方向提供了依据。
- 开源了数据集与工具链（项目页面：https://fveler.github.io/），推动领域协作。

（注：以上报告严格遵循学术规范，术语首次出现时标注英文原文，如“形式化验证（Formal Verification, FV）”。）