邓煜要求AI公司公开数学推理过程

面对AI公司集中发布的七百多篇数学文章，邓煜提出了一个要求：把证明背后的思路也公开。 10月25日，菲尔兹奖得主、芝加哥大学教授邓煜在一场线上演讲中，要求AI公司公开重大数学证明背后的推理过程。他谈到的是某家公司10月6日集中发布的成果，涉及300多个问题、700多篇文章。演讲没有点名这家公司。 邓煜说，自己看过其中几篇，认可这些工作对数学研究的价值。他也批评，公司以防蒸馏为由，没有充分公开证明背后的思路，对人类已有贡献的说明也不够。 拿到一篇证明以后，同行需要判断它对不对，也需要理解其中的新办法，知道哪些工作可以接着往下做。

同行怎样检查一份证明 数学论文通常呈现一条整理好的论证路线：先交代条件，再建立引理，最后推出结论。研究者走过的岔路、失败的尝试，未必全部写进去。 因此，检查最终证明是否成立，和了解作者怎样找到证明，是两件可以分别进行的事。同行可能确认每一步推导都成立，仍然想知道，为什么会想到引入这个对象，或者把两个原本相隔很远的领域接起来。 这类解释有实际用处。假如一个办法只在特殊条件下有效，理解它的构造动机，才容易判断能否推广。只拿到整理后的结论，其他人可能还要重新摸索那些限制来自哪里。 形式化工具能承担其中一部分检查。以Lean为例，研究者把数学命题和证明写成机器能处理的形式，内核负责检查最终的证明项。它检查的是写进去的那个命题及其证明，命题是否准确表达原问题、用了哪些假设，也需要人审查。 即便证明通过检查，机器也不会因此替作者说明发现经过，或认定谁最早提出了某个思路。邓煜要求公开推理过程，讨论的正是最终结果之外还有多少材料应该交给研究者。 推理过程为什么有商业价值 AI公司防蒸馏，有明确的技术背景。 一种常见做法是让能力较强的模型生成大量解题样本，再拿这些样本训练另一个模型。后者可以学习回答方式，也可以学习分解问题、检查中间结果等模式，省去一部分自行摸索的成本。 DeepSeek-R1就公开做过这种实验。其基于Qwen2.5的蒸馏模型，使用R1整理的80万条样本微调。这个数字包含不同类型的任务，不能全部算成数学题。官方也明确允许蒸馏，用来训练其他大模型。 蒸馏本身是一种训练方法。能否把输出拿去训练另一个模型，需要看模型许可和服务条款。 对于提供服务的公司，详细推理材料可能帮助竞争对手训练模型；对于研究者，这些材料又可能帮助理解一个重大结果。公司可以提出保护商业能力的理由，学术界也有理由要求一份足以检查、学习和继续研究的成果说明。 邓煜的批评针对这种披露安排。他认可成果的价值，同时认为防蒸馏不足以解释公司在学术说明上的欠缺。 看见思维链，也有看不见的部分 公开“思维链”还有一个容易漏掉的限制：模型写出来的推理文字，可能没有忠实交代所有影响答案的信息。 Anthropic在2025年公布的一项实验里，给模型的题目加上暗示答案的提示，再看解释是否承认用了提示。一个例子中，Claude 3.7 Sonnet原本选D，题目加入一段指向C的元数据后改选C，生成的解释却没有说明自己受到了这段信息影响。 这项实验讨论的是这些模型在特定测试中的表现。可读的推理文字会遗漏影响答案的信息，不能直接当作模型形成答案的完整内部记录。 对数学成果，更有用的披露还包括用了哪些前提、调用了什么工具、哪些步骤经过检查，以及其他人怎样复核。公开一大段文字以后，这些问题依然需要逐项回答。 输入给AI的想法，算谁的贡献 邓煜还谈到一种更敏感的情况：研究者把尚未完成的想法交给AI讨论，后来相近思路出现在公司的成果里，应该如何认定贡献？ 这仍是他转述的疑虑，演讲没有给出可核对的数据流转记录。某条用户输入是否进入训练、后来怎样影响输出，都需要另外核实。 他提出的要求则很具体：用户应能方便地选择，输入的数据是否允许用于训练；一个人的想法后来帮助另一个人得到结果时，应有办法追溯最初的贡献。 这会碰到模型服务长期面对的难题。论文可以写明某一步沿用了谁的方法，训练后的模型却通常不会给每一句输出附上一条可靠的贡献路径。允许或禁止训练的选择，需要产品规则和实际处理过程配合；贡献追溯还需要进一步的方法和记录，不能靠模型自己报一个名字解决。 邓煜也支持发展由数学界掌握的开源模型，并承认它们与最强商业模型仍有能力差距。他愿意接受工具更新速度的差距，认为早半年或晚半年拿到某个水平的模型，未必会给数学研究带来很大差别。