PSI用Anthropic模型证明量子计算猜想

物理超智能实验室PSI称，其利用一款尚未公开的Anthropic模型，在3天内找到了量子计算领域“阿伦森—安拜尼斯猜想”的证明。 该猜想自2008年提出以来一直悬而未决，涉及量子计算机在何种情况下能够大幅快于传统计算机。 PSI已经公开论文和证明代码，并称证明通过了数学证明辅助工具Lean的检验。 此前研究过这一问题的斯坦福大学学者已阅读证明并提供意见，但成果仍有待学界进一步独立审查。 这项研究使用的系统由PSI技术人员大卫·图尔图里安开发，在实验室自有基础设施上运行，调用了Anthropic尚未公开的模型。

PSI没有披露具体模型名称。 PSI表示，研究系统在运行的第3天给出了完整证明，随后又对结果进行了两次改进，最终版本也通过了Lean检验。 根据PSI公开的项目说明，数学陈述、论文初稿和形式化证明均由AI模型生成。 图尔图里安对论文进行了审阅，并对其正确性负责。 阿伦森—安拜尼斯猜想由计算机科学家斯科特·阿伦森和安德里斯·安拜尼斯提出，关注量子计算优势的边界。 PSI介绍，如果这一证明成立，对于特定的二选一计算问题，在大多数随机输入上，量子计算机读取输入的次数相较传统计算机无法获得指数级优势。

这意味着，某些显著的量子加速依赖问题或输入中存在特殊结构。 这里讨论的是算法读取输入的次数，不能直接等同于现实设备的总运行时间。 这一结论并不意味着量子计算失去价值。 PSI举例称，彼得·肖尔于1994年提出的量子算法利用问题中的特定结构，在大整数分解方面远快于已知的传统计算方法。 PSI称，斯坦福大学研究人员盖伊·布兰克、乔丹·多克特、卡门·斯特拉斯勒和李扬·谭此前已在一个特殊情况下解决了相关问题。 四人正在阅读PSI的完整证明，并准备为专业人士撰写一份更简洁的说明。

他们在给PSI的反馈中称，这是一项“重大成果”。 独立研究追踪平台State of Proof表示，PSI公开的Lean检验记录为审查提供了材料，但该平台尚未独立重现检验，也未确认研究已完成期刊同行评审。