姚顺雨拿50年数学难题成绩单,招人了
By 一水

AI 摘要
AI for Science方向
原文正文
姚顺雨拿50年数学难题成绩单,招人了
AI for Science方向
姚顺雨,亲自下场给腾讯混元招人了!
这次瞄准的,是AI for Science(以下简称AI4S)方向的人才。
不过,大佬招人就是不一样。
详细JD(职位描述),对不起,没有。
有的只是一句「混元AI4S正在招人了 :)」+一张图。
就这?凭什么认为一张图,就能把AI4S人才「钓」过来?
仔细一看,好家伙,还真有硬货。
图片展示的,是一张腾讯混元AI刚刚交出的科研成绩单:
一个困扰数学家约50年、长期没有取得突破的开放问题,被自研智能体Hyra推进到了新的最好结果。
所以,姚顺雨的潜台词也很明确了:
我们的AI已经开始自己搞科研了,现在,需要更多人来扩大战果。
Hyra解决了怎样的难题
先快速过一下Hyra这次做了什么。
根据混元官方最新介绍,基于本月开源的Hy3模型(总参数295B、激活参数21B):
Hyra找到了一个关键构造,为加法组合学中一个悬而未决半个多世纪的开放问题给出了完整答案。
把问题中译中一下,其实要解决的就是:
给你一组整数,任意挑出两个做加法,可以得到多少种不同答案?把加法换成减法,又能得到多少种?
比如同样一组数字,有些数字相加会不断产生新结果,相减却经常得到重复答案。
于是数学家开始追问:
能不能设计出一组特殊数字,让加法产生的不同结果,远远多于减法?最多又能多到什么程度?
此前的数学理论已经划出了一条上限——
加法结果的增长速度,最多接近减法结果的平方。
但问题在于,这条上限究竟只是一个宽松的估计,还是确实可以无限逼近?
这就像工程师算出,一列高铁的速度绝不会超过350公里每小时。
但「不能超过350」,不代表它真的能跑到350附近,它的实际极限,也可能只有200公里每小时。
数学家争论了50多年的问题就是:
350到底是真正可以逼近的极限,还是一个画得太高的上限?
半个多世纪里,数学家不断设计新的数字集合,尝试逼近这条上限。
1969年的结果约为1.0290,1973年提高到1.0598,2013年又推进至1.1259。
近一年来,多项AI辅助搜索将纪录提高到1.1449,Codex在有人类引导的实验中进一步做到了1.2851。
而Hyra给出的,不只是又高了一点的新纪录。
它找到了一整套可以不断扩展的数字构造,并证明随着集合规模增大,结果能够无限接近理论上限2。
就是说,那条看似遥不可及的上限,真的可以无限逼近。
与此同时,混元官方强调:
更关键的是,这不是一次单纯的暴力搜索。
Hyra先在有限范围内试出了更好的结果,随后转向用自然语言提出数学构造和论证。
经过约24小时运行,它找到了论文的核心思路。
研究团队随后独立检查并整理出完整证明,还给出了一份Lean 4形式化证明,让计算机逐步核验推导过程。