前文介绍:
北京时间2023年8月7日晚21:00 World Science Hill 独家专访了北京大学北京国际数学研究中心教授,国际机器学习研究中心副主任董彬教授。
(World Science Hill 创始人Mia王璟晗独家专访董彬教授视频截图)
专访嘉宾:董彬
董彬老师现担任北京大学北京国际数学中心、国际机器学习研究中心副主任,在此之前,董彬教授于2003年从北京大学本科毕业,随后于2005年获得新加坡国立大学硕士学位,并于2009年获得加州大学洛杉矶分校(UCLA)博士学位。
1.请您用一句话简单介绍一下自己的研究方向及兴趣。
我的主要科研兴趣,一是AI for Science其中的计算成像和医疗健康,其二就是最近我们正在北京大学快速推进的AI for Mathematics,这两个方向尤其是第二个更多是一个大团队协作的任务。在北京国际数学研究中心,我们有很多基础数学各个领域的老师参与,包括香港大学的何旭华老师,他也是个基础数学家,主要方向是代数。
我们之所以会想要推进AI for Mathematics是因为我们觉得这可能会逐渐发展成数学里面一个比较新的分支,同时基础数学家也更加希望能用到人工智能的工具去帮他们做探索,因此AI for Mathematics也是我们最近一直在大力推动的研究方向。
2.在推动AI在数学定理证明方面取得进展时,有哪些挑战需要克服呢?目前现有的AI技术足以达到完成数学定理证明,甚至是创造新数学定理的水平吗?
这里有两点,其一是自动定理证明(ATP),其二是自动定理生成(ATG),这两者难度非常不同。对于人类数学家而言,提出一个好的定理很多时候比证明一个定理要困难得多。现在的人工智能,可以肯定地讲,还不能提出非常有意义的数学定理,定理证明方面也是困难重重,但对于一些比较常规的定理证明,特别是在网上文献已经有过的定理证明,AI还是有较大的概率可以答对的。
比如像现在的GPT4、Claude这样的大语言模型,他虽然没有把定理内容都背下来,但是对以前见过的内容,它就更有可能得到正确的定理证明,即便是一些高年级研究生课程里所出现的一些定理,它只要见过,就能够推出来个八九不离十。
但如果是一些全新的、没有见过的,他能做出一部分,但证明并不完善,总有些错误。像现在国外有一个最好的数据集叫miniF2F,包含了一些高中数学竞赛题。如果你想让机器在该数据集上做可以被形式化验证的自动定理证明,其正确率是在50%以下的,所以说目前的水平距离全方位超越高年级数学本科生其实还有相当大的差距。
对于您刚提到的挑战,我觉得这里主要的挑战在于我们现在的这个人工智能系统,它在训练的时候并没有一个可验证的环境。如果你看大语言模型在训练的时候,它的预训练,包括后面的supervised finetuning,其实都是(自)监督学习,但也是相对比较简单的“监督”,距离数学证明所需要的可验证环境还差得很远。
光靠阅读大量的定理题干和证明,大模型其实是很难体会到数学的这种严谨的逻辑推理,它自己在训练过程中,就没有像我们人类做定理证明训练时候那样去练习数学里面的因果逻辑。
此外在训练的过程中,如果有哪一步出错的话,我们希望有一个系统能够告诉模型这块错了,这样他才能够获得推理能力的有效提升。就像人类在数学学习的时候会有老师教,给予学生及时的正确/错误反馈,这是提升模型自动定理证明的关键,也是挑战。
3.如果有一天AI攻克了一个人类从未能证明的数学难题,您认为这最有可能发生在哪一个数学分支?组合还是数论?
从表象上来看,代数、组合、数论这些都看起来像是最先能够取得突破的。我觉得根据机器学习的特点来看,当一个数学分支里的问题能够产生比较大量的数据,那么机器学习可以从这些数据中去找一些规律,这些规律是有可能启发数学家去做一些前沿探索的。
那么像2021年 DeepMind的工作,包括我跟港大何旭华老师最近做的论文,其实也是在代数这个领域,利用这个特点,我们可以产生大量的数据。来用机器学习帮助数学家去找一些规律(pattern),这些规律如果依靠人去观察,或者靠自己手算都是很难得到的。
因为有些规律并不是特别直观,但是我们通过机器学习方法,可以获得更多的这个直观去启发大家进行思考。那么通过这种人机互动的方式是可以创造出一些新的定理,或者对一些研究方向的难易程度做一个大致的判断。所以我觉得像您说的组合、数论这些领域,确实是能用人机互动的方式做探索的。
另外,如果你要让自动定理证明去求证数学里的一些猜想,那我觉得谁先有突破很大程度上取决于这个领域本身,它是不是能够尽快地完成自己领域的形式化进程,那么这其实也跟我刚才提出的挑战息息相关。
因此,形式化验证系统在具体某个领域的参与度越高,这个领域的数据就会越完善,它就能越早地享受到智能化给该领域的发展所带来的效率提升。也就更容易产生一些实质性的突破。
所以主要就是两个不同的方面,一个是在人机互动的工作模式下,围绕某个领域的某些问题是否容易生成大量数据,是一个关键。像代数里有些重要的问题,我们就可以生成很多的数据,但是相对而言分析和概率就没那么容易。
其二是在形式化验证的方法论下,这个领域迅速推进形式化验证需要多少人力、算力,完备的形式化验证覆盖率能让该领域尽早享受到人工智能所带来的效率提升。
4.目前类似于ChatGPT这样的AI工具都是以自然语言的方式与用户沟通的,这里面当遇到一些难度较大的问题时,偶尔也会出现词不达意或者胡言乱语的情况,您认为如果要让AI完成定理证明或者生成,AI是否也会以自然语言的方式输出自己的结论?那么是否需要有数学家对AI的证明进行语句的修改或者证明正确性和严谨性的检查,这是否还能被认为是AI完成的证明呢?
现在的GPT,它生成的定理证明确实是需要人去验证的,而且它经常会犯错误(当然让人去验证定理证明的正确性也是比较花时间的,也会犯错)。有些时候你需要不停地去提示它,它才有可能会改对,有些时候你出难一点的问题,你怎么提示它可能都改不对,这个其实跟它的训练方式有关,除非有一个形式化验证系统实时地告诉它哪一步对了或者错了,否则想要在定理证明方面保证其逻辑正确与逻辑完善是极其困难的。
那么通过这种人机互动的方式,最后得到的定理证明,你肯定是不能够说是由人工智能或者人类单独完成的,就像陶哲轩在博客里面提到的那样,使用GPT4人工智能系统会给他一个非常好的initial approximation to a solution(初始证明),它不是最终的完整证明,但对数学家来说是一个非常好的启发,数学家可以基于这一初始证明进行修改。
但是这里目前还没有办法做全自动验证,最终还是要依靠人工。就像我刚才说的,如果要彻底地解决定理证明的全自动化,也就是让人工智能能自动推出一个正确的定理证明。
那就需要先完成数学的形式化验证。这样我可以创造一个形式化系统去验证任何的逻辑推理,让人工智能在这个系统里训练。在该系统里面,数学定理就变成了一个类似于围棋的游戏。
在这个“game of mathematics”中,我们可以去微调这个训练好的大语言模型。让它在这个系统里面自己探索怎么去做数学推导,它比人类去探索要快很多,一分钟可能达到上万次,于是模型就能迅速学会应该怎么去做正确的数学推理。
至于到底是用人类的语言还是形式化来做定理证明,我认为如果数学到最后能被完全形式化。那么鉴于我们有大量的人类语言写的数学证明以及形式化系统里的证明,我们就很容易让大语言模型知道怎么在两者之间进行翻译。有了翻译之后,大语言模型跟人类交流肯定还是用人类的语言,但在做定理证明验证时肯定用的是数学的形式化语言。
5.有人担心AI可能会发展出超出人类理解的数学证明,从而导致数学基础的不稳定。对于这样的担忧,您有什么看法?
我认为如果我刚才说的这些能实现,就是说我们将数学的形式化定理证明验证变成了一个游戏。然后我在这个游戏里面训练出了一个类似AlphaGo这样的一个智能体,它可以自动地做非常复杂的定理证明,甚至能够证明一些猜想。另一方面,借助计算机的算力优势,AI甚至可能探索出全新的证明思路。我认为这并不会给数学带来负面影响,相反,我认为会对数学发展产生积极正面的影响。
你可以想象,它会创造出一些我们人类没有见过的定理证明,有些甚至会超出人类的理解,就像AlphaGo一样,虽然它的开局和终局的策略和顶尖棋手的差不多,但是它对中盘的理解实际上是非常复杂、非常透彻的,纵然中国围棋已经有几千年历史了,也没有探索出那么多种棋路和定式,我觉得让AI去自动探索定理证明也会是一样的结果。
虽然现代数学也有几百年的历史,非常多的天才探索出了各种各样的证明,但是这肯定不是数学的全部。人工智能一定能够探索出一些非常新奇的证明方法。而这对于数学来讲,并不会扰乱,反而会进一步充实它的基础。
就如同现在很多下围棋的人都会跟AlphaGo学习怎么下棋一样,以后我们学生或者老师就可以跟人工智能去学习怎么用各种不同方式去证明数学定理,从而获得一些全新的数学理解,我觉得这其实对数学发展是有积极正面影响的。
嘉宾:董彬
主持:Mia王璟晗
作者:Mia王璟晗
（来源：News快报）
