UMass Amherst的Baldur方法能够自动生成用于验证代码、防范漏洞的证明。
译自 Debugging Software Using Generative AI，作者 Jeffrey Burt 是一位资深记者，拥有三十多年的新闻工作经验，过去二十多年专注于科技领域。在过去的16年多里，他曾在eWEEK工作，并在之后成为一名自由科技记者。
自从OpenAI于2022年11月底推出其ChatGPT聊天机器人以来，生成式人工智能工具和大型语言模型（LLM）的采用只有加速，深入渗透到各种形状、大小和行业的组织中，而软件开发人员并未对其产生免疫。
生成式人工智能的用例，如内容创作、对话式人工智能和语言翻译，在软件开发中是多样化且不断增长的，涉及代码优化和生成、错误修复、文档编写以及持续集成等方面。
据卡内基梅隆大学SEI博客中的AI专家在2023年10月的一篇文章称，开发人员越来越认为生成式人工智能是一个有用的工具。
作者写道：“关于使用LLM进行软件开发的最初炒作已经开始冷却，现在的期望更加现实。”，“对话已经从期望LLM取代软件开发人员（即人工智能）转变为将LLM视为合作伙伴，并集中在最佳应用它们的地方（即增强型智能）。”
上个月，由马萨诸塞大学阿默斯特分校的计算机科学家领导的一组人表示，他们正在利用生成式人工智能和LLM的力量来解决验证代码的棘手挑战，以帮助防止软件中的漏洞。
具体而言，该团队专注于利用人工智能开发一种方法，自动生成完整的证明以用于验证软件代码。这是一项费时、昂贵且耗时的过程，通常通过手动程序完成。更加困难的过程是机器检查：创建一个数学证明来展示代码是否符合预期，然后使用定理提供者确保证明的正确性。
Emily First在完成她的计算机科学博士学位后成为加利福尼亚大学圣迭戈分校的博士后研究员，而她在马萨诸塞大学阿默斯特分校攻读博士学位期间的研究涉及LLM和软件验证，并成为她博士论文的一部分。她指出，手动编写证明所需的时间可能比编写软件代码本身还要多。
因此，根据马萨诸塞大学阿默斯特分校信息与计算机科学曼宁学院的教授、本文的高级作者Yuriy Brun的说法，实际上经过正式验证的系统数量相当有限。
“这很难，”Brun告诉The New Stack。“这就是我们介入的地方。我们试图解决的问题是自动生成这些证明。”
这样做将有助于解决一个更大的问题：软件中存在缺陷，这可能是烦人的，或者——如果被网络攻击者利用或存在于可能对广泛产生负面影响的复杂系统中——是危险的。
“软件是我们日常生活中重要的一部分，”布伦说。“你什么都做不了。你不能开车，不能坐电梯，都离不开软件。不幸的是，今天的软件通常是有漏洞的。我们几乎期望在商店购买的任何软件都会有一些错误。这只是一个难以解决的问题，因此有很多不同的方法来尝试提高软件的质量。”
其中一种方法是证明软件是正确的。这是一种有效的方法，但也是最困难的方法之一。在某些领域，这已经被实践，比如在医疗领域用于某些医疗设备或由NASA使用，“因为如果你的宇宙飞船上有一个错误，你的软件崩溃了，那将是代价高昂的，所以实际上有开发人员和软件工程师正式证明函数的正确性是值得的。”他说。
一些研究人员已经创建了能够一行一行地写证明的模型，先写证明的前10行，然后让模型基于已经写的内容以及试图证明的内容搜索，找出下一行最有可能是什么。
马萨诸塞大学阿默斯特分校的研究人员将目光投向LLM，作为自动生成证明的可能解决方案。然而，即使这也带来了挑战，最大的挑战之一是这些模型并不总是正确的。与其崩溃——从而让开发人员知道有些事情出错了——它们会“悄悄失败”，生成一个错误的答案但将其呈现为正确的。悄悄失败通常是最糟糕的事情，布伦说。
进入 Baldur，这是马萨诸塞大学阿默斯特分校团队创建的一种新的基于人工智能的证明方法。研究人员使用了Google的Minerva LLM，该模型经过大量自然语言文本的训练。然后，它进一步在118GB的数学科学论文和包含数学表达式的网页上进行训练，然后在Isabell/HOL上进行了更多的训练，这是一种用于编写数学证明的语言。
然后，Baldur生成了整个证明，使用Isabelle，一个定理证明器，对整个世界进行检查。如果检查器发现错误，有关错误的信息会反馈到LLM中，以便让它从错误中学习，然后生成另一个证明，减少或者——希望是没有错误。
这样做给了Baldur“一些上下文信息，以说，‘关于状态，关于你正在回答我的问题的问题，这里有更多的信息，’”布伦说。“当我们给它额外的信息时，它能够更好地回答问题。我们只修复了一次，但你可以想象多次修复，对于这些一次只能预测一个步骤的模型来说，即使它们使用大型语言模型逐步预测，这也更加低效。”
布伦及其团队（当时还包括在Google工作的Markus Rabe和伊利诺伊大学厄巴纳-香槟分校的助理教授Talia Ringer）研究了Thor，一个用于集成语言模型和自动定理证明器的框架。独立运行时，Thor能够在57%的情况下生成证明，他说。
将其与 Baldur 结合——在北欧神话中是托尔的兄弟——他们成功地在65.7%的时间内创建了证明。这两种方法相互补充。
Thor“使用大型语言模型尝试预测证明的下一个可能步骤，但它还使用了一些被称为‘锤子’的东西，”布伦说。“锤子是这些数学工具，它们说，‘我知道一堆数学标签。让我尝试一下。让我试试这个，试试这个，试试这个。’就像用锤子敲击问题，尝试不同的方法，看看是否有效。它同时尝试所有这些方法。”
Baldur方法不同之处在于它创建整个证明而不是逐行进行，尽管存在重叠，他说：“有一些它们都能证明的事情。但通过尝试一次性生成整个证明，我们能够证明一组不同的事情，而不是尝试逐步生成一件事。”
布伦承认错误程度仍然很大，但称Baldur仍然代表了验证软件代码正确性的最有效和高效的方式。AI技术不断改进，因此他预计Baldur的能力也会得到提升。
在未来，研究人员计划通过调整LLM训练的数据来提高65.7%的数字。对于验证而言，目前并没有太多的数据，因此创建数据集并不容易。他们正在努力创建一个数据集，以便对模型进行微调。
他们还希望使开发人员能够向模型提供反馈，这将进一步帮助模型在生成证明的过程中不断成长。
“开发人员说，‘好的，运行得很好，’”布伦说。“但如果它没有运行，开发人员通常可以查看 [然后说]，‘我看到你在这里尝试了归纳，但你把它用在了错误的地方。’ 它可以向模型提供一些反馈，然后模型可以再次尝试。这种迭代的方法很可能真正简化开发人员的工作，但也使模型能够证明它自己无法完成的事情。”
这创造了一种半自动化的方法。
“原始的迭代方法不涉及开发人员，”他说。“它是在自己进行迭代，一次只做一件事，因为它是……自己进行所有操作，自己检查。我们试图重新引入软件工程师到这个循环中，因此这是一种半自动化的方法，我们在很多自动化方面做了很多工作，但然后我们从工程师那里得到了一些反馈，以引导在我们无法自行完成整个过程的情况下进行处理。”
研究人员从2020年开始致力于这个挑战，但Baldur的工作始于2023年5月，从在Google内部构建到评估和确保科学正确性，历时约五个月。该项目得到了国防高级研究计划局（DARPA）和国家科学基金会的支持。