1000万美元 AI 数学奥林匹克奖

原文 ↗ Hacker News 讨论 ↗

一项新的 1000 万美元奖金，旨在打造能够在国际数学奥林匹克中获得金牌的 AI 系统，引发了关于当前模型距离真正高水平数学推理还有多远的讨论。评论者将常规的符号操作与创造性的证明发现进行对比，把这一目标与 Netflix Prize 和千禧年难题等过去的挑战相比较，并探讨将 LLM 与形式化证明助手结合是否能缩小差距。讨论还涉及数学作为人类职业的更广泛影响、开放模型的价值，以及这样一个系统是更适合私有化获利还是为了一次性奖项而公开发布。

奖项构想与目标

  • 设立一项 1000 万美元奖金，奖励一个能够用自然语言题目和解答赢得 IMO 金牌的 AI 系统（“非形式化到非形式化”）。
  • 许多人认为它类似 Netflix Prize：一个能够吸引众多团队并加速 AI 数学推理进展的聚焦性挑战。
  • 赞助方强调开放性：第一个公开共享的模型将获得主要奖项。

可行性与时间线

  • 乐观者：LLM + 强化学习可能在 1–5 年内达到 IMO 金牌水平；有人认为艺术/图像领域的进展表明，看似困难的领域也可能迅速发生转变。
  • 悲观者：当前系统仍然难以处理学校数学和基本精确计算；谈论千禧年大奖问题或深度研究被视为为时过早。
  • 线程中引用的类似 Metaculus 的预测大多集中在 4–5 年达到 IMO 级别性能，但参与者强调不确定性很高。

当前 AI 的数学能力与局限

  • GPT‑4 能解析并复述奥赛风格的问题，有时也能识别有用模式（例如，猜测某个示例 IMO 问题只有素数幂能够满足）。
  • 然而，它经常犯基本的逻辑或算术错误，写出同义反复式的“证明”，或者即使有提示也无法完成非平凡论证。
  • 在分析题和竞赛题中的例子表明，它可以模仿教科书风格，但往往缺乏连贯、端到端的推理能力。

形式化方法 vs 自然语言推理

  • 另一个正在进行的独立努力（IMO Grand Challenge）专注于“形式到形式”的 Lean 问题；AI MO Prize 面向人类风格的陈述和证明。
  • 有人认为先解决形式到形式是正确路径；也有人认为非形式化推理是一个不同且更难的挑战。
  • 当前的定理证明器和 ML 辅助工具只能解决极少一部分形式化后的奥赛问题。

对数学与职业的影响

  • 一些家长和学生担心 AI 数学求解器会削弱数学作为一种人类职业的地位。
  • 另一些人则反驳说：
    • 大多数数学毕业生本来就不会从事纯数学工作。
    • 新工具可能增加对受过数学训练的人的需求，类似编译器如何增加了对程序员的需求。
    • 人类仍然需要来选择有趣的问题并解释结果。

激励、开放性与经济价值

  • 讨论焦点还包括：考虑到以下因素，1000 万美元是否有意义：
    • 训练这样一个模型的成本可能更高。
    • 一个成功系统的价值可能达到数亿美元甚至更多。
  • 回应包括：
    • 该奖项主要激励学术界和开放研究者，而不是追求利润最大化的公司。
    • 有些人即使放弃专有利润，也会为了社会利益公开发布这样的模型。

其他提议与旁支话题

  • 关于基于区块链的证明悬赏，与更简单的中心化/加密替代方案的想法；许多人认为区块链是不必要的额外开销。
  • 讨论将这种系统用于算法交易；共识是奥赛式能力和交易优势相当不同。
  • 有几条评论提到网站分散注意力的动画背景，认为其 UX 很差。