谷歌AI拿下IMO奥数银牌，数学推理模型AlphaProof面世，强化学习 is so back
内容提要
谷歌DeepMind的人工智能通过AI系统参加了国际数学奥林匹克竞赛IMO，并获得了28分的银牌水平。AI系统由AlphaProof和AlphaGeometry 2组成，通过形式化数学推理和几何求解解决了多个问题。这一突破表明具有先进数学推理能力的通用人工智能有潜力开启科学技术新领域。
延伸解读
AI 数学推理的里程碑意义
谷歌 DeepMind 的 AI 系统在 IMO 中获得银牌，标志着 AI 在高级数学推理上取得重大突破。IMO 题目需要创造性思维和严密证明，AI 能解决其中四道，包括最难题，说明其推理能力接近人类顶尖选手。这为 AGI 在科学发现中的应用提供了可能。
强化学习与形式化方法的结合
AlphaProof 将预训练语言模型与 AlphaZero 强化学习算法结合，在 Lean 形式语言中生成和验证证明。这种方法利用形式化验证确保正确性，同时通过自我对弈提升能力。团队中多位 AlphaGo 核心成员参与，显示强化学习在复杂推理任务中的回归。
实际表现与限制
尽管 AI 在几分钟内解决了一个问题，但其他问题耗时三天，远超人类 4.5 小时的限制。这提示当前系统在效率上仍有不足，可能依赖大量计算。此外，问题需手动翻译为形式语言，自动化程度有限，距离完全自主解题还有差距。
几何求解的显著进步
AlphaGeometry 2 在几何问题上表现突出，解决了过去 25 年 IMO 几何题的 83%，远超前代 53%。其在 19 秒内解决今年问题 4，展示了神经-符号混合系统的潜力。这为未来 AI 辅助数学研究提供了实用工具。
Q&A
谷歌的AI在国际数学奥林匹克竞赛中获得了什么成绩？
谷歌的AI在国际数学奥林匹克竞赛中获得了28分，达到了银牌水平。
AlphaProof和AlphaGeometry 2分别是什么？
AlphaProof是用于形式化数学推理的强化学习系统，AlphaGeometry 2是改进的几何求解系统。
AI系统在解决数学问题时的表现如何？
AI系统在几分钟内解决了一个问题，但其他问题花费了三天时间。
国际数学奥林匹克竞赛的意义是什么？
IMO被广泛认为是衡量人工智能系统高级数学推理能力的理想基准。
AlphaProof是如何训练的？
AlphaProof通过证明或反证明数百万个数学问题进行训练，并使用强化学习算法不断提高能力。
AlphaGeometry 2相比于前一版本有什么改进？
AlphaGeometry 2在解决几何问题的速度和准确性上有显著提高，解决率从53%提升到83%。
