The IMO is the oldest, largest and most prestigious competition for young mathematicians, held annually since 1959. Each year, elite pre-college mathematicians train, sometimes for thousands of hours, to solve six exceptionally difficult problems in algebra, combinatorics, geometry and number theory. Many of the winners of the Fields Medal, one of the highest honors for mathematicians, have represented their country at the IMO. More recently, the annual IMO competition has also become widely recognised as a grand challenge in machine learning and an aspirational benchmark for measuring an AI system’s advanced mathematical reasoning capabilities.
核心贡献 · Key contributions
AlphaProof 将预训练语言模型与 AlphaZero 强化学习相结合，在 Lean 中证明数学命题。 AlphaProof combines a pre-trained language model with AlphaZero reinforcement learning to prove mathematical statements in Lean.
AlphaGeometry 2 采用基于 Gemini 的语言模型和更快的符号引擎，解决了 83% 的历史 IMO 几何问题。 AlphaGeometry 2 improves on its predecessor with a Gemini-based language model and a faster symbolic engine, solving 83% of historical IMO geometry problems.
该组合系统在 2024 年 IMO 中获得银牌水平，解决了 6 道题中的 4 道，得分 28 分。 The combined system achieved a silver-medal standard at IMO 2024, solving 4 out of 6 problems and scoring 28 points.
AlphaProof 使用形式化器将自然语言问题翻译为形式化陈述，从而能够通过验证的证明进行大规模训练。 AlphaProof uses a formalizer to translate natural language problems into formal statements, enabling large-scale training with verified proofs.
这些系统展示了高级数学推理能力，解决了仅五名人类参赛者解出的最难问题。 The systems demonstrate advanced mathematical reasoning, solving the hardest problem solved by only five human contestants.
局限 · Limitations
该系统需要手动将问题翻译为形式化语言，限制了自动化程度。 The system requires manual translation of problems into formal language, limiting automation.
AlphaProof 解决某些问题需要长达三天，远慢于人类参赛者。 AlphaProof took up to three days to solve some problems, far slower than human contestants.
两道组合数学问题仍未解决，表明在某些推理类型上存在差距。 Two combinatorics problems remained unsolved, indicating a gap in certain reasoning types.
该方法依赖于大规模合成数据生成，可能无法泛化到所有数学领域。 The approach relies on large-scale synthetic data generation, which may not generalize to all math domains.
该系统的性能是在固定问题集上评估的，其对对抗性或开放式问题的鲁棒性尚未测试。 The system's performance is evaluated on a fixed set of problems, and its robustness to adversarial or open-ended problems is untested.
论文章节 · Sections（共 4）
突破性 AI 在解决复杂数学问题上的表现Breakthrough AI performance solving complex math problems
AlphaProof：一种形式化的推理方法AlphaProof: a formal approach to reasoning
更具竞争力的 AlphaGeometry 2A more competitive AlphaGeometry 2