From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs

📄 arXiv: 2501.16207v4 📥 PDF

作者: Jialun Cao, Yaojie Lu, Meiziniu Li, Haoyang Ma, Haokun Li, Mengda He, Cheng Wen, Le Sun, Hongyu Zhang, Shengchao Qin, Shing-Chi Cheung, Cong Tian

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

发布日期: 2025-01-27 (更新: 2025-06-08)

备注: 20 pages

💡 一句话要点

利用LLM将自然语言需求转化为可验证的形式化证明，并进行评估

🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction)

关键词: 形式化验证 大型语言模型 指令微调 自然语言处理 形式化规约语言

📋 核心要点

  1. 现有方法在将自然语言需求转化为形式化证明方面存在不足，缺乏高质量的数据集和有效的模型。
  2. 论文核心思想是利用大型语言模型（LLM）的强大能力，通过指令微调，学习从自然语言到形式化语言的转换。
  3. 实验结果表明，微调后的7-8B小模型能够达到与大型模型Deepseek-R1-671B相当的性能，并且提升了数学、推理和编码能力。

📝 摘要（中文）

本文研究了基于AI的形式化数学推理，该领域已展现出不可阻挡的增长趋势，并在IMO等数学竞赛中表现出色。本文聚焦于形式化验证，这是形式化推理的一个直接应用场景，并将其分解为子任务。通过提炼GPT-4o，构建了包含五种形式化规约语言（Coq、Lean4、Dafny、ACSL和TLA+）的1.8万个高质量指令-响应对，并针对十个开源LLM（包括最近流行的DeepSeek-R1）进行了评估。同时，微调了几个7~8B的小模型，使其达到与Deepseek-R1-671B相当的性能。有趣的是，观察到使用形式化数据进行微调也能增强数学、推理和编码能力。微调后的模型已在https://huggingface.co/fm-universe上发布。

🔬 方法详解

问题定义：现有方法在形式化验证领域，特别是将自然语言需求转化为可验证的形式化证明方面，面临着缺乏高质量数据集和有效模型的问题。现有的方法难以充分利用大型语言模型的能力，并且在不同形式化规约语言之间的泛化能力有限。

核心思路：论文的核心思路是利用大型语言模型（LLM）的指令遵循能力，通过构建高质量的指令-响应对数据集，并对LLM进行微调，使其能够学习从自然语言需求到形式化证明的转换。这种方法旨在弥合自然语言和形式化语言之间的差距，提高形式化验证的效率和准确性。

技术框架：整体框架包括数据构建和模型微调两个主要阶段。数据构建阶段，利用GPT-4o生成包含五种形式化规约语言（Coq、Lean4、Dafny、ACSL和TLA+）的1.8万个高质量指令-响应对。模型微调阶段，选择多个7~8B的小模型，使用构建的数据集进行指令微调。

关键创新：关键创新在于构建了一个高质量、多语言的形式化验证数据集，并证明了通过指令微调，小模型也能达到与大型模型相当的性能。此外，论文还观察到使用形式化数据进行微调能够增强模型的数学、推理和编码能力，这为LLM在形式化验证领域的应用提供了新的思路。

关键设计：数据集构建的关键在于指令的设计，需要清晰明确地描述自然语言需求，并提供相应的形式化证明。模型微调的关键在于选择合适的损失函数和优化器，以及调整学习率等超参数。论文未明确说明具体的损失函数和优化器选择，但强调了微调数据的重要性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，通过在高质量形式化验证数据集上进行微调，7-8B的小模型可以达到与671B的DeepSeek-R1相当的性能。此外，微调后的模型在数学、推理和编码能力方面也得到了提升，证明了形式化数据对LLM能力提升的积极作用。

🎯 应用场景

该研究成果可应用于软件工程、硬件验证、智能合约安全等领域，通过自动化形式化验证过程，提高软件和硬件系统的可靠性和安全性。未来，该技术有望应用于更复杂的系统验证，并促进形式化方法的普及。

📄 摘要（原文）

The research in AI-based formal mathematical reasoning has shown an unstoppable growth trend. These studies have excelled in mathematical competitions like IMO and have made significant progress. This paper focuses on formal verification, an immediate application scenario of formal reasoning, and breaks it down into sub-tasks. We constructed 18k high-quality instruction-response pairs across five formal specification languages (Coq, Lean4, Dafny, ACSL, and TLA+) by distilling gpt-4o and evaluated against ten open-sourced LLMs, including recent popular DeepSeek-R1. We also fine-tuned several 7~8B small models to achieve comparable performance with Deepseek-R1-671B. Interestingly, we observed that fine-tuning with formal data also enhances mathematics, reasoning, and coding capabilities. Fine-tuned models are released at https: //huggingface.co/fm-universe.