| 送交者: xiaochuliu[♂★★大🇨🇳lngviva★★♂] 于 2023-07-01 11:40 已读 4529 次 | xiaochuliu的个人频道 |
加州理工让ChatGPT证明数学公式，数学成见证AI突破首个学科 6park.com
6park.com
6park.com用大语言模型定理证明，加州理工华人一作最新研究可能改变数学未来。 6park.com
6park.com大语言模型，可以用来证明数学定理了！ 6park.com
6park.com「数学天才」陶哲轩曾在一篇博客中称，2026年，AI将与搜索和符号数学工具相结合，成为数学研究中值得信赖的合著者。 6park.com
6park.com这个预言，如今已经成真！ 6park.com
6park.com加州理工、英伟达、MIT等机构的学者，构建了一个基于开源LLM的定理证明器。 6park.com
6park.com而这篇论文，或许将改变数学的未来。 6park.com
6park.com
6park.com项目地址：https://leandojo.org/ 6park.com
6park.com在此，研究人员提出一个开源平台LeanDojo，提供工具包、基准和模型，为LLM创造了一种定理证明的交互式环境。 6park.com
6park.com数学：首个见证AI重大突破的领域 6park.com
6park.com论文一作杨凯峪表示，公式证明是计算机程序，其正确性可以被验证。 6park.com
6park.com最重要的是，这项研究为解决LLM，在事实性和幻觉方面的缺陷开辟了一条新途径。 6park.com
6park.com因为，定理证明是一种具有严格评价的代码生成形式，根本没有让模型产生幻觉的空间。 6park.com
6park.com英伟达首席科学家Jim Fan激动转发称：见证人工智能实现重大突破的第一个学科，很可能就是数学！ 6park.com
6park.com他说：每个人都该读一读数学家陶哲轩的博客。在此博客中，陶预测在2026年，AI将与搜索和符号数学工具相结合，成为数学研究中值得信赖的合著者。 6park.com
6park.com
6park.com为什么AI的第一个重大突破会在数学？理由如下—— 6park.com
6park.com- 数学可以方便地表示为编码问题 6park.com
6park.com- 可以通过Lean这样的定理证明器进行严格的验证，而不是依赖经验结果 6park.com
6park.com- 不需要像生物学和医学这样的物理实验，机器人技术的发展还有待进步 6park.com
6park.comGPT擅长编码，Lean是公式数学的编码语言，还不会出现幻觉。 6park.com
6park.com人工智能数学co-pilots来了。发现新定理的全自动人工智能数学家就是下一个！ 6park.com
6park.com
6park.com有网友称，所以陶哲轩可以被解雇，很容易被取代，不是吗？ 6park.com
6park.com
6park.comLeanDojo究竟有多强？ 6park.com
6park.comLeanDojo：定理证明交互式环境 6park.com
6park.com机器学习，特别是大型语言模型，在使用证明助手Lean证明公式定理方面显示出广阔的前景。 6park.com
6park.comLeanDojo其主要特点包括： 6park.com
6park.com- 提供了用于数据提取和与Lean交互的工具 6park.com
6park.com- 证明中的前提（现有定理）的细粒度标注：使用和定义这些前提的位置 6park.com
6park.com- LeanDojo Benchmark：97000个人工编写的定理/证明，用于开发定理证明的机器学习模型 6park.com
6park.com- ReProver（检索增强证明器）：第一个基于LLM的证明器，专门增强了前提选择（Premise Selection）的检索 6park.com
6park.comLean是一个在数学家中非常受欢迎的证明助手工具。 6park.com
6park.com研究团队针对Lean进行了加工和改进，开发出了LeanDojo。它可以从Lean中提炼出人类撰写的证明过程，形成一个数据集。 6park.com
6park.com从而可以通过与Lean的证明环境互动，使得这个训练出来的模型可以用来证明定理。 6park.com
6park.comLeanDojo的工作流程和原理大致如下图所示： 6park.com
6park.com
6park.com顶部右边：LeanDojo从Lean中提取证明到数据库中，用来训练机器学习模型。 6park.com
6park.com这个流程也可以通过和Lean的证明环境进行交互后让训练好的模型来证明定理。 6park.com
6park.com顶部左边：这是Lean定理 6park.com
6park.com
6park.com的证明树。在这里gcd是最大公约数的意思。 6park.com
6park.com在证明定理时，我们从原始定理作为初始状态（根）开始，并重复应用策略（边）将状态分解为更简单的子状态，直到所有状态都得到解决（叶节点处）。 6park.com
6park.com策略可能依赖于大型数学库中定义的诸如 mod_self 和 gcd_zero_left 之类的前提。 6park.com
6park.com例如，mod_self 是证明中用于简化目标的现有定理 ： 6park.com
6park.com
6park.com底部：只要给定一个状态，Reprover模型就能从数学库中检索前提，这些前提与状态连接起来，输入到一个作为编码器和解码器的Transformer中以生成下一个策略。 6park.com
6park.comBenchmarks 基准测试 6park.com
6park.com- LeanDojo Benchmark：从mathlib中提取的96,962个定理/证明、212,787个策略和128,163个前提。 6park.com
6park.com- LeanDojo Benchmark 4：从mathlib4中提取的91,766个定理/证明和177,349个策略。前提信息将很快提供。 6park.com
6park.comLeanDojo可以从Lean中的任何GitHub存储库中提取数据（支持Lean 3和Lean 4）。 6park.com
6park.com这些数据包含原始Lean代码中不直接可见的丰富信息，包括文件依赖项、抽象语法树 (AST)、证明状态、策略和前提。 6park.com
6park.com主要特征 1：前提信息 6park.com
6park.comLeanDojo Benchmark包含前提的细粒度标注（在证明中使用它们以及在库中定义它们），为前提选择（定理证明中的关键瓶颈）提供有价值的数据。 6park.com
6park.com主要特征 2：具有挑战性的数据分割 6park.com
6park.com将定理随机分割到训练/测试中会导致高估模型性能。大语言模型可以通过在训练期间记住类似定理的证明，就可以证明看似困难的定理。 6park.com
6park.com研究人员通过设计具有挑战性的数据分割来缓解这个问题，要求模型基于从未在训练中使用的创新性前提来泛化到定理。 6park.com
6park.com与Lean产生交互 6park.com
6park.com
6park.com如上图所示，LeanDojo将Lean变成了一个类似体育馆的环境，数学家可以在其中观察证明状态，运行策略来改变状态，并接收有关错误或证明完成的反馈。 6park.com
6park.com这样的一个环境对于评估/部署证明器或通过强化学习进行训练是必不可少的。 6park.com
6park.com实验评估 6park.com
6park.com研究人员使用LeanDojo Benchmark来训练和评估ReProver。 6park.com
6park.com下图展示了10分钟内证明的定理的百分比。每一列代表不同的数据分割。 6park.com
6park.comReProver的性能优于Lean内置的证明自动化策略（tidy），提供了一个无需检索即可直接生成策略的测试基准。 6park.com
6park.com研究人员采用的另一个基准是使用GPT-4以零样本方式生成策略。 6park.com
6park.com
6park.com发现新证明&发现公式错误 6park.com
6park.com研究人员采用在miniF2F和FroofNet中的定理来评估ReProver。 6park.com
6park.com他们发现miniF2F中有33个证明，ProffNet中有39个证明在Lean中是不存在的。 6park.com
6park.com与此同时，最新研究还发现了ProofNet定理陈述公式中的多个错误。 6park.com
6park.com详见：https://github.com/zhangir-azerbayev/ProofNet/pull/14 6park.com
6park.comChatGPT插件 6park.com
6park.com研究人员还构建了一个LeanDojo的ChatGPT插件，使ChatGPT能够通过与Lean交互来证明定理。 6park.com
6park.com他们具体在三种数学公式上进行了尝试，包括a+b+c=a+c+b，斯特林公式（Stirling's formula），以及高斯求和公式（Gauss' summation formula）。 6park.com
6park.com结果发现，专业的定力证明LLM（ReProver）相比，ChatGPT可以将非正式数学与正式证明步骤交叉在一起，类似人类与证明助手的交互方式。 6park.com
6park.com它甚至可以解释Lean的错误信息，并且比专业证明器更容易控制（通过提示工程）。 6park.com
6park.com然而，由于搜索和规划方面的弱点，它在多数情况下很难找到正确的证明。 6park.com
6park.comGitHub上，开发者给出使用演示方法示例： 6park.com
6park.com插件安装成功后，你可以让ChatGPT证明定理，只需告诉它定理的名称和定义。比如： 6park.com
6park.comI want you to prove a theorem in Lean. The theorem's name is `hello_world`, and it is defined in the file `src/example.lean` in `https://github.com/yangky11/lean-example`. Please explain the theorem to me, lay out a high-level proof plan, and then try various tactics to prove the theorem. 6park.com初始化证明搜索可能需要一些时间。 6park.com
6park.com你可以用提示来控制ChatGPT的行为。例如，在尝试任何测术之前，你可以要求它「产生一个高级证明计划」。 6park.com
6park.com网友评论 6park.com
6park.com
6park.com这个发现是AI在数学领域的最佳应用，找到了一个非常现实的角度让AI能为数学研究做出了贡献。 6park.com
6park.com
6park.com我们离正式证明所有数学公式的伟大目标又进了一步！ 6park.com
6park.com
6park.com数学证明真的是为大语言模型量身定制地任务，因为结果的有效性是可以完全确保的。 6park.com
6park.com
6park.com网友们除了狂赞这个项目对于数学研究的加速，纷纷脑洞大开，幻想了很多未来的可能性。 6park.com
6park.com
6park.comCue了马老板，数学的飞速发展将使得人类进入一个科幻小说中才存在的世界。 6park.com
6park.com
6park.com因为数学是科学之母，数学的飞速发展将导致所有的自然科学不断加速。 6park.com
6park.com数学将成为第一个看到人工智能实现重大突破的科学学科，这确实是有道理的。 6park.com
6park.com
6park.com作者介绍 6park.com
6park.comKaiyu Yang（杨凯峪） 6park.com
6park.com杨凯峪是加州理工学院计算+数学科学（CMS）系的博士后研究员，导师是Anima Anandkumar。他曾在普林斯顿大学获得了博士学位，导师是Jia Deng，还与Olga Russakovsky和陈丹琦一起工作。 6park.com
6park.com他的研究重点是神经符号人工智能，旨在使机器学习能够进行符号推理。 6park.com
6park.com杨凯峪是两个角度实现目标：（1）将机器学习应用于符号推理任务，如形式逻辑或自然语言中的数学推理和定理证明；（2）将符号组件引入机器学习模型，使其更具可解释性、可验证性和数据高效。 6park.com
6park.com目前，他正在研究能够理解和推理数学的人工智能。数学推理是人类智能的一个重要里程碑，它有可能改变科学和工程中的许多重要问题，比如解决偏微分方程和公式验证。 6park.com
6park.comAlex Gu 6park.com
6park.comAlex Gu是麻省理工学院的博士生，导师是Armando Solar-Lezama。在Armando和Jacob Andreas的指导下，他还在麻省理工学院获得了学士和硕士学位。 6park.com
6park.comAlex Gu曾在Meta AI Research、Jane Street和pony.ai实习。 6park.com
6park.comPeiyang Song 6park.com
6park.comPeiYang Song是加州大学圣巴巴拉分校（UCSB）创意研究学院（CCS）荣誉计算机科学学士候选人。 6park.com
6park.com研究兴趣包括机器学习及其在自然语言处理、计算机视觉中的应用，以及它与计算机架构、编程语言等的交叉。 6park.com
6park.com他最近的研究工作主要在两个方向：1）结合大语言模型（LLM）和交互式定理证明器（ITP）的神经定理证明和自动推理；2）节能机器学习推理的时序逻辑。 6park.com
请点这里投票，“赞”助支持！