创新的AI系统在无Bug软件验证方面展现出前景

传统上，软件代码的验证是一个劳动密集型的流程，涉及手动代码审查或运行代码以识别异常。虽然这些方法很有价值，但它们容易受到人为错误的影响，并且对于复杂系统来说不切实际。

Baldur应运而生，这是一个精心设计的解决方案，利用大型语言模型（LLM）的力量自动生成数学证明。通过在广泛的数学内容和用于证明的Isabelle/HOL语言上微调LLM，Baldur朝着自动化这一曾经艰巨的任务迈出了巨大的一步。结果如何？一个与定理证明器协同工作的系统，显著减少了代码正确性验证中的错误率。

Baldur成功的关键在于与Thor的合作，Thor是负责自动生成证明的工具。Thor的成功率为57%，但当与Baldur结合时，两者在生成证明方面实现了惊人的65.7%的准确率。这对受北欧神话启发的“动态组合”展示了AI驱动软件验证的潜力。

LLM面临的挑战

在使用LLM（如ChatGPT）时遇到的主要挑战之一是它们偶尔缺乏正确性。它们不会发出红旗警告，而是可能“无声失败”，提供看似有效的错误结果。解决这一问题对于确保AI生成证明的可靠性至关重要。

Baldur的开发并非易事，历时数月并与Google进行了协作。该项目的主要作者Emily First使用了Minerva，这是一个在大量自然语言文本语料库上训练的LLM。随后，Minerva在一个包含118GB数学和科学论文以及包含数学表达式的网络内容的大型数据集上进行了微调。然而，关键的差异化因素是进一步微调了Isabelle/HOL语言，为生成全面的数学证明奠定了基础。

Baldur的错误纠正方法非常巧妙。当定理证明器在生成的证明中识别出错误时，它会将此信息反馈给Baldur，使系统能够从错误中学习。这种迭代过程提高了证明的准确性和可靠性，使其成为代码验证的高效工具。

无Bug软件的美好未来

虽然还有改进的空间，但Baldur代表了形式化软件验证的一个有希望的途径。工程师仍然负责开发软件，但现在他们有了一个强大的盟友——Baldur，它能够自动化数学证明的创建。

马萨诸塞大学阿默斯特分校曼宁信息与计算机科学学院教授Yuriy Brun评论道：“我们的工作集中在尝试自动化这些证明的编写。Baldur使用大型语言模型，给定一个数学定理，自动生成该定理的证明，然后由定理证明器进行验证。”

Baldur的成功归功于在这个项目上不知疲倦工作的团队。除了Emily First之外，当时受雇于Google的Markus Rabe和伊利诺伊大学厄巴纳-香槟分校的助理教授Talia Ringer也做出了重大贡献。该项目得到了国防高级研究计划局（DARPA）和国家科学基金会（NSF）的支持。

像Baldur这样的创新解决方案为科技行业应对软件系统日益增加的复杂性带来了希望。随着AI能力的不断发展和成熟，Baldur将软件正确性推向新高度的潜力仍然令人充满希望。