一家成立时长还不到两个月的公司, 利用其自主研发的AI科研系统, 在一次性操作之中解决掉了量子信息领域内五道被搁置时间将近二十年的开放性难题。那篇论文、Lean形式化的证明过程以及验证代码这些内容, 都已经全部在GitHub上面公开了, 这一举动迅速地引发了学术界和科技圈的大量热议。
01.五道题一次性上线
PSI这个单位, 最近这几天, 已经在GitHub上面同步发布了五篇论文的文章内容以及对应的以Lean这种方式进行形式化的证明工作, 还有验证代码的具体实现细节。
这里所说的这些工作涉及到的内容有纠缠提纯这个方法、量子场论这一门学问、高维量子通信这项技术、量子信道容量这个概念以及量子因果律这一条规则。总共就是这五个核心的主要研究方向。可以确定的事实是, 以上所说的一切内容, 全部都是属于量子信息理论当中所面临的经典难题的情况。
其中, OQP 2这道题、OQP 12这道题、还有OQP 27这三道题, 是在本世纪初的时候, 就被编进目录里面去了。这些题目是学术界公认的高难度课题。在此以前的时候, 没有任何基于人工智能的系统性方法, 给出过完整的形式化证明。这一次的成果, 可以被视为在这个研究的方向上取得的第一个突破。
02.二十七年的开放问题目录
这个目录叫做开放量子问题目录, 它是由一个叫Reinhard Werner的人做出来的。这个人是德国的物理学家。他把这个目录建立出来, 是在1999年那个时候。这个目录专门收录那些事儿。
收录的是啥事儿呢? 是量子信息学界里有长期悬而未决的重要研究问题。这个目录到今天为止,已经持续运营二十七年了。在领域内大家公认这个目录重要。认可它是研究路线图。同时也认可它是选题依据。
PSI这一次, 一共选出了五道题目, 这五道题, 涉及了五个不同的子方向, 它们是在近年来头一批出现的, 形式化验证的事情完全由AI系统自己做完的, 并且把全部的代码公之于众的案例, 这是一个具有标志性的案例, 它用到的那种方法, 对今后的在科研活动里使用AI进行辅助这件事, 能够提供非常直接的参考意见。
03.创始团队与背景
PSI的创始人, 另外也是首席科学家的Alex Wissner-Gross, 这个人当年是麻省理工学院历史上最后一个同时修完了三个专业的本科生, 因为这样学校随后就取消了那个选项让他选。
他在二零零七年拿到了哈佛大学的物理学博士学位, 到了二零一三年, 他又在Tedx的活动上面, 用因果熵力这个理论来解释了智能行为它本身的本质是什么。
联合创始人兼总裁Alex Klokus, 这个人, 他是科技媒体Futurism的创始人。
他们两个人, 在今年二月的时候, 发表了一篇构想性的文章, 在这篇文章里提出了一项提议, 就是要把“世界最先进物理研究实验室”建立起来, 他们核心的这样一个愿景, 是让科学发现这件事从之前那种依靠天才去驱动的模式, 转向一种规模化的生产模式。
04.Emmy系统的验证逻辑
PSI这个机构自己研发出了名为Emmy的这个人工智能科研系统, 这个名字是用来致敬在20世纪当过数学家的那个叫艾米·诺特的女性的, 这个系统首先使用前沿的大模型, 去把那些非常大的物理难题拆解成非常多的可以验证的数学上的小假设, 然后再把这些小假设投入到一个叫Lean的证明器里面, 以及一个计算精度非常高的符号计算引擎之中, 来进行严格的筛查工作。
把报错的情况假设成当场淘汰, 接着让那通过了局部验证的路径继续衍生展开。最终Lean代码编译通过就代表该定理在数学逻辑上是无懈可击的。而且验证的结果还作为奖励信号, 持续训练下一代AI物理模型形成闭环。
05.从超算能效到星际飞船
PSI这一观点认为, 在人工智能时代推进科学研究的主要障碍并不是因为好的创新想法比较少, 而是缺乏能够扎实地验证真理真实性的能力。
而在商业应用领域方面, 名为Emmy的企业将会把为超级计算集群提供电力支持、处理热量散发、建立通信网络以及进行算力分配这些环节当作一个整体的物理方程式来进行计算求解, 从而试图突破物理层面的限制去摸索出能效比更高的解决方案。
公司方面已经对外宣布, 准备去运用那个经过优化处理之后的轻量化工程方案, 来建造一艘专门用于星际航行的飞船, 这个计划设定的目标是在八万年的时间期限内飞行并跨越4.2光年的距离最终抵达半人马座这个地方, 不过现在的情况是这份计划依然只停留在概念的阶段上面, 至于具体的预算还有发射的具体时间表以及参与这项工程的团队规模等相关信息都没有被公布出来。
你认为人工智能完成了形式化证明这件事, 在究竟是不是等同于人类对量子力学定理的真正的理解这个层面上, 大家的看法是怎样的。欢迎大家在这里发表自己的观点进行互动, 如果对你来说内容是有意思的, 请给出一个点赞的操作, 并且把这些内容分享给你的同行朋友们看一看。


