AlphaProof

是什么

AlphaProof 是 Google DeepMind 于 2024 年 7 月 25 日公布的强化学习系统，用于形式化数学推理。^[1] 它在 Lean 形式语言中证明数学命题。^[1] Lean 是一种形式化语言，其中的证明必须写成足够精确的步骤序列，由计算机逐行检查。这样一来，系统给出的证明可以被机械地验证：检查器要么接受，要么不接受，不必由人来判断论证是否有说服力。形式化证明长期是自动推理研究的重要目标，原因正在于此——成功与否没有模糊地带。

怎么工作

AlphaProof 把一个预训练语言模型与 AlphaZero 强化学习算法结合起来。^[1] 两部分分工不同。经过微调的 Gemini 模型负责把自然语言表述的题目转写为形式化命题；在大量题目上反复做这种转写，就积累出一个难度不一的形式化题目库。^[1] 这个题库就是证明器练习的材料。强化学习大致是通过反复尝试、强化那些通向正确结果的选择来训练系统；在这里，正确结果就是检查器接受的证明，系统在找到这样的证明后，会把奏效的思路继续用下去。

为备战国际数学奥林匹克，AlphaProof 在赛前用数周时间证明或否证了数百万道题。^[1]

在 2024 年国际数学奥林匹克上的表现

国际数学奥林匹克共 6 道题，每题 7 分，满分 42 分。^[1] 在系统作答之前，题目先由人类专家翻译成形式化语言。^[1] AlphaProof 解出了两道代数题和一道数论题，其中包括该届比赛中最难的一道题。^[1] 与同时公布的另一套系统 AlphaGeometry 2 合计，成绩达到银牌水平，42 分中得到 28 分。^[1]

评分

解答由 Prof Sir Timothy Gowers 与 Dr Joseph Myers 按国际数学奥林匹克的评分规则评定。^[1] 也就是说，分数依照人类选手所用的同一套规则给出，由数学家判断论证能否成立，而不是直接从形式化检查器的结果折算。

位置与影响

AlphaProof 属于这样一条路线：把证明搜索当作形式化语言内部的学习问题，而不是当作普通数学文字的生成问题。分工在设计中看得很清楚：语言模型读懂题目并改写成 Lean 语句，强化学习证明器再去寻找证明。^[1] 2024 年的结果没有消除的一环是翻译：题目在系统开始工作之前，由人类专家逐题改写为形式化表述，而不是以原来的自然语言措辞直接交给系统。^[1]

更准确地说，这是一次测量：在一套为年轻数学家准备的、按考试条件命制的题目上，形式化自动推理走到了什么位置——6 道题解出 3 道，并与其他系统合计由人工按与人类选手相同的规则评分。^[1] 2025 年 11 月 12 日，一篇描述 AlphaProof 方法的文章发表在 Nature 上。^[1]