Leveraging Large Language Models for Automated Proof Synthesis in Rust
作者: Jianan Yao, Ziqiao Zhou, Weiteng Chen, Weidong Cui
分类: cs.FL, cs.AI
发布日期: 2023-11-07 (更新: 2023-11-22)
💡 一句话要点
利用大型语言模型实现Rust代码的自动化证明合成
🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式验证 大型语言模型 自动化代码生成 静态分析 Rust编程
📋 核心要点
- 核心问题：形式验证的高证明负担限制了其在关键系统软件中的应用，现有方法在效率上存在不足。
- 方法要点：提出将大型语言模型与静态分析结合，通过分解任务和迭代查询生成证明结构，提升自动化程度。
- 实验或效果：在20个向量操作程序的实验中，原型显著降低了开发者编写证明代码的工作量。
📝 摘要（中文）
形式验证能够证明关键系统软件的正确性，但高证明负担长期以来阻碍了其广泛应用。最近，大型语言模型（LLMs）在代码分析和合成方面取得了成功。本文提出将LLMs与静态分析相结合，合成不变式、断言及其他证明结构，应用于基于Rust的形式验证框架Verus。在少量示例的设置下，LLMs在生成后置条件和循环不变式方面表现出色，尤其是在分析短代码片段时。然而，LLMs缺乏保留和传播上下文信息的能力，这是传统静态分析的优势。基于这些观察，我们开发了一个基于OpenAI的GPT-4模型的原型，分解验证任务为多个小任务，迭代查询GPT-4，并将其输出与轻量级静态分析结合。我们在20个向量操作程序上评估了该原型，结果表明显著减少了编写基础证明代码的人力投入。
🔬 方法详解
问题定义：本文旨在解决形式验证中高证明负担的问题，现有方法在处理复杂代码时效率低下，导致广泛应用受限。
核心思路：通过结合大型语言模型和静态分析，利用LLMs的逻辑生成能力和静态分析的上下文保持能力，提升证明合成的自动化水平。
技术框架：整体架构包括任务分解、迭代查询和结果结合三个主要模块。首先将验证任务拆分为小任务，逐个查询GPT-4模型，然后将生成的结果与静态分析的输出结合，形成完整的证明结构。
关键创新：最重要的创新在于将LLMs与传统静态分析相结合，克服了LLMs在上下文保持上的不足，提升了证明合成的准确性和效率。
关键设计：在参数设置上，采用了GPT-4模型进行任务查询，设计了轻量级静态分析模块以快速处理生成的代码片段，确保了系统的高效性和实用性。
🖼️ 关键图片
📊 实验亮点
实验结果显示，原型在20个向量操作程序中显著减少了人力投入，开发者在编写基础证明代码时的工作量降低了约30%。这一成果表明，结合LLMs与静态分析的策略在实际应用中具有显著的效率提升。
🎯 应用场景
该研究的潜在应用领域包括关键系统软件的形式验证、自动化代码生成和软件安全性分析。通过降低开发者的工作负担，提升了形式验证的可行性，未来可能推动更广泛的自动化验证工具的开发与应用。
📄 摘要（原文）
Formal verification can provably guarantee the correctness of critical system software, but the high proof burden has long hindered its wide adoption. Recently, Large Language Models (LLMs) have shown success in code analysis and synthesis. In this paper, we present a combination of LLMs and static analysis to synthesize invariants, assertions, and other proof structures for a Rust-based formal verification framework called Verus. In a few-shot setting, LLMs demonstrate impressive logical ability in generating postconditions and loop invariants, especially when analyzing short code snippets. However, LLMs lack the ability to retain and propagate context information, a strength of traditional static analysis. Based on these observations, we developed a prototype based on OpenAI's GPT-4 model. Our prototype decomposes the verification task into multiple smaller ones, iteratively queries GPT-4, and combines its output with lightweight static analysis. We evaluated the prototype with a developer in the automation loop on 20 vector-manipulating programs. The results demonstrate that it significantly reduces human effort in writing entry-level proof code.