谷歌大模型获重大突破，首次拿下国际奥数银牌

1,008 0 0

文章摘要

【关键词】 数学竞赛、人工智能、AlphaProof、AlphaGeometry、技术突破

谷歌DeepMind在2024年国际数学奥林匹克竞赛（IMO）中取得了显著成绩，其开发的两个混合大模型AlphaProof和AlphaGeometry 2获得了银牌。IMO作为历史悠久且权威的数学竞赛，每年吸引全球精英数学家参与，也是衡量AI数学推理能力的重要平台。

AlphaProof在竞赛中解决了两道代数题和一个数论问题，而AlphaGeometry 2则答对了一道几何题。特别值得一提的是，AlphaProof解答了当年IMO最难的题目，仅有5位参赛者给出正确答案。AlphaGeometry 2的核心在于其神经符号框架，它能够自动解决欧几里得平面几何问题，绕过传统机器学习方法对大量人类证明数据的依赖，实现自我学习，并生成合成定理和证明。

AlphaGeometry的证明搜索是一个循环过程，语言模型和符号推理引擎交替运行，生成新的辅助构造并扩展推理闭包。证明修剪功能则去除不必要的辅助构造，确保证明的简洁性和可读性。此外，AlphaGeometry通过穷举试验和错误的方法进行证明修剪，找到并返回所有可能证明中的最短路径。

AlphaGeometry 2在一代的基础上进行了大量迭代和技术创新，使用了谷歌自研的Gemini作为语言模型，并在合成数据上从头开始训练。其符号引擎速度比前身快两个数量级，使用新的知识共享机制解决更复杂的数学难题。在IMO比赛前，AlphaGeometry 2能解决过去25年所有IMO几何问题的83%，而一代解决率只有53%。在正式比赛中，AlphaGeometry 2仅用19秒便解决了几何难题，展现了超高效率。

AlphaProof是谷歌最新开发的形式数学推理模型，结合预训练语言模型和AlphaZero强化学习算法，展现出强大的推理能力。它使用形式语言Lean进行数学证明，通过微调的Gemini大模型将自然语言问题转换为形式语言表述，创建大规模形式问题库。AlphaProof在面对新问题时生成解决方案候选，通过在Lean中搜索证明步骤来证明或反驳候选解，每个验证的证明都用来强化语言模型。

谷歌表示，尽管AI模型在解决一般数学问题时存在困难，但AlphaProof和AlphaGeometry 2已具备数学推理的AGI能力，可帮助数学专家发现新的解题方法，标志着AI在数学领域的重大技术突破。