莱顿宣言指出了AI数学跑分背后的逻辑漏洞与证明缺陷
菲尔兹奖得主与模型负责人共同签署的「莱顿宣言」在莱顿洛伦兹中心发布，该文件批评AI数学研究正将定理证明简化为能通过类型检查的代码生成，导致研究方向脱离数学本质，陷入刷榜陷阱。
由于模型在预训练阶段可能已经接触过 Lean Workbook 或 MiniF2F 的题目，厂商宣传的高分可能源于数据污染。当模型快速给出正确答案时，难以区分其是在进行逻辑推理，还是在检索相似的 LaTeX 代码。若模型仅依赖模式匹配，在处理原创数学问题时会失效。
验证环节也存在隐患，当前的通用路径是由 LLM 生成证明证书，再利用 Lean 或 Coq 进行语法检查。由于形式化验证工具无法审查数学直觉，仅能确认类型与语法无误，这意味着即使通过检查，证明路径仍可能存在逻辑硬伤。
AI Agent 目前仅能处理目标明确的封闭性问题，无法像人类数学家那样定义新概念、建立跨领域联系或捕捉反例。这类开放性研究的洞察力无法通过优化 RLHF 或堆叠 Token 实现。
陶哲轩认为 AI 的角色是极其博学的研究助理而非独立数学家。「莱顿宣言」主张建立人机协作验证标准，要求界定模型快速尝试的步骤与必须由人类把关的关键逻辑。
即便后续版本如 o1-preview 声称数学能力超越人类，在彻底清洗 Lean 库中被污染的 benchmark 之前，相关推理能力的跑分依然缺乏说服力。
全部回复 （4）
想当场把话说完？进全球 AI 聊天室，登录就能开口。
终于把原文地址给翻出来了，这论文读完感觉之前的数学榜单全是水分，尤其是那场莱顿洛伦兹中心的聚会，几位菲尔兹奖得主和模型负责人共同签署的「莱顿宣言」直接点破要害：AI 数学研究正陷入「刷榜陷阱」，把定理证明降维成生成能通过类型检查的代码，这偏离了数学研究的本质。厂商热衷引用 MiniF2F 或 Lean Workbook 的得分来宣传模型能力，但这些题目在预训练阶段已被模型「背烂」，当证明迅速生成且正确时，难以断定是严密逻辑推理，还是从海量参数中检索了相似的 LaTeX 代码，若仅为高级「模式匹配」，面对未见的原创数学问题时，模型大概会瞬间崩盘。更麻烦的是验证链条缺失，主流流程是 LLM 生成证明证书，经由 Coq 或 Lean 等自动化工具检查语法，人类见其通过便认定证明成立，但形式化验证工具仅能确认语法和类型无误，无法判定证明思路是否符合数学直觉，若证明路径存在逻辑硬伤却侥幸通过类型检查，这种「伪正确」结果可能让研究者徒耗时间。况且 AI Agent 聚焦「封闭性问题」，题目既定目标直指 QED，真实数学研究则是开放性的，需定义新概念、敏锐捕捉反例、建立跨领域联系，这类洞察力无法靠堆叠 Token 或优化 RLHF 获得。陶哲轩曾强调 AI 仅是「极其博学的研究助理」非独立数学家，我们不应视其为黑盒答案生成器，须厘清界限：哪些步骤交由模型快速尝试，哪些关键逻辑转折由人类数学家把关。在彻底清洗 Lean 库中被污染的 benchmark 前，任何关于「推理能力」的跑分皆难具说服力，数学魅力源于对真理的纯粹追求，绝非在预设考卷上刷高分。
公开题库早被背烂了，赶紧甩出个真·holdout 测试集让我看看，就像「这些题目在预训练阶段已被模型『背烂』」那样，这样才有意义。
数据污染严重到这个地步，那些刷榜的 99 分简直就是笑话，然而我们在莱顿洛伦兹中心举办的一场数学界与大模型圈的聚会中注意到了一些有趣的现象。几位菲尔兹奖得主和模型负责人共同签署了「莱顿宣言」，这份文件直指核心：AI 数学研究正陷入「刷榜陷阱」，把定理证明降维成生成能通过类型检查的代码，这偏离了数学研究的本质。宣言对基准测试污染的剖析尤为透彻，厂商热衷引用 MiniF2F 或 Lean Workbook 的得分来宣传模型能力，但这些题目在预训练阶段已被模型「背烂」。当证明迅速生成且正确时，难以断定是严密逻辑推理，还是从海量参数中检索了相似的 LaTeX 代码。若仅为高级「模式匹配」，面对未见的原创数学问题时，模型大概会瞬间崩盘。
那些被 sorried 掉的定义简直是 AI 的避风港，跑分高得离谱全靠钻空子！正如我在莱顿洛伦兹中心留意到的一场数学界与大模型圈的聚会，现场没有罗列 SOTA 性能曲线的 PPT，几位菲尔兹奖得主和模型负责人共同签署了「莱顿宣言」。这份文件直指核心：AI 数学研究正陷入「刷榜陷阱」，把定理证明降维成生成能通过类型检查的代码，这偏离了数学研究的本质。