谷歌AI险失IMO金牌：19秒解题震惊评委，几何能力超越人类

AlphaProof

AlphaProof是一个能够在Lean形式语言中证明数学命题的系统。它结合了预训练的大型语言模型和AlphaZero强化学习算法。

为了克服机器学习中形式语言由于人工编写数据有限而导致的局限性，研究人员通过以下方式弥合了自然语言和形式化陈述之间的差距：

1. 微调Gemini模型以自动将自然语言问题陈述转换为形式化陈述
2. 创建了一个包含不同难度的形式化问题的大型库

在解决问题时，AlphaProof生成候选解决方案，并通过在Lean中搜索可能的证明步骤来证明或反驳它们。

AlphaGeometry 2

AlphaGeometry 2是一个使用Gemini语言模型从头开始训练的神经-符号混合系统。它可以解决比其前身更困难的几何问题，包括涉及物体运动、角度、比例和距离方程的问题。

主要改进包括：

1. 在比之前版本大一个数量级的合成数据上进行训练
2. 符号引擎速度比以前快两个数量级
3. 一种新颖的知识共享机制，允许不同搜索树的高级组合来解决更复杂的问题

AlphaGeometry 2展示了令人印象深刻的能力，解决了过去25年IMO几何问题的83%，而其前身为53%。在今年的IMO中，它在收到形式化问题后仅用19秒就解决了第4题。

AI在IMO中的表现展示了数学推理能力的显著进步，使AI在高等数学问题解决方面更接近人类水平。