marquez 发表于 2024-7-31 20:05

Google DeepMind 新 AI 系统能在数学奥林匹克竞赛中取得银牌

Google DeepMind 新 AI 系统 AlphaProof 和 A​​lphaGeometry 2 能在 2024 年国际数学奥林匹克(IMO)竞赛获得银牌，解决了六道题中的四道，获得了 28/42 分，标志着 AI 在数学推理方面取得重大突破。IMO 是历史最悠久、规模最大、最负盛名的青年数学家竞赛，自 1959 年以来每年举办一次。选手要解决代数、组合学、几何和数论方面六个异常困难的问题。DeepMind 表示，IMO 的数学问题被人工翻译成数学语言，供系统理解。在正式比赛中，学生们分两次提交答案，每次 4.5 小时。而 AI 系统在几分钟内解决了一个问题，花了三天时间解决其他问题。基于强化学习的推理系统 AlphaProof 解决了两个代数问题和一个数论问题并被证明答案正确，这些问题包括今年 IMO 比赛中只有 5 名选手解决的最难的问题。AlphaGeometry 2 证明了几何问题，但两个组合问题仍未解决。

https://www.solidot.org/story?sid=78807
https://deepmind.google/discover ... silver-medal-level/
https://news.sciencenet.cn/htmlnews/2024/7/527125.shtm

已经是上周的旧闻了，然而搜了一下泥潭居然没人发？感觉是有趣的事情发一下

jojog 发表于 2024-7-31 20:07

>花了三天时间解决其他问题

这个改prompt的人自己怕不是已经解出来了吧
不然咋能算3天的，跑都把自己跑死了

beckuse 发表于 2024-7-31 20:24

玩玩而已 发表于 2024-7-31 20:28

说明奥数就是种复杂的智力游戏

囧Smith 发表于 2024-7-31 20:57

beckuse 发表于 2024-7-31 20:24
所以，9.11和9.9哪个大？
事实证明，现阶段的AI并没有什么逻辑推理能力，就是跟预设的算法和训练数据有关。 ...

deep mind和目前炒的火的语言大模型走的不是一个路子

logiccat 发表于 2024-7-31 20:58

beckuse 发表于 2024-7-31 20:24
所以，9.11和9.9哪个大？
事实证明，现阶段的AI并没有什么逻辑推理能力，就是跟预设的算法和训练数据有关。 ...

9.11和9.9这个是GPT模型的语义理解错误，这次用的这个不是GPT模型……

即使是GPT模型，在加载了各种辅助数学模型之后也能很好的理解数学语言和符号……

铃森冬 发表于 2024-7-31 23:08

本帖最后由 铃森冬 于 2024-7-31 23:13 编辑

不知道为啥讨论度不高，感觉算是大模型在推理任务上有一定里程碑意义的工作了，简单补充下自己了解的内容

光靠 prompt engineering 想做出 IMO 题现在应该还是几乎完全没戏的，大语言模型很难自己分辨出哪些中间结论是正确而且有价值的，之前阿赛 AI 组做初赛题好像全倒闭了足以说明问题

AlphaProof 这个工作最像的还是 16 年的 AlphaGo，粗看新闻很容易忽略的一点是模型输出的题解并不是自然语言证明，而是基于形式化语言 LEAN 的可被计算机检验的证明，可以理解成某种由编程语言描述的证明，这么做的好处是可以在 LEAN 提供的定理证明环境内进行有效的搜索跟，跟下棋有点像只不过搜索空间更开放想判断目前推的方向对不对也更困难，虽然搜了三天能搜出有效的证明也很了不起了

当然实际上用的还是大语言模型，应该是在 Gemini 1.5 上微调的，用的数据是另外的模型做了百万量级的应该是偏数竞范围内的数学问题形式化成的 LEAN 代码，也是 Deepmind 一贯的找对方向然后大力出奇迹的路子，最重要意义就是证明这个技术路线跑的通

据说马斯克也在搞类似的事，画的大饼是希望能靠这个训练大语言模型在复杂推理任务上的通用认知能力，主要是光靠正常的语料很难要求模型学到这方面技能所以现在的大语言模型才普遍缺乏逻辑推理能力，当然这点子靠不靠谱就另说了

b0207191 发表于 2025-1-10 19:17

跑题问下， 不同于自然语言， 数学题在形式上比较丰富，几何证明有直线曲线，代数题有各种复杂的数学符号，   先不说ai能否解答出来，   怎么把数学题按标准化输入给ai，这个是我好奇的地方

overflowal 发表于 2025-1-10 19:29

b0207191 发表于 2025-1-10 19:17
跑题问下， 不同于自然语言， 数学题在形式上比较丰富，几何证明有直线曲线，代数题有各种复杂的数学符号 ...

原样喂呗，公式用latex表示就好，甚至直接喂图片都行

—— 来自 鹅球 v3.3.96

even001 发表于 2025-1-10 20:10

b0207191 发表于 2025-1-10 19:17
跑题问下， 不同于自然语言， 数学题在形式上比较丰富，几何证明有直线曲线，代数题有各种复杂的数学符号 ...

lean语言

b0207191 发表于 2025-1-10 23:53

even001 发表于 2025-1-10 20:10
lean语言

我搜了下，几何证明不是使用这个，是用另外一个系统
https://news.qq.com/rain/a/20240227A01W0100

另外，lean好像是逻辑证明类的，代数类也不是用这个吧，比如证明代数不等式，求代数式最小值这种类型题目
页: [1]
查看完整版本: Google DeepMind 新 AI 系统能在数学奥林匹克竞赛中取得银牌