大模型帮陶哲轩解题、证明数学定理：数学真要成为首个借助AI实现突破的学科了？
机器之心 2023-06-30 13:30 发表于北京
机器之心报道
编辑：张倩、蛋酱
数学将成为第一门借助AI实现重大突破的学科？
去年 2 月份，DeepMind 发布了编程辅助利器 AlphaCode。它使用人工智能技术来帮助程序员更快地编写代码，可以自动完成代码、提供代码建议并检查错误，从而提高编程效率。AlphaCode 的问世意味着 AI 在解决现实世界问题的道路上又迈出了一大步。
巧合的是，在同一天，OpenAI 也展示了一项重要成果：他们开发的神经定理证明器成功解出了两道国际奥数题。这一成果是在微软打磨了多年的数学 AI——Lean 的基础上完成的。Lean 于 2013 年推出，数学家可以把数学公式转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。OpenAI 的成功表明，AI 不仅可以用于解决编程等应用学科的问题，还能用来攻克数学等自然学科。
值得注意的是，这并不是 AI 研究者的「一厢情愿」。就像快速接受 AlphaCode 的软件工程师一样，数学家也在越来越频繁地使用 AI，比如获得过菲尔茨奖的陶哲轩。他甚至预言，到 2026 年，AI 将成为数学研究领域可信赖的合著者（co-author）。
与此同时，主攻数学问题的 AI 也在不断发展壮大：一个名为 LeanDojo 的开放平台提供了一套基于大型语言模型的开源定理证明器，消除了在机器学习方法用于定理证明时存在的私有代码、数据和大量计算需求等障碍，为机器学习方法在定理证明领域的研究提供了便利。
「我相信，数学将成为第一门通过人工智能实现重大突破的学科。」在看到这些进展之后，英伟达高级 AI 研究科学家 Jim Fan 在一篇推特中预言说。
除了以上种种进展，Jim Fan 还列出了以下推断依据：
- 数学可以被方便地转化为编码问题，字符串在其中具有重要地位，这使得数学问题可以通过人工智能工具进行处理和分析；
- 与依赖实证结果的学科不同，数学可以通过定理证明器（如 Lean）进行严格验证；
- 与需要依赖物理实验的学科（如生物学和医学）不同，数学不需要进行物理实验，无需依赖尚未完全成熟的机器人技术或实验设备。
在数学与 AI 的这场交叉之旅中，数学家和 AI 研究科学家在共同探索更多可能性。或许，陶哲轩和 Jim Fan 的预言都将加速实现。
在陶哲轩手里，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 完成其他一些工作，包括但不限于：
- 提出问题：他将最近一些数学预印本论文的前几页输入给 GPT-4，并让其生成一些与该论文相关的问题，就像同行提出的问题一样。这可以帮助他更好地进行演讲准备。
- 回答问题：他现在经常使用 GPT-4 来回答随意和模糊的问题，以前他可能会通过精心准备的搜索引擎查询来尝试回答这些问题；
- 辅助写作：他曾经让 GPT-4 给复杂文档提供初稿建议，以辅助写作。
不过，陶哲轩也指出，AI 在数学等学术领域的广泛应用对出版界和教育界来说都是一个考验：当人工智能指导的研究生入门级数学论文可以在不到一天的时间内生成时，研究期刊将如何改变其出版和引用机制？我们的研究生教育方式将如何改变？我们会积极鼓励和训练学生使用这些工具吗？对于这些问题，陶哲轩并没有给出答案。
拿下数学定理证明，这项研究或让陶哲轩预言早日成真
一直以来，形式化的定理证明都是机器学习的重要挑战。形式化证明本质上是一种计算机程序，但与 C++ 或 Python 中的传统程序不同，证明的正确性可以用证明助手（如开头提到的 Lean）来验证。定理证明是代码生成的一种特殊形式，在评估上非常严格，没有让模型产生幻觉的空间。
这对目前的大型语言模型（LLM）来说是有挑战性的，尽管 LLM 在代码生成方面表现出了优秀的能力，但在事实性和幻觉性方面还有缺陷。
以往，对于用于定理证明的 LLM 研究面临着许多障碍：比如，现有的基于 LLM 的证明器没有一个是开源的；它们都使用私有的预训练数据，而且计算要求可以达到数千个 GPU 时；此外，有些基础设施是依赖于为分布式训练和与证明助手的互动而定制的，如果没有开源代码，这两者是不可能完全复现的。
在最近的一项研究中，来自加州理工学院、英伟达等机构的研究者在该命题的解决进程上走出了重要一步，提出了开放平台 LeanDojo。
论文链接：https://arxiv.org/pdf/2306.15626.pdf
总体来说，该研究有如下贡献：
- 首先，介绍了从 Lean 中提取数据并与之交互的工具；
- 第二，开发了第一个用于定理证明的检索增强的语言模型 ReProver；
- 第三，为基于学习的定理证明构建了一个具有挑战性的基准，并利用它来验证 ReProver 的有效性；
- 最后，公开发布数据、模型和代码，推动了对定理证明的 LLM 的研究。
LeanDojo 的诞生有望改变当前现状：从开源工具包、模型到基准，LeanDojo 让研究人员能够以适度的计算成本获得最先进的基于 LLM 的证明器。ReProver 不依赖私人数据集，并且可以在一周内在单个 GPU 上完成训练。
研究细节
Lean 是一种编程语言，既可以写传统的程序，也可以写定理和证明。它提供了两个机制：首先，基于具有依赖类型的函数式编程，Lean 为定义程序、数学对象、定理和证明提供了一种统一的语言；第二，Lean 提供了一个策略系统（tactic system），用于半自动地构建机器可检查的证明。
图 2 展示了一个简单的例子，以说明定理是如何在 Lean 中被形式化和证明的：
策略（tactic）的语法是相当灵活的，可以接受参数，也可以组合成复合策略。策略可以看作是特定领域语言（DSL）中的程序。用户可以通过定义新的策略来扩展 DSL。这种离散的、组合的和无界的行为空间使得定理证明对机器学习具有挑战性。
另一个挑战是前提的选择。前提是对证明一个定理有用的现有公理或定义，被用作策略的论据。证明不能使用尚未定义的前提，也不能使用未导入当前文件的前提。通常，前提是来自一个包含数十万个现有定义和定理的大型数学库，这使得人类和机器都很难在生成策略时选择正确的前提。这是定理证明中的一个关键瓶颈，也是研究者希望通过检索增强的 LLM 来解决的。
