新智元报道
编辑：alan
【新智元导读】在软件工程顶会ESEC/FSE上，来自马萨诸塞大学、谷歌和伊利诺伊大学厄巴纳-香槟分校（UIUC）的研究人员发表了新的成果，使用LLM解决自动化定理证明问题。
Transformer的技能树是越来越厉害了。
来自马萨诸塞大学、谷歌和伊利诺伊大学厄巴纳-香槟分校（UIUC）的研究人员发表了一篇论文，利用大语言模型自动生成定理的完整证明。
论文地址：https://arxiv.org/pdf/2303.04910.pdf
这篇工作以Baldur（北欧神话中雷神Thor的兄弟）命名，首次证明了使用Transformer生成全证明是可能的，并且当为模型提供额外的上下文时，还可以改进模型先前的证明。
文章发表于2023年12月在旧金山举行的ESEC/FSE（ACM欧洲软件工程联合会议和软件工程基础研讨会）上，并获得了杰出论文奖（Distinguished Paper award）。
众所周知，软件存在bug（废话），这在一般应用程序或者网站上问题不大，但对于比如加密协议、医疗设备和航天飞机等关键系统背后的软件而言，必须确保没有错误。
一般的代码审查和测试并不能给出这个保证，这需要形式验证（formal verification）。
对于formal verification，ScienceDirect给出的解释为：
the process of mathematically checking that the behavior of a system, described using a formal model, satisfies a given property, also described using a formal model
指的是从数学上检查，使用形式模型描述的系统行为，是否满足给定属性的过程。
简单来说就是，利用数学分析的方法，通过算法引擎建立模型，对待测设计的状态空间进行穷尽分析的验证。
形式化软件验证，对于软件工程师来说是最具挑战性的任务之一。例如CompCert，使用Coq交互式定理证明器验证的C编译器，是无处不在的GCC和LLVM等使用的唯一编译器。
然而，手动形式验证（编写证明）的成本却相当巨大，C编译器的证明是编译器代码本身的三倍以上。
所以，形式验证本身是一项“劳动密集型”的任务，研究人员也在探索自动化的方法。
比如Coq和Isabelle等证明助手，通过训练一个模型来一次预测一个证明步骤，并使用模型搜索可能的证明空间。
而本文的Baldur首次在这个领域引入了大语言模型的能力，在自然语言文本和代码上训练，并在证明上进行微调，
Baldur可以一次就生成定理的完整证明，而不是一次一个步骤。
如上图所示，仅使用定理语句作为证明生成模型的输入，然后从模型中抽取证明尝试，并使用Isabelle执行证明检查。
如果Isabelle接受了证明尝试而没有错误，就说明证明成功；否则从证明生成模型中抽取另一个证明尝试。
Baldur在6336个Isabelle/HOL定理及其证明的基准上进行评估，从经验上证明了完整证明生成、修复和添加上下文的有效性。
另外，这个工具之所以叫Baldur，可能是因为当前最好的自动证明生成工具叫做Thor。
Thor的证明率更高（57%），它使用较小的语言模型结合搜索可能证明空间的方法预测证明的下一步，而Baldur的优势在于它能够生成完整的证明。
不过Thor和Baldur两兄弟也可以一起工作，这样可能把证明率提升到接近66%。
自动生成完整证明
Baldur由Google的大语言模型Minerva提供支持，Minerva在科学论文和包含数学表达式的网页上进行训练，并对有关证明和定理的数据进行了微调。
Baldur可以与定理证明助手Isabelle合作，Isabelle对证明结果进行检查。当给定一个定理陈述时，Baldur几乎在41%的时间内能够生成一个完整的证明。
为了进一步提高Baldur的性能，研究人员向模型提供了额外的上下文信息（比如其他定义、或理论文件中的定理陈述），这使证明率提高到47.5%。
这意味着Baldur能够获取上下文，并使用它来预测新的正确证明，类似于程序员，当了解了相关方法和代码之后，他们更有可能修复程序中的错误。
下面举个例子（fun_sum_commute定理）：
这个定理来自形式证明档案中一个名为多项式的项目。
当人工编写证明的时候，会区分两种情况：集合是有限的或者不是有限的：
所以，对于模型来说，输入是定理陈述，而目标输出是这个人工编写的证明。
Baldur认识到这里需要归纳，并应用了一种特殊的归纳法则，称为infinite_finite_induct，遵循与人类书面证明相同的总体方法，但更简洁。
而因为需要归纳，Isabelle使用的Sledgehammer默认无法证明这个定理。
ѵ
相关文章
