加州理工华人用AI颠覆数学证明！提速5倍震惊陶哲轩，80%数学步骤全自动化

创作时间:

作者:

@小白创作中心

加州理工华人用AI颠覆数学证明！提速5倍震惊陶哲轩，80%数学步骤全自动化

引用

澎湃

https://m.thepaper.cn/newsDetail_forward_27132801

加州理工学院团队近日发布了Lean Copilot工具的扩展版本，该工具能够自动化完成80%以上的数学证明步骤，这一突破性进展在数学界引起了广泛关注。

Lean Copilot是一个用于辅助人类编写形式化数学证明的工具，它解决了在Lean中运行LLM推理的关键技术挑战。通过这个工具，可以让LLM在Lean中提出证明策略，并允许人类以无缝的方式干预和修改。

为什么开发Lean Copilot？

自动化定理证明一直是数学领域的一个重要挑战。虽然LLM在数学和推理任务中表现出一定的能力，但它们时常会犯错误、产生幻觉，因此到目前为止，数学证明大多是手动推导的，需要仔细验证。像Lean这样的定理证明工具，虽然可以形式化证明过程的每一步，但人类编写起来却十分费力。在这种情况下，Lean Copilot的诞生就显得意义重大。

Lean Copilot的核心功能

Lean Copilot构建了一些工具，用于建议证明步骤（策略建议）、完成中间证明目标（证明搜索）和使用LLM选择相关前提（前提选择）。实验结果表明，与Lean中现有的基于规则的证明自动化相比，Lean Copilot在辅助人类自动化定理证明上是有效的。

生成策略建议

Lean Copilot可以生成策略建议，当用户输入suggest_tropics时，会在右边看到策略建议。第一个策略显示为绿色，表示证明已成功完成。接下来的建议均为蓝色，表明无法直接完成证明，但不会导致错误，它们很有可能是有效的中间证明步骤。

搜索完整证明

此外，Lean Copilot还构建了一个基于LLM的证明搜索工具。对于图3中的原始目标，用户只需输入search_prrof，找到可以解决目标的完整证明，就显示在了信息视图中。

选择注释好的前提

定理证明中另一项具有挑战性的重要任务是，找到减少或完成证明的相关前提。Lean Copilot通过高效的矩阵乘法库和C++的numpy矩阵阅读器，可以快速选择相关前提。

实验结果

研究团队在两种情况下验证了基于LLM的搜索证明与aesop相比的有效性：

自主证明定理（LLM独立完成）
协助人类进行定理证明（人类与AI协作）

实验结果显示，证明搜索可以自动完成定理中约81.2%的证明步骤，明显高于策略建议（48.6%）和aesop（35.2%）。证明搜索的性能比策略建议高出1.67倍，比基于规则的基线aesop高2.31倍。

技术实现

Lean Copilot通过外部功能接口(FFI)在Lean中本地运行LLM。默认情况下，采用LeanDojo预训练的repver模型，该模型基于一个编码器-解码器转换器BVT5。Lean Copilot通过将模型包装成一个对字符串操作的c++函数，使其在Lean中可运行，该函数可以通过FFI在精益中调用。