主要证据
- AI achieves silver-medal standard solving International Mathematical Olympiad problemsS2 · 官方机构来源 · 官方公告 · 2024-07-25
- Olympiad-level formal mathematical reasoning with reinforcement learningS1 · 主要研究来源 · 论文 · 2025-11-12
AlphaProof 与 AlphaGeometry 2 在 IMO 2024 题目上达到银牌标准
AlphaProof 在 Lean 中使用强化学习进行形式证明搜索，AlphaGeometry 2 则以更快的神经符号系统处理几何题。2024 年的流程需要专家将题目翻译为形式化表示，并使用最长数日的计算时间。
发生了什么？
AlphaProof 解出 3 道非几何的 IMO 2024 题目，AlphaGeometry 2 解出几何题；4 道满分解答合计 28/42 分，对应当年银牌区间上沿，距金牌线 1 分。
为什么重要？
该结果把形式证明搜索与一个公众熟知的外部竞赛基准连接到奖牌水平，并成为后续端到端自然语言奥赛系统的重要参照点。
重要性说明：该组合系统被报告为首个在当届完整 IMO 题集上达到奖牌水平的 AI 系统，同时也清楚暴露了人工形式化与多日计算的实际代价。
历史脉络
证据与状态一览
- 重要性
- H1 · 历史里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号, 混合
- AI 贡献
- AlphaProof 通过强化学习与测试时适应搜索 Lean 证明；AlphaGeometry 2 在其专用系统中生成并检查几何证明。
- 人类贡献
- 专家将竞赛题人工翻译为形式化或专用表示，研究团队设计并训练系统，数学家按 IMO 评分规则评阅最终解答。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- alphaproof, alphageometry-2
- 机构
- google-deepmind, international-mathematical-olympiad
- 数学问题
- international-mathematical-olympiad-2024
- 方法
- reinforcement-learning, lean, formal-theorem-proving, neuro-symbolic-reasoning
全部来源与工件
- AI achieves silver-medal standard solving International Mathematical Olympiad problemsS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-10
- Olympiad-level formal mathematical reasoning with reinforcement learningS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
验证历史
- 2024-07-25 · 尚属声明 · E1 · 原始声明
Google DeepMind 公布竞赛结果，并说明由数学家按竞赛规则进行外部评分。
- 2025-11-12 · 论文已发布 · E2 · 研究记录
AlphaProof 方法与 IMO 2024 结果在经同行评审的 Nature 论文中发表。
更正
当前没有记录的更正。