Automated Repair of AI Code with Large Language Models and Formal Verification

📄 arXiv: 2405.08848v1 📥 PDF

作者: Yiannis Charalambous, Edoardo Manino, Lucas C. Cordeiro

分类: cs.SE, cs.AI

发布日期: 2024-05-14

💡 一句话要点

利用大语言模型和形式化验证自动修复AI代码中的内存安全漏洞

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: AI代码修复 大语言模型 形式化验证 内存安全 神经网络 程序变异 ESBMC

📋 核心要点

  1. 现有AI系统，特别是神经网络的软件实现，面临着内存安全漏洞的挑战，如空指针解引用和内存泄漏。
  2. 该论文提出一种结合形式化验证（ESBMC）和大语言模型的方法，自动检测并修复神经网络代码中的内存安全问题。
  3. 通过程序变异扩展数据集，并结合提示工程和迭代调用大语言模型，验证了该方法在修复内存安全漏洞方面的有效性。

📝 摘要（中文）

下一代人工智能系统需要强大的安全保障。本报告关注神经网络软件实现中的内存安全属性，包括空指针解引用、越界访问、双重释放和内存泄漏。我们的目标是检测这些漏洞，并在大型语言模型的帮助下自动修复它们。为此，我们首先通过自动程序变异过程将现有的神经网络代码数据集NeuroCodeBench扩展到大约81k个程序。然后，我们使用最先进的软件验证器ESBMC验证变异后的神经网络实现的内存安全性。每当ESBMC发现漏洞时，我们都会调用大型语言模型来修复源代码。对于后一个任务，我们比较了各种最先进的提示工程技术的性能，以及一种重复调用大型语言模型的迭代方法。

🔬 方法详解

问题定义：论文旨在解决神经网络代码中常见的内存安全漏洞，例如空指针解引用、越界访问、双重释放和内存泄漏。现有方法通常依赖人工审计或不完备的测试，效率低下且难以保证覆盖率。这些漏洞可能导致程序崩溃、数据损坏甚至安全风险，严重影响AI系统的可靠性和安全性。

核心思路：论文的核心思路是结合形式化验证和大语言模型，实现AI代码的自动修复。形式化验证（ESBMC）用于精确检测内存安全漏洞，大语言模型则根据漏洞信息生成修复代码。这种结合既保证了漏洞检测的准确性，又利用了大语言模型的代码生成能力，提高了修复效率。

技术框架：整体框架包含以下几个主要阶段：1) 数据集扩展：通过程序变异技术，自动生成大量的神经网络代码样本，扩充NeuroCodeBench数据集。2) 漏洞检测：使用ESBMC对变异后的代码进行形式化验证，检测内存安全漏洞。3) 代码修复：当ESBMC检测到漏洞时，将漏洞信息作为提示输入给大语言模型，生成修复后的代码。4) 迭代优化：采用迭代的方式，多次调用大语言模型，逐步优化修复效果。

关键创新：该论文的关键创新在于将形式化验证和大语言模型相结合，实现AI代码的自动修复。与传统方法相比，该方法能够更准确地检测漏洞，并利用大语言模型的代码生成能力自动修复漏洞，大大提高了修复效率和可靠性。此外，论文还探索了不同的提示工程技术和迭代优化策略，进一步提升了修复效果。

关键设计：在提示工程方面，论文比较了不同的提示策略，例如提供漏洞描述、代码上下文等信息。在迭代优化方面，论文设计了一种迭代调用大语言模型的机制，每次调用都基于上次的修复结果进行改进。具体的大语言模型选择和参数设置（例如温度系数）在论文中可能有所提及，但此处信息未知。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

论文通过实验验证了该方法在修复神经网络代码中的内存安全漏洞方面的有效性。具体性能数据和对比基线未知，但论文强调了不同提示工程技术和迭代优化方法对修复效果的影响。实验结果表明，结合形式化验证和大语言模型能够显著提高AI代码的安全性。

🎯 应用场景

该研究成果可应用于提高AI系统的可靠性和安全性，特别是在安全攸关的应用领域，如自动驾驶、医疗诊断等。通过自动检测和修复内存安全漏洞，可以有效降低AI系统发生故障的风险，提高系统的稳定性和可信度。此外，该方法还可以应用于AI代码的质量保证和代码审查，帮助开发者编写更安全可靠的AI代码。

📄 摘要（原文）

The next generation of AI systems requires strong safety guarantees. This report looks at the software implementation of neural networks and related memory safety properties, including NULL pointer deference, out-of-bound access, double-free, and memory leaks. Our goal is to detect these vulnerabilities, and automatically repair them with the help of large language models. To this end, we first expand the size of NeuroCodeBench, an existing dataset of neural network code, to about 81k programs via an automated process of program mutation. Then, we verify the memory safety of the mutated neural network implementations with ESBMC, a state-of-the-art software verifier. Whenever ESBMC spots a vulnerability, we invoke a large language model to repair the source code. For the latest task, we compare the performance of various state-of-the-art prompt engineering techniques, and an iterative approach that repeatedly calls the large language model.