由马萨诸塞大学阿默斯特分校领导的计算机科学家团队最近宣布了一种自动生成完整证明的新方法，可用于防止软件错误并验证底层代码是否正确。这种名为 Baldur 的新方法利用了大型语言模型 (LLM) 的人工智能能力，与最先进的工具 Thor 结合使用时，可产生近 66% 的前所未有的效率。该团队最近在 ACM 欧洲软件工程联合会议和软件工程基础研讨会上获得了令人垂涎的杰出论文奖。
麻省大学阿默斯特分校曼宁信息与计算机科学学院教授、该论文的高级研究员尤里·布伦(Yuriy Brun)表示：“不幸的是，我们预计我们的软件会存在缺陷，尽管事实上它无处不在，而且我们每天都在使用它。”作者。
有缺陷的软件的影响范围很广，从烦人的格式错误或突然崩溃到潜在的灾难性安全漏洞或用于太空探索或控制医疗保健设备的精密软件。
当然，自从软件存在以来，就有了检查软件的方法。一种流行的方法是最简单的：让人逐行检查代码，手动验证是否没有错误。或者您可以运行代码并检查它是否符合您的预期。例如，如果您希望每次按“返回”键时文字处理软件都会换行，但它却输出一个问号，那么您就知道代码中有问题。
这两种方法的问题在于，它们很容易出现人为错误，并且检查每一个可能的故障都非常耗时、昂贵，而且对于除了微不足道的系统之外的任何系统都是不可行的。
一种更彻底但更困难的方法是生成一个数学证明，表明代码执行了预期的操作，然后使用定理证明器来确保证明也是正确的。这种方法称为机器检查。
但手动编写这些证明非常耗时，并且需要广泛的专业知识。“这些证明可能比软件代码本身长很多倍，”该论文的主要作者Emily First说道，她在麻省大学阿默斯特分校的博士论文中完成了这项研究。
随着法学硕士的兴起(其中最著名的例子是 ChatGPT)，一种可能的解决方案是尝试自动生成此类证明。然而，“法学硕士面临的最大挑战之一是它们并不总是正确的，”布伦说。“他们不会崩溃并让你知道出了什么问题，而是倾向于‘默默地失败’，产生一个错误的答案，但却表现得好像它是正确的。而且，通常情况下，你能做的最糟糕的事情就是默默地失败。”
这就是博德尔发挥作用的地方。
首先，其团队在 Google 开展工作，使用了 Minerva(一种在大型自然语言文本语料库上进行训练的法学硕士)，然后在 118GB 的数学科学论文和包含数学表达式的网页上对其进行了微调。接下来，她进一步对法学硕士课程进行了微调，使用一种名为 Isabelle/HOL 的语言，数学证明就是用这种语言编写的。然后，Baldur 生成了完整的证明，并与定理证明者一起检查其工作。当定理证明者发现错误时，它将证明以及有关错误的信息反馈回 LLM，以便它可以从错误中学习并生成新的且有望无错误的证明。
此过程可显着提高准确性。最先进的自动生成证明的工具称为 Thor，它可以在 57% 的时间内生成证明。当博德(Baldur，根据北欧神话，是雷神托尔的兄弟)与雷神托尔配对时，两人可以在 65.7% 的时间内生成证明。
尽管仍然存在很大程度的错误，但 Baldur 是迄今为止验证软件正确性的最有效和高效的方法，并且随着 AI 功能的日益扩展和完善，Baldur 的有效性也应该随之提高。