《机器之心》(ID:more Human 2014)，张骞编译，蛋酱，原题:《大模型帮助陶哲轩解题，证明数学定理:数学真的是第一个用AI实现突破的学科吗？》，头部图片来自:UCLA去年2月，DeepMind发布了编程辅助工具AlphaCode。它利用人工智能技术帮助程序员更快地编写代码，并能自动完成代码，提供代码建议和检查错误，从而提高编程效率。AlphaCode的问世意味着AI在解决现实世界问题上又迈出了一大步。无独有偶，在同一天，OpenAI也展示了一项重要成果:他们开发的神经定理证明器成功解决了两道国际奥林匹克数学难题。这个成绩是基于微软打磨多年的数学AI Lean。精益于2013年推出。数学家可以将数学公式转换成代码，然后输入到Lean中，让程序验证定理是否正确。OpenAI的成功表明，AI不仅可以用来解决编程等应用学科的问题，还可以用来征服数学等自然学科。值得注意的是，这并不是AI研究人员的“一厢情愿”。就像软件工程师很快接受字母代码一样，数学家也越来越频繁地使用人工智能，比如获得菲尔兹奖的陶哲轩。他甚至预言，到2026年，AI将成为数学研究领域可靠的合著者。与此同时，专注于数学问题的AI也在成长:一个名为LeanDojo的开放平台提供了基于大型语言模型的开源定理证明器，消除了机器学习方法用于定理证明时的私有代码、数据和大量计算需求等障碍，方便了机器学习方法在定理证明领域的研究。”我相信数学会是第一个通过人工智能实现重大突破的学科。"在看到这些发展后，英伟达高级人工智能研究科学家吉姆·范(Jim Fan)在一条推文中预测道。除了上述进展，Jim Fan还列举了以下推理依据:数学可以很容易地转化为编码问题，字符串在其中发挥了重要作用，使得数学问题可以被人工智能工具处理和分析；与依赖经验结果的学科不同，数学可以被定理证明者严格验证(比如精益)；与需要依赖物理实验的学科(如生物、医学)不同，数学不需要进行物理实验，不需要依赖机器人技术或尚未完全成熟的实验设备。在这场数学与人工智能的跨越之旅中，数学家和人工智能研究科学家正在共同探索更多的可能性。或许，陶哲轩和吉姆·范的预言将会实现。1.在手里，艾成了数学家的左膀右臂。”我预测，如果使用得当，到2026年，AI将成为数学研究和其他许多领域值得信赖的合著者。”数学家陶哲轩在最近的博客中说道。在众多知名数学家中，陶哲轩是最早接受并发现ChatGPT等大AI模型数学价值的人之一。早在今年3月，当ChatGPT无法解决鸡兔同笼的问题时，陶哲轩就给了它积极的态度，认为这种大型模型完全可以胜任一些辅助工作，比如帮助数学研究者进行语义搜索，生成一些提示。在这个例子中，陶哲轩问，“我在寻找一个关于xx的公式。我认为这是一个经典定理，但是我不记得名字了。有印象吗？“在这一轮问答中，虽然ChatGPT未能给出正确答案(库马尔定理)，但根据其近似答案(勒让德公式)，结合传统搜索引擎，我们很容易找到正确答案。不久之后，OpenAI发布了数学能力显著提高的GPT-4。陶哲轩一直试图解开这个强大的人工智能工具。在使用它的过程中，他总结了一些经验:不要试图让AI直接回答数学问题(答案很可能是废话)，而是让它扮演合作者的角色，让它提供策略建议。根据这个提示方法，陶哲轩在GPT-4的帮助下成功解决了一个数学证明问题(GPT-4提出了8种方法，其中一种成功解决了问题)。陶哲轩用GPT-4解决了这个问题。陶哲轩提供了GPT-4解决上述证明题的提示:“你好，我是数学教授，希望你能扮演一个善于提出解题技巧的数学专家合作者。我试图在MathOverflow中回答以下问题...“GPT-4给出的一些建议。当然，除了这个证明问题，陶哲轩还在使用GPT-4完成一些其他工作，包括但不限于:提问:他将最近的一些数学预印论文的前几页输入到GPT-4，并要求它生成一些与论文相关的问题，就像他的同龄人提出的问题一样。这可以帮助他更好地准备演讲。回答问题:他经常使用GPT-4来回答随机和模糊的问题。在过去，他可能会尝试通过精心准备的搜索引擎查询来回答这些问题。辅助写作:他曾经要求GPT-4为复杂的文件提供初稿建议来辅助写作。不过，陶哲轩也指出，AI在数学和其他学术领域的广泛应用是对出版界和教育界的考验:当人工智能指导下的研究生入门级数学论文可以在不到一天的时间内生成时，研究期刊将如何改变其出版和引用机制？我们的研究生教育模式会发生怎样的变化？我们会积极鼓励和培训学生使用这些工具吗？陶哲轩没有回答这些问题。第二，赢得数学定理证明，这项研究可能使陶哲轩的预言尽快实现。形式定理证明一直是机器学习的一个重要挑战。形式证明本质上是一个计算机程序，但与C++或Python中的传统程序不同，证明的正确性可以由一个证明助手(比如开头提到的Lean)来验证。定理证明是代码生成的一种特殊形式，评估非常严格，没有模型幻想的余地。这是对当前大规模语言模型(LLM)的挑战。虽然LLM在代码生成方面表现出了优秀的能力，但它仍然存在事实上的缺陷和假象。过去，用于定理证明的LLM研究面临许多障碍:例如，现有的基于LLM的证明器都不是开源的；都是使用私有的预训练数据，计算需求可以达到上千GPU小时；此外，一些基础设施是为分布式培训和与认证助理的交互而定制的，没有开源代码就无法完全复制。在最近的一项研究中，来自加州理工学院、英伟达等机构的研究人员在解决这一命题的过程中迈出了重要一步，提出了一个开放平台LeanDojo。论文链接:https://arxiv.org/pdf/2306.15626.pdf项目主页:https://leandojo.org/总的来说，研究有以下贡献:一是介绍了从精益中提取数据并与之交互的工具；其次，开发了定理证明搜索增强的第一语言模型。第三，为基于学习的定理证明构造了一个具有挑战性的基准，并用来验证重证明器的有效性。最后，公开发布数据、模型和代码，促进了定理证明LLM的研究。LeanDojo的诞生有望改变目前的局面:从开源工具包、模型到基准，LeanDojo使研究人员能够以适中的计算成本获得最先进的基于LLM的证明者。ReProver不依赖私有数据集，一周内可以在单个GPU上完成训练。研究详情Lean是一种编程语言，不仅可以写传统程序，还可以写定理和证明。它提供了两种机制:一是基于依赖类型的函数式编程，精益提供了定义程序、数学对象、定理和证明的统一语言；第二，精益提供了一个半自动构造机器可检查证明的策略系统。图2显示了一个简单的例子来说明这个定理是如何在精益中被形式化和证明的:tactic的语法非常灵活，它可以接受参数或者被组合成一个复合策略。策略可以被视为特定领域语言(DSL)中的程序。用户可以通过定义新的策略来扩展DSL。这种离散、组合和无界的行为空间使得定理证明对于机器学习来说具有挑战性。另一个挑战是前提的选择。前提是对证明一个定理有用的现有公理或定义被用作策略的论据。证明不能使用尚未定义的前提或尚未导入当前文件的前提。通常情况下，前提来自于一个包含数十万个现有定义和定理的大型数学库，这使得人类和机器在生成策略时都很难选择正确的前提。这是定理证明中的一个关键瓶颈，研究人员希望通过搜索增强的LLM来解决这个问题。LeanDojo基准测试研究人员使用LeanDojo构建了一个基准测试，其中包含从mathlib中提取的96，962个定理/证明。该基准测试是最大的专注于数学的定理证明数据集之一，涵盖了不同的主题，如分析、代数和几何。与现有的精益数据集不同，LeanDojo Benchmark还包含128，163个前提定义，不仅包括定理，还包括其他可以作为前提的定义，如图2中的gcd。此外，数据集有212，787个策略，其中126，058个策略至少有一个前提。在有前提条件的策略中，前提条件的平均数是2.12。LeanDojo Benchmark解决了两个关键问题:前提信息Lean repos(例如mathlib或lean-liquid)包含人类编写的定理/证明的源代码。然而，原始代码并不适合训练验证者，它缺乏人类在使用精益时可以获得的运行时信息，比如证明步骤之间的中间状态。LeanDojo可以从精益的任何GitHub repo中提取数据，这些数据包含了在原始精益代码中无法直接看到的丰富信息，包括文件依赖、抽象语法树(AST)、证明状态、策略和前提。LeanDojo Benchmark包含细粒度的前提注释(在证明中使用，在库中定义)，为前提选择提供了有价值的数据，也是定理证明的关键瓶颈。具有挑战性的数据分割研究人员发现，将定理随机分为训练/测试的常见做法导致了之前论文中对性能的高估。LLM只需要在训练时记住相似定理的证明，就能证明看似困难的定理。在人类编写的精益代码中，常见的惯用语法是为同一数学概念的略有不同的属性设置类似的定理/证明块。例如，在图3中，最后两个定理不仅看起来相似，而且具有相同的证明。如果其中一个在训练中，模型可以很容易地通过记忆证明另一个。这种捷径使模型能够证明看似简单的定理，包括那些需要前提证明的定理。在LeanDojo Benchmark中，研究人员通过设计一个具有挑战性的数据分区novel_premises来缓解这个问题，这个数据分区需要测试来证明至少有一个从未在训练中使用过的前提可以使用。例如，图3中的最后两个定理都使用了前提conj_mul。如果一个定理在新颖前提分割的训练集中，则另一个定理也必须在训练中。以编程方式与精益交互LeanDojo的另一个重要功能是以编程方式与精益交互。它将精益变成了一个类似健身房的环境，在这个环境中，证明者可以观察认证状态，运行策略来改变状态，并接收错误或认证完成的反馈。这个环境对于通过RL评估/部署验证器或训练证明器是必不可少的。以下是LeanDojo的主要形式，用于通过策略与Lean进行交互。Lean还支持其他不基于策略的证明风格，但是LeanDojo只支持策略风格的证明。但只要有足够的一般性，任何证明都可以转化为策略风格的证明。随后，研究者使用LeanDojo Benchmark来训练和评估ReProver。其核心是通过检索增强的策略生成器(图1的底部)。它可以根据当前的证明状态，检索出几个可能有用的前提，并根据状态和检索到的前提之间的联系生成一个策略。在证明定理时，模型会在每一步生成多个策略候选，在标准的最优搜索算法中使用这些策略候选来寻找证明。值得注意的是，ReProver的训练在单个GPU上只需要五天时间(120 GPUs)，所需计算量远低于之前的方法(1000多个小时)。先前基于LLM的证明者都是在数学和编码的特定数据集上预先训练的，因此计算成本高并且数据集是保密的。相比之下，ReProver避免了特定领域的预训练，并基于“google/byt5-small”构建，这是一个通用的、公开可用的、相对较小的模型检查点。此外，ReProver只对人类编写的策略进行了微调，没有辅助数据或通过与精益在线交互收集的数据。虽然这些正交方向是有价值的，但它们会大大增加方法的复杂性和计算要求。在评测实验中，ReProver可以证明51.4%的定理，优于不需要搜索直接生成策略的基线(47.5%)和另一个使用GPT-4生成零样本策略的基线(28.8%)。研究人员还在MiniF2F和ProofNet两个数据集上测试了ReProver。它可以在MiniF2F中证明26.5%的定理，在ProofNet中证明13.8%的定理，几乎可以与强化学习的SOTA方法相媲美，而且在训练中使用的资源要少得多。此外，许多定理在精益中没有地面真理证明。ReProver可以证明65个目前在Lean中尚未证明的定理，其中33个在MiniF2F中已经证明，39个在ProofNet中已经证明。研究人员表示，ReProver也可以作为一种有效的工具来增强精益中现有的数学库。第三，ChatGPT插件研究者还构建了一个LeanDojo ChatGPT插件，使得ChatGPT能够通过与Lean交互来证明定理。相对于专门精调定理证明的LLM(如ReProver)，ChatGPT可以将非形式数学与形式证明步骤交织在一起，类似于人类与证明助手的交互。它可以解释来自精益的错误信息，并且比特殊的证明者更容易操作。然而，由于搜索和规划的弱点，在大多数情况下很难找到正确的证明。例子如下:A+B+C = A+C+BSTIRLING公式Gauss的求和公式最后，让我们来认识一下这篇文章的作者:第一部分:杨凯·于目前是加州理工学院计算与数学科学系(CMS)的博士后研究员，之前在普林斯顿大学获得博士学位。亚历克斯·古是麻省理工学院的博士生，他的导师是阿曼多·太阳能-莱萨马。此前，他在麻省理工学院获得了学士和硕士学位，并在Meta AI Research、Jane Street和pony.ai等多家公司拥有实习经验。杨佩·宋目前是加州大学圣巴巴拉分校(UCSB)创意研究学院(CCS)计算机科学专业的本科生。他的研究工作主要集中在两个方向:1)神经定理证明和自动推理，结合大规模语言模型(LLMs)和交互式定理证明器(ITPS)；2)能效机器学习推理的时间逻辑。石星宇目前是美国康奈尔大学计算机科学专业的博士生。他之前在奥斯汀的德克萨斯大学获得了硕士学位，并研究eecs。参考链接:https://unlocked.microsoft.com/ai-anthology/terence-tao/'s机器之心(ID:近人类2014)，编译:张骞，蛋酱此内容为作者独立观点，不代表虎嗅立场。未经允许不得转载。请联系hezuo@huxiu.com获得授权。如果你对这份手稿有任何异议或抱怨，。