陶哲轩初步玩了一会儿 OpenAI 的 o1，它在运行 LLM 之前会执行一个初始推理步骤。陶哲轩认为与之前的迭代版本相比，它无疑是一个能力更强的工具，不过在处理最先进的数学研究任务时，它仍然显得有些吃力

照例先给大家划划重点：

o1 确实比之前的模型更强， 但解决最前沿的数学研究问题还很困难

o1 现在能找到合适的定理来回答问题了， 比如陶哲轩之前问过的一个问题，o1 成功找到了 Cramer 定理并给出了令人满意的答案

解决复杂分析问题的能力有所提升，但还是令人失望。 o1 只有在给出大量提示的情况下才能找到正确答案，而且还会犯一些错误。它的水平大概相当于一个“平庸但不完全无能”的研究生

o1 能理解形式化证明的任务，并能进行初步的分解， 在形式化证明方面很有潜力，但需要进行专门的微调和集成

以下是原文：

我稍微试用了下 OpenAI 的新版本 GPT，即 GPT-o1，它在运行大语言模型（LLM）之前会先进行初步的推理步骤。相比之前的迭代版本，该模型显然更加强大，但在处理最复杂的数学研究任务时依然存在一些挑战。

这里是一些具体实验（我获得了该模型原型版本的访问权限）。在 https://chatgpt.com/share/2ecd7b73-3607-46b3-b855-b29003333b87 中，我重复了 https://mathstodon.xyz/@tao/109948249160170335 的实验，我要求 GPT 回答一个表述含糊不清的数学问题，这个问题可以通过从文献中找到合适的定理（克莱默定理）来解决。之前，GPT 虽提到了一些相关概念，但细节部分却是凭空捏造的无稽之谈。而这次，GPT 识别了克莱默定理，并给出了非常令人满意的解答。

在 https://chatgpt.com/share/94152e76-7511-4943-9d99-1118267f4b2b 中，我给了新模型一个复杂分析问题的挑战（此前我在 https://chatgpt.com/share/63c5774a-d58a-47c2-9149-362b05e268b4 中曾让 GPT4 协助编写这个问题的证明）。结果虽然比之前的模型有所提升，但仍然略显令人失望：新模型在大量提示和引导下能够得出正确且写得不错的解答，但它没能自主生成关键的概念性思路，还犯了几个明显的错误。感觉就像在指导一个能力平平但不至于毫无能力的研究生。不过，这已经比之前的模型有所改进，之前的模型更像是一个完全无能的研究生。再经过一两次能力的提升（并且与其他工具如计算代数包和证明助手结合），模型可能就能达到“合格研究生”的水平。到那时，我可以预见这个工具将在研究级别的任务中发挥显著作用。

作为第三个实验，我要求新模型开始在 Lean 中形式化一个结果的任务（具体是通过一种形式的素数定理推导出另一种形式），让它把问题分解为子引理并形式化这些引理的陈述，但不包括证明。结果令人鼓舞，因为模型理解了任务，并对问题进行了合理的初步分解，但由于缺乏关于 Lean 和它的数学库的最新训练数据，生成的代码中存在一些错误。不过，我可以想象，一个经过专门微调的 Lean 和 Mathlib 模型，集成到 IDE 中后，将在形式化项目中极具实用性。