7.3
深览指数
科技腾讯新闻·环球科学··AI 生成
科学家相信了30年的假说，发过数百篇论文，可能被OpenAI证伪了
OpenAI于10月26日发布论文《指数时间假说是错误的》，称其AI系统在亚指数时间内解决了3-SAT精确计数问题，若成立将直接推翻计算机科学沿用近30年的ETH假说。文章梳理了ETH的由来——1998年Impagliazzo等人提出该假说，此后数百篇论文以其为前提推导计算下界——并指出Lean形式化验证只能检查命题本身、无法保证定义与假设恰当，结果远未获学界公认。作者还记录了审查机制的争议：OpenAI请ETH提出者组织核查，AGMAI则公开反对AI公司挑选少数数学家优先解读成果。原文 ↗
核心观点
- ▍OpenAI声称其AI找到亚指数时间算法精确统计3-SAT解的数量，若成立将直接与ETH假说冲突，但结果尚未通过独立审查，远不能称ETH已被推翻。
- 011998年Impagliazzo、Paturi与Zane在IEEE FOCS发表论文提出ETH：面对3-SAT，总存在足够刁钻的实例，使任何通用算法都无法在亚指数时间内求解。
- 02ETH作为条件性假设被广泛使用：研究人员以它为起点推导地图着色、数据库、计算生物学等问题的计算下界，估计已有数百篇论文以ETH为前提。
- 03OpenAI称AI在10月16日生成自然语言证明，次日完成Lean形式化验证；但Lean所验证的时间上界比论文主要结果稍弱，且形式化证明与原始问题的对应关系仍需人类审视。
- 04ETH提出者Impagliazzo本人早在2012年就表示学界对ETH真假并无共识，且无论真假都能帮助理解其他问题的计算难度。
- 05即使ETH被证伪，建立在它之上的数百篇论文也不会作废：它们多为条件性命题，前提被否定后推理逻辑仍成立，只是不能再断言某种算法真的不存在。
- 06OpenAI邀请Impagliazzo、Paturi和MIT的Ryan Williams组织审查，三人声明未签保密协议、不收报酬，并要求OpenAI公开论文与Lean代码、出资支持学界讨论会议，OpenAI已同意。
- 0710月25日，Timothy Gowers、Martin Hairer等组成的AGMAI发表声明，反对由AI公司挑选少数学者优先解读新成果，认为这会造成信息不平等并借科学家声誉为未充分审查的发现背书。
反方 / 局限
- — Lean只能验证写给它的命题是否得到证明，不能保证形式化证明准确对应原始问题、所用定义与假设是否恰当——这是AI数学成果验证的核心盲区。
- — AGMAI对OpenAI同日声称的局部平滑猜想和四维量子场论突破提出公开材料要求，显示AI公司主导的成果发布机制本身正受到学界质疑。
- — 文章未交代OpenAI新算法的具体构造与思路，读者无法判断其亚指数时间界限的强弱，也无法评估该结果对ETH的实际威胁程度。
指数时间假说（ETH）布尔可满足性问题（SAT / 3-SAT）拉塞尔·因帕利亚佐（Russell Impagliazzo）拉马莫汉·帕图里（Ramamohan Paturi）瑞安·威廉姆斯（Ryan Williams）OpenAILean形式化验证数学与人工智能咨询小组（AGMAI）蒂莫西·高尔斯（Timothy Gowers）马丁·海雷尔（Martin Hairer）《指数时间假说是错误的》论文《量子杂志》（Quanta Magazine）
12 分钟 · 6 卡片 · 16 资料
读原文 →