这篇论文就两页,正好 FM 领域做的人不多,这篇经典论文貌似没被翻译,所以做一下翻译工作,正好夯实一下自己在这个领域的语言基础

摘要

   作者提出了一种“允许用户与 Isabelle 服务器进行递进式交互”的环境。在这种环境的帮助下,作者深挖 Isabelle 标准库和形式化证明存档(AFP)并从中提取了 183K 条引理(lemmas)与定理(theorems)。作者还在这样大规模的语料库下训练了大语言模型并展示了他们在证明 AFP 定理的有效性。

介绍

   近来“将机器学习模型应用于定理证明”之风盛行。[3,6-8,12,14]等论文都展示了用机器学习模型证明新定理的希望。在本工作中,作者提出挖掘被 Isabelle ITP 使用的库,即 Isabelle 标准库和 AFP。之前研究者已经从标准库和 AFP 中提取数据,用手工设计的特征来训练推荐系统,从而帮助用户选择证明方法。

   总而言之,作者做出了以下贡献:

  1. 构建了一套agents能以渐进方式与 Isabelle 定理证明器交互的环境。这使得 learning-based agents 以 Isar 语言进行推理成为可能。

  2. 从 AFP 和 Isabelle 标准库中提取数据,得到了 183K 条定理和 2.16M 条证明步骤。这是当前 ITP 的最大的证明数据集之一。

  3. 在上述数据集上训练llm,在这个新的数据集中获得了使用此类模型证明定理的第一个结果

环境与数据集

   作者创建了一个定理证明被建模成顺序决策过程的ENV。最初,ENV会装载一条被选择的定理,我们可以得到这条定理的最顶层状态。在每一个 time-step,agent 会生成一条任意长的证明步骤。之后,ENV 将证明步骤应用于顶层状态并迭代上述流程,只要定理还没被证明成功。作者在图1演示了这样的证明过程。定理声明初始化了最初的证据状态。中间一行的 "proof state" 代表了证明过程的阶段,而最底层的证明步骤是agent需要生成的内容。作者设计的ENV支持三种不同的输入:只有 "proof state" 、只有前序步骤和二者兼有。举个例子,当 agent 应该生成 done 时,前序步骤应该包含"apply (rule impI)" 和 "apply assumption"。因为 Isabelle 提供 Partially Observable Markov Decision Process(POMDP),而 "proof state" 作为 observation,证明的前序步骤给出的条件帮助 agent 重构 "proof state" 。(这里我也不是很明白,有时间深入看一下什么是 POMDP)

   Isabelle 在我们的系统中启用的独特特性是我们可以逐token地执行证明。这一特性带来的优点包括我们可以复制某个 "proof state" 并非常方便地尝试多种不同的方法。这也允许我们改变 proof 被写的顺序,这也使得给 proof 做 sketch 成为可能:我们可以大概构建一个证明的骨架并向其中填充 sorry 关键字(这一关键字假设该语句之前的陈述是可证明的)。然后,通过保存sorry前的所有状态以及在骨架被完成后尝试每一种状态,我们让机器以人类证明的顺序去构造证明。

   有了这样的ENV,我们从 Isabelle 标准库和 AFP 中提取了 183K 条定理以及 2.16M 条(输入, "proof state" )对。这形成了对定理证明十分有帮助的一套数据集,如果 agent 在任意 "proof state" 的 prompt 下可以生成正确的证明步骤,则它就能正确证明定理。作者按 95%/1%/4% 的比例将语料库随机地分为训练/验证/测试集,并在表1中展示了数据集详细数据。

实验

实验设计

作者采用在 WebMath 数据集上预先训练的 72B 标记语言模型,类似于应用于 Metamath [12] 和 Lean [5] 的 GPT-f 模型。然后用数据集的 AFP 部分微调了模型(由于时间限制)。选择的架构是一个类似于 GPT-3 的 decoder-only transformer。所有模型有 163M 个非嵌入的参数,使用与 GPT-3 相同的 BPE 编码。微调方面,作者使用 2048 大小的 batch size,0.005 的学习率,100-step ramp-up(学习率预热),以及根据 64B tokens 的余弦策略衰减学习率。在 35B 经过的 tokens 后根据 validation perplexity 提前停止。

实验评估

与参考文献[5, 12]类似,作者在评估中使用了最佳优先搜索策略。作者初始化并维护顶级状态的优先级队列,按其累积对数概率排序。顶级状态的累积对数概率是代理为达到当前状态而采取的所有先前证明步骤的对数概率之和。最初,优先级队列仅包含定理声明之后的顶级状态,累积对数概率为 0。在每个搜索步骤中,弹出优先级队列的头部以检索具有最高概率的顶级状态。然后查询语言模型以获取一组 16 个验证步骤候选项,temperature 为 1.0。对于每个候选状态,我们复制顶级状态,将候选状态应用于该状态,并计算更新的累积对数概率。如果候选状态的应用是成功的,则将生成的顶级状态添加到队列中,队列的长度为 16(即它只维护 16 个具有最高累积对数概率的条目)。如果生成的顶级状态之一显示证明已完成,则我们认为证明尝试成功。如果队列为空,或者一次尝试超时 120 秒,或者查询次数超过 100 次,则认为该尝试失败

实验结果

作者在 4000 个定理的测试集上使用最佳优先搜索策略评估了他们的llm。33.2% 的定理被成功证明。作者还分析了其余定理的失败原因。59.1% 的尝试因时间限制而失败,0.2% 的尝试因查询数量限制而失败,7.6% 的尝试失败,因为优先级队列在验证过程中的某个时间点为空。作者接下来展示了该llm生成的两个成功证明,并将它们与 AFP 中的证明进行对比。

定理 1 是 Utility.thy 中的一个引理,来自 AFP 条目 Executable Matrix Operations on Matrices of Arbitrary Dimensions [13]。作者的证明是 one-liner 的,比原始证明简单得多。通过在 Isabelle 中编写一些生成的证明可以手动检查它们的有效性,这些证明与原始证明具有相同的依赖关系。

定理 2 是 AFP 条目 Finite Machine Word Library [2] 中 Word_Lemmas.thy 中的引理。虽然我们的证明比原文长,但它使用了一组不同的 lemmas 来完成证明,并且与原文相比,它的编写风格非常不同。这表明,作者设计的带有语言模型的证明搜索agent能够发现新颖有趣的证明。

作为 baseline,作者还考虑了使用贪婪搜索。这相当于队列长度 = 1 的最佳优先搜索。因此,这个代理只证明了 28.3% 的定理。

结论以及未来工作

作者从 Isabelle 证明中提取了大量 corpus,并检查了语言模型在数据集上证明定理的性能。作者还展示了 AFP 上很多的问题可以通过应用语言模型和最佳优先搜索来解决。成功的proofs证明了语言模型编写简洁或新颖证明的能力。

Isabelle 提供了一个非常方便的命令,允许用户猜想(“have”)。凭借以非常灵活的方式与 Isabelle 交互的环境,以及丰富的数据集,可以着手进一步研究机器如何学习猜想,并更普遍地推理证明构造。具体来说,通过从人类猜想中学习,计算机辅助定理证明者被赋予了绘制证明 sketch 的能力。这可以与 “nitpick” 和 “sledgehammer” 等符号方法有机地整合在一起。