本周，OpenAI发布了数百个据称针对困难数学问题的解答，试图展示其模型处理高级问题的能力。但这次发布并未完全遵循由数学研究人员组成的咨询小组制定的指导方针，从而再次引发一个根本问题：模型能够生成一个可形式化为程序的解答是否就足够了，还是说，该解答还必须能够被数学家理解并审查？
数学与人工智能咨询小组（Advisory Group on Mathematics and Artificial Intelligence，AGMAI）由九名杰出研究人员组成，由普林斯顿大学高等研究院承办。该小组在9月底发布了面向开发高级数学问题求解模型的实验室的指导方针。
对研究人员指导方针的部分遵循
AGMAI指出，评估对其建议的遵循程度，最终应由数学界负责。其最重要的建议之一，是停止使用商业专有模型测试高级数学问题；而OpenAI明确表示，它使用开放研究问题来评估自己的模型。
OpenAI遵循了部分原则，例如迅速发布结果，并提供有关模型如何得出结论的信息。然而，在719份文稿中，只有10份包含模型的思维链。此外，已发布的证明中有42%未经过形式化。
该小组认为，人类难以理解的证明应当转换为正式形式。但它也强调，实验室有责任确保结果发布时附带人类对这些结果的理解，并建议资助数学家，帮助使这些结果真正具有科学意义。
自然语言与Lean代码之间的差距
模型通常先用自然语言生成解释，然后尝试将其转换为Lean。Lean是一种编程语言，其编译器可以确认证明在可执行形式下的一致性。然而，自动转换可能会改变证明的内容，或造成解释所说内容与代码所证明内容之间的脱节。
剑桥大学和伦敦国王学院的数学家发表的一篇论文记录了自然语言证明与相关Lean代码之间至少两处差异；这两者对应于OpenAI针对一个源自Navier-Stokes方程、涉及复杂流体行为的问题所提供的解答。这些差异并不一定证明其中任何一个解答是错误的，但它们使人们对完全不经人工干预、让模型负责正式表述自身解答的做法产生了疑问。
AGMAI还要求纳入可由机器读取的元数据，用于关联文本证明与正式版本；OpenAI在这些版本中并未提供此类元数据。这篇被称为“lost in translation”的论文的作者得出结论认为，文本证明和自动转换的Lean证明原则上不应在未经同行评审、也未经过与其他证明相类似的审查之前被接受。
为什么这则消息很重要？
问题不仅在于证明代码能够成功编译，还在于证明代码确实代表了文本所解释的数学思想。在传统研究中，科学家对自己的成果负责，并通过论文、讲座和研讨会对其进行讨论；这一过程有助于发现错误，也有助于理解可重复使用的方法。
而当模型为一个困难问题生成解答时，发布之际可能并不存在这种人类理解。因此，OpenAI目前的成果看起来更接近科学验证过程的起点，而不是问题的终点；在这些证明被数学界采纳之前，人工审查以及建立文本输出与正式输出之间的关联，仍是两个有待满足的条件。