今日应用
今日话题
谷歌大模型获重大突破，首次拿下国际奥数银牌
重点标签 AI数学竞赛、AlphaProof、AlphaGeometry、神经符号框架、形式数学推理
文章摘要
谷歌DeepMind在2024年国际数学奥林匹克竞赛（IMO）中取得了显著成绩，其开发的两个混合大模型AlphaProof和AlphaGeometry 2获得了银牌。IMO是全球最古老、最权威的数学竞赛之一，吸引了世界各地的精英数学家参与，同时也是AI模型竞技的舞台。AlphaProof在本次比赛中解决了两道代数题和一个数论问题，而AlphaGeometry 2则答对了一道几何题，两者共获得28分，仅比金牌少1分。
AlphaGeometry模型的核心在于其神经符号框架，这是一个能够自动解决欧几里得平面几何问题的复杂模型。它绕过了传统机器学习方法中对大量人类证明数据的依赖，实现了从零开始的自我学习，生成大量的合成定理和证明。证明搜索和证明修剪是AlphaGeometry的两个重要功能，通过循环过程和穷举试验，模型能够找到并返回所有可能证明中的最短路径。
AlphaGeometry 2在一代的基础上进行了大量迭代和技术创新，使用了谷歌自研的Gemini作为语言模型，并在比一代多一个数量级的合成数据上从头开始训练。AlphaGeometry 2的符号引擎比前身快两个数量级，能够解决更复杂的数学难题。
AlphaProof是谷歌最新开发的专门用于形式数学推理的模型，结合了预训练语言模型和AlphaZero强化学习算法，在复杂的数学问题上展现出强大的推理能力。AlphaProof使用形式语言Lean进行数学证明，通过微调的Gemini大模型将自然语言问题自动转换为形式语言表述，创建了包含各种难度和数学主题的大规模形式问题库。
谷歌表示，目前的AI模型在解决一般的数学问题时仍然存在困难，但AlphaProof和AlphaGeometry 2已经具备数学推理的AGI（通用人工智能）能力，可以帮助数学专家发现新的解题方法，也是AI在数学领域的重大技术突破。
文章来源
原文地址: 点我阅读全文
原文作者: AIGC开放社区
相关文章
