Nature公开谷歌IMO金牌模型技术细节！核心团队仅10人，一年给AI编出8000万道数学题训练

2025-11-13 16:08:11

发布在

快讯

阅读：1125

正文：谷歌DeepMind团队在Nature上公开了其IMO金牌模型AlphaProof的技术细节。核心团队仅10人，开发历时一年，生成8000万道数学题用于AI训练。AlphaProof基于Lean定理证明器构建强化学习环境，将数学证明过程转化为游戏关卡，使用30亿参数的Transformer模型作为核心，并结合改进的树搜索算法。2024年IMO比赛中，AlphaProof成功解决三道难题（包括最难的P6），最终夺得金牌。系统通过测试时强化学习生成变体问题并进行针对性训练，展现了强大的解题能力。尽管依赖Lean定理证明器且在处理全新定义时存在局限性，但其反证功能和形式化能力受到数学家高度评价。谷歌已开放AlphaProof供科研使用。

原文链接

本文链接：https://kx.umi6.com/article/28349.html

转载请注明文章出处

AlphaProof