https://www.qbitai.com/2024/09/191241.html 在研究数学层面的实用性正在增加 白小交衡宇发自凹非寺 好羡慕！原来早在8月份，陶哲轩就已经用了OpenAI o1。 还是现在大家都用不上的满血版本（眼泪不争气地从嘴角流出来）。 提前批大佬是怎麽玩最新天花板的呢？ 他向o1模型 提出一个措辞模糊的数学问题，发现它竟然能成功辨识出克莱姆定理 。 而且答案是「完全令人满意的」那种。 当然，陶哲轩也做了一些其它测试，肉测下来整体体验就是： 比以前的模型更牛，多堆点提示词表现还不错，但还是会犯不小的错误，也没有产生啥自 己的思想。 陶哲轩是这样形容的： 这种感觉， 就像是给一个平庸无奇但又有点小能力的研究生建议 。 不过，这已经比以前的模型有所改进，因为以前的模型的能力更接近实际上不称职的研究 生。 但如果给以前的模型加点助力，例如电脑代数包和证明辅助工具啥的，改进一两次，就能 实现进一步迭代，摇身一变，成为「有能力的研究生」。 陶哲轩对使用体验的这个神奇比喻在HackerNews等多个平台引起了激烈讨论。 有网友愤愤：GPT是什麽**！我承认LLMs对写入程式码有很大帮助，但事实上有一些非常 好的工具可以帮助解决这个问题，例如程式码片段、模板和程式码产生器。 有人就用陶哲轩的话回应了他： “任何聪明到足以以程式设计为生的人，智商都足以成为一个平平无奇但又小有能力的数 学研究生。” 陶哲轩实测ChatGPT vs o1 陶哲轩展示了他自己的三轮测试。 第一轮，用去年3月份测试ChatGPT的题目，要求大模型回答一个措辞含糊的数学问题 ， 只要从文献中找出一个适当的定理（克莱姆法则）就能解决。 假设我有一个正测度，其闭包（支持度）=某个紧凑凸子集 S。缩小n，取对数，除以 n，取极限以获得S上的一些舍入的东西。 当时，ChatGPT倒是有模有样地回答了，期间还提到了一个高度相关的术语：对数矩生成 函数，甚至在给出的答案中还讨论了一个具体的例子。不过不能注意细节，全是幻觉，而 且答案也是错的。 这次，同样有模有样，但相较之下更有条理（更长还有大小标题区分度）。 最重要的是，o1成功找到了克莱姆定理，并给出了完全令人满意的答案。 ps，看纪录，早在8月陶哲轩就用上了o1。 第二轮，上一点难度，挑战复杂分析研究生课程的一个问题。 （之前他用来测试GPT-4的，请他来协助写一个证明） 结果这次陶哲轩的结论是，是要比之前GPT-4好些，但仍有点失望。 如果提供大量的提示和鼓励，新模型可以透过自己的努力得到一个正确的（而且写得 很好的）解决方案，但它自己并没有产生关键的概念想法，而且确实犯了一些非同小可的 错误。 光看到这几轮提示交互，确实是有点不满意的。 也难怪陶哲轩代入自己， 把调教o1像是在教一个平庸、但又不是完全不称职的研究生。 紧接着来第三轮测试，这次是要求将质数定理的一种形式转化为Lean中的定理形式，方法 是将其分解为若干个子问题分别描述，但不给出证明。 结果模型很好地理解了这个任务，并进行了 合理 的初步分解，不过程式码中出现了几个 小错误。 陶哲轩解释道，这是由於训练时缺乏有关Lean及其数学库的最新资讯。 并表示，如果能专门针对Lean和Mathlib进行微调，并整合到一个IDE中，应该会对公式化 专案很有用。 在研究数学层面的实用性正在增加 用大模型来搞研究，其实已经飞进寻常百姓家了。 一位帐号名为wenc的网友分享了ta使用大模型来做研究的经验。 wenc从事运筹学相关的工作，而OpenAI的模型们，从GPT 4o开始，就吸收了足够多的运筹 学数据，能够输出很多非常有用的混合整数规划（MIP） 公式。 举个栗子： 给4o一个逻辑问题，例如“我需要根据分数将i个项目放入n个桶中，但我想按顺序填充每 个桶”，4o会输出一个非常有用的数学公式。 通常情况下， 只要把公式微调一下 就能完全搞定问题了。 此外， 有些prompt太弱了的时候，4o还会预警：这可能导致输出不尽如人意 ——可以说 对避免无效回答非常有用了。 回过头看咱还用不上大模型的时候，传统方法是需要大家在周末绞尽脑汁，试图找出有关 MIP优化问题的无懈可击的公式。 对於非直觉问题来说，这一点通常都令人头秃。 wenc很坚定地表示， 每月从ChatGPT上获得的价值，远远超出了20美元 （每月订阅费用 ）。 一旦GPT在Lean上得到更多调整——就像在Python 上一样——我预计它在研究数学层 面的实用性会有提升。 wenc也对那些抱怨Claude和GPT最新模型不好用的网友进行了分析： 不知道如何最大化自己的优势来使用大模型们； 把大模型想得无所不能，抱着「这玩意儿是解决一切的灵丹妙药」的期待； 大模型确实在他们的领域不适用。 wenc在最後弱弱补了一句，很多抱怨的人，其实都是属於前两种啦～～～ 陶哲轩回应争议 尽管大多数网友都觉得大模型能帮助自己省下许多功夫，还是有人对陶哲轩「调教大模型 如同调教不咋靠谱的研究生」的言论，充满了疑惑和不解。 有网友在陶哲轩的mathstodon底下留言： 亲，也许你可以展开说说「研究生」这块不？ 我理解一下子， 你的意思是o1之前大模型放在Lean微调，再结合电脑代数包，那输 出效果就可以媲美研究生程度？ 简单点来说，这种情况下的大模型能够解决一些新发现的重要课题？ 陶哲轩倒是很及时回覆了这则评论。 他表示，他正在考虑一个具体的指标，即「助手能够在专家数学家的指导下，协助完成复 杂数学研究计画中的一个或多个具体任务」的程度。 一个有能力的研究生可以为这样的计画作出贡献，而这种贡献比「让学生加快计画进度并 监督他们出了几成力」更有价值。 不过，即使使用最新的工具，让大模型输出正确且有用的回答，其实比输入精准prompt和 验证结果都要难多了——当然，这之间的差距并不是特别巨大，前者大概要难个2-5倍的 样子。 陶哲轩表示自己有理由相信，未来几年内，这个差距会降低到1倍以内（其实有些特定子 任务，比如语义搜索、数据格式化或生成数字代码以协助数学研究探索，这个比率已经低 於1了）。 他视「差距降到1倍以内」为数学领域将更广泛采用这些的转折点。 至於「研究生程度」嘛—— 陶哲轩表示，自己这麽说，只是为了方便大家感知啦！ 虽然大模型可以协助研究人员完成目前的项目，但培养研究生的目的，是为了以後有更多 的下一代独立研究者。 “我无意暗示研究生学习的各个方面，与数学中AI辅助的各个方面之间存在一一对应的关 系。” 还有一件事 最後，分享一则陶哲轩这个话题下，我们发现网友讨论出的、呼声挺高的一个结论—— 虽然很难量化学会用大模型到底省了多少时间，但随着一个人提示词工程能力的提升，大 夥儿能用更少的时间得到更好的效果。 但是！ 显而易见， 大模型的价值是因人而异的，它几乎取决於每个人的提示词等级。 呃，羞愧中… 不说了，过什麽中秋节假期，咱这就去精进自己的prompt技巧去！ 参考连结： [1]https://mathstodon.xyz/@tao/113132502735585408 [2]https://news.ycombinator.com/item?id=41540902 [3]https://mathstodon.xyz/@tao/109948249160170335 --

※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 111.253.149.41 (台湾) ※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1726464318.A.36C.html