当OpenAI本周发布数百份据称解决了世界最难数学问题的答案时，这家前沿实验室表示，他们已经咨询了一个由顶尖数学家组成的咨询团队，以避免此前该公司某款模型解决一个长期存在的数学难题时所引发的争议再次重演。
但OpenAI的做法仍未达到这些专业标准，尤其是在数学家们强调需要人类理解数学结果这一点上。这一点格外令人担忧，因为一篇新论文指出，在OpenAI模型所称解决的一个百万美元难题中，自然语言解答与形式化解答之间存在明显差距。
由普林斯顿高等研究院主办的数学与人工智能咨询小组（AGMAI），由来自全球各机构的九位知名研究人员组成。
该组织在九月底发布了针对前沿实验室解决数学问题的指导方针。在针对最新一批证明的声明中，AGMAI表示："最终应由数学界来评估我们的建议被遵循的程度。"
然而，该组织提出的第一项要求便是"停止在专有模型上测试高难度数学问题"。而OpenAI的发布说明中明确表示，他们正是在用开放的数学研究问题来评估其专有模型。
当TechCrunch请该咨询小组对OpenAI最新发布的证明进行更详细评估时，该组织没有做出回应。这家实验室确实遵循了部分原则，例如尽快发布结果并提供模型得出结论的相关信息。但并非所有原则都得到了遵守：在719份手稿中，只有10份公开了模型的思维链过程。
对于人们难以理解的证明，数学家们建议应将其形式化处理——但OpenAI发布的证明中，仍有42%没有经过这一处理过程。
归根结底，目前仍不清楚OpenAI是否按照AGMAI的原则，在发布证明时真正"承担起确保人类理解能够随之而来的责任"。AGMAI建议，OpenAI应该资助人类数学家的工作，因为正是这些数学家才能让该实验室的解答在现实中具有真正的意义。
"这些问题正在被那些对更广泛领域本身毫无兴趣的AI操作者自主解决，一旦最初的目标被'解决'，他们便不再关心该领域，也无法充分理解AI的输出结果，以至于无法回答相关问题、作学术报告，或与该领域的其他人进行有效交流，"知名数学家陶哲轩在OpenAI发布结果后于社交媒体上写道，他此前已多次批评OpenAI的做法。
剑桥大学和伦敦国王学院的数学家本周发布的一篇论文，恰恰印证了这一问题，该论文质疑了前沿实验室处理这类难题的方式。
当AI模型解决数学问题时，它们首先会给出一个"自然语言"解释，然后尝试用Lean（一种编程语言）来表达这一结果，理论上通过将证明编译为代码来确认其准确性。
然而，模型将自然语言证明转化为代码的过程可能存在问题；这篇论文记录了至少两处不一致之处，涉及OpenAI针对一个源自纳维-斯托克斯方程（描述流体复杂行为的方程）衍生问题所给出的解答中，自然语言证明与背后Lean代码之间的差异。
这些不一致之处并不一定能证明两种解答中的任何一个是错误的，但它们确实引发了一个问题：我们是否可以仅仅依赖模型自行将解答形式化，而不需要人类的参与。这正是AGMAI要求OpenAI"提供能够关联自然语言与形式化成果的机器可读元数据"的原因之一，但这家前沿实验室在此次发布中并未这样做。
"由于存在翻译错误的现象——正如本文所强调的那样——OpenAI的自然语言证明以及其他经过自动形式化处理的Lean证明，在未经过与其他证明同等的同行评审和审查之前，不应被想当然地信任，"这篇"翻译中迷失"论文的作者们总结道。
数学家们强调，当人类发现新的研究成果时，他们会对这些成果负责，并通过论文、演讲和研讨会与更广泛的学术界进行交流。这一过程能够加深对解答的理解，找到可用于解决其他问题的策略，并使这些新知识能够应用于实际领域。
当一个模型被要求解决一个难题并给出解答时，"在发布的那一刻，人类并没有真正理解这些结果，而真正的工作才刚刚开始，"哈佛大学数学教授梅兰妮·伍德对TechCrunch表示。
Q&A
Q1：AGMAI对OpenAI的数学证明发布提出了哪些主要批评？
A：AGMAI批评OpenAI未能完全遵循其发布的指导方针，包括仍在专有模型上测试高难度数学问题、仅公开少量模型思维链、未对多数证明进行形式化处理，以及没有确保人类对结果的理解能够跟进。
Q2：为什么自然语言证明与Lean代码之间的差异值得关注？
A：剑桥大学和伦敦国王学院的研究人员发现，OpenAI针对纳维-斯托克斯方程相关问题的解答中，自然语言证明与其对应的Lean代码之间存在至少两处不一致，这表明模型自动形式化证明的过程可能存在翻译错误，不应未经同行评审就被直接信任。
Q3：陶哲轩对AI解决数学问题的方式有什么看法？
A：陶哲轩批评称，一些AI操作者在问题被"解决"后便对该领域失去兴趣，也不够理解AI给出的结果，以至于无法回答相关问题、作学术报告或与数学界其他人进行有效交流，这不利于真正的知识积累和传播。
