Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
作者: Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First
分类: cs.LO, cs.AI, cs.PL
发布日期: 2024-10-25 (更新: 2025-08-04)
备注: 14 pages, 14 figures
💡 一句话要点
Cobblestone：一种用于自动化形式化验证的分治方法
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式化验证 自动化证明 大型语言模型 分治算法 Coq 软件可靠性 定理证明 程序验证
📋 核心要点
- 形式化验证依赖专家知识且耗时，机器学习方法虽能自动生成证明，但覆盖率有限，难以证明复杂软件属性。
- Cobblestone采用分治策略，利用LLM生成潜在证明，将问题分解为更简单的子问题，并迭代求解。
- 实验表明，Cobblestone在多个Coq项目基准测试中优于现有非LLM和LLM工具，且成本较低，并能有效利用外部输入。
📝 摘要（中文）
使用Coq等证明辅助工具进行形式化验证是提高软件质量的有效方法，但需要大量的努力和专业知识。机器学习可以自动合成证明，但此类工具只能证明所需软件属性的一小部分。我们介绍了Cobblestone，一种用于证明合成的分治方法。Cobblestone使用大型语言模型（LLM）生成潜在的证明，使用这些证明将问题分解为更简单的部分，自动识别哪些部分已成功证明，并迭代剩余部分以构建正确的证明，保证其可靠性，尽管依赖于不可靠的LLM。我们在四个开源Coq项目的基准上评估了Cobblestone，控制了训练数据泄漏。完全自动地，Cobblestone优于最先进的非LLM工具，并证明了许多其他基于LLM的工具无法证明的定理，并且在许多基准上优于它们。平均而言，每次Cobblestone运行仅花费1.25美元，耗时14.7分钟。Cobblestone还可以与来自用户或其他工具的外部输入一起使用，提供证明结构或相关引理。在这样的预言机评估中，Cobblestone证明了高达58%的定理。总的来说，我们的研究表明，工具可以利用部分进展和外部输入来更有效地自动化形式化验证。
🔬 方法详解
问题定义：论文旨在解决形式化验证自动化程度低的问题。现有方法，特别是基于机器学习的方法，在证明复杂软件属性时能力不足，需要大量人工干预和专业知识。现有方法的痛点在于难以生成完整、正确的证明，且对训练数据依赖性强。
核心思路：Cobblestone的核心思路是“分而治之”。它利用大型语言模型（LLM）生成潜在的证明，然后将原始验证问题分解为多个更小的、更易于验证的子问题。通过迭代地解决这些子问题，并结合已验证的部分，最终构建出完整的证明。这种方法旨在利用LLM的生成能力，同时通过分解问题降低验证难度。
技术框架：Cobblestone的整体框架包含以下几个主要阶段：1) LLM证明生成：使用LLM生成初始的潜在证明。2) 问题分解：基于LLM生成的证明，将原始问题分解为多个子问题。3) 子问题验证：自动识别并验证已成功证明的子问题。4) 迭代求解：对剩余未解决的子问题重复上述过程，直到所有子问题都被解决或达到最大迭代次数。5) 证明组装：将已验证的子问题组合成完整的证明。
关键创新：Cobblestone的关键创新在于将LLM的生成能力与分治策略相结合，实现了一种更有效的自动化形式化验证方法。与现有方法相比，Cobblestone能够处理更复杂的验证问题，并且对训练数据的依赖性较低。此外，Cobblestone还能够利用外部输入（例如，用户提供的证明结构或相关引理）来进一步提高验证效率。
关键设计：Cobblestone的关键设计包括：1) 使用预训练的LLM作为证明生成器，并针对形式化验证任务进行微调。2) 设计了一种有效的子问题分解策略，确保子问题之间的独立性和可验证性。3) 实现了一种自动化的子问题验证机制，利用现有的定理证明器或模型检查器来验证子问题的正确性。4) 采用迭代求解策略，逐步构建完整的证明，并避免陷入局部最优解。
🖼️ 关键图片
📊 实验亮点
Cobblestone在四个开源Coq项目基准测试中表现出色，显著优于现有非LLM和LLM工具。实验结果表明，Cobblestone能够自动证明许多其他LLM工具无法证明的定理。在许多基准测试中，Cobblestone的性能也优于其他LLM工具。此外，Cobblestone的运行成本较低，平均每次运行仅需1.25美元，耗时14.7分钟。当与外部预言机结合使用时，Cobblestone能够证明高达58%的定理。
🎯 应用场景
Cobblestone具有广泛的应用前景，可用于提高软件的可靠性和安全性。它可以应用于各种软件开发领域，例如操作系统、嵌入式系统、网络协议和智能合约。通过自动化形式化验证过程，Cobblestone可以帮助开发人员更早地发现和修复软件缺陷，从而降低开发成本并提高软件质量。此外，Cobblestone还可以用于验证现有软件的正确性，并为关键系统提供额外的安全保障。
📄 摘要（原文）
Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can automatically synthesize proofs, but such tools are able to prove only a fraction of desired software properties. We introduce Cobblestone, a divide-and-conquer approach for proof synthesis. Cobblestone uses a large language model (LLM) to generate potential proofs, uses those proofs to break the problem into simpler parts, automatically identifies which of those parts were successfully proven, and iterates on the remaining parts to build a correct proof that is guaranteed to be sound, despite the reliance on unsound LLMs. We evaluate Cobblestone on four benchmarks of open-source Coq projects, controlling for training data leakage. Fully automatically, Cobblestone outperforms state-of-the-art non-LLM tools, and proves many theorems that other LLM-based tools cannot, and on many benchmarks, outperforms them. Each Cobblestone run costs only $1.25 and takes 14.7 minutes, on average. Cobblestone can also be used with external input, from a user or another tool, providing a proof structure or relevant lemmas. Evaluated with such an oracle, Cobblestone proves up to 58% of theorems. Overall, our research shows that tools can make use of partial progress and external input to more effectively automate formal verification.