谷歌AlphaProof攻克国际奥赛数学题 数学家会不会被淘汰？

谷歌AlphaProof攻克国际奥赛数学题数学家会不会被淘汰？

谷歌DeepMind发布消息称，它所开发的AI系统AlphaProof和AlphaGeometry 2在数学上取得突破，解答了今年国际数学奥林匹克竞赛（IMO）6道题中的4道，相当于银牌水平。

谷歌还自豪宣称，这是AI第一次取得如此耀眼的成绩。可惜就像之前所鼓吹的其它AI一样，谷歌的说法也有夸大之嫌。

离金牌线只有一步之遥

根据谷歌的解释，AlphaProof用增强学习技术在开源求证辅助系统Lean环境中证明数学命题。Lean是微软公司计算机科学家莱昂纳多·德莫拉开发的，采用了由所谓“有效的老式人工智能”(GOFAI)——即从逻辑学汲取灵感的符号人工智能——所驱动的自动推理。

谷歌系统具备自我学习能力，它生成并验证数百万个数学证明，在解决复杂数学问题时进步明显。在此之前，谷歌开发过几何AI模型，AlphaGeometry 2相当于升级版本，它是谷歌以Gemini语言模型作为基础，用大量数据训练出来的。

知名数学家Sir Timothy Gowers和Dr. Joseph Myers用国际数学奥林匹克竞赛标准对谷歌AI系统进行评估，国际数学奥林匹克竞赛的金牌线为29分，总分42分，谷歌系统拿到28分，离金牌线只有一步之遥。在最难的问题上谷歌系统完美解答，今年只有5人解决此问题。

国际数学奥林匹克竞赛始于1959年，面向预科数学天才（也就是还没进入大学的数学天才），主要涉及代数、组合数学、几何和数论。

用竞赛问题测试AI已经成为评估AI推理能力的重要标准。AlphaProof解决了两个代数问题，一个数论问题；AlphaGeometry 2解决了一个几何问题，但谷歌AI被两个组合数学问题挫败。在解决问题时，有一个只用了几分钟，其它耗时较长，最多三天。

谷歌AI用于数学也有局限

为什么说谷歌的说法也有夸大之嫌呢？

首先，谷歌将竞赛问题转化为正式数学语言，方便AI模型处理。这一做法与官方竞赛流程不符，人类参赛者会直接面对问题。

AI模型可以生成文章或者其它形式的文本，但面对复杂数学问题时往往会捉襟见肘，因为当中牵涉到复杂的逻辑推理，这正是目前AI系统所欠缺的。复杂数学问题会涉及到抽象概念、子目标设定、回溯、尝试新路径，这些都给AI带来挑战。

专注于数学和AI研究的剑桥大学研究人员Katie Collins说：“如果你有办法检查答案（也就是正式语言），训练数学AI模型就会容易很多，难点在于网上自然语言（非正式语言）数据超级多，但正式数学语言数据却很少。”

谷歌DeepMind AI可以自动将用自然非正式语言编写的数学问题转化为正式语言，这是谷歌之所以取得突破的关键。爱丁堡大学混合AI讲师Wenda Li说，对于数学社区而言，自动将非正式语言转化为非正式语言是一大进步。

在参加今年的竞赛之前，AlphaGeometry 2曾尝试解答之前25年积累的国际数学奥林匹克竞赛几何问题，83%都能解答——之前的AI只能解答53%。面对今年的几何问题，谷歌系统只用19秒就给出答案。

其次，谷歌AI模型花费的时间有时显著过长。Sir Timothy Gowers承认DeepMind模型取得突破，表现远超之前的自动定理证明者，但AI解答时花费的时间远长于人类参赛者，有些问题需要的时间甚至超过60个小时，AI的处理速度本来比人类快很多，但还是需要更长时间，如果人类参赛者有同样长的时间解答，得分肯定更高。

Sir Timothy Gowers还说，在正式答题之前，人类已经手动将题目转化为正式语言Lean，然后AI才着手处理，虽然核心数学推理是由AI完成的，但“自动化”步骤却由人类操刀。