关于前沿AI模型是否能产出数学家此前并不掌握的数学成果,还是说它们只是速度极快的文献检索工具,这一直是今夏争论的焦点。周一,Anthropic发布了一份关于Claude数学能力的研究说明,称该模型一个尚未发布的研究版本改进了一项与黎曼猜想相关的长期结果,将一个已证明的下界从41.6%提高到67.2%。
黎曼猜想提出于1859年,是七个附带Clay Mathematics Institute 100万美元奖金的问题之一。该猜想认为,一个决定素数间距的函数的零点都位于同一条竖直线上。至今无人能证明对每一个零点都如此,因此数学家退而求其次,证明其中一部分满足这一性质。几十年来循序渐进的工作将这一比例提升到41.6%。这一新数字并不是通往证明的进度条,Anthropic也在同一份说明中表示,不预计Claude的技术会给出完整证明。
对投资者而言,更关键的细节是究竟哪个模型做到了这一点。Anthropic没有说明具体是哪个检查点版本,也没有发布模型权重,亦未向外界开放该系统。OpenAI在8月1日也做了同样的事,当时它公布了10个开放问题的解答,涉及数学和理论计算机科学,并将成果归功于Astra的一个内部版本,一个没有发布日期或价格的模型。如今,这两家实验室都把自己最强能力的主张建立在外界无人能够测试的系统之上。
这份说明发布的时间,也距离Anthropic上一次数学成果仅过去三周。7月,该公司数论学家Levent Alpöge发布了一个借助Claude Fable 5找到的反例,推翻了已有87年历史的雅可比猜想在三维及更高维度下的成立性;次日,Terence Tao公开推演了这一反例。Alpöge是随后继续核查该ζ函数结果的两位Anthropic数学家之一。
一位非数学家运行了这次会话
这段叙述中最受关注的部分是谁坐在键盘前。负责操作的员工Jarred Sumner并不是数学家,而Anthropic称,他把数学上的选择留给了模型。迄今为止,这类结果通常来自数学家用专家级提示来引导模型。Anthropic写道,在这次关键运行期间,Sumner的输入“基本上仅限于给Claude发送鼓励信息”,大多是“继续下去”或“相信自己”之类的变体。公司称,这似乎帮助模型克服了它自己早期对能否取得进展的怀疑。
计算过程本身则没那么精细。Claude在第一轮尝试了650个想法,但无一奏效。在被要求再试一次后,它花了大约一天半时间协调约60个自己的副本,Anthropic称之为“子代理”。它们合计运行了2,400条Shell命令,并编写了数百个Python脚本,用已知零点来检验候选论证。其中60个副本里有2个提出了关键想法,30个没有产出任何可用内容,而这两次会话总共消耗了3,100万个输出词元(token)——这是AI实验室据以计费的单位。
随后,Claude又对自己的结果发起检验,让“子代理”寻找反例、从arXiv预印本平台调取54篇论文以确认该发现具有新颖性,并从头重新推导。它还提议将这项工作写成论文,并建议由一位人类数论学家进行核查。
该结果尚未经过同行评审
Alpöge和Ralph Furman在Anthropic内部验证了这篇论文。应公司请求,Brian Conrey和Dan Goldston这两位数论该分支领域的专家也在很短时间内阅读了它。1989年,Conrey曾将这一同一下界推进到40%。但专家在短时间内过目,并不等同于期刊审稿;后者以月为单位推进,而不是按新闻周期运转。
Claude还给出了一个可由计算机检验的证明版本,使用Lean证明助手编写,并以公开代码库形式发布。这排除了那些让大多数著名难题“证明”失败的隐蔽逻辑漏洞。但这并不能证明形式化后的命题就是数论学家真正关心的那个命题,也无法说明生成它的模型本身。
还缺少一个数字。Anthropic披露了3,100万个输出词元(token),但没有给出美元成本,而由于该模型尚未发布,也没有公开费率可供相乘。OpenAI估计,其那10个证明背后的词元成本约为2,000美元。任何想判断这类研究是否已便宜到足以进行工业化规模运行的人,都需要看到Anthropic版本的这个数字。
在那之前,可检验的说法只有一个较窄的版本:一个需要被告知“继续下去”的模型,把人类数学家自Conrey结果以来37年间仅推进了1.6个百分点的下界,向前推到了新的水平。
