-
潘禺:今年有另一场更值得关注的数学竞赛
【文/观察者网专栏作者 潘禺】
今年,一场数学竞赛初赛结果的出圈传播,导致了媒体的聚焦和全社会的讨论。而在该事件不久之后,其实还有另外一场数学竞赛的结果,具有深远的影响和重要的意义,在媒体上得到的关注却小得多。那就是2024年的国际数学奥林匹克竞赛 (IMO),主角中同样有科技互联网巨头的身影,Google DeepMind的人工智能AlphaProof和AlphaGeometry 2,答对了6道题中的4道,首次达到了IMO银牌获奖者的水平。
AlphaProof解决了2道代数问题和1道数论问题,包括本届IMO中最难的问题,只有5名参赛者解决了这个问题。AlphaGeometry 2证明了几何问题,而2个组合问题AI没能解决。每道题最高可得7分,总共最高42分。人工智能的最终得分为28分,在解决的每个问题上都获得了满分,相当于银牌类别的最高水平,因为今年的金牌从29分开始。
这一结果表明,AI处理复杂数学推理能力有了显著飞跃。而数学推理是人类认知能力的一个重要方面,推动了科学发现和技术进步。
对中国来说,这一结果也意味着重大的机遇和挑战。
中国的人工智能企业在一些领域处于领先地位,比如图像识别。这是因为,人脸识别、物体检测、医疗影像分析等许多技术成果,已经应用在支付、安防、智慧零售、交通监控和智能医疗等,相比于AI的其它应用领域,是率先落地的。又得益于中国巨大的人口规模和丰富的应用场景,加上基建项目的政策与资金支持,中国企业能积累大量的图像数据,进而推动了模型的训练和算法的优化,在各类国际比赛中处于领先。
下一个在中国能广泛应用于实际场景的AI领域是哪里呢?有潜力的肯定包括智能网联车和文体教等,这些也是国内企业投入的重点。中国社会历来高度重视教育,家庭在教育上的投入巨大,学区房、课外辅导、留学费用等占到了许多家庭支出的大头。AI对教育的改变,将深刻冲击中国社会,数学这一被中国人视为重中之重的基础学科,又是我们观察这种影响的一个窗口。
从计算到证明
虽然数学一直被称为人类心智的荣耀,但人类使用机器作为数学的辅助,有着几千年的历史。
早在公元前2400年,类似算盘这样的工具就已经被发明。17世纪的科学家和发明家布莱兹·帕斯卡(Blaise Pascal)发明了早期的机械计算器,这种机器可以进行简单的加减运算。20世纪60年代,第一台电子计算器问世。早在20世纪70年代到80年代,世界上的部分高中和大学考试就开始允许学生使用计算器,90年代起,许多国家的教育体系开始正式将计算器作为教学工具,并编写了相应的课程,鼓励学生使用计算器进行复杂运算。
美国的SAT数学考试在1994年首次允许学生使用计算器。目前,世界许多国家的标准化数学考试,如AP数学考试、SAT、ACT以及国际数学竞赛,允许考生使用特定类型的计算器。用计算器可以帮助学生专注于数学概念的理解,而非繁琐的计算,这已经没有太大争议。中国的基础数学教育以严格和系统著称,中国学生在PISA这类国际数学评估中的表现十分优异,尽管我们注重学生的计算能力,但也并不在高考中排斥计算器的使用。
机器帮助人类解决数学计算,无论在日常生活、教学还是科研领域,都已经被普遍接受。强大的数学计算工具如MATLAB、Mathematica、Maple已经是许多人工作的必备,适合简单数学运算和统计分析的Excel更是普及。而在数学证明上,目前机器也在发挥越来越大的作用,这正是巨大变革可能产生的开始。
这次在IMO 2024,数学家陶哲轩做了一场演讲,回顾了从早期计算工具到现代的机器学习,数学研究的范式转变。他谈到了许多例子,心智观察所在这里结合自己的理解做一些总结和评论。
第一个例子是表格。数学领域的许多重要成果都是通过数论中的表格首次发现的,许多猜想也是通过大量的表格发现的。表格可以理解为数据库,计算机的一个基本用途就是建立这些有用的数据库。比如,很多数学家,包括陶哲轩自己,使用一个叫做“整数序列在线百科全书”(Online Encyclopedia of Integar Sequences,OEIS)的数据库。
第二个例子是科学计算。比如用计算机来建模各种事物,求解大量线性方程或偏微分方程,这几乎是现代科学研究和工程应用的基石,从天气预报到风洞实验,从新材料和药物的研发到期权定价、核反应堆设计,其应用无处不在。
另一种科学计算是SAT求解器,可以解决一些逻辑难题(布尔可满足性问题),其原理是通过检查大量的布尔变量,寻找是否存在一组变量的赋值,使得整个布尔公式为真。通俗地说,比如给你1000个陈述,有的是真的,有的是假的,再给你一些限制条件、变量和法则,让你证明某些句子的组合逻辑上是真的。通过把数学问题,比如毕达哥拉斯三元组问题,转换为布尔逻辑问题,利用SAT求解器强大的组合求解能力,能够有效寻找整数解。
第三个例子是形式化证明辅助。四色定理(任一地图只用四种颜色就能让相邻的国家染上不同的颜色)和开普勒猜想(在三维空间中最有效地堆叠球体,以最大限度填充空间)的证明,都是计算机辅助证明的著名例子。
为了更加简洁地形式化复杂的证明过程,数学家开始使用Lean平台,Lean将数学命题用形式化语言表达并通过计算机验证,使得每一个推理步骤都可以自动检查。这为数学研究提供了极大的便利,也降低了证明复杂定理的出错率。目前本科数学课程中的基础内容,比如微积分、群论或拓扑学的基本概念等,都已经被形式化,更多数学领域的内容也在被加入到这个库中。
数学家Peter Scholze就利用Lean试图形式化验证自己的高深数学理论,这些理论需要高层次数学背景和对非常抽象的概念的理解,涉及到对现代代数几何、范畴论、同调代数和拓扑学的深入掌握。Scholze对自己的证明存有疑虑,也没有人有本事详细查看其中的细节。Lean的形式化证明如果能够成功,意味着形式化数学能处理现代数学的前沿问题。用Lean证明费马大定理的项目,目前也已经获得资助并启动。
陶哲轩自己则致力于以众包方式来用Lean探索数学。其方法是为大型的复杂证明编写一个蓝图,将证明分解成数百个小步骤,每个步骤都可以单独形式化,然后组合起来,最后将长达数万行的形式化证明转换回人类可读的版本,最后这步也是计算机自动生成的。
这样的好处是,证明过程更加开放,让数学家们可以更好地分工合作,每个人处理任务图中自己负责的部分,通常是自己擅长解决的,而不需要理解整个证明。由于Lean可以自动检查,就能保证每个人的工作达到质量标准。另外,遇到修改,编译器会自动指出关联的地方,不需要像传统的方式重写整个证明,效率大大提高。
最后一个例子就是当下炙手可热的机器学习。
标签 心智观察所- 原标题:今年有另一场更值得关注的数学竞赛 本文仅代表作者个人观点。
- 责任编辑: 李昊 
-
中国货运航天飞机,来了
2024-10-30 07:26 航空航天 -
马斯克拥抱特朗普的隐秘心境,藏在这部美剧中
2024-10-29 14:35 心智观察所 -
神十九将带果蝇上太空 小鼠:等我
2024-10-29 13:34 航空航天 -
我国首艘深远海多功能科学考察及文物考古船完成试航
2024-10-26 19:44 中国精造 -
“把大象装进冰箱”,鸿蒙为什么行?
2024-10-25 14:41 心智观察所 -
我国科研人员揭示过敏反应关键机制
2024-10-25 13:40 -
我国成功发射天平三号卫星
2024-10-22 08:55 航空航天 -
肖克利的幽灵重现硅谷
2024-10-22 08:39 心智观察所 -
中方代表:防止出现机器自主杀人
2024-10-22 08:26 科技前沿 -
中国科学家让“死亡”50分钟猪脑“复活”
2024-10-20 15:05 科技前沿 -
污蔑宁德时代,美国有着怎样的怨念与悔恨?
2024-10-17 14:33 心智观察所 -
我国成功发射高分十二号05星
2024-10-16 08:33 航空航天 -
我国首个空间科学规划公布!明确这些目标
2024-10-15 09:54 航空航天 -
拿下诺贝尔化学奖的中国血统,还将拯救谷歌?
2024-10-15 08:33 心智观察所 -
星舰第五次试飞实现重大突破,但我国类似火箭可能得等一等
2024-10-13 23:04 航空航天 -
中国汽车电子产业将站上两个世界之巅
2024-10-12 08:29 心智观察所 -
世界最大!地下700米的这个玻璃球,将探寻宇宙之初
2024-10-11 10:00 科技前沿 -
我国成功发射卫星互联网高轨卫星
2024-10-10 22:49 航空航天 -
我国科技成果转化问题到了必须要解决的地步
2024-10-08 16:58 心智观察所 -
2024年诺贝尔生理学或医学奖揭晓
2024-10-07 17:45 诺贝尔奖
相关推荐 -
“欧盟将派特使赴华探索关税替代方案” 评论 144“德国经济深陷停滞,执政联盟却还在内讧” 评论 84美陆军为与中国开战做准备?“都是生意” 评论 287“美国围堵6年,中国拿下5个关键技术领先” 评论 207欧盟公布终裁结果,中方:不认同、不接受 评论 558最新闻 Hot