AI达到国际数学奥林匹克竞赛银牌标准解题水平

某研究机构推出基于强化学习的数学推理系统AlphaProof和几何解题系统AlphaGeometry 2。这两个系统共同解决了今年国际数学奥林匹克竞赛（IMO）六道题目中的四道，首次达到竞赛银牌得主水平。

突破性AI性能解决复杂数学问题

IMO是自1959年起每年举办的全球最具声望的青年数学竞赛。今年，该AI系统应对由IMO组委会提供的竞赛题目，解题方案由著名数学家按照IMO评分规则进行评定。

系统首先将问题人工翻译为形式化数学语言。在官方竞赛中，学生需在两个4.5小时的时段内提交答案，而AI系统在几分钟内解决了一道题，最长耗时三天解决其他题目。AlphaProof解决了两道代数题和一道数论题（包括本届IMO只有五名选手解决的最难题），AlphaGeometry 2证明了一道几何题，两道组合题未能解决。

六道题每题最高7分，总分42分。该系统最终获得28分，在已解题上均获满分——相当于银牌类别高端水平。本届竞赛金牌门槛为29分，609名选手中58人达到。

AlphaProof：形式化推理方法

AlphaProof是在形式化语言Lean中训练自我证明数学陈述的系统。它将预训练语言模型与AlphaZero强化学习算法结合，该算法曾自学掌握国际象棋、将棋和围棋。

形式化语言的关键优势在于数学推理证明可被形式化验证正确性。但此前在机器学习中的应用受限于有限的人工编写数据。相比之下，基于自然语言的方法可能产生看似合理但错误的中间推理步骤。

通过微调Gemini模型自动将自然语言问题陈述翻译为形式化陈述，创建了包含不同难度形式化问题的大型库。面对问题时，AlphaProof生成候选解决方案，通过在Lean中搜索可能的证明步骤来证明或反驳。每个找到并验证的证明都用于增强AlphaProof的语言模型。

为备战IMO，AlphaProof在数周时间内证明或反驳了数百万道覆盖不同难度和数学主题的问题。训练循环也在竞赛期间应用，强化自生成的竞赛问题变体证明直至找到完整解决方案。

更具竞争力的AlphaGeometry 2

AlphaGeometry 2是显著改进的版本，作为神经符号混合系统，其语言模型基于Gemini，并使用比前代多一个数量级的合成数据从头训练。这帮助模型应对更复杂的几何问题，包括物体移动和角度、比例或距离方程问题。

AlphaGeometry 2采用的符号引擎比前代快两个数量级。面对新问题时，使用新颖的知识共享机制实现不同搜索树的高级组合以处理更复杂问题。

在本届竞赛前，AlphaGeometry 2能解决过去25年所有IMO几何题的83%（前代为53%）。对于IMO 2024，AlphaGeometry 2在收到形式化表述后19秒内解决了第4题。

数学推理的新前沿

作为IMO工作的一部分，还实验了基于Gemini的自然语言推理系统，不需要将问题翻译为形式化语言，并可与其他AI系统结合。在今年IMO问题上的测试结果显示出巨大潜力。

团队继续探索多种AI方法推进数学推理，计划很快发布AlphaProof的更多技术细节。期待数学家与AI工具合作探索假设、尝试解决长期问题的新方法，并快速完成证明的耗时环节，使AI系统在数学和更广泛推理方面更强大。