去年2月份，DeepMind发布了编程辅助利器AlphaCode。它使用人工智能技术来帮助程序员更快地编写代码，可以自动完成代码、提供代码建议并检查错误，从而提高编程效率。AlphaCode的问世意味着AI在解决现实世界问题的道路上又迈出了一大步。
巧合的是，在同一天，OpenAI也展示了一项重要成果：他们开发的神经定理证明器成功解出了两道国际奥数题。这一成果是在微软打磨了多年的数学AI——Lean的基础上完成的。Lean于2013年推出，数学家可以把数学公式转换成代码，再输入到Lean中，让程序来验证定理是否正确。OpenAI的成功表明，AI不仅可以用于解决编程等应用学科的问题，还能用来攻克数学等自然学科。
值得注意的是，这并不是AI研究者的“一厢情愿”。就像快速接受AlphaCode的软件工程师一样，数学家也在越来越频繁地使用AI，比如获得过菲尔茨奖的陶哲轩。他甚至预言，到2026年，AI将成为数学研究领域可信赖的合著者（co-author）。
与此同时，主攻数学问题的AI也在不断发展壮大：一个名为LeanDojo的开放平台提供了一套基于大型语言模型的开源定理证明器，消除了在机器学习方法用于定理证明时存在的私有代码、数据和大量计算需求等障碍，为机器学习方法在定理证明领域的研究提供了便利。
“我相信，数学将成为第一门通过人工智能实现重大突破的学科。”在看到这些进展之后，英伟达高级AI研究科学家JimFan在一篇推特中预言说。
除了以上种种进展，JimFan还列出了以下推断依据：
在数学与AI的这场交叉之旅中，数学家和AI研究科学家在共同探索更多可能性。或许，陶哲轩和JimFan的预言都将加速实现。
一、在陶哲轩手里，AI成了数学家的得力助手
“我预计，如果使用得当，到2026年，AI将成为数学研究和许多其他领域值得信赖的合著者。”数学家陶哲轩在前不久的一篇博客中说道。
在众多知名数学家中，陶哲轩是较早接受并发现ChatGPT这类AI大模型数学价值的一个。早在今年3月份ChatGPT连鸡兔同笼问题都搞不定的时候，陶哲轩就给予了它肯定的态度，认为这类大模型完全可以胜任一些辅助性质的工作，比如帮数学研究者进行语义搜索、生成一些提示。
在这个例子中，陶哲轩提出的问题是：“我在寻找一个关于xx的公式。我想这是一个经典的定理，但我不记得名字了。你有什么印象吗？”在这轮问答中，虽然ChatGPT没能给出正确答案（库默尔定理），但根据它给出的近似答案（Legendre公式），我们可以结合传统搜索引擎轻松找到正确答案。
没过多久，OpenAI就发布了数学能力显著提升的GPT-4。陶哲轩也一直在尝试解锁这一强大的AI工具。
在使用过程中，他总结出了一些经验：不要试图让AI直接回答数学问题（这样得到的答案八成是废话），而是让它扮演合作者的角色，要求它提供策略建议。
按照这种提示方法，陶哲轩在GPT-4的帮助下成功解决了一个数学证明题（GPT4提出了8种方法，其中1种成功解决了问题）。
陶哲轩利用GPT-4解决的问题。
陶哲轩为了解决上述证明题提供给GPT-4的Prompt：“你好，我是一名数学教授，我希望你能扮演一位善于提出解题技巧的数学专家合作者。我正试图回答MathOverflow中的以下问题……”
GPT-4给出的部分建议。
当然，除了这个证明题外，陶哲轩也在用GPT-4完成其他一些工作，包括但不限于：
二、拿下数学定理证明，这项研究或让陶哲轩预言早日成真
一直以来，形式化的定理证明都是机器学习的重要挑战。形式化证明本质上是一种计算机程序，但与C++或Python中的传统程序不同，证明的正确性可以用证明助手（如开头提到的Lean）来验证。定理证明是代码生成的一种特殊形式，在评估上非常严格，没有让模型产生幻觉的空间。
这对目前的大型语言模型（LLM）来说是有挑战性的，尽管LLM在代码生成方面表现出了优秀的能力，但在事实性和幻觉性方面还有缺陷。
以往，对于用于定理证明的LLM研究面临着许多障碍：比如，现有的基于LLM的证明器没有一个是开源的；它们都使用私有的预训练数据，而且计算要求可以达到数千个GPU时；此外，有些基础设施是依赖于为分布式训练和与证明助手的互动而定制的，如果没有开源代码，这两者是不可能完全复现的。
在最近的一项研究中，来自加州理工学院、英伟达等机构的研究者在该命题的解决进程上走出了重要一步，提出了开放平台LeanDojo。
总体来说，该研究有如下贡献：
LeanDojo的诞生有望改变当前现状：从开源工具包、模型到基准，LeanDojo让研究人员能够以适度的计算成本获得最先进的基于LLM的证明器。ReProver不依赖私人数据集，并且可以在一周内在单个GPU上完成训练。
研究细节
Lean是一种编程语言，既可以写传统的程序，也可以写定理和证明。它提供了两个机制：首先，基于具有依赖类型的函数式编程，Lean为定义程序、数学对象、定理和证明提供了一种统一的语言；第二，Lean提供了一个策略系统（tacticsystem），用于半自动地构建机器可检查的证明。
图2展示了一个简单的例子，以说明定理是如何在Lean中被形式化和证明的：
策略（tactic）的语法是相当灵活的，可以接受参数，也可以组合成复合策略。策略可以看作是特定领域语言（DSL）中的程序。用户可以通过定义新的策略来扩展DSL。这种离散的、组合的和无界的行为空间使得定理证明对机器学习具有挑战性。
另一个挑战是前提的选择。前提是对证明一个定理有用的现有公理或定义，被用作策略的论据。证明不能使用尚未定义的前提，也不能使用未导入当前文件的前提。通常，前提是来自一个包含数十万个现有定义和定理的大型数学库，这使得人类和机器都很难在生成策略时选择正确的前提。这是定理证明中的一个关键瓶颈，也是研究者希望通过检索增强的LLM来解决的。
LeanDojoBenchmark
研究者使用LeanDojo构建了一个包含96962条从mathlib提取的定理/证明的基准。该基准是目前最大的以数学为重点的定理证明数据集之一，涵盖了不同的主题，如分析、代数和几何。
与现有的Lean数据集不同，LeanDojoBenchmark还包含了128，163个前提的定义，不仅包括定理，还包括可以作为前提的其他定义，例如图2中的gcd。此外，该数据集有212，787个策略，其中126，058个策略至少有一个前提。在有前提的策略中，前提的平均数量为2.12。
LeanDojoBenchmark解决了两项关键问题：
Leanrepos（例如，mathlib或lean-liquid）包含人写定理/证明的源代码。然而，原始代码并不适合用于训练验证器，它缺乏人类在使用Lean时可以获得的运行时信息，例如证明步骤之间的中间状态。
而LeanDojo可以从Lean的任何GitHubrepo中提取数据，这些数据包含在原始Lean代码中无法直接看到的丰富信息，包括文件依赖关系、抽象语法树（AST）、证明状态、策略和前提。LeanDojoBenchmark包含细粒度的前提注释（它们在证明中使用的位置和在库中定义的位置），为前提选择提供有价值的数据，也是定理证明的关键瓶颈。
研究者发现，将定理随机分成训练/测试的常见做法导致了之前论文中高估了性能。LLM只需在训练期间记住类似定理的证明，就能证明看似困难的定理。
在人类编写的Lean代码中，一个常见的惯用语法是为同一数学概念的略微不同的属性设置了一个类似的定理/证明块。例如，在图3中，最后两个定理不仅看起来相似，而且有相同的证明。如果其中一个在训练中，模型可以通过记忆轻松证明另一个。这种捷径使模型能够证明看似不简单的定理，包括那些需要前提才能证明的定理。
在LeanDojoBenchmark中，研究者通过设计具有挑战性的数据分割novel_premises来缓解这个问题，它需要测试证明可以使用至少一个从未在训练中使用过的前提。
例如，图3中的最后两个定理都使用了前提conj_mul。如果一个定理在novel_premises分割的训练集中，另一个也必须在训练中。
LeanDojo的另一个重要功能是以编程方式与Lean交互。它把Lean变成了一个类似健身房的环境，在这个环境中，证明器可以观察证明状态，运行策略来改变状态，并接收错误或证明完成的反馈。这个环境对于评估/部署验证器或通过RL训练证明器是不可缺少的。
下面是LeanDojo的主要形式，用于通过策略与Lean交互。Lean同样支持不基于策略的其他证明风格，不过LeanDojo只支持策略风格的证明。但只要有足够的通用性，任何证明都可以转换为策略风格的证明。
随后，研究者使用LeanDojoBenchmark来训练和评估了ReProver。其核心是一个由检索增强的策略生成器（图1底部）。
根据当前的证明状态，它可以检索出少数可能有用的前提，并根据状态和检索出的前提的连接情况生成一个策略。在证明定理时，该模型在每一步都会生成多个策略候选者，这些候选者被用于标准的最优搜索算法来寻找证明。
此前的基于LLM的证明器都在数学和编码的特定数据集上进行预训练，计算成本很高而且数据集是保密的。相比之下，ReProver避免特定领域的预训练，建立在“google/byt5-small”之上，这是一个通用的、公开可用的、相对较小的模型检查点。
此外，ReProver只在人类写的策略上进行了微调，没有辅助数据或通过与Lean在线互动收集的数据。虽然这些正交方向是有价值的，但会大大增加方法的复杂性和计算要求。
在评估实验中，ReProver可以证明51.4%的定理，优于直接生成策略而不进行检索的baseline（47.5%）和另一个使用GPT-4以零样本方式生成策略的baseline（28.8%）。
研究者还在MiniF2F和ProofNet两个数据集上测试了ReProver。它可以在MiniF2F中证明26.5%的定理，在ProofNet中证明13.8%的定理，这几乎能够媲美强化学习的SOTA方法，且训练时使用的资源少得多。
此外，许多定理在Lean中没有ground-truth证明。而ReProver能够证明65个目前在Lean中没有得到证明的定理，其中MiniF2F发现了33条证明，ProofNet中发现了39条。研究者表示，ReProver也可以作为一个有效的工具来增强Lean中现有的数学库。
三、ChatGPT插件
研究者还构建了一个LeanDojoChatGPT插件，使ChatGPT能够通过与Lean交互来证明定理。与专门针对定理证明进行微调的LLM（例如ReProver）相比，ChatGPT可以将非形式化数学与形式化证明步骤交织在一起，类似于人类与证明助手的交互方式。它可以解释来自Lean的错误消息，并且比专门的证明器更容易操纵。然而，由于搜索和规划方面的弱点，在大多数情况下很难找到正确的证明。
示例如下：
a+b+c=a+c+b
Stirling’sformula
论文一作杨凯峪目前是加州理工学院计算和数学科学（CMS）系的博士后研究员，此前在普林斯顿大学获得博士学位。
AlexGu是麻省理工学院的一名博士生，导师为ArmandoSolar-Lezama。此前，他在麻省理工学院获得了学士和硕士学位，拥有MetaAIResearch、JaneStreet和pony.ai多家公司的实习经历。
ShixingYu目前是美国康奈尔大学计算机科学专业博士生，此前在德州大学奥斯汀分校获硕士学位，本科就读于北京大学信息科学技术学院。