本文经AI新媒体量子比特（公众号ID：QbitAI）授权转载，转载请联系出处。今年可能是最后一次有“纯人类”参赛的IMO（国际奥林匹克运动会）。△参加2020年IMO的中国代表队（李金民官方年龄信息有误）因为明年AI也有可能加入到本次金牌争夺战中，成为“种子选手”。潜入IMO活动的AI被称为Lean，由微软的研究人员开发。目前，他们正计划让莱恩参加明年的国际数学奥林匹克竞赛。也就是说，它将与来自世界各地的奥运选手争夺IMO金牌。准备在IMO大显身手的精益实际上，微软研究人员之所以让AI参与IMO，是因为它是一个很好的实验工具（工具人）。微软研究员、IMOGrandChallenge联合创始人Selsam表示，比赛的目的是训练人工智能系统在世界顶级数学竞赛中赢得金牌。因为这里不仅有数学中“最简单”的问题（你连高等数学都不会，就是做不来），还汇集了全世界顶尖的专家。如果AI能像人类一样证明这些数学定理，也能从某种程度上说明，让它“像人类一样思考”并不会太难。基于这样的想法，微软的研究人员在2013年开始研发Lean，希望让AI具备基于假设进行独立判断和推论的能力。也就是说，它是一个开源项目，旨在弥合交互式定理证明和自动定理证明之间的差距。自动定理证明：找到一种方法来证明或反驳数学中提出的定理或猜想。系统不仅可以根据假设进行推演，还具有一定的判断能力。交互式定理证明：借助计算机辅助证明工具，理解和检验数学定理的正确性，完成数学定理的证明。Lean推出了3个版本，现在第四个版本Lean4还在完善中。当前的逻辑系统基于依赖类型理论，它的功能强大到足以证明所有常规的数学定理。也就是说，要让它去证明IMO中提出的那些前所未见的数学问题，还是非常困难的。目前，Lean4还没有完全准备好，作者LeonardodeMoura表示，如果被允许参加今年的IMO，“可能只能获得0分”。因为，精益目前甚至无法理解某些数学问题需要涉及到哪些概念，以及这些概念本身“是什么意思”。证明的“第一步”阻碍了算法。对于很多人来说，数学是非常抽象的，很难学好。事实上，人工智能的感觉和你一样。在一般的工程应用问题中，AI是得心应手的，因为在预训练阶段，算法模型已经理解了一类问题。也就是说，现阶段AI能做的还是有限的。通常，必须给出条件和数据，经过不断的“研究问题”，才能进行“更复杂的计算”。这是一个从“1”到“2”、“3”，乃至无限的过程。但是，数学问题的证明性质不同。要证明一个公理或一个复杂的方程，需要从头开始。证明的第一步：提出合理的证明路径。从0到1的关键目前只有人脑才有能力。对于绝大多数人工智能来说，很难给出证明想法的第一步。以最简单、最古老的数学公理之一为例。公元前300年，欧几里得证明素数有无穷多个。证明这一点的关键是要认识到，通过将所有已知素数相乘并加1，总能找到一个新素数。考虑到这一点，下一个证明就非常简单了。但是“想到这个点子”这个行为本身对于人工智能来说是极其困难的。说到IMO，正式比赛的三道题虽然不涉及微积分等高等数学，但都要求选手运用中学阶段的全部数学知识，出奇思妙想，给出解决方案。比如这道2005年的IMO真题：当时不同国家的选手至少给出了3种不同的证明。其中，被广泛认可和讨论的解是基于简化柯西不等式的思路，长度大约需要半页A4纸。而另一位来自摩尔多瓦的选手则创造性地用两行完成了证明：上行是“because”，下行是“so”。其简洁、精准，甚至“粗犷而有效”，震撼了全场。精妙的思维也获得了当年的IMO特别奖。需要注意的是，IMO特别奖不看总分，只颁发给解题方法独特的选手。这惊天动地的“第一步”对于现在的AI来说几乎是不可能的。这或许就是微软研究人员将目标定为“震撼金牌”的原因。巧合的是，精益用什么方法来与人脑竞争？精益如何学习数学？与所有人工智能算法一样，精益需要“输入数据”进行训练。现在的Lean不仅无法为IMO问题设计出完整的证明流程，甚至无法理解其中一些问题涉及的概念。所以，精益的首要任务就是学习更多的数学知识。训练数据来自Mathlib库。Mathlib是一个基础数学数据库，包含了大学二年级以下几乎所有的数学知识。不过Mathlib在中学数学方面还有一些差距，团队正在完善Mathlib数据库。掌握知识只是第一步，如何灵活运用才是关键。团队采用的方法与国际象棋、围棋AI等相同——遵循决策树，直到算法找到最优解。IMO解决许多问题的关键是找到某种证明模式。深入了解数学证明是一系列非常具体、合乎逻辑的步骤。研究人员试图通过IMO问题证明的全部细节来训练精益。但这种方法也有局限性。每个特定问题都被证明对于算法来说过于“专业”，下一个不同类型的问题仍然无法解决。为了解决这个问题，团队需要数学家对之前的IMO问题写出详细的形式化证明。然后，该团队改进了证明中采用的不同策略。接下来，精益的任务是在这些策略中找到一个“致胜”组合。这项任务实际上比听起来更难，团队将其比喻为：在围棋游戏中，目标是找到最佳着法。而在数学中，目标是找到最好的棋局，然后找到该局的最佳走法。球队表示，或许明年，金牌仍将是艰难的，但至少利恩还有机会一争高下。对此，有网友感叹AI这几年的突飞猛进：先是国际象棋，后是围棋……如今，AI要在国际奥林匹克竞赛中夺金了。但也有部分网友持悲观态度，认为AI现阶段只能在某些方面接近人类水平。现在的AI算法都是基于人类的认知……所以我对（证明数学定理）这样的特殊任务持否定态度，毕竟世界上只有一小部分人可以帮忙。“什么是数学思维？”这个问题出奇地难以解释清楚。当数学家试图解决一个新问题时，大脑活动很难描述，更不用说用算法实现了。一些AI团队虽然向数学思维的深层次迈进了一步，但从他们采用的策略来看，他们还是借鉴了过去的思路，选择了成功率最高的“排列组合”。这样的AI算法要在创造力和突破性上超越人类，还差得很远。隔壁的GPT在数学证明方向也取得了初步成果。近期，OpenAI针对数学问题推出了GPT-f，利用Transformer语言模型的生成能力进行自动定理证明。GPT-f发现的23个简短证明已被Metamath主库接受。这是人工智能的数学证明首次被业界认可。GPT真的要砸了所有人的饭碗，连数学家也不例外。那么，Lean和GPT-f，你更喜欢哪一个？项目链接：https://leanprover.github.io/在线试玩：https://leanprover.github.io/live/master/
