自动证明数学定理是人工智能的一个初衷，也是一直以来的难题。到目前为止，人类数学家使用了两种不同的方式来书写数学。
第一种是大家都熟悉的方式，即用自然语言来描述数学证明。大部分的数学都是以这种方式书写的，这包括数学课本，数学论文，等等。
第二种称之为形式化数学（formal mathematics）。这是近半个世纪计算机科学家创造的，用来检验数学证明的一种工具。
如今看来，计算机可以被用来验证数学证明，但它们只有在使用专门设计的证明语言时才能做到这一点，而无法处理数学符号和数学家使用的书面文本的混合体。如果把用自然语言编写的数学问题转换为形式化代码，让计算机更容易解决它们，或许能够帮助构建能探索数学新发现的机器。这个过程被称为形式化（formalisation），自动形式化（autoformalization）指的是自动从自然语言数学翻译成形式化语言的任务。
形式化证明的自动化是一项具有挑战性的任务，深度学习方法在该领域尚未大获成功，这主要是因为形式化数据的稀缺。事实上，形式化证明本身是非常困难的，且只有少数专家能做到，这使得大规模的注释工作并不现实。最大的形式化证明语料库是用 Isabelle 代码 (Paulson, 1994) 编写的，大小不到 0.6GB，比视觉或自然语言处理中常用的数据集小几个数量级。为了解决形式证明的稀缺性，以往的研究提出使用合成数据、自监督或强化学习来合成额外的形式化训练数据。虽然这些方法在一定程度上缓解了数据的不足，但都无法将大量人工撰写的数学证明充分利用起来。
我们以语言模型 Minerva为例。当在足够多的数据训练之后，我们发现它的数学能力非常强，可以在高中数学测试中拿到高于平均分水平。然而这样的语言模型也有不足，它只能模仿，而不能自主训练而提高数学水平。形式化证明系统提供了一个训练环境，但形式化数学的数据非常少。
与形式化的数学不同，非形式化的数学数据是丰富和广泛可用的。最近，在非形式化数学数据上训练的大型语言模型展示了令人印象深刻的定量推理能力。然而，它们经常产生错误的证明，而自动检测这些证明中的错误推理是很有挑战性的。
在最近的一项工作中，谷歌的吴宇怀 (Yuhuai Tony Wu)等研究者设计了一种叫做 DSP（Draft, Sketch, and Prove ）的新方法，将非形式化的数学证明转化为形式化的证明，从而同时具备形式化系统提供的逻辑严谨性和大量的非形式化数据。
论文链接：https://arxiv.org/pdf/2210.12283.pdf
内容中包含的图片若涉及版权问题，请及时与我们联系删除
评论
沙发等你来抢