AlphaProof 与 AlphaGeometry 2 达到国际数学奥赛银牌水平

背景

国际数学奥林匹克（International Mathematical Olympiad，IMO）是一项数学竞赛，题目要求参赛者写出严格论证，而不只是给出数值答案。这样的题目通常需要构造证明、寻找关键思路。2024年7月25日，Google DeepMind 公布了 AlphaProof 和 AlphaGeometry 2 两个系统在2024年 IMO 题目上的测评结果。^[1]

这次公布描述的是对系统解题能力的测评。题目由人类专家翻译成形式化语言。^[1] 形式化语言是一种把证明的每一步写成精确符号、并可由程序逐步检查的写法。因此，人类翻译构成了流程的一部分：原始题目被转换成系统可以处理的形式。^[1]

发生了什么

Google DeepMind 表示，这两个系统解出了6道题中的4道。^[1] 其中，AlphaProof 解出2道代数题和1道数论题，AlphaGeometry 2 解出1道几何题。^[1] 2道组合题没有解出。^[1] 这些解答合计得到42分中的28分。^[1] 金牌线是29分，因此成绩略低于金牌，达到银牌水平。^[1] Google DeepMind 称，这是首次达到与银牌得主相同的水平。^[1]

关键细节

按题目类型看，AlphaProof 覆盖了代数和数论，AlphaGeometry 2 覆盖了几何。^[1] 组合题仍留在未解出的一侧。^[1] 分数差距也很具体：28分对29分，只差1分。^[1] 另一项关键细节是题目翻译：题目由人类专家译成形式化语言，而不是由系统直接从自然语言题目开始。^[1] 这说明公布的结果针对的是翻译之后的解题环节，人类翻译是流程中的前置步骤。^[1]

为什么重要

IMO 题目常被用作检验数学解题能力的公开测试，因为解题者必须组织推理并写出可检验的论证。形式化语言让证明的每一步都可以被精确表达和检查，因而适合作为系统输出证明的目标格式。^[1] 在这次测评中，系统需要在形式化题目上给出解答，而题目到形式化语言的转换由人类专家完成。^[1]

结果同时划出了边界：代数和数论题有解出，几何题有解出，但2道组合题没有解出。^[1] 总分28分，低于29分的金牌线，达到 Google DeepMind 所说的银牌水平。^[1] 这些数字和题目类型一起，说明了这次测评做到了什么、还剩下什么未解决。^[1]