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和软件验证

上个月，由马萨诸塞大学阿默斯特分校的计算机科学家领导的一组人表明，他们正在运用生成式人工智能和LLM的力量来处理验证代码的棘手应战，以协助避免软件中的缝隙。

具体而言，该团队专注于运用人工智能开发一种办法，主动生成完好的证明以用于验证软件代码。这是一项费时、昂贵且耗时的进程，一般经过手动程序完结。愈加困难的进程是机器查看：创立一个数学证明来展现代码是否符合预期，然后运用定理供给者保证证明的正确性。

Emily First在完结她的计算机科学博士学位后成为加利福尼亚大学圣迭戈分校的博士后研讨员，而她在马萨诸塞大学阿默斯特分校攻读博士学位期间的研讨触及LLM和软件验证，并成为她博士论文的一部分。她指出，手动编写证明所需的时刻或许比编写软件代码自身还要多。

因而，根据马萨诸塞大学阿默斯特分校信息与计算机科学曼宁学院的教授、本文的高级作者Yuriy Brun的说法，实际上经过正式验证的系统数量适当有限。

“这很难，”Brun告知The New Stack。“这就是咱们介入的地方。咱们企图处理的问题是主动生成这些证明。”

不应该接受有过错的软件

这样做将有助于处理一个更大的问题：软件中存在缺点，这或许是烦人的，或许——如果被网络攻击者运用或存在于或许对广泛发生负面影响的复杂系统中——是危险的。

“软件是咱们日常日子中重要的一部分，”布伦说。“你什么都做不了。你不能开车，不能坐电梯，都离不开软件。不幸的是，今日的软件一般是有缝隙的。咱们简直希望在商店购买的任何软件都会有一些过错。这只是一个难以处理的问题，因而有很多不同的办法来测验进步软件的质量。”

其间一种办法是证明软件是正确的。这是一种有用的办法，但也是最困难的办法之一。在某些范畴，这现已被实践，比如在医疗范畴用于某些医疗设备或由NASA运用，“由于如果你的宇宙飞船上有一个过错，你的软件溃散了，那将是价值高昂的，所以实际上有开发人员和软件工程师正式证明函数的正确性是值得的。”他说。

一些研讨人员现已创立了能够一行一行地写证明的模型，先写证明的前10行，然后让模型根据现已写的内容以及企图证明的内容查找，找出下一行最有或许是什么。

构建Baldur

马萨诸塞大学阿默斯特分校的研讨人员将目光投向LLM，作为主动生成证明的或许处理方案。然而，即便这也带来了应战，最大的应战之一是这些模型并不总是正确的。与其溃散——然后让开发人员知道有些作业出错了——它们会“悄然失利”，生成一个过错的答案但将其呈现为正确的。悄然失利一般是最糟糕的作业，布伦说。

EnterBaldur，这是马萨诸塞大学阿默斯特分校团队创立的一种新的根据人工智能的证明办法。研讨人员运用了Google的Minerva LLM，该模型经过很多自然言语文本的练习。然后，它进一步在118GB的数学科学论文和包含数学表达式的网页进步行练习，然后在Isabell/HOL进步行了更多的练习，这是一种用于编写数学证明的言语。

然后，Baldur生成了整个证明，运用Isabelle，一个定理证冥具，对整个国际进行查看。如果查看器发现过错，有关过错的信息会反应到LLM中，以便让它从过错中学习，然后生成另一个证明，削减或许——希望是没有过错。

这样做给了Baldur“一些上下文信息，以说，‘关于状态，关于你正在答复我的问题的问题，这里有更多的信息，’”布伦说。“当咱们给它额外的信息时，它能够更好地答复问题。咱们只修正了一次，但你能够想象屡次修正，关于这些一次只能猜测一个过程的模型来说，即便它们运用大型言语模型逐渐猜测，这也愈加低效。”

Enter Thor

布伦及其团队（其时还包含在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）和国家科学基金会的支撑。

本文在云云众生（yylives.cc/）首发，欢迎我们拜访。