本研究由Jialun Cao（香港科技大学）、Yaojie Lu（中国科学院软件研究所）、Meiziniu Li（香港科技大学）、Haoyang Ma（香港科技大学）、Haokun Li（西安电子科技大学广州研究院）、Mengda He（西安电子科技大学广州研究院）、Cheng Wen（西安电子科技大学广州研究院）、Le Sun（中国科学院软件研究所）、Hongyu Zhang（重庆大学）、Shengchao Qin（西安电子科技大学ICT与ISN实验室）、Shing-Chi Cheung（香港科技大学）和Cong Tian（西安电子科技大学ICT与ISN实验室）共同完成，发表于2025年7月27日至8月1日举行的第63届ACL年会论文集（Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics）第一卷。

学术背景

该研究属于人工智能与形式化验证（formal verification）交叉领域。随着AlphaProof在国际数学奥林匹克竞赛（IMO）中获得银牌级表现，以及AlphaGeometry在欧几里得几何定理证明中的突破，基于AI的形式化数学推理（formal mathematical reasoning）研究呈现爆发式增长。然而，现有研究通常将问题解决、数学推理和形式化规范编写（formal specification writing）等多种能力混合评估，难以精确衡量大型语言模型（LLMs）在形式化验证任务中的专项能力。因此，本研究聚焦形式化验证这一形式化推理的直接应用场景，将其分解为子任务进行系统性评估。

研究流程与方法

任务分解与数据集构建

研究团队首先将”从自然语言需求到可验证形式化证明”的过程分解为六个任务：
1. 需求分析（Requirement Analysis, ReqAna）：将自然语言需求分解为详细步骤描述（样本量：627条）
2. 完整证明生成（Full Proof Generation, ProofGen）：将自然语言需求转换为形式化语言证明（样本量：700条）
3. 证明片段生成（Proof Segment Generation, SegGen）：根据详细描述生成形式化证明片段（样本量：14,843条）
4. 证明补全（Proof Completion, ProofComplete）：根据前缀补全形式化证明（样本量：658条）
5. 证明填充（Proof Infilling, ProofInfill）：在掩码位置填充形式化内容（样本量：1,439条）
6. 代码到证明生成（Code to Proof, Code2Proof）：为给定代码生成形式化规范（样本量：70条）

研究团队通过蒸馏GPT-4o构建了18,337个高质量指令-响应对，覆盖5种主流形式化规范语言（Coq、Lean4、Dafny、ACSL、TLA+），并划分为14,372条微调数据集（FM-Alpaca）和3,965条基准测试集（FM-Bench）。数据构建流程包括：
1. 从GitHub开源仓库收集形式化证明及依赖配置
2. 通过自动化验证筛选可验证的证明（过滤率未披露）
3. 使用GPT-4o生成自然语言描述（配备三示例提示和专业领域知识）
4. 任务特异性数据配对（如随机行号删除生成ProofComplete数据）

评估方法创新

研究团队开发了包含以下特征的验证机制：
- 为所有形式化规范提供可执行上下文
- 对独立验证困难的片段使用模板验证法
- 对ACSL规范实施双重验证模式：基础检查（语法/语义）和WP插件验证
- 对自然语言输出采用BLEU评分（Papineni et al., 2002）

实验设计

评估涵盖10个开源LLM（7B-671B参数），包括DeepSeek-R1等最新模型。采用：
- 零样本/少样本（3-shot）评估
- 贪心搜索（温度0.0）和核采样（温度0.2）策略
- 指令微调三基座模型（Llama3.1-8B、Qwen2.5-7B、DeepSeek-Coder-7B）

主要发现

RQ1：基础性能表现

• 任务维度：LLM在ProofComplete（18.31%）和Code2Proof（16.79%）表现最佳，ProofGen（7.70%）和SegGen（9.16%）最弱
  
• 模型维度：DeepSeek-R1-671B平均准确率最高（24.36%），Qwen2.5-Coder-32B次之（19.05%）
  
• 语法错误占失败案例的12.43%，印证形式化语言与常规编程语言的语法差异挑战
  

RQ2：形式化语言差异

• ACSL（34.92%）和Dafny（15.97%）表现最优，因语法接近C/C#
  
• 少样本学习使ACSL准确率提升325.56%，证明上下文学习潜力
  

RQ3：微调效果

• 微调后7B-8B模型性能超越未微调70B+模型
  
• SegGen任务提升最显著（29.98%-90.48%）
  
• Qwen2.5-Coder-7B微调后达27.31%，接近DeepSeek-R1-671B（27.11%）
  

RQ4：能力迁移

• 形式化数据微调提升数学（GSM-8K +1.61%）、推理（BBH +1.10%）和编码（Humaneval +62.53%）能力
  
• 在UltrChat基线上，Humaneval提升62.53%最为显著
  

研究价值

1. 科学价值：首次系统解耦LLM在形式化验证中的多维能力，建立细粒度评估框架
   
2. 工程价值：发布FM-Alpaca数据集、FM-Bench基准和微调模型（HuggingFace仓库fm-universe），降低研究门槛
   
3. 方法论创新：
   
   • 设计可执行环境与自动化验证脚本
     
   • 提出多语言联合微调策略
     
4. 领域启示：验证形式化数据可增强LLM的数学/推理/编码能力，为”领域知识迁移”假说提供实证支持
   

研究亮点

1. 问题分解创新性：通过六任务框架剥离混合能力，揭示LLM在形式化验证中的真实表现
   
2. 数据规模与质量：18K跨语言指令对包含完整验证上下文，是目前最大规模形式化验证基准
   
3. 发现颠覆性：
   
   • 7B微调模型可逼近671B基础模型性能
     
   • 形式化训练产生跨域能力迁移
     
4. 工具生态贡献：提供Docker容器简化验证环境部署
   

局限与未来方向

1. 数据依赖模型生成可能引入偏差，建议补充人工标注数据
   
2. 掩码任务中可能遗漏关键属性验证，需改进评估设计
   
3. 未来可探索：
   
   • 更多形式化语言支持
     
   • 结合符号推理的混合方法
     
   • 面向工业级验证场景的优化
     

该研究为AI辅助形式化验证建立了新的方法论基准，其发布的资源将持续推动该领域发展，实现Terence Tao预言的”未来数学家将向GPT解释证明”的愿景。