陶哲轩对 o1 的点评：更强大，但是在处理最复杂的数学研究任务还不够好，就像指导一个水平一般但不算太无能的研究生。

https://t.co/HMJkEFit3S

我体验了一下 OpenAI 最新版本的 GPT，即 GPT-o1，它在运行大语言模型 (LLM) 之前会进行一个初步的推理步骤。与之前的版本相比，它确实是一个更强大的工具，但在处理最复杂的数学研究任务时仍然表现不佳。

以下是我使用获得访问权限的模型原型进行的一些具体实验。在 https://t.co/qQoDiQpVkc 中，我重复了这个实验 https://t.co/24nsEm1GRM ，询问 GPT 解决一个措辞模糊的数学问题，该问题可以通过查找文献中的合适定理（克拉默定理）来解决。此前，GPT 能提到一些相关概念，但细节部分是凭空捏造的胡言乱语。而这次，GPT 正确识别了克拉默定理，并给出了一个完全令人满意的答案。

在另一个实验 https://t.co/EU9PmRHNqC 中，我给新模型提供了一个复杂的分析问题（此前我曾在这个实验 https://t.co/SlNb8c9NyI 中要求 GPT-4 帮助撰写证明）。结果比之前的模型有所改善，但仍有些令人失望：新模型在有大量提示和推动的情况下能够得出正确且书写良好的解决方案，但无法独立生成关键的概念，并且还犯了一些非微不足道的错误。体验类似于指导一个水平一般但不算太无能的研究生。不过，这确实比之前的模型有了进步，之前的模型能力更接近于一个真正无能的研究生。再经过一两次能力的迭代改进（并与其他工具整合，如计算代数软件和证明助理），它可能达到“称职的研究生”水平，届时这个工具在研究任务中可能会有显著的应用价值。

作为第三个实验，我要求新模型在此链接 https://t.co/BCzCtaRC5y 中，开始将一个结果形式化到 Lean 中（特别是通过子引理来建立一种素数定理的形式作为另一种形式的结果），其中它只会形式化陈述而不是证明。结果很有前景，模型理解了任务并进行了合理的初步问题分解，但由于其训练中缺乏关于 Lean 及其数学库的最新信息，代码中出现了几个错误。不过，我可以想象如果有一个专门针对 Lean 和 Mathlib 进行微调并集成到 IDE 中的模型，它在形式化项目中将会非常有用。

点击图片查看原图

点击图片查看原图

点击图片查看原图