首页 > 科技快讯 > 陶哲轩点评OpenAI o1 :像指导一个水平一般但不算太无能的研究生

陶哲轩点评OpenAI o1 :像指导一个水平一般但不算太无能的研究生

来源:AI寒武纪

陶哲轩初步玩了一会儿 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 中后,将在形式化项目中极具实用性。

发布于:北京

相关推荐

陶哲轩点评OpenAI o1 :像指导一个水平一般但不算太无能的研究生
陶哲轩发文缅怀数学家约翰·康威:他将游戏变成了研究
陶哲轩用了“满血”GPT-4:人类对信息技术的期待需要校准
“编程作为一个职业在今日终结”,OpenAI新模型o1的可怕之处
陶哲轩用AI证明数学猜想实乃误读,但数学界仍大受震动
面对数学史上最简单的未解之谜,陶哲轩给出了几十年来最重要的证明
Open AI发布新一代大模型“o1”:会像人类一样“花时间思考”
OpenAI最强模型o1,仍分不出“9.11和9.8哪个大”
重磅!颠覆AI领域!OpenAI发布o1模型,解锁博士级科学难题
OpenAI震撼发布新模型,Sam Altman:耐心时刻结束了

网址: 陶哲轩点评OpenAI o1 :像指导一个水平一般但不算太无能的研究生 http://m.xishuta.com/newsview125355.html

所属分类:行业热点