OpenAI“解题”风波：当AI证明遭遇数学界的信任危机

【科技24时区】本周，OpenAI高调发布了数百个号称能解决全球最棘手数学难题的方案。这家前沿实验室声称，为避免重蹈覆辙——此前其模型因解决领域内长期悬而未决的问题而引发争议——他们特意咨询了一个由精英数学家组成的顾问小组。然而，现实情况却远未达到既定标准，尤其是在数学家们反复强调的“人类对数学结果的理解”这一核心维度上，OpenAI的表现显得捉襟见肘。

令人担忧的是，一篇新近发表的论文揭示了自然语言表述与形式化表达之间的巨大鸿沟。该论文指出，在OpenAI模型看似解决的某个百万美元级别难题中，两者存在明显脱节。这并非危言耸听，而是对当前AI科研范式的一次深刻警示。

这个名为“数学与人工智能顾问小组”（AGMAI）的组织，依托于普林斯顿大学高等研究院，汇聚了来自全球机构的九位顶尖研究者。早在9月底，该组织便为前沿实验室解决数学问题制定了指导方针。针对此次OpenAI发布的最新证明集，AGMAI在声明中措辞谨慎：“最终，数学界将自行评估我们的建议在多大程度上得到了成功遵循。”值得注意的是，该组织的首要诉求本是“停止在专有模型上测试高级数学问题”，但OpenAI的发布说明明确表示，他们正在利用开放的数学研究问题来评估其专有模型。面对TechCrunch关于更深入评估的请求，顾问小组保持了沉默。

从表面看，OpenAI确实遵循了部分原则，比如尽快发布结果并披露模型得出结论的过程。但细节之处，破绽频出。在719份手稿中，仅有10份包含了模型的思维链（chain of thought）释放。对于普通人难以理解的论文，数学家建议应将证明形式化，然而OpenAI发布的证明中，高达58%未经过这一关键流程。换言之，超过四成的证明缺乏形式化验证，这使得“确保人类理解随之而来”的责任归属变得模糊不清。

AGMAI曾建议OpenAI资助人类数学家的工作，以使实验室的解决方案具有真正的现实意义。毕竟，正如著名数学家陶哲轩在社交媒体上所批评的那样：“问题正被那些对更广泛领域毫无兴趣的AI提示者自主解决，一旦初始目标‘达成’，他们便不再关心后续。这些人甚至无法充分理解AI的输出，以至于无法回答关于结果的问题、进行演讲或与领域内的其他人互动。”

这种困境在本周剑桥大学和伦敦国王学院数学家发布的一篇论文中得到了具象化体现。该论文质疑了前沿实验室应对这些挑战的方式。通常，AI模型在解决数学问题时，首先生成“自然语言”解释，随后尝试将其转化为Lean代码——一种理论上可通过编译确认证明准确性的编程语言。然而，模型在将自然语言证明翻译为代码的过程中可能出现偏差。这篇论文记录了至少两处不一致：在OpenAI提供的基于纳维-斯托克斯方程（描述流体复杂行为）衍生问题的解决方案中，自然语言证明与其背后的Lean代码存在出入。

这些差异未必直接证伪任一方案，但它们抛出了一个尖锐的问题：我们能否单纯依赖模型在没有人类介入的情况下自我形式化？这也正是AGMAI要求OpenAI“包含关联自然语言与形式化工件的机器可读元数据”的原因所在，而OpenAI在此次发布中并未做到这一点。“由于存在误译现象——正如本文所强调的——OpenAI的自然语言证明及其他自动形式化的Lean证明，不应在未经历与其他证明相同的同行评审和审查过程的情况下，被初步信任。”这篇题为“迷失在翻译中”的论文作者如此总结道。

数学家们强调，当人类发现新成果时，他们会通过论文、演讲和研讨会承担起责任并与更广泛的社区互动。这一过程不仅加深了对解决方案的理解，还发掘出可应用于其他问题的策略，并使新知识得以在实际领域落地。哈佛大学数学教授梅兰妮·伍德向TechCrunch坦言，当模型被提示去解决一个难题并吐出答案时，“在发布的那一刻，并不存在人类对它们的理解，而现在，真正的工作才刚刚开始。”