https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/ 一年一度的国际奥林匹克数学竞赛（IMO）是最负盛名的高中数学竞赛，每年的IMO会设有 6道代数、几何、数论以及组合学方面的题目。 近来，IMO被认为是机器学习领域的重要 挑战，可用於衡量人工智慧（AI）系统的高级数学推理能力，这种能力对实现通用人工智 慧（AGI）很重要。 Google的DeepMind公司在今年年初推出了AlphaGeometry，该模型擅 长解决几何证明题，已逼近人类金牌选手的水平，但无法应对几何之外的代数、数论等问 题。 7月25日， DeepMind宣布推出基於强化学习、可用於形式数学推理的AlphaProof， 以及改进的几何证明模型AlphaGeometry 2。 这两个系统共同解决了今年IMO6题目中的4 道，首次达到了人类银牌选手的水准 。 相较於上一代AlphaGeometry，DeepMind基於Gemini重新训练了AlphaGeometry 2用到的语 言模型，并优化了符号引擎，提升了它解决复杂几何问题的能力和效率。 对於IMO 2024 的问题4，AlphaGeometry 2只用19秒便给了答案。 AlphaProof则结合了预先训练的语言 模型与强化学习演算法AlphaZero（通用棋类AI），并接受了一种名为Lean的形式化语言 的训练。 其中，Lean是一种互动式定理证明语言，可用来检验数学证明的可靠性。 因此 用它训练的模型可以避免自然语言训练常出现的看似合理但不正确的答案。 对於IMO 2024的题目，AlphaProof花了三天时间解决了两道代数问题，和一道数论问题，包括比赛 中最难的、仅有5位参赛选手解决的问题，但无法解决其余两道组合问题。 最终，经过数 学家评分，AlphaProof和AlphaGeometry 2共获得了28分（满分42），与金牌线29分相差 仅有1分，首次达到了银牌选手的水平。 --

※ 发信站: 批踢踢实业坊(ptt.cc), 来自: 111.253.162.64 (台湾) ※ 文章网址: https://webptt.com/cn.aspx?n=bbs/Math/M.1721979825.A.1CB.html