建设网站公司谁家好,重庆建一科技发展有限公司,专业商城网站建设价格低,网站开发语言介绍来源#xff1a;机器之心编谷歌的吴宇怀 (Yuhuai Tony Wu)等研究者设计了一种叫做「Draft, Sketch, and Prove」 (DSP)的新方法将非形式化的数学证明转化为形式化的证明。实验结果显示#xff0c;自动证明器在 miniF2F 上解决的问题比例从 20.9% 提高到了 38.9%。自动证明数学…来源机器之心编谷歌的吴宇怀 (Yuhuai Tony Wu)等研究者设计了一种叫做「Draft, Sketch, and Prove」 (DSP)的新方法将非形式化的数学证明转化为形式化的证明。实验结果显示自动证明器在 miniF2F 上解决的问题比例从 20.9% 提高到了 38.9%。自动证明数学定理是人工智能的一个初衷也是一直以来的难题。到目前为止人类数学家使用了两种不同的方式来书写数学。第一种是大家都熟悉的方式即用自然语言来描述数学证明。大部分的数学都是以这种方式书写的这包括数学课本数学论文等等。第二种称之为形式化数学formal mathematics。这是近半个世纪计算机科学家创造的用来检验数学证明的一种工具。如今看来计算机可以被用来验证数学证明但它们只有在使用专门设计的证明语言时才能做到这一点而无法处理数学符号和数学家使用的书面文本的混合体。如果把用自然语言编写的数学问题转换为形式化代码让计算机更容易解决它们或许能够帮助构建能探索数学新发现的机器。这个过程被称为形式化formalisation自动形式化autoformalization指的是自动从自然语言数学翻译成形式化语言的任务。形式化证明的自动化是一项具有挑战性的任务深度学习方法在该领域尚未大获成功这主要是因为形式化数据的稀缺。事实上形式化证明本身是非常困难的且只有少数专家能做到这使得大规模的注释工作并不现实。最大的形式化证明语料库是用 Isabelle 代码 (Paulson, 1994) 编写的大小不到 0.6GB比视觉或自然语言处理中常用的数据集小几个数量级。为了解决形式证明的稀缺性以往的研究提出使用合成数据、自监督或强化学习来合成额外的形式化训练数据。虽然这些方法在一定程度上缓解了数据的不足但都无法将大量人工撰写的数学证明充分利用起来。我们以语言模型 Minerva为例。当在足够多的数据训练之后我们发现它的数学能力非常强可以在高中数学测试中拿到高于平均分水平。然而这样的语言模型也有不足它只能模仿而不能自主训练而提高数学水平。形式化证明系统提供了一个训练环境但形式化数学的数据非常少。与形式化的数学不同非形式化的数学数据是丰富和广泛可用的。最近在非形式化数学数据上训练的大型语言模型展示了令人印象深刻的定量推理能力。然而它们经常产生错误的证明而自动检测这些证明中的错误推理是很有挑战性的。在最近的一项工作中谷歌的吴宇怀 (Yuhuai Tony Wu)等研究者设计了一种叫做 DSPDraft, Sketch, and Prove 的新方法将非形式化的数学证明转化为形式化的证明从而同时具备形式化系统提供的逻辑严谨性和大量的非形式化数据。论文链接https://arxiv.org/pdf/2210.12283.pdf今年早些时候吴宇怀与几位合作者使用了 OpenAI Codex 的神经网络进行自动形式化工作证明了用大型语言模型将非形式化语句自动翻译成形式化语句的可行性。DSP 则更进一步利用大型语言模型从非形式化证明中生成形式化证明草图。证明草图由高层次的推理步骤组成可以由交互式定理证明器这样的形式化系统来解释。它们与完整的形式化证明不同因为它们包含无理由的中间猜想的序列。在 DSP 的最后一步形式化证明草图被阐述为一个完整的形式化证明使用一个自动验证器来证明所有中间猜想。吴宇怀表示现在我们展示了 LLM 可以将其生成的非形式化证明转化为经过验证的形式化证明方法方法部分描述了用于形式化证明自动化的 DSP方法该方法利用非形式化证明来指导自动形式化定理证明器的证明草图。这里假设每个问题都有一个非形式化命题和一个描述该问题的形式化命题。整体 pipeline 包括三个阶段如图 1 所示。图 1.非形式化证明的起草DSP 方法的初始阶段包括根据问题的自然数学语言描述可能用 LATEX为其寻找非形式化证明。由此产生的非形式化证明被看作是后续阶段的草稿。在数学教科书中一般都会提供定理的证明但有时会缺失或不完整。因此研究者考虑了与非形式化证明的存在或不存在相对应的两种情况。在第一种情况下研究者假设有一个「真实的」非形式化证明即由人写的证明这是现有数学理论形式化实践中的典型情况。在第二种情况下研究者做了一个更普遍的假设即没有给出真实的非形式化证明并且用一个经过非形式化数学数据训练的大型语言模型来起草证明候选。该语言模型消除了对人类证明的依赖并能为每个问题产生多种备选解决方案。虽然没有简单的方法来自动验证这些证明的正确性但非形式化证明只需要在下一阶段对生成一个好的形式化证明草图有用。将非形式化证明映射为形式化草图形式化证明草图对解决方案的结构进行编码并撇开低层次的细节。直观地说它是一个部分证明概述了高层次的猜想命题。图 2 是一个证明草图的具体例子。尽管非形式化证明经常撇开低层次的细节这些细节不能在形式化证明中排出这使得非形式化证明到形式化证明的直接转换变得困难。相反本文建议将非形式化证明映射到共享相同高层结构的形式化证明草图上。证明草图中缺少的低层次细节可以由自动证明器来填补。由于大型非形式化 - 形式化平行语料库不存在标准的机器翻译方法不适合这项任务。相反这里使用一个大型语言模型的小样本学习能力。具体来说用了一些包含非形式化证明及其相应的形式化草图的例子对来 prompt 该模型然后是一个有待转换的非形式化证明然后让模型生成后续的 token以获得所需的形式化草图。这个模型称为「自动形式化器」。图 2.证明草图中的公开猜想作为这个过程的最后一部分研究者执行现成的自动证明器来填补证明草图中缺失的细节这里的「自动证明器」是指能够产生形式上可验证的证明的系统。该框架对自动证明器的具体选择是不可知的它可以是符号证明器如启发式证明自动化工具、基于神经网络的证明器或者混合方法。如果自动证明器成功地填补了证明草图中的所有空白它就会返回最终的形式化证明可以对照问题的规格进行检查。如果自动证明器失败例如它超过了分配的时间限制则认为评估是不成功的。实验研究者进行了一系列实验包括从 miniF2F 数据集中生成问题的形式化证明并表明很大一部分定理可以用这种方法自动证明。此处研究了两种环境其中非形式化证明是由人类写的或者是由一个在数学文本上训练的大型语言模型起草的。这两种设置对应于现有理论形式化过程中经常出现的情况即通常有非形式化证明但有时作为练习留给读者或者由于空白处的限制而缺失。表 1 展示了在 miniF2F 数据集上发现的成功形式化证明的比例。结果包括本文实验的四条 baseline以及带有人类编写的证明和模型生成的证明的 DSP 方法。可以看出附加了 11 种启发式策略的自动证明器大大增加了 Sledgehammer 的性能在 miniF2F 的验证集上将其成功率从 9.9% 提高到 18.0%在测试集上从 10.4% 提高到 20.9%。两个使用语言模型和证明搜索的 baseline 在 miniF2F 的测试集上分别达到 29.9% 和 35.2% 的成功率。基于人类编写的非形式化证明DSP 方法在 miniF2F 的验证和测试集上取得了 42.6% 和 39.3% 的成功率。488 个问题中共有 200 个可以通过这种方式进行证明。Codex 模型和 Minerva8B模型在解决 miniF2F 上的问题时给出了非常相似的结果它们都指导自动验证器分别解决了验证集和测试集上 40.6% 和 35.3% 的问题。当切换到 Minerva62B模型时成功率分别上升到 43.9% 和 37.7%。与人编写的非形式化证明相比其在验证集上的成功率要高 1.3%在测试集上要低 1.6%。总的来说Minerva62B模型能够解决 miniF2F 上的 199 个问题比用人编写的证明少一个。Minerva540B模型在 miniF2F 的验证集和测试集中分别解决了 42.6% 和 38.9% 的问题也生成了 199 个成功的证明。在两种情况下DSP 方法都能有效地指导自动证明器使用人类的非形式化证明或语言模型生成的非形式化证明。DSP 几乎将证明器的成功率提高了一倍并在使用 Isabelle 的 miniF2F 上产生了 SOTA 性能。此外更大的 Minerva 模型在指导自动形式化证明器方面几乎和人类一样有帮助。如下图所示DSP 方法显着提高了 Sledgehammer 启发式证明器的性能~20% - ~40%在 miniF2F 上实现了新的 SOTA。Minerva 的 62B 和 540B 版本生成的证明与人类的证明非常相似。更多内容请参考原论文。未来智能实验室的主要工作包括建立AI智能系统智商评测体系开展世界人工智能智商评测开展互联网城市大脑研究计划构建互联网城市大脑技术和企业图谱为提升企业行业与城市的智能水平服务。每日推荐范围未来科技发展趋势的学习型文章。目前线上平台已收藏上千篇精华前沿科技文章和报告。 如果您对实验室的研究感兴趣欢迎加入未来智能实验室线上平台。扫描以下二维码或点击本文左下角“阅读原文”
