人工智能在解决国际数学奥林匹克问题上达到银牌标准 - Google DeepMind

DeepMind 的 AI 系统 AlphaProof 和 AlphaGeometry 2 首次实现了解决国际数学奥林匹克（IMO）问题的银牌水平，解决了四个出题。

DeepMind 宣布其人工智能系统 AlphaProof 和 AlphaGeometry 2 在国际数学奥林匹克（IMO）问题上的突破。AlphaProof 系统通过自我训练来证明数学陈述，它结合了预训练的语言模型和 AlphaZero 强化学习算法。AlphaGeometry 2 是一个改进的神经象征混合系统，用于解决几何问题。这两个系统在 IMO 2024 的问题上得分 28 分，相当于银牌水平。DeepMind 还探索了基于自然语言的推理系统，该系统不需要将问题翻译成形式语言。AlphaProof 通过证明数百万个问题来训练自己，而 AlphaGeometry 2 在历史上的 IMO 几何问题上的解决率达到了 83%。DeepMind 对这些 AI 系统在数学推理领域的应用表示兴奋，并计划发布更多关于 AlphaProof 的技术细节。该项目得到了多位数学家和 AI 专家的支持和协作。

要点

• AlphaProof 和 AlphaGeometry 2 的 AI 系统在 IMO 上的表现证明了人工智能在高级数学推理方面的潜力。
• AlphaProof 利用形式数学语言 Lean 来验证证明的正确性，这是一个关键优势，因为它能够避免自然语言方法中的幻觉问题。
• AlphaGeometry 2 通过从头开始训练语言模型，并使用大量的合成数据，显著提高了解决复杂几何问题的能力。
• AlphaProof 通过自我生成的问题变体进行训练，这有助于提高其解决更具挑战性问题的能力。
• DeepMind 正在探索将 AI 与数学家的合作模式结合起来，以便在未来解决长期存在的数学问题。
• AI 系统的进步可能会帮助数学家探索假设、尝试新的解决方法，并加快证明过程中繁琐的部分。
• DeepMind 计划发布更多关于 AlphaProof 的技术细节，以促进人工智能在数学推理领域的进一步发展。`