文章摘要
【关 键 词】 AlphaProof、AlphaGeometry、数学竞赛、AI推理、智能挑战
谷歌DeepMind的人工智能系统在国际数学奥林匹克竞赛（IMO）中取得了显著成绩，其中AI系统AlphaProof和AlphaGeometry 2成功完成了6道题目中的4道，获得了相当于银牌的最高分28分，仅差1分即可获得金牌。这一成绩在609名参赛选手中表现突出，其中只有58人获得了金牌。
AlphaProof是一个基于强化学习的形式数学推理系统，能够在Lean的形式化语言中证明数学命题。它结合了预训练的大语言模型和AlphaZero强化学习算法，通过微调Gemini模型将自然语言问题陈述自动翻译成形式化陈述，建立了一个包含不同难度的形式化问题的大型库。AlphaProof在解题时会生成候选解决方案，并通过在Lean中搜索可能的证明步骤来证明或反驳它们，每个被找到并验证的证明都被用于强化其语言模型。
AlphaGeometry 2是一个神经符号混合系统，基于Gemini的语言模型从头开始训练，能够解决难度更高的几何问题。它采用了比前一代快两个数量级的符号引擎，并采用了新颖的知识共享机制，使不同搜索树的高级组合能够解决更复杂的问题。在IMO中，AlphaGeometry 2在接收到形式化问题的19秒内就完成了一道题目的解答，展现了惊人的速度。
AI的数学推理能力得到了著名数学家Timothy Gowers教授和Joseph Myers博士的高度评价。Gowers教授表示，AI能够提出非显而易见的解法，远超出他对当前技术水平的预期。然而，尽管AI在解决数学问题上取得了突破，但在一些基本问题上仍然存在挑战。例如，一些大型模型在回答“9.11和9.9哪个数字更大”这样的问题时可能会出错。这表明，尽管AI在特定领域表现出色，但在通用智能方面仍有待提高。
总的来说，谷歌DeepMind的AI系统在国际数学奥林匹克竞赛中的表现证明了其在数学推理和解题方面的强大能力。这一突破不仅展示了AI在解决专业竞赛问题上的潜力，也为未来AI在更广泛领域的应用提供了新的可能性。同时，这也提醒我们，AI的发展仍需在通用智能方面进行更多的探索和研究。
原文和模型
【原文链接】 阅读原文 [ 2840字 | 12分钟 ]
【原文作者】 新智元
【摘要模型】 moonshot-v1-32k
【摘要评分】 ★★★★★
