OpenAI宣称下一代AI模型解决了10个世界级难题,其中包括推翻了Connes刚性猜想。
第二天,就有一篇人类论文回应:AI提出的反例不成立。
作者是堪萨斯大学拓扑物理中心的J. L. Nielsen,他把OpenAI公开的37000行Lean 4代码从头追到尾,把每一个对象对回它的数学原型,最后给出两条互相独立的失败路径。
具体的证明过程咱一般人也看不太懂,让AI和数学家神仙打架去吧。
但通过这件事,说明人类对AI科研结果的审查仍然很关键。
什么是Connes刚性猜想
Connes刚性猜想说的是这样一件事。
数学上可以给一个群配一套代数结构。有时候两个长得不一样的群,配出来的结构却完全一样。
Connes在1980年左右提出猜测:只要这个群满足两个附加条件,这种情况就不会发生,结构一样,群就必须一样。
这两个附加条件,一个叫ICC,一个叫Kazhdan性质(T)。
换句话说,想反驳这个猜想,需要举出满足两个条件,但构造不一样的群。
OpenAI新模型的做法是构造两个不同构的群,让它们生成同样的代数,并给出两个群都满足ICC和性质(T)的证明。
整套论证写成37000行Lean 4代码,由Lean内核逐条验证通过,另外附了一份说明文档,解释这两个群是怎么搭出来的。
Nielsen指出:AI构造的其中一个群,其实没有满足附加条件,既不是ICC,也没有性质(T)。
这其中有三种可能:
代码里性质(T)没有忠实对应Kazhdan的原始定义;或者证明只对部分成立,却被算到了整个群上;又或者代码里那个群根本不是说明文档里描述的样子。
37000行,逐行对号
为了验证这个结论,Nielsen还做了一件更费力的事。
公开发布的代码是一个整合成单文件的版本,早期分模块源码里的那些名字全都不见了。
他于是列了一张对照表,把每个数学对象在新代码里的名字和行号一一标出:
零上闭链群在第13700行,扭曲群在第14069行,两套代数同构的证明在第36712行,主定理在第36954行。
他还把代码证明ICC的整条推理链追了一遍。这条链从第31430行起步,一层层往上传递,最后在第31610行合成结论。
Nielsen指出的问题是,这些引理处理的是经过对偶变换之后的对象,不是原来那个带中心元素的群,因此并没有直接覆盖到关键的那部分元素。
至于它们是否对最终进入定理的那个具体的群里每一个元素都成立,取决于两块构造之间的接口怎么对接。
这说明“要证什么”就出了问题,不是“证得对不对”的问题。Lean只负责验证后者。
对于另一个扭曲的群,Nielsen的态度是保守的。他说自己没有从代码里独立核实它到底满不满足ICC,也承认代码里的引理有可能确实证明了它满足,但那不改变结论,已经有一个条件不满足。
他把自己的两条反驳也写成了Lean代码,在Lean 4.32.2下编译。
机器检查的是形式,不是意思
论文最后一节把这件事放进了一个更大的背景。
Lean内核能保证的事情,只是一段证明在形式上严丝合缝,但不负责是否真的能证明原结论。
这里可以直接引用陶哲轩的说法:验证证明的是形式陈述本身,而不是这个陈述和意图相符,所以人类的审查不能直接被取代。
过去这类事故已经有记录。
一份针对五个常用Lean基准的审计给出了4833条发现,包括反例、空洞定理和不可靠公理,全都通过了机器验证。最后是人类构造出反例,才发现被证明的那句话本身是错的。
在统计学习理论的形式化工作中,最危险情形被描述为“不是一个失败的证明,而是一个对错误陈述的成功证明”。
张量网络方面的研究也记录过同类现象:系统给出的证明形式上完全正确,只是它证的那个命题比预期的要弱。
Nielsen写道,OpenAI那份形式化可能把它声称的每一条结论都建立对了。但它没有建立、Lean内核也检查不了的,是这些结论和猜想的原话有没有关系。
人读猜想会看到前提,证明助手拿到一个不满足前提的结论,会照样验证关于它的任何断言。
Connes刚性猜想仍然开放。
论文地址:
https://philarchive.org/archive/NIEWTCv17
参考链接:
[1]https://openai.com/index/ten-advances-in-mathematics/
[2]https://github.com/openai/ten-proofs/blob/main/ConnesRigidity.lean
本文来自微信公众号“量子位”,作者:梦晨
