在人工智能领域，DeepMind一直处于创新前沿。从击败世界围棋冠军的AlphaGo到蛋白质结构预测的AlphaFold，DeepMind的AI系统不断突破人类能力的边界。如今，他们最新推出的AlphaProof系统在国际数学竞赛中取得了令人瞩目的成绩，标志着AI在数学推理领域迈出了重要一步。
突破：AI在数学竞赛中的银牌表现
2024年国际数学奥林匹克竞赛(IMO)上，DeepMind的AlphaProof系统展现了惊人的实力。在六道高难度数学问题中，AlphaProof成功解决了其中四道，获得了28分，与银牌得主的成绩持平，仅差一分即可获得金牌。这一成绩标志着AI首次能够在人类最高水平的数学竞赛中与顶尖人类选手一较高下。
"计算机在数字处理方面极为擅长，但它们还没有让多少人类数学家失业。"这一状况正在改变。AlphaProof的出现，意味着AI不再局限于简单的计算任务，而是开始涉足需要深度逻辑推理的数学领域。
理解数学：从计算到推理
传统计算机在数学竞赛中表现不佳的原因在于，虽然它们在计算速度上远超人类，但在高级数学所需的逻辑和推理能力上却相对薄弱。换句话说，计算机擅长快速执行计算，但通常不理解为何要执行这些计算。
数学家托马斯·休伯特(Thomas Hubert)指出："伯特兰·罗素曾出版了一本500页的书来证明1+1=2。"这一例子生动说明了数学证明的复杂性和深度。
AlphaProof的开发目标是让AI能够真正理解数学的结构和本质，而不仅仅是进行机械计算。这需要AI掌握数学证明的构建方式、步骤设计以及数学推理的优雅性。
形式化语言：数学问题的翻译
大型语言模型如ChatGPT从海量文本数据中学习，虽然包含数学相关内容，但其推理本质上是统计性的，只能生成"听起来正确"的答案，无法保证数学证明的绝对确定性。
DeepMind团队需要一个能够"真正正确"的AI系统，这要求采用全新的、更形式化的训练环境。为此，他们使用了名为Lean的软件包。
Lean是一个帮助数学家编写精确定义和证明的计算机程序，它使用一种精确的形式化编程语言，将数学语句转化为机器可处理的形式。一旦形式化语句被上传到程序中，它可以验证其正确性，并返回"正确"、"缺少内容"或"使用了未经证明的事实"等反馈。
然而，网上大多数数学陈述和证明都是以自然语言形式存在，用Lean编写的数量有限。"使用形式化语言的主要困难在于数据量极少，"休伯特解释道。
为了解决这一问题，研究人员训练了一个Gemini大型语言模型，将数学陈述从自然语言翻译为Lean。这个模型充当自动形式化器，产生了约8000万条形式化数学陈述。虽然不完美，但团队找到了利用这些近似翻译的方法。
学习思考：AlphaProof的架构设计
AlphaProof借鉴了DeepMind之前开发的AlphaZero系统架构，将数学证明构建视为一种需要掌握的"游戏"。"我们通过试错来学习这个游戏，"休伯特表示。
AlphaProof主要使用两个组件：
大型神经网络：拥有数十亿参数，通过试错学习在Lean环境中工作。每证明或证伪一个陈述都会获得奖励，而每一步推理都会受到惩罚，这促使系统生成简短、优雅的证明。
树搜索算法：探索所有可能的行动，推动证明向前发展。由于数学中的可能行动数量近乎无限，神经网络负责评估搜索树中的分支分支，并将计算资源分配给最有希望的方向。
经过几周训练，该系统在大多数基于高中竞赛题目的数学竞赛基准测试中表现良好，但在最困难的问题上仍存在挑战。
人性火花：测试时间强化学习
为了解决最困难的问题，团队添加了AlphaZero中未曾存在的第三个组件：测试时间强化学习(Test-Time Reinforcement Learning, TTRL)。
TTRL大致模拟了数学家处理最困难问题的方式。与依赖广泛数据库不同，AlphaProof在TTRL模式下首先基于当前问题生成全新的训练数据集。这个过程涉及创建原始陈述的无数变体——有些稍微简化，有些更一般化，有些仅与原始问题松散相关。然后系统尝试证明或证伪这些变体。
这类似于人类面对特别困难谜题时的做法："我不理解，所以让我们先尝试一个更简单的版本来练习。"这种方法使AlphaProof能够实时学习，效果显著。
成绩背后的代价
尽管AlphaProof在IMO上取得了银牌成绩，但这"银牌"是有代价的。首先，该系统并非独立工作——人类必须先将问题与Lean兼容化，软件才能开始工作。
在六道奥林匹克问题中，第四道是几何题，AlphaProof未针对此优化。为此，它调用了名为AlphaGeometry 2的几何专业AI助手，后者在几分钟内轻松解决了任务。单独计算，AlphaProof得分为21分，而非28分，理论上应获得铜牌而非银牌。
人类参赛者需要在两个4.5小时的会话中解决六个问题，而AlphaProof则使用多个张量处理单元全力工作了数天。最耗时耗能的组件是TTRL，它为解决的三个问题分别花费了三天时间。如果按照人类参赛者的标准衡量，AlphaProof基本上会耗尽时间。如果不是诞生于价值数千亿美元的技术巨头，它也会耗尽资金。
DeepMind团队在论文中承认，运行AlphaProof的计算要求可能对大多数研究机构和有抱负的数学家来说成本过高。AI应用中的计算能力通常以TPU-天衡量(即张量处理单元全天候运行一天)。AlphaProof每道问题需要数百TPU-天。
未来展望：从竞赛到研究级数学
尽管存在局限性，DeepMind相信可以克服这些障碍，优化AlphaProof使其资源消耗更少。"我们不希望停留在数学竞赛层面，我们希望建立一个真正能够贡献于研究级数学的AI系统，"休伯特表示。
他的目标是让AlphaProof对更广泛的研究社区可用。"我们还将发布一种AlphaProof工具，"他补充道，"这将是一个小型可信测试者计划，以评估这对数学家是否有用。"
国际数学奥林匹克竞赛是高中水平的竞赛，虽然题目确实困难，但基于数学家已知的知识。研究级数学需要发明全新概念，而不仅仅是使用现有概念。
技术影响：数学研究的范式转变
AlphaProof的出现代表了数学研究范式的潜在转变。传统上，数学研究依赖于人类直觉、创造力和多年积累的经验。AI系统的引入可能带来以下影响：
辅助证明验证：AI可以快速检查复杂证明的每一步，减少人为错误的可能性。
猜想生成：通过分析大量数学数据，AI可能提出新的猜想或研究方向。
跨领域连接：AI能够发现不同数学领域间的隐藏联系，促进跨学科研究。
教育革新：AI可以成为数学学习的强大工具，为学生提供个性化的指导和即时反馈。
伦理考量：AI与数学的未来
随着AI在数学领域的能力不断提升，一些伦理和哲学问题也随之浮现：
原创性问题：如果AI能够解决数学难题，这些成果的归属权应如何界定？
人类技能价值：当AI能够执行复杂的数学推理时，人类数学家的独特价值体现在何处？
可及性差距：先进AI工具可能加剧数学研究资源的不平等分配，如何确保公平获取？
理解vs.性能：AI可能在解决问题时缺乏真正的理解，这是否会影响数学作为人类智力追求的本质？
结论：AI与数学的共生关系
AlphaProof代表了AI在数学推理领域的重要里程碑，但它不是终点，而是起点。正如休伯特所强调的，DeepMind的目标是构建能够真正贡献于研究级数学的AI系统。
未来，AI不太可能取代数学家，而是会成为强大的合作伙伴，扩展人类思维的能力边界。数学研究将进入人机协作的新时代，AI处理计算密集型任务和探索广阔可能性空间，而人类则专注于创造性思维、概念创新和方向设定。
随着技术的不断进步和优化，我们可以期待AlphaProof及其后续系统能够在资源消耗、问题理解和创新潜力方面取得进一步突破，为数学科学的发展开辟新的可能性。
